Compfiles/Imo2014P4.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2014, Problem 4

Let P and Q be on segment BC of an acute triangle ABC such that ∠PAB = ∠BCA and ∠CAQ = ∠ABC. Let M and N be points on lines AB and AQ, respectively, such that P is the midpoint of AM and Q is the midpoint of AN. Prove that BM and CN meet on the circumcircle of triangle ABC.

Imports (2)
Imported by 1 file
  1. lemma Imo2014P4.angle_eq_of_oangle_eq line 43 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, Real.Angle, EuclideanGeometry.oangle, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Ne, EuclideanGeometry.angle

    Proof uses: Eq.mpr, abs, Real.Angle.toReal, id, congrArg, EuclideanGeometry.angle_eq_abs_oangle_toReal, Eq.refl

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Imo2014P4.angle_eq_of_cos_angle_eq line 49 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, Real.cos, EuclideanGeometry.angle, ENNReal

    Proof uses: id, InnerProductGeometry.angle, VSub.vsub, Eq.mpr, Real.arccos, HDiv.hDiv, Inner.inner, HMul.hMul, Norm.norm, congrArg, Eq.mp, InnerProductGeometry.cos_angle, Eq.refl

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. lemma Imo2014P4.eq_max_of_max_ne_top line 56 source

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

    Statement uses: Submodule, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Eq, Module.finrank, Subtype, Membership.mem, Ne, Max.max, Top.top

    Proof uses: Submodule.eq_of_le_of_finrank_eq, le_sup_left, Eq.mpr, id, congrArg, LE.le, Submodule.finrank_le, congrFun', Eq.symm, Submodule.finrank_mono, Mathlib.Tactic.Contrapose.contrapose₄, Submodule.eq_top_of_finrank_eq, Fact.out, Imo2014P4.planeFiniteDim, Eq.refl, dite, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Eq.mp and 5 more

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  4. lemma Imo2014P4.affineSpan_pair_finrank line 73 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Ne, Eq, Module.finrank, Subtype, Membership.mem, Submodule, ENNReal, AffineSubspace.direction, affineSpan, Insert.insert, Set, Singleton.singleton

    Proof uses: Eq.mpr, vectorSpan, id, congrArg, direction_affineSpan, AffineIndependent, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, affineIndependent_of_ne, Set.range, congrFun', Eq.trans, Union.union, Matrix.range_cons, EmptyCollection.emptyCollection, Matrix.range_empty, Set.union_empty, Set.union_singleton, Set.pair_comm and 10 more

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  5. lemma Imo2014P4.inter_nonempty_of_not_parallel line 84 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Ne, Not, AffineSubspace.Parallel, ENNReal, affineSpan, Insert.insert, Set, Singleton.singleton, Set.Nonempty, Inter.inter, AffineSubspace

    Proof uses: Exists.intro, Membership.mem, mem_affineSpan, of_eq_true, Eq.trans, Or, Eq, True, congr, congrArg, eq_self, true_or, AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top, Mathlib.Tactic.Contrapose.contrapose₂, Submodule, Max.max, AffineSubspace.direction, Top.top, id, Eq.mpr and 18 more

    83 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  6. lemma Imo2014P4.mem_affineSpan_pair_of_collinear line 111 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Ne, Collinear, ENNReal, Insert.insert, Set, Singleton.singleton, Membership.mem, AffineSubspace, affineSpan

    Proof uses: Collinear.mem_affineSpan_of_mem_of_ne, of_eq_true, Eq.trans, Or, Eq, True, congrArg, congr, eq_self, true_or, or_true

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  7. lemma Imo2014P4.mem_circumsphere_of_concyclic line 116 source

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

    Statement uses: Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, EuclideanGeometry.Concyclic, Insert.insert, Set, Affine.Simplex.points, HAdd.hAdd, Singleton.singleton, Membership.mem, EuclideanGeometry.Sphere, Affine.Simplex.circumsphere

    Proof uses: EuclideanGeometry.Cospherical, EuclideanGeometry.Concyclic.Cospherical, LE.le, Metric.sphere, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.radius, Exists, Eq.mp, congrArg, propext, EuclideanGeometry.cospherical_iff_exists_sphere, And, AffineSubspace, affineSpan, Set.range, Eq, And.right, Affine.Simplex.circumsphere_unique_dist_eq, And.intro, Eq.mpr and 36 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  8. structure Imo2014P4.Imo2014q4Cfg line 138 source

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

  9. def Imo2014P4.Imo2014q4Cfg.symm line 155 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg

    Proof uses: Imo2014P4.Imo2014q4Cfg.mk, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.Q, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.N, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.hQAN, Imo2014P4.Imo2014q4Cfg.hPAM

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  10. def Imo2014P4.Imo2014q4Cfg.L line 190 source

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

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

    Proof uses: midpoint, ENNReal, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.C

    32 instances, coercions and auxiliary constants left out.

  11. def Imo2014P4.Imo2014q4Cfg.ABC line 192 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal

    Proof uses: Affine.Simplex.mk, Matrix.vecCons, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.C, Matrix.vecEmpty, Imo2014P4.Imo2014q4Cfg.hABC

    52 instances, coercions and auxiliary constants left out.

  12. def Imo2014P4.Imo2014q4Cfg.D_set line 195 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

    Proof uses: Inter.inter, AffineSubspace, ENNReal, affineSpan, Insert.insert, Imo2014P4.Imo2014q4Cfg.B, Singleton.singleton, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.N

    32 instances, coercions and auxiliary constants left out.

  13. lemma Imo2014P4.Imo2014q4Cfg.L_symm line 197 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.symm

    Proof uses: id, midpoint_comm, ENNReal, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.C

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. lemma Imo2014P4.Imo2014q4Cfg.D_symm line 201 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.D_set, Imo2014P4.Imo2014q4Cfg.symm

    Proof uses: id, Eq.mpr, Inter.inter, AffineSubspace, ENNReal, affineSpan, Insert.insert, Imo2014P4.Imo2014q4Cfg.B, Singleton.singleton, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.N, congrArg, Set.inter_comm, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  15. lemma Imo2014P4.Imo2014q4Cfg.B_ne_A line 205 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.A

    Proof uses: Function.Injective.ne, Nat.succ, Matrix.vecCons, Imo2014P4.Imo2014q4Cfg.C, Matrix.vecEmpty, AffineIndependent.injective, ENNReal, Imo2014P4.Imo2014q4Cfg.hABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  16. lemma Imo2014P4.Imo2014q4Cfg.C_ne_A line 208 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.A

    Proof uses: Function.Injective.ne, Nat.succ, Matrix.vecCons, Imo2014P4.Imo2014q4Cfg.B, Matrix.vecEmpty, AffineIndependent.injective, ENNReal, Imo2014P4.Imo2014q4Cfg.hABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  17. lemma Imo2014P4.Imo2014q4Cfg.C_ne_B line 211 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.B

    Proof uses: Function.Injective.ne, Nat.succ, Matrix.vecCons, Imo2014P4.Imo2014q4Cfg.A, Matrix.vecEmpty, AffineIndependent.injective, ENNReal, Imo2014P4.Imo2014q4Cfg.hABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  18. lemma Imo2014P4.Imo2014q4Cfg.sin_angle_in_ABC_pos line 214 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Fin, OfNat.ofNat, Nat, Function.Injective, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne, Real, Real.sin, EuclideanGeometry.angle, EuclideanSpace, ENNReal, Affine.Simplex.points, Imo2014P4.Imo2014q4Cfg.ABC

    Proof uses: EuclideanGeometry.sin_ne_zero_of_not_collinear, Eq.mpr, Not, Collinear, Insert.insert, Set, Singleton.singleton, AffineIndependent, id, Eq, congrArg, Eq.symm, propext, affineIndependent_iff_not_collinear_set, Function.comp, HAdd.hAdd, funext, PiLp.ext, List, List.Mem and 25 more

    85 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  19. lemma Imo2014P4.Imo2014q4Cfg.angle_in_ABC_pos line 225 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Fin, OfNat.ofNat, Nat, Function.Injective, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne, Real, EuclideanGeometry.angle, EuclideanSpace, ENNReal, Affine.Simplex.points, Imo2014P4.Imo2014q4Cfg.ABC

    Proof uses: Real.sin, Imo2014P4.Imo2014q4Cfg.sin_angle_in_ABC_pos, Mathlib.Tactic.Contrapose.contrapose₄, Eq, Eq.mpr, id, congrArg, Real.sin_zero

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  20. lemma Imo2014P4.Imo2014q4Cfg.P_ne_B line 232 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.B

    Proof uses: Eq, EuclideanGeometry.angle, ENNReal, Imo2014P4.Imo2014q4Cfg.A, EuclideanGeometry.angle_self_of_ne, Imo2014P4.Imo2014q4Cfg.B_ne_A, Mathlib.Tactic.Contrapose.contrapose₃, id, Not, Eq.mpr, congrArg, Eq.symm, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.hPAB, Imo2014P4.Imo2014q4Cfg.angle_in_ABC_pos, of_decide_eq_true, Function.Injective, Nat.succ, Matrix.vecCons, Matrix.vecEmpty and 4 more

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  21. lemma Imo2014P4.Imo2014q4Cfg.oangle_PBA_eq_CBA line 239 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: Wbtw.oangle_eq_left, Imo2014P4.Imo2014q4Cfg.hP, Imo2014P4.Imo2014q4Cfg.P_ne_B

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  22. lemma Imo2014P4.Imo2014q4Cfg.PBA_eq_CBA line 243 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: Imo2014P4.angle_eq_of_oangle_eq, Imo2014P4.Imo2014q4Cfg.oangle_PBA_eq_CBA, Imo2014P4.Imo2014q4Cfg.P_ne_B, Ne.symm, Imo2014P4.Imo2014q4Cfg.B_ne_A, Imo2014P4.Imo2014q4Cfg.C_ne_B

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  23. lemma Imo2014P4.Imo2014q4Cfg.P_ne_A line 246 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.A

    Proof uses: Eq, EuclideanGeometry.angle, ENNReal, Imo2014P4.Imo2014q4Cfg.B, EuclideanGeometry.angle_self_of_ne, Ne.symm, Imo2014P4.Imo2014q4Cfg.B_ne_A, Mathlib.Tactic.Contrapose.contrapose₃, id, Not, Eq.mpr, congrArg, Eq.symm, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.PBA_eq_CBA, Imo2014P4.Imo2014q4Cfg.angle_in_ABC_pos, of_decide_eq_true, Function.Injective, Nat.succ, Matrix.vecCons and 5 more

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  24. lemma Imo2014P4.Imo2014q4Cfg.oangle_PAB_eq_BCA line 253 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq, Imo2014P4.Imo2014q4Cfg.hPAB, Eq.mpr, SignType, Real.Angle.sign, Neg.neg, id, congrArg, Eq.symm, EuclideanGeometry.oangle_swap₂₃_sign, EuclideanGeometry.oangle_swap₁₂_sign, Imo2014P4.Imo2014q4Cfg.oangle_PBA_eq_CBA, Eq.refl

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  25. lemma Imo2014P4.Imo2014q4Cfg.APB_eq_CBA line 259 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: HAdd.hAdd, Real.pi, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Imo2014P4.Imo2014q4Cfg.B_ne_A, Eq.mpr, id, congrArg, Eq.mp, propext, add_left_cancel_iff, add_right_comm, EuclideanGeometry.angle_comm, Imo2014P4.Imo2014q4Cfg.PBA_eq_CBA, Imo2014P4.Imo2014q4Cfg.hPAB, Eq.symm, Eq.refl

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  26. lemma Imo2014P4.Imo2014q4Cfg.AB_to_AP_eq_CB_to_CA line 267 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, HDiv.hDiv, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: HMul.hMul, Real.sin, EuclideanGeometry.angle, EuclideanGeometry.law_sin, Eq.mpr, id, congrArg, propext, div_eq_div_iff, Iff.mpr, Ne, dist_ne_zero, Ne.symm, Imo2014P4.Imo2014q4Cfg.P_ne_A, Imo2014P4.Imo2014q4Cfg.C_ne_A, Imo2014P4.Imo2014q4Cfg.sin_angle_in_ABC_pos, of_decide_eq_true, Function.Injective, Nat.succ, Matrix.vecCons and 32 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  27. lemma Imo2014P4.Imo2014q4Cfg.AB_to_AM_eq_CL_to_CA line 284 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, HDiv.hDiv, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.L

    Proof uses: Eq.mpr, midpoint, id, congrArg, Imo2014P4.Imo2014q4Cfg.L.eq_1, HMul.hMul, Inv.inv, Norm.norm, dist_right_midpoint, dist_comm, mul_div_assoc, Imo2014P4.Imo2014q4Cfg.P, Eq.symm, Imo2014P4.Imo2014q4Cfg.AB_to_AP_eq_CB_to_CA, Imo2014P4.Imo2014q4Cfg.hPAM, dist_left_midpoint, Real.norm_ofNat, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow and 34 more

    107 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  28. lemma Imo2014P4.Imo2014q4Cfg.wbtw_APM line 289 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Wbtw, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.M

    Proof uses: Eq.mpr, midpoint, id, Eq, congrArg, Imo2014P4.Imo2014q4Cfg.hPAM, wbtw_midpoint

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  29. lemma Imo2014P4.Imo2014q4Cfg.wbtw_CLB line 293 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Wbtw, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.B

    Proof uses: Eq.mpr, midpoint, id, Eq, congrArg, Imo2014P4.Imo2014q4Cfg.L.eq_1, propext, wbtw_comm, wbtw_midpoint

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  30. lemma Imo2014P4.Imo2014q4Cfg.C_ne_L line 297 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.L

    Proof uses: Eq.mpr, LT.lt, Dist.dist, ENNReal, id, Eq, congrArg, Eq.symm, propext, dist_pos, midpoint, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.L.eq_1, HMul.hMul, Inv.inv, Norm.norm, dist_right_midpoint, Real.norm_ofNat, mul_pos, Mathlib.Meta.NormNum.isNNRat_lt_true and 10 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  31. lemma Imo2014P4.Imo2014q4Cfg.oangle_BAM_eq_LCA line 303 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: Eq.mpr, Imo2014P4.Imo2014q4Cfg.P, id, congrArg, Eq.symm, Wbtw.oangle_eq_left, Imo2014P4.Imo2014q4Cfg.wbtw_APM, Imo2014P4.Imo2014q4Cfg.P_ne_A, Imo2014P4.Imo2014q4Cfg.wbtw_CLB, Ne.symm, Imo2014P4.Imo2014q4Cfg.C_ne_L, Imo2014P4.Imo2014q4Cfg.oangle_PAB_eq_BCA

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  32. lemma Imo2014P4.Imo2014q4Cfg.M_ne_A line 308 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.A

    Proof uses: Imo2014P4.Imo2014q4Cfg.P, Imo2014P4.Imo2014q4Cfg.P_ne_A, Mathlib.Tactic.Contrapose.contrapose₄, Eq, Eq.mpr, Dist.dist, ENNReal, id, congrArg, Eq.symm, propext, dist_eq_zero, midpoint, Imo2014P4.Imo2014q4Cfg.hPAM, dist_comm, HMul.hMul, Inv.inv, Norm.norm, dist_left_midpoint, mul_eq_zero_of_right

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  33. lemma Imo2014P4.Imo2014q4Cfg.BAM_eq_LCA line 316 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: Imo2014P4.angle_eq_of_oangle_eq, Imo2014P4.Imo2014q4Cfg.oangle_BAM_eq_LCA, Imo2014P4.Imo2014q4Cfg.M_ne_A, Imo2014P4.Imo2014q4Cfg.B_ne_A, Ne.symm, Imo2014P4.Imo2014q4Cfg.C_ne_L, Imo2014P4.Imo2014q4Cfg.C_ne_A

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  34. lemma Imo2014P4.Imo2014q4Cfg.BM_to_AM_eq_LA_to_CA line 319 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, HDiv.hDiv, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Eq.symm, propext, mul_self_inj, div_nonneg, dist_nonneg, HPow.hPow, pow_two, div_pow, HSub.hSub, HAdd.hAdd, Real.cos, EuclideanGeometry.angle, EuclideanGeometry.law_cos, sub_div, add_div, EuclideanGeometry.angle_comm and 16 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  35. lemma Imo2014P4.Imo2014q4Cfg.L_ne_A line 340 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.A

    Proof uses: Wbtw, ENNReal, Imo2014P4.Imo2014q4Cfg.B, midpoint, Imo2014P4.Imo2014q4Cfg.C, wbtw_midpoint, Mathlib.Tactic.Contrapose.contrapose₃, Eq, Eq.mpr, Not, id, congrArg, Affine.Simplex.points, Imo2014P4.Imo2014q4Cfg.ABC, AffineIndependent.not_wbtw_of_injective, of_decide_eq_true, Function.Injective, Nat.succ, Matrix.vecCons, Matrix.vecEmpty and 8 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  36. lemma Imo2014P4.Imo2014q4Cfg.B_ne_M line 348 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.M

    Proof uses: Eq, HDiv.hDiv, Dist.dist, ENNReal, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.L, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.BM_to_AM_eq_LA_to_CA, Mathlib.Tactic.Contrapose.contrapose₁, Or, False, Eq.mpr, Not, True, And, id, implies_congr, not_false_eq_true, congrArg, propext and 9 more

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  37. lemma Imo2014P4.Imo2014q4Cfg.MBA_eq_CLA line 359 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.L

    Proof uses: Imo2014P4.angle_eq_of_cos_angle_eq, HSub.hSub, HAdd.hAdd, HMul.hMul, Dist.dist, Real.cos, Eq.symm, EuclideanGeometry.law_cos, Eq.mpr, id, congrArg, EuclideanGeometry.angle_comm, mul_left_cancel₀, HDiv.hDiv, Ne, mul_assoc, mul_ne_zero, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 29 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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

  38. lemma Imo2014P4.Imo2014q4Cfg.oangle_MBA_eq_CLA line 395 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.L

    Proof uses: EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq, Imo2014P4.Imo2014q4Cfg.MBA_eq_CLA, Eq.mpr, SignType, Real.Angle.sign, Neg.neg, id, congrArg, Eq.symm, EuclideanGeometry.oangle_swap₂₃_sign, EuclideanGeometry.oangle_swap₁₂_sign, Imo2014P4.Imo2014q4Cfg.oangle_BAM_eq_LCA, Eq.refl

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  39. lemma Imo2014P4.Imo2014q4Cfg.oangle_NCA_eq_BLA line 401 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.N, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.L

    Proof uses: Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.symm, Imo2014P4.Imo2014q4Cfg.oangle_MBA_eq_CLA, Eq.mp, congrArg, Eq.symm, Imo2014P4.Imo2014q4Cfg.L_symm

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  40. lemma Imo2014P4.Imo2014q4Cfg.oangle_NCA_MBA line 407 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Eq, Real.Angle, HSMul.hSMul, Int, OfNat.ofNat, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, Nat, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.N, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.B

    Proof uses: Eq.mpr, Imo2014P4.Imo2014q4Cfg.L, id, congrArg, Imo2014P4.Imo2014q4Cfg.oangle_MBA_eq_CLA, Imo2014P4.Imo2014q4Cfg.oangle_NCA_eq_BLA, Sbtw, midpoint, sbtw_midpoint_of_ne, Ne.symm, Imo2014P4.Imo2014q4Cfg.C_ne_B, HAdd.hAdd, Real.pi, Sbtw.oangle_eq_add_pi_left, Eq.mp, Eq.symm, Imo2014P4.Imo2014q4Cfg.L.eq_1, Imo2014P4.Imo2014q4Cfg.L_ne_A, smul_add, two_zsmul and 3 more

    111 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  41. lemma Imo2014P4.Imo2014q4Cfg.N_ne_Q line 414 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.P

    Proof uses: Eq.mpr, midpoint, ENNReal, Imo2014P4.Imo2014q4Cfg.A, id, Eq, congrArg, Imo2014P4.Imo2014q4Cfg.hPAM, Dist.dist, Eq.symm, propext, dist_ne_zero, HMul.hMul, Inv.inv, Norm.norm, dist_right_midpoint, mul_ne_zero, of_eq_true, Eq.trans, HDiv.hDiv and 21 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  42. lemma Imo2014P4.Imo2014q4Cfg.D_ne_C line 420 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, Set, Imo2014P4.Imo2014q4Cfg.D_set, Ne, Imo2014P4.Imo2014q4Cfg.C

    Proof uses: Eq, Collinear, ENNReal, Insert.insert, Imo2014P4.Imo2014q4Cfg.B, Singleton.singleton, Imo2014P4.Imo2014q4Cfg.M, collinear_insert_of_mem_affineSpan_pair, And.left, AffineSubspace, affineSpan, Imo2014P4.Imo2014q4Cfg.N, Eq.mp, And, congrArg, Inter.inter, propext, Set.mem_inter_iff, Imo2014P4.Imo2014q4Cfg.D_set.eq_1, Imo2014P4.Imo2014q4Cfg.P and 31 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

  43. lemma Imo2014P4.Imo2014q4Cfg.D_ne_B line 448 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, Set, Imo2014P4.Imo2014q4Cfg.D_set, Ne, Imo2014P4.Imo2014q4Cfg.B

    Proof uses: Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.symm, Imo2014P4.Imo2014q4Cfg.D_ne_C, Eq.mp, congrArg, Imo2014P4.Imo2014q4Cfg.D_symm

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  44. lemma Imo2014P4.Imo2014q4Cfg.oangle_DBA_MBA line 454 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, Set, Imo2014P4.Imo2014q4Cfg.D_set, Eq, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.M

    Proof uses: Collinear, Insert.insert, Singleton.singleton, collinear_insert_of_mem_affineSpan_pair, And.left, AffineSubspace, affineSpan, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.N, Eq.mp, Inter.inter, And, congrArg, propext, Set.mem_inter_iff, Imo2014P4.Imo2014q4Cfg.D_set.eq_1, Collinear.two_zsmul_oangle_eq_left, Imo2014P4.Imo2014q4Cfg.D_ne_B, Ne.symm, Imo2014P4.Imo2014q4Cfg.B_ne_M

    71 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  45. lemma Imo2014P4.Imo2014q4Cfg.oangle_DCA_NCA line 460 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, Set, Imo2014P4.Imo2014q4Cfg.D_set, Eq, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, ENNReal, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.N

    Proof uses: Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.symm, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.oangle_DBA_MBA, Eq.mp, congrArg, Imo2014P4.Imo2014q4Cfg.D_symm

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  46. theorem Imo2014P4.Imo2014q4Cfg.result₁ line 467 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, Set.Nonempty, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.D_set

    Proof uses: Imo2014P4.inter_nonempty_of_not_parallel, Imo2014P4.Imo2014q4Cfg.B, Imo2014P4.Imo2014q4Cfg.M, Imo2014P4.Imo2014q4Cfg.symm, Imo2014P4.Imo2014q4Cfg.B_ne_M, id, Not, AffineSubspace.Parallel, ENNReal, affineSpan, Insert.insert, Set, Singleton.singleton, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.N, AffineSubspace.Parallel.refl, Eq, Real.Angle, HSMul.hSMul, Int and 51 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  47. theorem Imo2014P4.Imo2014q4Cfg.result₂ line 491 source

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

    Statement uses: Imo2014P4.Imo2014q4Cfg, LE.le, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2014P4.Imo2014q4Cfg.D_set, Metric.sphere, ENNReal, EuclideanGeometry.Sphere.center, Affine.Simplex.circumsphere, Imo2014P4.Imo2014q4Cfg.ABC, EuclideanGeometry.Sphere.radius

    Proof uses: Membership.mem, Eq, Real.Angle, HSMul.hSMul, Int, EuclideanGeometry.oangle, Imo2014P4.planeFiniteDim, Imo2014P4.someOrientation, Imo2014P4.Imo2014q4Cfg.C, Imo2014P4.Imo2014q4Cfg.A, Imo2014P4.Imo2014q4Cfg.B, Eq.mpr, Imo2014P4.Imo2014q4Cfg.M, id, congrArg, Imo2014P4.Imo2014q4Cfg.oangle_DBA_MBA, Imo2014P4.Imo2014q4Cfg.N, Imo2014P4.Imo2014q4Cfg.oangle_DCA_NCA, Imo2014P4.Imo2014q4Cfg.oangle_NCA_MBA, EuclideanGeometry.Concyclic and 24 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  48. problem Imo2014P4.imo2014_p4 line 517 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, Wbtw, Eq, midpoint, Affine.Triangle, Affine.Simplex.mk, Set and 12 more

    Proof uses: Imo2014P4.Imo2014q4Cfg, Imo2014P4.Imo2014q4Cfg.mk, And.intro, Imo2014P4.Imo2014q4Cfg.result₁, Imo2014P4.Imo2014q4Cfg.result₂

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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