Compfiles/Usa2025P4.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

9 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2025, Problem 4

Let H be the orthocenter of an acute triangle ABC, let F be the foot of the altitude from C to AB, and let P be the reflection of H across BC. Suppose that the circumcircle of triangle AFP intersects line BC at two distinct points X and Y. Prove that CX = CY.

Imports (3)
Imported by 1 file
  1. def Usamo2025P4.Mc line 35 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

    Proof uses: HSMul.hSMul, ENNReal, Inv.inv, HAdd.hAdd, HSub.hSub

    27 instances, coercions and auxiliary constants left out.

  2. lemma Usamo2025P4.vsub_smul_of_mem_pair A point on line RS differs from R by a multiple of S -ᵥ R line 39 source

    Source documentation

    A point on line RS differs from R by a multiple of S -ᵥ R.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, AffineSubspace, ENNReal, affineSpan, Insert.insert, Set, Singleton.singleton, Exists, Eq, VSub.vsub, HSMul.hSMul

    Proof uses: Submodule, vectorSpan, Eq.mpr, AffineSubspace.direction, id, congrArg, Eq.symm, direction_affineSpan, AffineSubspace.vsub_mem_direction, left_mem_affineSpan_pair, Iff.mp, Submodule.span, Submodule.mem_span_singleton, Eq.mp, vectorSpan_pair, Exists.intro, Neg.neg, neg_smul, smul_neg, neg_vsub_eq_vsub_rev and 1 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

    lemma vsub_smul_of_mem_pair {R S Q : EuclideanSpace ℝ (Fin 2)}
    (hQ : Q ∈ affineSpan ℝ ({R, S} : Set (EuclideanSpace ℝ (Fin 2)))) :
    ∃ k : ℝ, Q -ᵥ R = k • (S -ᵥ R) := by
…

    Mentions: S

  3. lemma Usamo2025P4.p4_reduction line 49 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, Inner.inner, ENNReal, VSub.vsub, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Singleton.singleton, Dist.dist

    Proof uses: HSMul.hSMul, Exists, Usamo2025P4.vsub_smul_of_mem_pair, HSub.hSub, Eq.mpr, HAdd.hAdd, id, congrArg, vsub_add_vsub_cancel, Eq.refl, Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval, Mathlib.Tactic.Module.NF.cons, Prod.mk, HMul.hMul, RingHom, Int, Algebra.algebraMap, Neg.neg, List.nil, Prod and 91 more

    205 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

  4. lemma Usamo2025P4.p4_circumcenter line 78 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, Inner.inner, ENNReal, VSub.vsub, Membership.mem, AffineSubspace, affineSpan, Insert.insert, Set, Singleton.singleton, midpoint, And, Dist.dist, Usamo2025P4.Mc

    Proof uses: Eq.mpr, HSub.hSub, id, congrFun', congrArg, Eq.trans, inner_sub_right, congr, inner_sub_left, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow and 129 more

    244 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

    Open to load the checked before-and-after goal states.

  5. lemma Usamo2025P4.p4_perp line 114 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, Inner.inner, ENNReal, VSub.vsub, Usamo2025P4.Mc

    Proof uses: id, Eq.mpr, HSMul.hSMul, Inv.inv, HAdd.hAdd, HSub.hSub, HMul.hMul, WithLp.ofLp, HDiv.hDiv, Mathlib.Meta.NormNum.instAtLeastTwo, Eq.trans, congrFun', congrArg, Finset.sum, Finset.univ, Finset.sum_congr, Eq.refl, Finset, Membership.mem, AddMonoidHom and 93 more

    183 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  6. lemma Usamo2025P4.angle_lt_pi_div_two_inner_pos line 120 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Ne, LT.lt, EuclideanGeometry.angle, ENNReal, HDiv.hDiv, Real.pi, Inner.inner, VSub.vsub

    Proof uses: Eq, Real.cos, HMul.hMul, Norm.norm, Eq.mpr, InnerProductGeometry.angle, id, congrArg, EuclideanGeometry.angle.eq_1, InnerProductGeometry.cos_angle, Real.cos_pos_of_mem_Ioo, And.intro, Neg.neg, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, inferInstance and 78 more

    159 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

    Open to load the checked before-and-after goal states.

  7. lemma Usamo2025P4.p4_not_collinear line 132 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, AffineIndependent, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LT.lt, EuclideanGeometry.angle, HDiv.hDiv, Real.pi, Eq, Inner.inner, VSub.vsub, Membership.mem, AffineSubspace, affineSpan and 7 more

    Proof uses: Ne, id, Function.Injective.ne, AffineIndependent.injective, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Usamo2025P4.angle_lt_pi_div_two_inner_pos, Ne.symm, Eq.mp, congrArg, real_inner_comm, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd, HSub.hSub, Mathlib.Tactic.Ring.of_eq and 182 more

    316 instances, coercions and auxiliary constants left out.

    Tactic trace: 108 steps

    Open to load the checked before-and-after goal states.

  8. lemma Usamo2025P4.p4_lin_indep line 232 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Not, Collinear, ENNReal, Insert.insert, Set, Singleton.singleton, LinearIndependent, Nat.succ, Matrix.vecCons, VSub.vsub, Matrix.vecEmpty

    Proof uses: Membership.mem, of_eq_true, Eq.trans, Or, Eq, True, congr, congrArg, eq_self, true_or, Eq.mpr, And, Ne, HSMul.hSMul, id, propext, linearIndependent_fin2, And.intro, Iff.mpr, Exists and 24 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

    Open to load the checked before-and-after goal states.

  9. problem Usamo2025P4.usa2025_p4 line 262 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, AffineIndependent, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LT.lt, EuclideanGeometry.angle, HDiv.hDiv, Real.pi, Eq, Inner.inner, VSub.vsub, Membership.mem, AffineSubspace, affineSpan and 8 more

    Proof uses: Decidable.byContradiction, Not, Eq.mpr, LE.le, id, congrArg, Eq.symm, propext, dist_le_zero, False, Eq.trans, eq_false, False.elim, Eq.mp, congr, congrFun', dist_self, Usamo2025P4.Mc, Usamo2025P4.p4_circumcenter, EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq and 89 more

    210 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

    Open to load the checked before-and-after goal states.