Submission cmpgy2x3

-- AUTO-GENERATED by ProofGarden Lean Judge. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgy2x310001k65nbg0967ca

import ProofGarden.Challenges.C0001.Statement
import Mathlib

namespace ProofGarden.Challenges.C0001.Submissions.Submission_cmpgy2x310001k65nbg0967ca

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
lemma helper (n : Nat) : n + 0 = n := Nat.add_zero n
theorem answer (n : Nat) : n + 0 = n := helper n
-- └── USER SUBMISSION BODY END ────────────────────────────

/-- App-appended type check. Refuses to compile unless
    `answer` has type `∀ (n : Nat), n + 0 = n`. -/
def solution_target : ∀ (n : Nat), n + 0 = n := answer

#print axioms solution_target

end ProofGarden.Challenges.C0001.Submissions.Submission_cmpgy2x310001k65nbg0967ca