`Compfiles/Imo2025P6.lean`

247 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2025, Problem 6

Consider a 2025 × 2025 grid of unit squares. Matilda wishes to place on the grid some rectangular tiles, possibly of different sizes, such that each side of every tile lies on a grid line and every unit square is covered by at most one tile. Determine the minimum number of tiles Matilda needs to place so that each row and each column of the grid has exactly one unit square that is not covered by any tile.

Imports (7)

Imported by 1 file

Compfiles.lean

abbrev Imo2025P6.Point line 38 source
no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin
abbrev Imo2025P6.px line 43 source
no axioms what this means
Statement uses: Nat, Imo2025P6.Point
Proof uses: Prod.fst, Fin
1 instances, coercions and auxiliary constants left out.
abbrev Imo2025P6.py line 44 source
no axioms what this means
Statement uses: Nat, Imo2025P6.Point
Proof uses: Prod.snd, Fin
1 instances, coercions and auxiliary constants left out.
structure Imo2025P6.Matilda line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point
2 instances, coercions and auxiliary constants left out.
def Imo2025P6.Matilda.mem line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, NeZero, Imo2025P6.Matilda
Proof uses: And, LE.le, Imo2025P6.Matilda.x_min, Imo2025P6.px, Imo2025P6.Matilda.x_max, Imo2025P6.Matilda.y_min, Imo2025P6.py, Imo2025P6.Matilda.y_max
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.IsValidConfiguration line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Imo2025P6.Matilda
Proof uses: And, Eq, Finset.card, Membership.mem, Imo2025P6.px, Imo2025P6.py, Not, ExistsUnique, Imo2025P6.Matilda.mem
6 instances, coercions and auxiliary constants left out.
def Imo2025P6.IsMinMatildaCount line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
Proof uses: And, Finset, Imo2025P6.Point, Imo2025P6.Matilda, Imo2025P6.IsValidConfiguration, LE.le, Finset.card, Exists, Eq
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.incSequencesTo line 88 source
def Imo2025P6.decSequencesTo line 92 source
lemma Imo2025P6.one_mem_incSequencesTo line 96 source
lemma Imo2025P6.one_mem_decSequencesTo line 98 source
lemma Imo2025P6.incSequencesTo_nonempty line 101 source
lemma Imo2025P6.decSequencesTo_nonempty line 104 source
def Imo2025P6.maxIncSequencesTo line 107 source
def Imo2025P6.maxDecSequencesTo line 110 source
lemma Imo2025P6.one_le_maxIncSequencesTo line 113 source
lemma Imo2025P6.one_le_maxDecSequencesTo line 116 source
lemma Imo2025P6.maxIncSequencesTo_mem line 119 source
lemma Imo2025P6.maxDecSequencesTo_mem line 122 source
lemma Imo2025P6.maxIncSequencesTo_lt line 125 source
lemma Imo2025P6.maxDecSequencesTo_gt line 151 source
def Imo2025P6.paired line 155 source
lemma Imo2025P6.paired_injective line 158 source
theorem Imo2025P6.erdos_szekeres line 165 source
def Imo2025P6.rect line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, And, LE.le, Imo2025P6.px, LT.lt, Imo2025P6.py, Finset.univ, Fin
7 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_rect line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2025P6.Point, Iff, Membership.mem, Finset, Imo2025P6.rect, And, LE.le, Imo2025P6.px, LT.lt, Imo2025P6.py
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.univ, Fin, true_and, iff_self
15 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.chain_u_mono_le line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq, LE.le
Proof uses: Or, lt_or_eq_of_le, le_of_lt, Eq.le, congrArg
13 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.chain_v_mono_le line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq, LE.le
Proof uses: Or, lt_or_eq_of_le, le_of_lt, Eq.le, congrArg, Eq.symm
13 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.chain_u_inj_y line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq
Proof uses: Or, lt_trichotomy, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Int, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, HPow.hPow, Nat.rawCast and 41 more
67 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.chain_v_inj_y line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq
Proof uses: Or, lt_trichotomy, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Int, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, HPow.hPow, Nat.rawCast and 41 more
67 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.u_lower line 257 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.biUnion, Fin, Imo2025P6.rect, Imo2025P6.px, OfNat.ofNat, HAdd.hAdd, Imo2025P6.py
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.u_upper line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.biUnion, Fin, Imo2025P6.rect, OfNat.ofNat, HAdd.hAdd, Imo2025P6.px, Imo2025P6.py
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.v_lower line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.biUnion, Fin, Imo2025P6.rect, OfNat.ofNat, HAdd.hAdd, Imo2025P6.px, Imo2025P6.py
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.v_upper line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.biUnion, Fin, Imo2025P6.rect, Imo2025P6.px, Imo2025P6.py
2 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_u_lower line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.u_lower, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py
Proof uses: of_eq_true, Eq.trans, Fin, Prod.mk, Prod.fst, Prod.snd, True, congr, congrArg, Finset.biUnion, Imo2025P6.rect, OfNat.ofNat, HAdd.hAdd, funext, LT.lt, true_and, Prod, iff_self
36 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_u_upper line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.u_upper, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py
Proof uses: of_eq_true, Eq.trans, Fin, Prod.mk, Prod.fst, Prod.snd, True, congr, congrArg, Finset.biUnion, Imo2025P6.rect, OfNat.ofNat, HAdd.hAdd, funext, LT.lt, and_true, true_and, Prod, iff_self
36 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_v_lower line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.v_lower, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py
Proof uses: of_eq_true, Eq.trans, Fin, Prod.mk, Prod.fst, Prod.snd, True, congr, congrArg, Finset.biUnion, Imo2025P6.rect, OfNat.ofNat, HAdd.hAdd, funext, LT.lt, true_and, Prod, iff_self
35 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_v_upper line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.v_upper, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py
Proof uses: of_eq_true, Eq.trans, Fin, Prod.mk, Prod.fst, Prod.snd, True, congr, congrArg, Finset.biUnion, Imo2025P6.rect, funext, LT.lt, and_true, true_and, Prod, iff_self
15 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.regionWExtend line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Inter.inter, Fin, Imo2025P6.u_lower, Imo2025P6.v_lower
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.regionNExtend line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Inter.inter, Fin, Imo2025P6.u_upper, Imo2025P6.v_lower
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.regionSExtend line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Inter.inter, Fin, Imo2025P6.u_lower, Imo2025P6.v_upper
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.regionEExtend line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Inter.inter, Fin, Imo2025P6.u_upper, Imo2025P6.v_upper
3 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_regionWExtend line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.regionWExtend, And, Imo2025P6.u_lower, Imo2025P6.v_lower
Proof uses: id, of_eq_true, Inter.inter, Fin, Eq.trans, Exists, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Imo2025P6.px, Imo2025P6.py, funext, Prod, iff_self
14 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_regionNExtend line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.regionNExtend, And, Imo2025P6.u_upper, Imo2025P6.v_lower
Proof uses: id, of_eq_true, Inter.inter, Fin, Eq.trans, Exists, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Imo2025P6.px, Imo2025P6.py, funext, Prod, iff_self
14 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_regionSExtend line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.regionSExtend, And, Imo2025P6.u_lower, Imo2025P6.v_upper
Proof uses: id, of_eq_true, Inter.inter, Fin, Eq.trans, Exists, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Imo2025P6.px, Imo2025P6.py, funext, Prod, iff_self
14 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_regionEExtend line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.regionEExtend, And, Imo2025P6.u_upper, Imo2025P6.v_upper
Proof uses: id, of_eq_true, Inter.inter, Fin, Eq.trans, Exists, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Imo2025P6.px, Imo2025P6.py, funext, Prod, iff_self
14 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.targetsW line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, Membership.mem, Imo2025P6.regionWExtend, Fin
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.targetsN line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, Membership.mem, Imo2025P6.regionNExtend, Fin
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.targetsS line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, Membership.mem, Imo2025P6.regionSExtend, Fin
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.targetsE line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, Membership.mem, Imo2025P6.regionEExtend, Fin
5 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_targetsW line 313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsW, And, Imo2025P6.regionWExtend
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, Imo2025P6.u_lower, Imo2025P6.v_lower, Imo2025P6.px, Imo2025P6.py, funext and 2 more
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_targetsN line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsN, And, Imo2025P6.regionNExtend
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, Imo2025P6.u_upper, Imo2025P6.v_lower, Imo2025P6.px, Imo2025P6.py, funext and 2 more
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_targetsS line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsS, And, Imo2025P6.regionSExtend
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, Imo2025P6.u_lower, Imo2025P6.v_upper, Imo2025P6.px, Imo2025P6.py, funext and 2 more
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_targetsE line 325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsE, And, Imo2025P6.regionEExtend
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, Imo2025P6.u_upper, Imo2025P6.v_upper, Imo2025P6.px, Imo2025P6.py, funext and 2 more
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.targetsWin line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, LT.lt, OfNat.ofNat, Imo2025P6.py, Imo2025P6.targetsW
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.targetsNin line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, LT.lt, OfNat.ofNat, Imo2025P6.px, Imo2025P6.targetsN
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.targetsSin line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, LT.lt, Imo2025P6.px, HSub.hSub, OfNat.ofNat, Imo2025P6.targetsS
5 instances, coercions and auxiliary constants left out.
def Imo2025P6.targetsEin line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Finset.filter, LT.lt, Imo2025P6.py, HSub.hSub, OfNat.ofNat, Imo2025P6.targetsE
5 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_targetsWin line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsWin, And, Imo2025P6.targetsW, LT.lt, OfNat.ofNat, Imo2025P6.py
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Imo2025P6.regionWExtend, Imo2025P6.u_lower, Imo2025P6.v_lower, Imo2025P6.px, funext, Prod, iff_self
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_targetsNin line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsNin, And, Imo2025P6.targetsN, LT.lt, OfNat.ofNat, Imo2025P6.px
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Imo2025P6.regionNExtend, Imo2025P6.u_upper, Imo2025P6.v_lower, Imo2025P6.py, funext, Prod, iff_self
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_targetsSin line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsSin, And, Imo2025P6.targetsS, LT.lt, Imo2025P6.px, HSub.hSub, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Imo2025P6.regionSExtend, Imo2025P6.u_lower, Imo2025P6.v_upper, Imo2025P6.py, funext, Prod, iff_self
22 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_targetsEin line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Iff, Membership.mem, Imo2025P6.targetsEin, And, Imo2025P6.targetsE, LT.lt, Imo2025P6.py, HSub.hSub, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Exists, Fin, Prod.mk, LE.le, Prod.fst, Prod.snd, True, congr, congrArg, Finset.filter, congrFun', Imo2025P6.regionEExtend, Imo2025P6.u_upper, Imo2025P6.v_upper, Imo2025P6.px, funext, Prod, iff_self
22 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.card_filter_ge_sub_one line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, DecidablePred, LE.le, Nat, Finset.card, Finset.filter, Not, OfNat.ofNat, GE.ge, HSub.hSub
Proof uses: Eq, HAdd.hAdd, Eq.symm, Finset.card_filter_add_card_filter_not
11 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.targetsWin_inequality line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Eq, Imo2025P6.py, GE.ge, Finset.card, Imo2025P6.targetsWin, HSub.hSub, Imo2025P6.targetsW, OfNat.ofNat
Proof uses: Imo2025P6.card_filter_ge_sub_one, Fin, LT.lt, Eq.mpr, LE.le, Finset.filter, Not, id, congrArg, propext, Finset.card_le_one_iff, Iff, And, Imo2025P6.regionWExtend, Imo2025P6.mem_targetsW, And.left, Eq.mp, Eq.trans, congrFun', Finset.filter_congr and 5 more
24 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.targetsNin_inequality line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Eq, Imo2025P6.px, GE.ge, Finset.card, Imo2025P6.targetsNin, HSub.hSub, Imo2025P6.targetsN, OfNat.ofNat
Proof uses: Imo2025P6.card_filter_ge_sub_one, Fin, LT.lt, Eq.mpr, LE.le, Finset.filter, Not, id, congrArg, propext, Finset.card_le_one_iff, Iff, And, Imo2025P6.regionNExtend, Imo2025P6.mem_targetsN, And.left, Eq.mp, Eq.trans, congrFun', Finset.filter_congr and 5 more
24 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.targetsSin_inequality line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Eq, Imo2025P6.px, GE.ge, Finset.card, Imo2025P6.targetsSin, HSub.hSub, Imo2025P6.targetsS, OfNat.ofNat
Proof uses: Imo2025P6.card_filter_ge_sub_one, Fin, LT.lt, Eq.mpr, LE.le, Finset.filter, Not, id, congrArg, propext, Finset.card_le_one_iff, Iff, And, Imo2025P6.regionSExtend, Imo2025P6.mem_targetsS, And.left, Eq.mp, Eq.trans, congrFun', Finset.filter_congr and 5 more
26 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.targetsEin_inequality line 390 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Eq, Imo2025P6.py, GE.ge, Finset.card, Imo2025P6.targetsEin, HSub.hSub, Imo2025P6.targetsE, OfNat.ofNat
Proof uses: Imo2025P6.card_filter_ge_sub_one, Fin, LT.lt, Eq.mpr, LE.le, Finset.filter, Not, id, congrArg, propext, Finset.card_le_one_iff, Iff, And, Imo2025P6.regionEExtend, Imo2025P6.mem_targetsE, And.left, Eq.mp, Eq.trans, congrFun', Finset.filter_congr and 5 more
26 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.incidence_count line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: HAdd.hAdd, ite, Membership.mem, Imo2025P6.targetsW, Fin, OfNat.ofNat, Imo2025P6.targetsN, Imo2025P6.targetsE, Imo2025P6.targetsS
8 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.sum_card_eq_sum_incidence line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Eq, HAdd.hAdd, Finset.card, Imo2025P6.targetsW, Imo2025P6.targetsN, Imo2025P6.targetsE, Imo2025P6.targetsS, Finset.sum, Imo2025P6.incidence_count
Proof uses: id, Eq.mpr, ite, Membership.mem, Fin, OfNat.ofNat, congrArg, Finset.sum_add_distrib, HAdd, Eq.rec, Eq.refl, Finset.card_eq_sum_ones, Finset.filter, Eq.symm, Finset.sum_filter, Finset.sum_congr, Finset.ext, Iff, And, of_eq_true and 24 more
36 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.u_parts_intersection_eq_u line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq, Inter.inter, Fin, Imo2025P6.u_lower, Imo2025P6.u_upper
Proof uses: Finset.ext, Eq.mpr, Iff, And, Exists, Prod.mk, LE.le, Prod.fst, Prod.snd, id, congrFun', congrArg, Eq.trans, congr, funext, Prod, Iff.intro, Or, lt_trichotomy, False.elim and 63 more
89 instances, coercions and auxiliary constants left out.
Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.v_parts_intersection_eq_v line 442 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq, Inter.inter, Fin, Imo2025P6.v_lower, Imo2025P6.v_upper
Proof uses: Finset.ext, Eq.mpr, Iff, And, Exists, Prod.mk, LE.le, Prod.fst, Prod.snd, id, congrFun', congrArg, Eq.trans, congr, funext, Prod, Iff.intro, Or, lt_trichotomy, False.elim and 63 more
89 instances, coercions and auxiliary constants left out.
Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.inter_card_le_one line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq, LE.le, Finset.card, Inter.inter, Fin, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, Exists, And, Ne, False, Eq.mp, congrArg, propext, Finset.one_lt_card_iff, not_le, Or, lt_trichotomy, And.left, Finset.mem_inter, And.right, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Int, HAdd.hAdd and 57 more
85 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.incidence_count_of_pivot line 481 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Eq, Inter.inter, Fin, Singleton.singleton, Membership.mem, Imo2025P6.incidence_count, OfNat.ofNat
Proof uses: Finset.mem_of_mem_inter_left, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, eq_self, Finset.mem_of_mem_inter_right, Imo2025P6.u_lower, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py, propext, Imo2025P6.mem_u_lower, Exists.intro, And.intro, le_refl and 26 more
26 instances, coercions and auxiliary constants left out.
Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.incidence_count_of_u_diff line 501 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Not, Eq, Inter.inter, Fin, Singleton.singleton, LE.le, LT.lt, Imo2025P6.px, Imo2025P6.py, Imo2025P6.incidence_count, OfNat.ofNat
Proof uses: Finset.mem_of_mem_inter_right, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, eq_self, Finset.mem_of_mem_inter_left, Imo2025P6.u_lower, Exists, And, propext, Imo2025P6.mem_u_lower, Exists.intro, And.intro, le_refl, Imo2025P6.u_upper, Imo2025P6.mem_u_upper, Iff and 38 more
39 instances, coercions and auxiliary constants left out.
Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.incidence_count_of_v_diff line 549 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Not, Eq, Inter.inter, Fin, Singleton.singleton, LE.le, LT.lt, Imo2025P6.px, Imo2025P6.py, Imo2025P6.incidence_count, OfNat.ofNat
Proof uses: Finset.mem_of_mem_inter_right, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, eq_self, Finset.mem_of_mem_inter_left, Imo2025P6.v_lower, Exists, And, propext, Imo2025P6.mem_v_lower, Exists.intro, And.intro, le_refl, Imo2025P6.v_upper, Imo2025P6.mem_v_upper, Iff and 38 more
39 instances, coercions and auxiliary constants left out.
Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.covering_of_maximal_u line 596 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Not, LT.lt, Imo2025P6.px, Imo2025P6.py, False, Or, Imo2025P6.u_lower, Imo2025P6.u_upper
Proof uses: Decidable.byContradiction, Fin, And, Eq.mp, Nat.lt_of_not_le, LE.le, Eq.trans, Exists, congrArg, forall_congr, implies_congr, Eq.refl, le_of_lt
18 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.covering_of_maximal_v line 616 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Not, LT.lt, Imo2025P6.px, Imo2025P6.py, False, Or, Imo2025P6.v_lower, Imo2025P6.v_upper
Proof uses: Decidable.byContradiction, Fin, And, Eq.mp, LE.le, le_of_lt, Nat.lt_of_not_le, Eq.trans, Exists, congrArg, forall_congr, implies_congr, Eq.refl
18 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.incidence_count_of_others line 638 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Membership.mem, Not, LT.lt, Imo2025P6.px, Imo2025P6.py, Eq, False, Imo2025P6.incidence_count, OfNat.ofNat
Proof uses: Or, Imo2025P6.u_lower, Imo2025P6.u_upper, Imo2025P6.covering_of_maximal_u, And, Eq.mpr, Inter.inter, Fin, id, congrArg, Eq.symm, Imo2025P6.u_parts_intersection_eq_u, Iff.mpr, Finset.mem_inter, And.intro, Imo2025P6.v_lower, Imo2025P6.v_upper, Imo2025P6.covering_of_maximal_v, Imo2025P6.v_parts_intersection_eq_v, HAdd.hAdd and 27 more
25 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.px_mk_val line 678 source
no axioms what this means
Statement uses: Nat, Fin, Eq, Imo2025P6.px, Prod.mk
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.py_mk_val line 679 source
no axioms what this means
Statement uses: Nat, Fin, Eq, Imo2025P6.py, Prod.mk
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.fin_val_sub_one_eq line 683 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, LT.lt, OfNat.ofNat, Eq, HSub.hSub
Proof uses: Fin.val_sub_one_of_ne_zero, ne_of_gt, Fin.neZero
17 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.fin_val_add_one_eq line 687 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, LT.lt, HSub.hSub, OfNat.ofNat, Eq, HAdd.hAdd
Proof uses: Eq.mpr, HMod.hMod, id, congrArg, Fin.val_add, congrFun', Nat.add_mod_mod, Nat.mod_eq_of_lt, Eq.refl
25 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.source_on_face_W line 691 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Imo2025P6.Matilda, Membership.mem, LT.lt, OfNat.ofNat, Imo2025P6.py, Imo2025P6.Matilda.mem, Prod.mk, Fin, Prod.fst, HSub.hSub, Prod.snd, And, Eq, HAdd.hAdd, Imo2025P6.Matilda.y_max, LE.le and 3 more
Proof uses: Imo2025P6.fin_val_sub_one_eq, id, Not, Imo2025P6.Matilda.y_min, Imo2025P6.Matilda.h_disjoint, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, And.intro
36 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.source_on_face_E line 702 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Imo2025P6.Matilda, Membership.mem, LT.lt, Imo2025P6.py, HSub.hSub, OfNat.ofNat, Imo2025P6.Matilda.mem, Prod.mk, Fin, Prod.fst, HAdd.hAdd, Prod.snd, And, Eq, Imo2025P6.Matilda.y_min, LE.le and 3 more
Proof uses: Imo2025P6.fin_val_add_one_eq, id, Not, Imo2025P6.Matilda.y_max, Imo2025P6.Matilda.h_disjoint, Decidable.byContradiction, dite, False, absurd, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl
40 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.source_on_face_N line 716 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Imo2025P6.Matilda, Membership.mem, LT.lt, OfNat.ofNat, Imo2025P6.px, Imo2025P6.Matilda.mem, Prod.mk, Fin, HSub.hSub, Prod.fst, Prod.snd, And, Eq, HAdd.hAdd, Imo2025P6.Matilda.x_max, LE.le and 3 more
Proof uses: Imo2025P6.fin_val_sub_one_eq, id, Not, Imo2025P6.Matilda.x_min, Imo2025P6.Matilda.h_disjoint, Decidable.byContradiction, dite, False, absurd, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl
39 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.source_on_face_S line 729 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Imo2025P6.Matilda, Membership.mem, LT.lt, Imo2025P6.px, HSub.hSub, OfNat.ofNat, Imo2025P6.Matilda.mem, Prod.mk, Fin, HAdd.hAdd, Prod.fst, Prod.snd, And, Eq, Imo2025P6.Matilda.x_min, LE.le and 3 more
Proof uses: Imo2025P6.fin_val_add_one_eq, id, Not, Imo2025P6.Matilda.x_max, Imo2025P6.Matilda.h_disjoint, Decidable.byContradiction, dite, False, absurd, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl
40 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.matilda_eq_iff_bounds_eq line 747 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, NeZero, Imo2025P6.Matilda, Iff, Eq, And, Imo2025P6.Matilda.x_min, Imo2025P6.Matilda.x_max, Imo2025P6.Matilda.y_min, Imo2025P6.Matilda.y_max
Proof uses: Iff.intro, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, eq_self, and_self, LE.le, LT.lt, Membership.mem, Not, Imo2025P6.px, Imo2025P6.py, Imo2025P6.Matilda.mk, Eq.refl
11 instances, coercions and auxiliary constants left out.
Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
instance Imo2025P6.(instance at line 760) line 760 source
instance Imo2025P6.(instance at line 774) line 774 source
inductive Imo2025P6.LabelType line 777 source
no axioms what this means
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Imo2025P6.(instance at line 781) line 781 source
structure Imo2025P6.Label line 785 source
no axioms what this means
Statement uses: Nat
lemma Imo2025P6.Label.source_ne_of_ne line 791 source
def Imo2025P6.Label.emb line 796 source
no axioms what this means
Statement uses: Nat, Imo2025P6.LabelType, Function.Embedding, Imo2025P6.Point, Imo2025P6.Label
Proof uses: Function.Embedding.mk, Imo2025P6.Label.mk
1 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.label_pos line 800 source
standard axioms: propext what this means
Statement uses: Nat, NeZero, Imo2025P6.Label, Prod, Imo2025P6.Point
Proof uses: Imo2025P6.Label.source, Imo2025P6.label_pos.match_1, Imo2025P6.LabelType, Imo2025P6.Label.type, Unit, Prod.mk, Fin, Prod.fst, HSub.hSub, Prod.snd, OfNat.ofNat, HAdd.hAdd
9 instances, coercions and auxiliary constants left out.
def Imo2025P6.covers line 810 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, NeZero, Imo2025P6.Matilda, Imo2025P6.Label
Proof uses: Imo2025P6.Matilda.mem, Prod.snd, Imo2025P6.label_pos
4 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance Imo2025P6.(instance at line 813) line 813 source
lemma Imo2025P6.matilda_count_ge_label_count line 823 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Imo2025P6.Label, Membership.mem, Not, Prod.snd, Imo2025P6.label_pos, Imo2025P6.Matilda, LE.le, Finset.card, Finset.filter, Imo2025P6.covers, OfNat.ofNat, ExistsUnique, And, Imo2025P6.Matilda.mem
Proof uses: Subtype, Exists.choose, Eq, Subtype.mk, And.left, Exists.choose_spec, Function.Injective, And.right, Eq.mpr, Subtype.property, id, congrArg, Eq.mp, rfl, Subtype.mk.injEq, Subtype.ext, propext, Finset.card_le_one_iff, Iff.mpr, Finset.mem_filter and 2 more
17 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.fin_ne_sub_one line 854 source
lemma Imo2025P6.fin_ne_add_one line 863 source
lemma Imo2025P6.label_pos_W_absurd line 871 source
lemma Imo2025P6.label_pos_N_absurd line 879 source
lemma Imo2025P6.label_pos_E_absurd line 887 source
lemma Imo2025P6.label_pos_S_absurd line 895 source
lemma Imo2025P6.am_gm_bound_nat line 903 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, Nat.sqrt, OfNat.ofNat, HAdd.hAdd
Proof uses: Nat.mul_le_mul_left, Trans.trans, Eq, HPow.hPow, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right and 25 more
52 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
structure Imo2025P6.BaseSetup line 917 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
2 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.BaseSetup.u_mono_le line 948 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.BaseSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, LE.le, Imo2025P6.px, Imo2025P6.py
Proof uses: Imo2025P6.chain_u_mono_le, Imo2025P6.BaseSetup.h_u_mono, Imo2025P6.BaseSetup.h_u_inj
7 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.BaseSetup.v_mono_le line 950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.BaseSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, LE.le, Imo2025P6.px, Imo2025P6.py
Proof uses: Imo2025P6.chain_v_mono_le, Imo2025P6.BaseSetup.h_v_mono, Imo2025P6.BaseSetup.h_v_inj
7 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.BaseSetup.u_inj_y line 952 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.BaseSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Eq, Imo2025P6.py
Proof uses: Imo2025P6.chain_u_inj_y, Imo2025P6.BaseSetup.h_u_mono, Imo2025P6.BaseSetup.h_u_inj
6 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.BaseSetup.v_inj_y line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.BaseSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Eq, Imo2025P6.py
Proof uses: Imo2025P6.chain_v_inj_y, Imo2025P6.BaseSetup.h_v_mono, Imo2025P6.BaseSetup.h_v_inj
6 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.BaseSetup.union_sub line 957 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.BaseSetup, LE.le, Finset, Imo2025P6.Point, Union.union, Fin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black
Proof uses: Finset.union_subset, Imo2025P6.BaseSetup.hu_sub, Imo2025P6.BaseSetup.hv_sub
12 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.matilda_covers_at_most_one_core line 961 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Finset, Imo2025P6.Point, Membership.mem, Eq, Imo2025P6.px, Imo2025P6.py, LE.le, Imo2025P6.Matilda, Imo2025P6.Label, Ne, Imo2025P6.Matilda.mem, Prod.snd, Imo2025P6.label_pos, And, Imo2025P6.LabelType, Imo2025P6.Label.type, Imo2025P6.LabelType.W, Imo2025P6.targetsWin and 9 more
Proof uses: And.left, HAdd.hAdd, Imo2025P6.Matilda.y_max, OfNat.ofNat, Imo2025P6.Matilda.x_min, Imo2025P6.Matilda.x_max, Imo2025P6.source_on_face_W, Imo2025P6.regionWExtend, LT.lt, Eq.mp, Eq.trans, Imo2025P6.targetsW, congrFun', congrArg, And.right, Prod.fst, Fin, Imo2025P6.Matilda.y_min, HSub.hSub, congr and 97 more
124 instances, coercions and auxiliary constants left out.
Tactic trace: 266 steps (first 200 of 266)
Open to load the checked before-and-after goal states.
structure Imo2025P6.IntersectionSetup line 1236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
2 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.pivot_mem_u line 1244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Membership.mem, Imo2025P6.Point, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.IntersectionSetup.pivot
Proof uses: Finset.mem_of_mem_inter_left, Fin, Imo2025P6.BaseSetup.v, Eq.mpr, Inter.inter, Singleton.singleton, id, Eq, congrArg, Imo2025P6.IntersectionSetup.h_inter, of_eq_true, Eq.trans, True, eq_self
13 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.pivot_mem_v line 1246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Membership.mem, Imo2025P6.Point, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.IntersectionSetup.pivot
Proof uses: Finset.mem_of_mem_inter_right, Fin, Imo2025P6.BaseSetup.u, Eq.mpr, Inter.inter, Singleton.singleton, id, Eq, congrArg, Imo2025P6.IntersectionSetup.h_inter, of_eq_true, Eq.trans, True, eq_self
13 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.a_pos line 1249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, LE.le, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.IntersectionSetup.toBaseSetup
Proof uses: Eq.rec, Finset.card, Imo2025P6.Point, Imo2025P6.BaseSetup.u, Eq, Iff.mpr, LT.lt, Finset.Nonempty, Finset.card_pos, Exists.intro, Membership.mem, Finset, Imo2025P6.IntersectionSetup.pivot, Imo2025P6.IntersectionSetup.pivot_mem_u, Imo2025P6.BaseSetup.hu
11 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.b_pos line 1251 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, LE.le, OfNat.ofNat, Imo2025P6.BaseSetup.b, Imo2025P6.IntersectionSetup.toBaseSetup
Proof uses: Eq.rec, Finset.card, Imo2025P6.Point, Imo2025P6.BaseSetup.v, Eq, Iff.mpr, LT.lt, Finset.Nonempty, Finset.card_pos, Exists.intro, Membership.mem, Finset, Imo2025P6.IntersectionSetup.pivot, Imo2025P6.IntersectionSetup.pivot_mem_v, Imo2025P6.BaseSetup.hv
11 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.disj_piv_u line 1254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Disjoint, Finset, Imo2025P6.Point, Singleton.singleton, Imo2025P6.IntersectionSetup.pivot, SDiff.sdiff, Fin, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup
Proof uses: disjoint_sdiff_self_right
14 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.disj_piv_v line 1255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Disjoint, Finset, Imo2025P6.Point, Singleton.singleton, Imo2025P6.IntersectionSetup.pivot, SDiff.sdiff, Fin, Imo2025P6.BaseSetup.v, Imo2025P6.IntersectionSetup.toBaseSetup
Proof uses: disjoint_sdiff_self_right
14 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.disj_u_v_diff line 1256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Disjoint, Finset, Imo2025P6.Point, SDiff.sdiff, Fin, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Singleton.singleton, Imo2025P6.IntersectionSetup.pivot, Imo2025P6.BaseSetup.v
Proof uses: Eq.mpr, Eq, Inter.inter, EmptyCollection.emptyCollection, id, congrArg, propext, Finset.disjoint_iff_inter_eq_empty, Finset.ext, Iff, Membership.mem, Not, Eq.trans, And, False, congr, congrFun', Finset.sdiff_inter_self_left, Finset.sdiff_inter_self_right, iff_false and 3 more
28 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.disj_middle line 1258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Disjoint, Finset, Imo2025P6.Point, Union.union, Fin, Singleton.singleton, Imo2025P6.IntersectionSetup.pivot, SDiff.sdiff, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v
Proof uses: Eq.mpr, And, id, Eq, congrArg, propext, Finset.disjoint_union_left, And.intro, Imo2025P6.IntersectionSetup.disj_piv_v, Imo2025P6.IntersectionSetup.disj_u_v_diff
18 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.IntersectionSetup.Others line 1261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Finset, Imo2025P6.Point
Proof uses: SDiff.sdiff, Fin, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, Union.union, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v
8 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.partition_eq line 1263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Eq, Finset, Imo2025P6.Point, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, Union.union, Fin, Singleton.singleton, Imo2025P6.IntersectionSetup.pivot, SDiff.sdiff, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Imo2025P6.IntersectionSetup.Others
Proof uses: Eq.mpr, Inter.inter, id, congrArg, Eq.symm, Imo2025P6.IntersectionSetup.h_inter, Finset.ext, Membership.mem, Imo2025P6.BaseSetup.hu_sub, Imo2025P6.BaseSetup.hv_sub, Iff, Or, And, Not, Eq.trans, congr, Decidable.not_or_of_imp, Iff.intro, Iff.mpr, Classical.or_iff_not_imp_left and 7 more
25 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.disj_others line 1271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Disjoint, Finset, Imo2025P6.Point, Union.union, Fin, Singleton.singleton, Imo2025P6.IntersectionSetup.pivot, SDiff.sdiff, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.IntersectionSetup.Others
Proof uses: Eq.mpr, Eq, Inter.inter, EmptyCollection.emptyCollection, id, congrArg, propext, Finset.disjoint_iff_inter_eq_empty, Finset.ext, Iff, Membership.mem, Eq.symm, Imo2025P6.IntersectionSetup.h_inter, Or, And, Not, Imo2025P6.BaseSetup.all_black, Eq.trans, False, congr and 8 more
32 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.IntersectionSetup.total_labels_eq_sum line 1275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Eq, HAdd.hAdd, Finset.card, Imo2025P6.Point, Imo2025P6.targetsW, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.targetsN, Imo2025P6.targetsE, Imo2025P6.targetsS, Imo2025P6.BaseSetup.a, Imo2025P6.BaseSetup.b, OfNat.ofNat
Proof uses: Finset, Imo2025P6.IntersectionSetup.pivot, Eq.mpr, Finset.sum, Imo2025P6.incidence_count, id, congrArg, Imo2025P6.sum_card_eq_sum_incidence, Union.union, Fin, Singleton.singleton, SDiff.sdiff, Imo2025P6.IntersectionSetup.Others, Imo2025P6.IntersectionSetup.partition_eq, Finset.sum_union, Imo2025P6.IntersectionSetup.disj_others, Imo2025P6.IntersectionSetup.disj_middle, Imo2025P6.IntersectionSetup.disj_piv_u, Finset.sum_singleton, Imo2025P6.incidence_count_of_pivot and 69 more
72 instances, coercions and auxiliary constants left out.
Tactic trace: 69 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.IntersectionSetup.labels_total_intersection line 1352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, GE.ge, HAdd.hAdd, Finset.card, Imo2025P6.Point, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.targetsNin, Imo2025P6.targetsEin, Imo2025P6.targetsSin, HSub.hSub, Imo2025P6.BaseSetup.a, Imo2025P6.BaseSetup.b, OfNat.ofNat
Proof uses: Eq, Imo2025P6.targetsW, Imo2025P6.targetsN, Imo2025P6.targetsE, Imo2025P6.targetsS, Imo2025P6.IntersectionSetup.total_labels_eq_sum, Nat.le_add_of_sub_le, Imo2025P6.targetsWin_inequality, Imo2025P6.BaseSetup.h_unique_y, Imo2025P6.targetsNin_inequality, Imo2025P6.BaseSetup.h_unique_x, Imo2025P6.targetsSin_inequality, Imo2025P6.targetsEin_inequality, LE.le, Imo2025P6.IntersectionSetup.a_pos, Imo2025P6.IntersectionSetup.b_pos, Trans.trans, Eq.symm, Imo2025P6.BaseSetup.hu, Finset.card_le_card and 78 more
85 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.IntersectionSetup.validLabels line 1376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Finset, Imo2025P6.Label
Proof uses: Union.union, Finset.map, Imo2025P6.Point, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.LabelType.N, Imo2025P6.targetsNin, Imo2025P6.LabelType.E, Imo2025P6.targetsEin, Imo2025P6.LabelType.S, Imo2025P6.targetsSin
6 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.IntersectionSetup.card_validLabels line 1382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Eq, Finset.card, Imo2025P6.Label, Imo2025P6.IntersectionSetup.validLabels, HAdd.hAdd, Imo2025P6.Point, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.targetsNin, Imo2025P6.targetsEin, Imo2025P6.targetsSin
Proof uses: Eq.mpr, Union.union, Finset, Finset.map, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Imo2025P6.LabelType.N, Imo2025P6.LabelType.E, Imo2025P6.LabelType.S, id, congrArg, Imo2025P6.IntersectionSetup.validLabels.eq_1, Finset.card_union_of_disjoint, Disjoint, Membership.mem, Not, propext, Finset.disjoint_left, Or, Exists and 47 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.not_valid_label_X line 1399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Imo2025P6.Label, Membership.mem, Finset, Imo2025P6.IntersectionSetup.validLabels, Eq, Imo2025P6.LabelType, Imo2025P6.Label.type, Imo2025P6.LabelType.X, False
Proof uses: Exists, Imo2025P6.Point, And, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Function.Embedding, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Or, Imo2025P6.targetsNin, Imo2025P6.LabelType.N, Imo2025P6.targetsEin, Imo2025P6.LabelType.E, Imo2025P6.targetsSin, Imo2025P6.LabelType.S, Eq.mp, Eq.trans and 8 more
19 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.matilda_covers_at_most_one line 1405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, LE.le, Finset.card, Imo2025P6.Label, Finset.filter, Imo2025P6.covers, Imo2025P6.IntersectionSetup.validLabels, OfNat.ofNat
Proof uses: Eq.mpr, Membership.mem, Finset, Eq, id, congrArg, propext, Finset.card_le_one_iff, And, Eq.mp, Finset.mem_filter, Decidable.byContradiction, Not, Imo2025P6.LabelType, Imo2025P6.Label.type, Imo2025P6.LabelType.W, Imo2025P6.Point, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v and 58 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.grid_size_ge_two_of_label line 1428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Imo2025P6.Point, Imo2025P6.LabelType, Membership.mem, Imo2025P6.Label, Finset, Imo2025P6.IntersectionSetup.validLabels, Imo2025P6.Label.mk, LE.le, OfNat.ofNat
Proof uses: Eq, Imo2025P6.LabelType.W, Eq.mp, Or, Exists, And, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.regionWExtend, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, LT.lt, Imo2025P6.py, Function.Embedding, Imo2025P6.Label.emb, Imo2025P6.targetsNin, Imo2025P6.LabelType.N, Imo2025P6.targetsEin, Imo2025P6.LabelType.E, Imo2025P6.targetsSin and 43 more
54 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.IntersectionSetup.valid_label_pos_not_black line 1437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Imo2025P6.Label, Membership.mem, Finset, Imo2025P6.IntersectionSetup.validLabels, Not, Imo2025P6.Point, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, Prod.snd, Imo2025P6.label_pos
Proof uses: False, Imo2025P6.LabelType, Imo2025P6.Label.mk, LE.le, OfNat.ofNat, Imo2025P6.IntersectionSetup.grid_size_ge_two_of_label, Imo2025P6.label_pos.match_1, Prod, Unit, Prod.mk, Fin, Prod.fst, HSub.hSub, HAdd.hAdd, Or, Exists, And, Imo2025P6.regionWExtend, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v and 99 more
116 instances, coercions and auxiliary constants left out.
Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.IntersectionSetup.matildas_count_ge_intersection_bound line 1477 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Finset, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.Point, Not, Membership.mem, ExistsUnique, And, Imo2025P6.Matilda.mem, LE.le, HSub.hSub, HAdd.hAdd, Imo2025P6.BaseSetup.a, Imo2025P6.BaseSetup.b, OfNat.ofNat, Finset.card
Proof uses: Imo2025P6.Label, Imo2025P6.IntersectionSetup.validLabels, Imo2025P6.matilda_count_ge_label_count, Imo2025P6.IntersectionSetup.valid_label_pos_not_black, Imo2025P6.IntersectionSetup.matilda_covers_at_most_one, GE.ge, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Imo2025P6.targetsNin, Imo2025P6.targetsEin, Imo2025P6.targetsSin, Imo2025P6.IntersectionSetup.labels_total_intersection, Nat.le_trans, Eq.mp, congrArg, Imo2025P6.IntersectionSetup.card_validLabels
20 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.IntersectionSetup.intersection_case_final_bound line 1490 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.IntersectionSetup, Finset, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.IntersectionSetup.toBaseSetup, Imo2025P6.Point, Not, Membership.mem, ExistsUnique, And, Imo2025P6.Matilda.mem, LE.le, HMul.hMul, Imo2025P6.BaseSetup.a, Imo2025P6.BaseSetup.b, HSub.hSub, HAdd.hAdd, Nat.sqrt and 2 more
Proof uses: Imo2025P6.IntersectionSetup.matildas_count_ge_intersection_bound, Imo2025P6.am_gm_bound_nat, Trans.trans, Eq, Nat.sub_le_sub_right, Nat.add_le_add_left, of_eq_true, Eq.trans, True, congrFun', congrArg, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Eq.refl and 9 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
structure Imo2025P6.DisjointSetup line 1505 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
2 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.DisjointSetup.mem_of_mem_lower_of_mem_upper line 1512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.v_lower, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.v_upper
Proof uses: Eq.mpr, Inter.inter, Fin, id, Eq, congrArg, Eq.symm, Imo2025P6.v_parts_intersection_eq_v, Imo2025P6.BaseSetup.h_v_mono, Imo2025P6.BaseSetup.h_v_inj, And, propext, Finset.mem_inter, And.intro
11 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.px_ne_of_mem_disjoint line 1517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Ne, Imo2025P6.px
Proof uses: Eq, Imo2025P6.BaseSetup.h_unique_x, Imo2025P6.BaseSetup.hu_sub, Imo2025P6.BaseSetup.hv_sub, False, Iff.mp, Disjoint, Not, Finset.disjoint_left, Imo2025P6.DisjointSetup.h_disj
11 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.py_ne_of_mem_disjoint line 1524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Ne, Imo2025P6.py
Proof uses: Eq, Imo2025P6.BaseSetup.h_unique_y, Imo2025P6.BaseSetup.hu_sub, Imo2025P6.BaseSetup.hv_sub, False, Iff.mp, Disjoint, Not, Finset.disjoint_left, Imo2025P6.DisjointSetup.h_disj
11 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.u_min_mem_v_lower line 1531 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.px, Imo2025P6.v_lower, Imo2025P6.BaseSetup.v
Proof uses: Imo2025P6.v_upper, Or, Imo2025P6.covering_of_maximal_v, Imo2025P6.BaseSetup.all_black, Imo2025P6.BaseSetup.hu_sub, Iff.mp, Disjoint, Not, Finset.disjoint_left, Imo2025P6.DisjointSetup.h_disj, Imo2025P6.BaseSetup.h_v_max, False.elim, And, Imo2025P6.py, Exists, False, Eq.mp, congrArg, propext, Imo2025P6.mem_v_upper and 12 more
24 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.u_max_mem_v_upper line 1547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.px, Imo2025P6.v_upper, Imo2025P6.BaseSetup.v
Proof uses: Imo2025P6.v_lower, Or, Imo2025P6.covering_of_maximal_v, Imo2025P6.BaseSetup.all_black, Imo2025P6.BaseSetup.hu_sub, Iff.mp, Disjoint, Not, Finset.disjoint_left, Imo2025P6.DisjointSetup.h_disj, Imo2025P6.BaseSetup.h_v_max, False.elim, And, Imo2025P6.py, Exists, False, Eq.mp, congrArg, propext, Imo2025P6.mem_v_lower and 11 more
24 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.v_min_mem_u_upper line 1563 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.px, Imo2025P6.u_upper, Imo2025P6.BaseSetup.u
Proof uses: Imo2025P6.u_lower, Or, Imo2025P6.covering_of_maximal_u, Imo2025P6.BaseSetup.all_black, Imo2025P6.BaseSetup.hv_sub, Iff.mp, Disjoint, Not, Finset.disjoint_right, Imo2025P6.DisjointSetup.h_disj, Imo2025P6.BaseSetup.h_u_max, False.elim, And, Imo2025P6.py, Exists, False, Eq.mp, congrArg, propext, Imo2025P6.mem_u_lower and 12 more
24 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.v_max_mem_u_lower line 1579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.px, Imo2025P6.u_lower, Imo2025P6.BaseSetup.u
Proof uses: Imo2025P6.u_upper, Or, Imo2025P6.covering_of_maximal_u, Imo2025P6.BaseSetup.all_black, Imo2025P6.BaseSetup.hv_sub, Iff.mp, Disjoint, Not, Finset.disjoint_right, Imo2025P6.DisjointSetup.h_disj, Imo2025P6.BaseSetup.h_u_max, False.elim, And, Imo2025P6.py, Exists, False, Eq.mp, congrArg, propext, Imo2025P6.mem_u_upper and 12 more
24 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.a_ge_two line 1595 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, LE.le
Proof uses: Decidable.byContradiction, Not, Imo2025P6.Point, Eq, Finset, Imo2025P6.BaseSetup.u, Singleton.singleton, Exists, False, Iff.mp, Finset.card, Finset.card_eq_one, Eq.mpr, id, congrArg, Imo2025P6.BaseSetup.hu, Membership.mem, Finset.mem_singleton_self, Eq.mp, propext and 13 more
19 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.exists_crossing_u line 1604 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, Exists, Imo2025P6.Point, And, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.px, LE.le, Imo2025P6.v_lower, Imo2025P6.BaseSetup.v, Imo2025P6.v_upper
Proof uses: Finset.Nonempty, Iff.mp, Finset.card, Finset.card_pos, Eq.mpr, id, Eq, congrArg, Imo2025P6.BaseSetup.hu, Finset.filter, Fin, Finset.exists_min_image, Exists.intro, Iff.mpr, Finset.mem_filter, And.intro, Imo2025P6.DisjointSetup.u_min_mem_v_lower, Finset.exists_max_image, Eq.mp, propext and 16 more
35 instances, coercions and auxiliary constants left out.
Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.b_ge_two line 1635 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.b, Imo2025P6.DisjointSetup.toBaseSetup, LE.le
Proof uses: Decidable.byContradiction, Not, Imo2025P6.Point, Eq, Finset, Imo2025P6.BaseSetup.v, Singleton.singleton, Exists, False, Iff.mp, Finset.card, Finset.card_eq_one, Eq.mpr, id, congrArg, Imo2025P6.BaseSetup.hv, Membership.mem, Finset.mem_singleton_self, Eq.mp, propext and 21 more
22 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.exists_crossing_v line 1647 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.b, Imo2025P6.DisjointSetup.toBaseSetup, Exists, Imo2025P6.Point, And, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.px, LE.le, Imo2025P6.u_upper, Imo2025P6.BaseSetup.u, Imo2025P6.u_lower
Proof uses: Finset.Nonempty, Iff.mp, Finset.card, Finset.card_pos, Eq.mpr, id, Eq, congrArg, Imo2025P6.BaseSetup.hv, Finset.filter, Fin, Finset.exists_min_image, Exists.intro, Iff.mpr, Finset.mem_filter, And.intro, Imo2025P6.DisjointSetup.v_min_mem_u_upper, Finset.exists_max_image, Eq.mp, propext and 20 more
36 instances, coercions and auxiliary constants left out.
Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
structure Imo2025P6.DisjointSetup.CrossingPoints line 1681 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup
2 instances, coercions and auxiliary constants left out.
def Imo2025P6.DisjointSetup.getCrossingPoints line 1699 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.b, Imo2025P6.DisjointSetup.CrossingPoints
Proof uses: Classical.choice
9 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.DisjointSetup.Pivot line 1711 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Finset, Imo2025P6.Point
Proof uses: Inter.inter, Finset.Ico, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.py, Finset.filter, And, Membership.mem, Finset.univ, Fin
14 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.DisjointSetup.pivot_nonempty line 1716 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Finset.Nonempty, Imo2025P6.Point, Imo2025P6.DisjointSetup.Pivot
Proof uses: Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Decidable.byContradiction, Not, Finset, Inter.inter, Finset.Ico, Imo2025P6.px, Imo2025P6.py, Or, Eq, EmptyCollection.emptyCollection, Membership.mem, False, And.left, Eq.mp, And, Eq.trans and 67 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 135 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.u_not_between_uk_uk1 line 1820 source
lemma Imo2025P6.DisjointSetup.v_not_between_vl_vl1 line 1824 source
lemma Imo2025P6.DisjointSetup.pivot_no_black line 1828 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.DisjointSetup.Pivot, Not, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup
Proof uses: Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.CrossingPoints.mem_uk, Imo2025P6.DisjointSetup.CrossingPoints.mem_uk1, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.CrossingPoints.mem_vl, Imo2025P6.DisjointSetup.CrossingPoints.mem_vl1, Finset.univ, Fin, And, Inter.inter, Finset.Ico, Imo2025P6.px, Imo2025P6.py, False, Eq.mp, Finset.filter and 36 more
32 instances, coercions and auxiliary constants left out.
Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.incidence_count_of_u_disjoint line 1899 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, Eq, Imo2025P6.incidence_count, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, OfNat.ofNat
Proof uses: Imo2025P6.u_lower, Eq.mpr, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py, id, congrArg, propext, Imo2025P6.mem_u_lower, Exists.intro, And.intro, le_refl, Imo2025P6.u_upper, Imo2025P6.mem_u_upper, Not, Iff.mp, Disjoint, Finset.disjoint_left and 40 more
32 instances, coercions and auxiliary constants left out.
Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.incidence_count_of_v_disjoint line 1920 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, Eq, Imo2025P6.incidence_count, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.all_black, OfNat.ofNat
Proof uses: Imo2025P6.v_lower, Eq.mpr, Exists, And, LE.le, Imo2025P6.px, Imo2025P6.py, id, congrArg, propext, Imo2025P6.mem_v_lower, Exists.intro, And.intro, le_refl, Imo2025P6.v_upper, Imo2025P6.mem_v_upper, Not, Iff.mp, Disjoint, Finset.disjoint_right and 43 more
33 instances, coercions and auxiliary constants left out.
Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.DisjointSetup.total_labels_eq_sum_disjoint line 1941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Eq, HAdd.hAdd, Finset.card, Imo2025P6.Point, Imo2025P6.targetsW, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.targetsN, Imo2025P6.targetsE, Imo2025P6.targetsS, Imo2025P6.BaseSetup.a, Imo2025P6.BaseSetup.b
Proof uses: Eq.mpr, Finset.sum, Imo2025P6.incidence_count, id, congrArg, Imo2025P6.sum_card_eq_sum_incidence, Finset, SDiff.sdiff, Fin, Union.union, Disjoint, Imo2025P6.DisjointSetup.h_disj, disjoint_sdiff_self_right, Eq.symm, Finset.union_sdiff_of_subset, Imo2025P6.BaseSetup.union_sub, Finset.sum_union, HMul.hMul, OfNat.ofNat, Finset.sum_congr and 42 more
46 instances, coercions and auxiliary constants left out.
Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.DisjointSetup.labels_total_disjoint line 1984 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.b, GE.ge, HAdd.hAdd, Finset.card, Imo2025P6.Point, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.targetsNin, Imo2025P6.targetsEin, Imo2025P6.targetsSin, HSub.hSub
Proof uses: Eq, Imo2025P6.targetsW, Imo2025P6.targetsN, Imo2025P6.targetsE, Imo2025P6.targetsS, Imo2025P6.DisjointSetup.total_labels_eq_sum_disjoint, Nat.le_add_of_sub_le, Imo2025P6.targetsWin_inequality, Imo2025P6.BaseSetup.h_unique_y, Imo2025P6.targetsNin_inequality, Imo2025P6.BaseSetup.h_unique_x, Imo2025P6.targetsSin_inequality, Imo2025P6.targetsEin_inequality, Eq.mpr, LE.le, Int, id, Eq.trans, congrArg, Nat.cast_add and 70 more
84 instances, coercions and auxiliary constants left out.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.DisjointSetup.wx line 2005 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point
Proof uses: Exists.choose, Membership.mem, Finset, Imo2025P6.DisjointSetup.Pivot, Imo2025P6.DisjointSetup.pivot_nonempty
6 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.DisjointSetup.wx_mem_pivot line 2008 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Membership.mem, Imo2025P6.Point, Finset, Imo2025P6.DisjointSetup.Pivot, Imo2025P6.DisjointSetup.wx
Proof uses: Exists.choose_spec, Imo2025P6.DisjointSetup.pivot_nonempty
8 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.DisjointSetup.wx_bounds line 2011 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Imo2025P6.DisjointSetup.wx, And, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk, LT.lt, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.py
Proof uses: Membership.mem, Finset, Imo2025P6.DisjointSetup.Pivot, Imo2025P6.DisjointSetup.wx_mem_pivot, Eq.mp, Finset.Ico, congrArg, propext, Finset.mem_Ico, Inter.inter, Finset.mem_inter, Eq.trans, Finset.filter, Finset.univ, Fin, True, congrFun', true_and, And.intro
23 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.wx_not_black line 2024 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Not, Membership.mem, Imo2025P6.Point, Finset, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.DisjointSetup.wx
Proof uses: Imo2025P6.DisjointSetup.pivot_no_black, Imo2025P6.DisjointSetup.wx_mem_pivot
6 instances, coercions and auxiliary constants left out.
def Imo2025P6.DisjointSetup.validLabels line 2027 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Finset, Imo2025P6.Label
Proof uses: Union.union, Finset.map, Imo2025P6.Point, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.LabelType.N, Imo2025P6.targetsNin, Imo2025P6.LabelType.E, Imo2025P6.targetsEin, Imo2025P6.LabelType.S, Imo2025P6.targetsSin, Imo2025P6.LabelType.X, Singleton.singleton, Imo2025P6.DisjointSetup.wx
7 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.DisjointSetup.pivot_overlap_x line 2034 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, LT.lt, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.uk1
Proof uses: Imo2025P6.Point, Imo2025P6.DisjointSetup.wx, And, LE.le, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.py, Imo2025P6.DisjointSetup.wx_bounds, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul and 44 more
65 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.u_y_le_uk_of_x_lt_uk1 line 2039 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, LT.lt, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk1, LE.le, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.uk
Proof uses: Decidable.byContradiction, Not, Imo2025P6.DisjointSetup.CrossingPoints.h_u_adj, Iff.mp, not_le, Imo2025P6.BaseSetup.u_mono_le, Imo2025P6.DisjointSetup.CrossingPoints.mem_uk
19 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.v_y_le_vl1_of_x_ge_uk1 line 2047 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.vl1
Proof uses: Imo2025P6.BaseSetup.v_mono_le, Imo2025P6.DisjointSetup.CrossingPoints.mem_vl1, Imo2025P6.DisjointSetup.CrossingPoints.h_v_adj, lt_of_lt_of_le, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.pivot_overlap_x
11 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.DisjointSetup.disjoint_label_X_W line 2052 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.Point, Membership.mem, Finset, LT.lt, OfNat.ofNat, Imo2025P6.py, Imo2025P6.Matilda.mem, Prod.mk, Fin, Prod.fst, HSub.hSub, Prod.snd, Imo2025P6.DisjointSetup.wx and 4 more
Proof uses: And, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.DisjointSetup.wx_bounds, Eq, HAdd.hAdd, Imo2025P6.Matilda.y_max, Imo2025P6.Matilda.x_min, Imo2025P6.Matilda.x_max, Imo2025P6.source_on_face_W, Imo2025P6.u_lower, Imo2025P6.v_lower, Eq.mp, congrArg, propext, Imo2025P6.mem_regionWExtend and 67 more
86 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.u_x_le_uk_of_y_lt_uk1 line 2077 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, LT.lt, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.uk1, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk
Proof uses: Decidable.byContradiction, Not, Imo2025P6.DisjointSetup.CrossingPoints.h_u_adj, Iff.mp, not_le, Imo2025P6.BaseSetup.u_mono_le, Imo2025P6.DisjointSetup.CrossingPoints.mem_uk1
19 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.pivot_overlap_y line 2084 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, LT.lt, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.DisjointSetup.CrossingPoints.uk1
Proof uses: Imo2025P6.Point, Imo2025P6.DisjointSetup.wx, And, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.wx_bounds, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul and 44 more
65 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.v_x_le_vl_of_y_ge_uk1 line 2089 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.vl
Proof uses: Decidable.byContradiction, Not, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.DisjointSetup.CrossingPoints.h_v_adj, Iff.mp, LT.lt, not_le, Imo2025P6.BaseSetup.v_mono_le, Imo2025P6.DisjointSetup.CrossingPoints.mem_vl1, Imo2025P6.DisjointSetup.pivot_overlap_y
18 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.disjoint_label_X_N line 2097 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.Point, Membership.mem, Finset, LT.lt, OfNat.ofNat, Imo2025P6.px, Imo2025P6.Matilda.mem, Prod.mk, Fin, HSub.hSub, Prod.fst, Prod.snd, Imo2025P6.DisjointSetup.wx and 4 more
Proof uses: And, LE.le, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.py, Imo2025P6.DisjointSetup.wx_bounds, Eq, HAdd.hAdd, Imo2025P6.Matilda.x_max, Imo2025P6.Matilda.y_min, Imo2025P6.Matilda.y_max, Imo2025P6.source_on_face_N, Imo2025P6.u_upper, Imo2025P6.v_lower, Eq.mp, congrArg, propext, Imo2025P6.mem_regionNExtend and 67 more
86 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.v_y_ge_vl_of_x_lt_vl1 line 2122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.v, Imo2025P6.DisjointSetup.toBaseSetup, LT.lt, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.vl1, LE.le, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.vl
Proof uses: Decidable.byContradiction, Not, Imo2025P6.DisjointSetup.CrossingPoints.h_v_adj, Iff.mp, not_le, Imo2025P6.BaseSetup.v_mono_le, Imo2025P6.DisjointSetup.CrossingPoints.mem_vl
19 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.disjoint_label_X_E line 2130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.Point, Membership.mem, Finset, LT.lt, Imo2025P6.py, HSub.hSub, OfNat.ofNat, Imo2025P6.Matilda.mem, Imo2025P6.DisjointSetup.wx, Prod.mk, Fin, Prod.fst, HAdd.hAdd and 5 more
Proof uses: And, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.DisjointSetup.wx_bounds, Eq, Imo2025P6.Matilda.y_min, Imo2025P6.Matilda.x_min, Imo2025P6.Matilda.x_max, Imo2025P6.source_on_face_E, Imo2025P6.u_upper, Imo2025P6.v_upper, Eq.mp, congrArg, propext, Imo2025P6.mem_regionEExtend, dite and 81 more
98 instances, coercions and auxiliary constants left out.
Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.pivot_overlap_y_2 line 2168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, LT.lt, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.vl
Proof uses: Imo2025P6.Point, Imo2025P6.DisjointSetup.wx, And, LE.le, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.DisjointSetup.wx_bounds, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 44 more
65 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.u_x_ge_uk1_of_y_ge_vl line 2173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Membership.mem, Finset, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Imo2025P6.py, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.px, Imo2025P6.DisjointSetup.CrossingPoints.uk1
Proof uses: Imo2025P6.DisjointSetup.CrossingPoints.h_u_adj, Decidable.byContradiction, LT.lt, Imo2025P6.DisjointSetup.CrossingPoints.uk, Not, Imo2025P6.BaseSetup.u_mono_le, Imo2025P6.DisjointSetup.CrossingPoints.mem_uk, Iff.mp, not_lt, Imo2025P6.DisjointSetup.pivot_overlap_y_2
18 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.disjoint_label_X_S line 2181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.Point, Membership.mem, Finset, LT.lt, Imo2025P6.px, HSub.hSub, OfNat.ofNat, Imo2025P6.Matilda.mem, Prod.mk, Fin, HAdd.hAdd, Prod.fst, Prod.snd and 5 more
Proof uses: And, LE.le, Imo2025P6.DisjointSetup.CrossingPoints.uk, Imo2025P6.DisjointSetup.CrossingPoints.uk1, Imo2025P6.DisjointSetup.CrossingPoints.vl, Imo2025P6.DisjointSetup.CrossingPoints.vl1, Imo2025P6.py, Imo2025P6.DisjointSetup.wx_bounds, Eq, Imo2025P6.Matilda.x_min, Imo2025P6.Matilda.y_min, Imo2025P6.Matilda.y_max, Imo2025P6.source_on_face_S, Imo2025P6.u_lower, Imo2025P6.v_upper, Eq.mp, congrArg, propext, Imo2025P6.mem_regionSExtend, dite and 78 more
97 instances, coercions and auxiliary constants left out.
Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.covers_X_other line 2209 source
lemma Imo2025P6.DisjointSetup.matilda_covers_at_most_one line 2231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.DisjointSetup.toBaseSetup, LE.le, Finset.card, Imo2025P6.Label, Finset.filter, Imo2025P6.covers, Imo2025P6.DisjointSetup.validLabels, OfNat.ofNat
Proof uses: Eq.mpr, Membership.mem, Finset, Eq, id, congrArg, propext, Finset.card_le_one_iff, And, Eq.mp, Finset.mem_filter, Decidable.byContradiction, Not, Imo2025P6.Point, Imo2025P6.Label.source, Imo2025P6.LabelType, Imo2025P6.Label.type, Imo2025P6.LabelType.W, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u and 77 more
66 instances, coercions and auxiliary constants left out.
Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.grid_size_ge_two_of_label line 2272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Imo2025P6.Point, Imo2025P6.LabelType, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.b, Membership.mem, Imo2025P6.Label, Finset, Imo2025P6.DisjointSetup.validLabels, Imo2025P6.Label.mk, LE.le
Proof uses: Exists, And, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Eq, Function.Embedding, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Or, Imo2025P6.targetsNin, Imo2025P6.LabelType.N, Imo2025P6.targetsEin, Imo2025P6.LabelType.E, Imo2025P6.targetsSin, Imo2025P6.LabelType.S, Singleton.singleton, Imo2025P6.DisjointSetup.wx, Imo2025P6.LabelType.X and 43 more
57 instances, coercions and auxiliary constants left out.
Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.valid_label_pos_not_black line 2289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.b, Imo2025P6.Label, Membership.mem, Finset, Imo2025P6.DisjointSetup.validLabels, Not, Imo2025P6.Point, Imo2025P6.BaseSetup.all_black, Prod.snd, Imo2025P6.label_pos
Proof uses: LE.le, Imo2025P6.DisjointSetup.grid_size_ge_two_of_label, Imo2025P6.Label.source, Imo2025P6.Label.type, False, Imo2025P6.LabelType, Imo2025P6.Label.mk, Exists, And, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Eq, Function.Embedding, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Or, Imo2025P6.targetsNin, Imo2025P6.LabelType.N, Imo2025P6.targetsEin and 39 more
45 instances, coercions and auxiliary constants left out.
Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.DisjointSetup.card_validLabels_disjoint line 2323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, Imo2025P6.DisjointSetup.CrossingPoints, Eq, Finset.card, Imo2025P6.Label, Imo2025P6.DisjointSetup.validLabels, HAdd.hAdd, Imo2025P6.Point, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.v, Imo2025P6.BaseSetup.all_black, Imo2025P6.targetsNin, Imo2025P6.targetsEin, Imo2025P6.targetsSin, OfNat.ofNat
Proof uses: Eq.mpr, Union.union, Finset, Finset.map, Imo2025P6.Label.emb, Imo2025P6.LabelType.W, Imo2025P6.LabelType.N, Imo2025P6.LabelType.E, Imo2025P6.LabelType.S, Imo2025P6.LabelType.X, Singleton.singleton, Imo2025P6.DisjointSetup.wx, id, congrArg, Imo2025P6.DisjointSetup.validLabels.eq_1, Finset.card_union_of_disjoint, Disjoint, Membership.mem, Not, propext and 49 more
54 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.DisjointSetup.disjoint_case_final_bound line 2341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Imo2025P6.DisjointSetup, LT.lt, OfNat.ofNat, Imo2025P6.BaseSetup.a, Imo2025P6.DisjointSetup.toBaseSetup, Imo2025P6.BaseSetup.b, Imo2025P6.DisjointSetup.CrossingPoints, Finset, Imo2025P6.Matilda, Imo2025P6.BaseSetup.all_black, Imo2025P6.Point, Not, Membership.mem, ExistsUnique, And, Imo2025P6.Matilda.mem, LE.le, HMul.hMul and 4 more
Proof uses: GE.ge, Imo2025P6.Label, Imo2025P6.DisjointSetup.validLabels, Eq.mpr, Imo2025P6.targetsWin, Imo2025P6.BaseSetup.u, Imo2025P6.BaseSetup.v, Imo2025P6.targetsNin, Imo2025P6.targetsEin, Imo2025P6.targetsSin, id, Eq, congrArg, Imo2025P6.DisjointSetup.card_validLabels_disjoint, Imo2025P6.DisjointSetup.labels_total_disjoint, Imo2025P6.matilda_count_ge_label_count, Imo2025P6.DisjointSetup.valid_label_pos_not_black, Imo2025P6.DisjointSetup.matilda_covers_at_most_one, Imo2025P6.am_gm_bound_nat, Trans.trans and 22 more
53 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.exists_y_for_x line 2373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, NeZero, Eq, Finset.card, Membership.mem, Imo2025P6.px, Fin, Exists, Prod, Prod.mk
Proof uses: Decidable.byContradiction, Not, Finset.image, Prod.fst, Finset.erase, Finset.univ, LE.le, And, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, Ne, id, Finset.mem_erase, And.intro, Prod.snd, Prod.ext, Fin.ext and 17 more
34 instances, coercions and auxiliary constants left out.
Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.blackPerm line 2406 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Eq, Finset.card, Membership.mem, Imo2025P6.px, NeZero, Fin
Proof uses: Exists.choose, Prod, Prod.mk, Imo2025P6.exists_y_for_x
8 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.blackPerm_spec line 2409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Eq, Finset.card, Membership.mem, Imo2025P6.px, NeZero, Fin, Prod, Prod.mk, Imo2025P6.blackPerm
Proof uses: Exists.choose_spec, Imo2025P6.exists_y_for_x
8 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.blackPerm_injective line 2412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, Eq, Finset.card, Membership.mem, Imo2025P6.px, NeZero, Imo2025P6.py, Function.Injective, Fin, Imo2025P6.blackPerm
Proof uses: Prod.mk, Prod, Imo2025P6.blackPerm_spec, id, Eq.mpr, congrArg, Eq.refl, HEq, eq_of_heq
10 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.IsChain line 2426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.IsAntiChain line 2428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point
Proof uses: Membership.mem, LT.lt, Imo2025P6.px, Imo2025P6.py
3 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.exists_maximal_subset line 2431 source
lemma Imo2025P6.exists_maximal_chain line 2455 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, LE.le, Imo2025P6.IsChain, Exists, And, Not, Membership.mem, Insert.insert, Fin
12 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.exists_maximal_antichain line 2460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, LE.le, Imo2025P6.IsAntiChain, Exists, And, Not, Membership.mem, Insert.insert, Fin
12 instances, coercions and auxiliary constants left out.
def Imo2025P6.incSubsets line 2466 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset
Proof uses: Finset.filter, StrictMonoOn, Membership.mem, Set, LT.lt, Finset.powerset, Finset.univ
13 instances, coercions and auxiliary constants left out.
def Imo2025P6.decSubsets line 2468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset
Proof uses: Finset.filter, StrictAntiOn, Membership.mem, Set, LT.lt, Finset.powerset, Finset.univ
13 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_incSubsets line 2472 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Iff, Membership.mem, Imo2025P6.incSubsets, StrictMonoOn
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, Finset.univ, Finset.filter, Set, LT.lt, Finset.filter.congr_simp, Eq.refl, Finset.powerset, Finset.powerset_univ, true_and, iff_self
22 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_decSubsets line 2476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Iff, Membership.mem, Imo2025P6.decSubsets, StrictAntiOn
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, Finset.univ, Finset.filter, Set, LT.lt, Finset.filter.congr_simp, Eq.refl, Finset.powerset, Finset.powerset_univ, true_and, iff_self
22 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.incSubsets_nonempty line 2480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset.Nonempty, Finset, Imo2025P6.incSubsets
Proof uses: Exists.intro, Membership.mem, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, And, Finset.univ, LT.lt, True, Finset.filter, congrFun', congrArg, Finset.filter.congr_simp, StrictMonoOn, funext, Set, forall_congr, implies_congr, Eq.refl, Finset.powerset and 5 more
23 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.decSubsets_nonempty line 2483 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset.Nonempty, Finset, Imo2025P6.decSubsets
Proof uses: Exists.intro, Membership.mem, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, And, Finset.univ, LT.lt, True, Finset.filter, congrFun', congrArg, Finset.filter.congr_simp, StrictAntiOn, funext, Set, forall_congr, implies_congr, Eq.refl, Finset.powerset and 5 more
23 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.lisLength line 2486 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin
Proof uses: Finset.sup, Finset, Imo2025P6.incSubsets, Finset.card
3 instances, coercions and auxiliary constants left out.
def Imo2025P6.ldsLength line 2488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin
Proof uses: Finset.sup, Finset, Imo2025P6.decSubsets, Finset.card
3 instances, coercions and auxiliary constants left out.
theorem Imo2025P6.erdos_szekeres_direct line 2491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Function.Injective, LE.le, HMul.hMul, Imo2025P6.lisLength, Imo2025P6.ldsLength
Proof uses: Decidable.byContradiction, Not, LT.lt, Fintype.card, Eq.mpr, id, Eq, congrArg, Fintype.card_fin, Eq.mp, propext, not_le, Or, Exists, Finset, And, Finset.card, StrictMonoOn, StrictAntiOn, False and 63 more
93 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.toGridSubset line 2511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Imo2025P6.Point
Proof uses: Finset.image, Prod.mk
2 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.card_toGridSubset line 2515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Eq, Finset.card, Imo2025P6.Point, Imo2025P6.toGridSubset
Proof uses: Finset.card_image_of_injective, Prod.mk, HEq, eq_of_heq
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.is_chain_of_strict_mono line 2519 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, StrictMonoOn, Imo2025P6.IsChain, Imo2025P6.toGridSubset
Proof uses: Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, And, Eq, Prod.mk, Exists, Imo2025P6.py, Eq.mp, Iff.mp, Prod.snd, Fin.lt_def
18 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.is_antichain_of_strict_anti line 2528 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, StrictAntiOn, Imo2025P6.IsAntiChain, Imo2025P6.toGridSubset
Proof uses: Imo2025P6.Point, Membership.mem, LT.lt, Imo2025P6.px, And, Eq, Prod.mk, Exists, Imo2025P6.py, Eq.mp, Iff.mp, Prod.snd, Fin.lt_def
18 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.exists_optimal_u_v line 2537 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, NeZero, Eq, Finset.card, Membership.mem, Imo2025P6.px, Imo2025P6.py, Exists, And, LE.le, HMul.hMul, LT.lt, Not, False
Proof uses: Fin, Imo2025P6.blackPerm, Function.Injective, Imo2025P6.blackPerm_injective, Imo2025P6.lisLength, Imo2025P6.ldsLength, Imo2025P6.erdos_szekeres_direct, Imo2025P6.incSubsets, Finset.sup, Finset.exists_mem_eq_sup, Imo2025P6.incSubsets_nonempty, Imo2025P6.decSubsets, Imo2025P6.decSubsets_nonempty, Imo2025P6.toGridSubset, Prod.mk, Eq.mp, Eq.trans, Finset.image, congrFun', congrArg and 71 more
93 instances, coercions and auxiliary constants left out.
Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.matilda_lower_bound line 2622 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, NeZero, Eq, Finset.card, Membership.mem, Imo2025P6.px, Imo2025P6.py, Imo2025P6.Matilda, Not, ExistsUnique, And, Imo2025P6.Matilda.mem, LE.le, HSub.hSub, HAdd.hAdd, Nat.sqrt, HMul.hMul, OfNat.ofNat
Proof uses: Exists, LT.lt, False, Imo2025P6.exists_optimal_u_v, lt_of_lt_of_le, NeZero.pos, pos_of_mul_pos_left, Nat.zero_le, pos_of_mul_pos_right, Imo2025P6.BaseSetup, Imo2025P6.BaseSetup.mk, rfl, dite, Finset.Nonempty, Inter.inter, Fin, Exists.choose, Exists.choose_spec, Singleton.singleton, Imo2025P6.inter_card_le_one and 19 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
abbrev Imo2025P6.mod_base line 2687 source
standard axioms: propext what this means
Statement uses: Nat, Int
Proof uses: HAdd.hAdd, HPow.hPow, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mod_base_pos line 2689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Int, OfNat.ofNat, Imo2025P6.mod_base
Proof uses: Right.add_pos_of_nonneg_of_pos, HPow.hPow, Even.pow_nonneg, HMul.hMul, even_two_mul, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble
48 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
abbrev Imo2025P6.val_s line 2691 source
no axioms what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Int
Proof uses: HAdd.hAdd, Prod.fst, Fin, Prod.snd, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
abbrev Imo2025P6.val_t line 2692 source
standard axioms: propext what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Int
Proof uses: HAdd.hAdd, HSub.hSub, Prod.fst, Fin, Prod.snd, HPow.hPow, OfNat.ofNat
17 instances, coercions and auxiliary constants left out.
def Imo2025P6.calc_s line 2694 source
standard axioms: propext what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Int
Proof uses: HDiv.hDiv, Imo2025P6.val_s, Imo2025P6.mod_base
6 instances, coercions and auxiliary constants left out.
def Imo2025P6.calc_t line 2695 source
standard axioms: propext what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Int
Proof uses: HDiv.hDiv, Imo2025P6.val_t, Imo2025P6.mod_base
6 instances, coercions and auxiliary constants left out.
def Imo2025P6.all_black_k line 2696 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Imo2025P6.Point, HMul.hMul
Proof uses: Finset.filter, And, Eq, Bool, BEq.beq, Int, HMod.hMod, Imo2025P6.val_s, Imo2025P6.mod_base, OfNat.ofNat, Bool.true, Imo2025P6.val_t, Finset.univ, Fin
13 instances, coercions and auxiliary constants left out.
def Imo2025P6.b_st_coords line 2701 source
no axioms what this means
Statement uses: Nat, Int, Prod
Proof uses: Prod.mk, HAdd.hAdd, HSub.hSub, OfNat.ofNat, HMul.hMul
9 instances, coercions and auxiliary constants left out.
def Imo2025P6.make_b_point line 2702 source
standard axioms: propext what this means
Statement uses: Nat, Int, Prod, Imo2025P6.b_st_coords, And, LE.le, OfNat.ofNat, Prod.fst, LT.lt, HMul.hMul, Prod.snd, Imo2025P6.Point
Proof uses: Prod.mk, Fin, Fin.mk, Int.toNat
18 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.M_st line 2710 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset, Imo2025P6.Point, HMul.hMul
Proof uses: Finset.filter, And, Not, Membership.mem, Imo2025P6.all_black_k, Eq, Imo2025P6.calc_s, Imo2025P6.calc_t, Fin, Finset.univ
14 instances, coercions and auxiliary constants left out.
def Imo2025P6.in_white_rect line 2712 source
no axioms what this means
Statement uses: Nat, Int, Imo2025P6.Point, HMul.hMul
Proof uses: And, LE.le, HAdd.hAdd, HSub.hSub, OfNat.ofNat, Prod.fst, Fin, Prod.snd
14 instances, coercions and auxiliary constants left out.
structure Imo2025P6.BlackPointProps line 2716 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Imo2025P6.Point, HMul.hMul
2 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.b_st_props line 2721 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Prod, Imo2025P6.b_st_coords, And, LE.le, OfNat.ofNat, Prod.fst, LT.lt, HMul.hMul, Prod.snd, Imo2025P6.BlackPointProps, Imo2025P6.make_b_point
Proof uses: Imo2025P6.Point, Imo2025P6.mod_base, Int.add_pos_of_nonneg_of_pos, HPow.hPow, sq_nonneg, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Fin, And.intro, Int.toNat, HAdd.hAdd, HSub.hSub, Int.toNat_of_nonneg, And.left, And.right and 78 more
83 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.M_subset_rect line 2741 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Imo2025P6.Point, HMul.hMul, LE.le, OfNat.ofNat, Membership.mem, Finset, Imo2025P6.M_st, Imo2025P6.in_white_rect
Proof uses: Finset.univ, Fin, And, Not, Imo2025P6.all_black_k, Eq, Imo2025P6.calc_s, Imo2025P6.calc_t, Eq.mp, Finset.filter, congrArg, propext, Finset.mem_filter, Imo2025P6.M_st.eq_1, LT.lt, Imo2025P6.mod_base, Imo2025P6.mod_base_pos, HSub.hSub, Imo2025P6.val_s, Imo2025P6.val_t and 113 more
118 instances, coercions and auxiliary constants left out.
Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.rect_subset_M line 2797 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Imo2025P6.Point, HMul.hMul, LE.le, OfNat.ofNat, Imo2025P6.in_white_rect, Membership.mem, Finset, Imo2025P6.M_st
Proof uses: Imo2025P6.mod_base, LT.lt, Imo2025P6.mod_base_pos, And, HAdd.hAdd, HSub.hSub, Prod.fst, Fin, Prod.snd, Imo2025P6.val_s, And.intro, Trans.trans, Eq, rfl, id, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 111 more
146 instances, coercions and auxiliary constants left out.
Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
instance Imo2025P6.(instance at line 2858) line 2858 source
def Imo2025P6.rect_finset line 2861 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset, Imo2025P6.Point, HMul.hMul
Proof uses: Finset.filter, Imo2025P6.in_white_rect, Finset.univ, Fin
7 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.M_st_eq_rect line 2864 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, Eq, Finset, Imo2025P6.Point, HMul.hMul, Imo2025P6.M_st, Imo2025P6.rect_finset
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Imo2025P6.in_white_rect, id, congrArg, Eq.trans, Finset.filter, Finset.univ, Fin, And, True, congrFun', true_and, Iff.intro, Imo2025P6.M_subset_rect, Imo2025P6.rect_subset_M
15 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_rect_iff_idx_eq line 2870 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Int, LE.le, OfNat.ofNat, Iff, Membership.mem, Finset, Imo2025P6.rect_finset, And, Not, Imo2025P6.all_black_k, Eq, Imo2025P6.calc_s, Imo2025P6.calc_t
Proof uses: Eq.mpr, Imo2025P6.M_st, id, congrArg, Eq.symm, Imo2025P6.M_st_eq_rect, of_eq_true, Eq.trans, True, congrFun', Finset.filter, Fin, Finset.univ, true_and, iff_self
22 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.s_t_range line 2875 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2025P6.Point, HMul.hMul, And, Int, Imo2025P6.calc_s, Imo2025P6.calc_t
Proof uses: Imo2025P6.mod_base, LT.lt, Imo2025P6.mod_base_pos, Prod.fst, Fin, HSub.hSub, HPow.hPow, And.intro, Int.natCast_nonneg, Fin.isLt, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast and 97 more
134 instances, coercions and auxiliary constants left out.
Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.M_00_empty line 2923 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset, Imo2025P6.Point, HMul.hMul, Imo2025P6.M_st, Int, EmptyCollection.emptyCollection
Proof uses: Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, Finset.univ, Fin, And, Imo2025P6.all_black_k, Imo2025P6.calc_s, Imo2025P6.calc_t, False, Eq.mp, Finset.filter, Finset.mem_filter, Imo2025P6.M_st.eq_1, Imo2025P6.mod_base, LT.lt and 105 more
119 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.M_k0_empty line 2948 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Imo2025P6.Point, HMul.hMul, Imo2025P6.M_st, Int, OfNat.ofNat, EmptyCollection.emptyCollection
Proof uses: Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, Imo2025P6.all_black_k, And, Imo2025P6.calc_s, Imo2025P6.calc_t, False, Eq.mp, Eq.trans, Finset.filter, Fin, Finset.univ, True, congrFun', true_and and 93 more
117 instances, coercions and auxiliary constants left out.
Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.M_0k_empty line 2969 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset, Imo2025P6.Point, HMul.hMul, Imo2025P6.M_st, Int, EmptyCollection.emptyCollection
Proof uses: Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, Imo2025P6.all_black_k, And, Imo2025P6.calc_s, Imo2025P6.calc_t, False, Eq.mp, Eq.trans, Finset.filter, Fin, Finset.univ, True, congrFun', true_and and 95 more
120 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.M_kk_empty line 2988 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset, Imo2025P6.Point, HMul.hMul, Imo2025P6.M_st, Int, EmptyCollection.emptyCollection
Proof uses: Eq.mpr, Not, Membership.mem, id, congrArg, propext, Finset.eq_empty_iff_forall_notMem, Imo2025P6.all_black_k, And, Imo2025P6.calc_s, Imo2025P6.calc_t, False, Eq.mp, Eq.trans, Finset.filter, Fin, Finset.univ, True, congrFun', true_and and 100 more
124 instances, coercions and auxiliary constants left out.
Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.clipped_rect line 3039 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, LE.le, OfNat.ofNat, Int, Option, Imo2025P6.Matilda, HMul.hMul, Imo2025P6.all_black_k
Proof uses: HAdd.hAdd, HSub.hSub, Max.max, Min.min, dite, And, Option.some, Imo2025P6.Matilda.mk, Int.toNat, Not, Option.none
32 instances, coercions and auxiliary constants left out.
Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.matilda_upper_bound_sum line 3089 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Int, Finset, Prod, SProd.sprod, Finset.Icc, Insert.insert, Prod.mk, Singleton.singleton, SDiff.sdiff, Eq, Finset.card, HSub.hSub, HAdd.hAdd, HPow.hPow, HMul.hMul
Proof uses: id, Eq.mpr, congrArg, Finset.card_product, Int.toNat, congrFun', congr, Int.card_Icc, of_eq_true, Eq.trans, True, sub_zero, eq_self, Eq.refl, Ne, Finset.card_insert_of_notMem, Not, Membership.mem, Or, And and 47 more
89 instances, coercions and auxiliary constants left out.
Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.eq_of_modEq_fin line 3121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HMul.hMul, Int.ModEq, Imo2025P6.mod_base, Int, Eq
Proof uses: HSub.hSub, id, Dvd.dvd, Decidable.byContradiction, Not, LT.lt, abs, Eq.mpr, And, congrArg, propext, abs_sub_lt_iff, HPow.hPow, pow_two, Iff.mpr, Int.ofNat_lt, Fin.isLt, And.intro, Trans.trans, rfl and 64 more
98 instances, coercions and auxiliary constants left out.
Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.unique_row_all_black line 3146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2025P6.Point, HMul.hMul, Membership.mem, Finset, Imo2025P6.all_black_k, Eq, Imo2025P6.px
Proof uses: Finset.univ, Fin, And, Int, HMod.hMod, Imo2025P6.val_s, Imo2025P6.mod_base, Imo2025P6.val_t, Eq.mp, Eq.trans, Finset.filter, congrFun', congrArg, Finset.filter_congr, Bool, BEq.beq, Bool.true, Iff.of_eq, congr, GT.gt and 63 more
69 instances, coercions and auxiliary constants left out.
Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.unique_col_all_black line 3171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2025P6.Point, HMul.hMul, Membership.mem, Finset, Imo2025P6.all_black_k, Eq, Imo2025P6.py
Proof uses: Finset.univ, Fin, And, Int, HMod.hMod, Imo2025P6.val_s, Imo2025P6.mod_base, Imo2025P6.val_t, Eq.mp, Eq.trans, Finset.filter, congrFun', congrArg, Finset.filter_congr, Bool, BEq.beq, Bool.true, Iff.of_eq, congr, GT.gt and 38 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.card_all_black_le line 3192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset.card, Imo2025P6.Point, HMul.hMul, Imo2025P6.all_black_k
Proof uses: Eq.mpr, Fintype.card, Fin, id, Eq, congrArg, Eq.symm, Fintype.card_fin, Finset.univ, Finset.card_univ, Finset.card_le_card_of_injOn, Prod.fst, Membership.mem, Set, Finset, Finset.mem_univ, Imo2025P6.unique_row_all_black
13 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.b_st_bounds_valid line 3201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, And, Prod, Int, Imo2025P6.b_st_coords, Prod.fst, LT.lt, HMul.hMul, Prod.snd
Proof uses: id, And.intro, HAdd.hAdd, HSub.hSub, add_nonneg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos and 76 more
96 instances, coercions and auxiliary constants left out.
Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Imo2025P6.card_all_black_ge line 3222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Finset.card, Imo2025P6.Point, Imo2025P6.all_black_k
Proof uses: Finset, Prod, Fin, Finset.univ, Int, HAdd.hAdd, And, Decidable.byContradiction, Not, Imo2025P6.make_b_point, Imo2025P6.b_st_bounds_valid, And.intro, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq and 72 more
97 instances, coercions and auxiliary constants left out.
Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.card_all_black_k_eq_n line 3273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset.card, Imo2025P6.Point, HMul.hMul, Imo2025P6.all_black_k
Proof uses: le_antisymm, Imo2025P6.card_all_black_le, Imo2025P6.card_all_black_ge
9 instances, coercions and auxiliary constants left out.
def Imo2025P6.construct_partition line 3277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NeZero, DecidableEq, Imo2025P6.Matilda, HMul.hMul, Imo2025P6.all_black_k, Finset
Proof uses: Int, Prod, SDiff.sdiff, SProd.sprod, Finset.Icc, Insert.insert, Prod.mk, Singleton.singleton, List, List.filterMap, Imo2025P6.construct_partition.match_1, Option, Imo2025P6.clipped_rect, Prod.fst, Prod.snd, Option.some, cast, Unit, Option.none, Finset.toList and 1 more
27 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2025P6.f line 3293 source
standard axioms: propext what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Prod, Int
Proof uses: Prod.mk, Imo2025P6.calc_s, Imo2025P6.calc_t
4 instances, coercions and auxiliary constants left out.
lemma Imo2025P6.mem_M_st_iff_fiber line 3295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2025P6.Point, HMul.hMul, Int, Iff, Membership.mem, Finset, Imo2025P6.M_st, And, Eq, Prod, Imo2025P6.f, Prod.mk, Not, Imo2025P6.all_black_k
Proof uses: Eq.mpr, Imo2025P6.calc_s, Imo2025P6.calc_t, id, congr, congrArg, Eq.trans, Finset.filter, Fin, Finset.univ, True, congrFun', true_and, Prod.mk.injEq, Iff.intro, And.intro
19 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.mem_matilda_iff_mem_M_st line 3299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NeZero, Prod, Int, Imo2025P6.Matilda, HMul.hMul, Imo2025P6.all_black_k, Eq, Option, Imo2025P6.clipped_rect, Prod.fst, Prod.snd, Option.some, Imo2025P6.Point, Iff, Imo2025P6.Matilda.mem, Membership.mem, Finset and 1 more
Proof uses: Eq.mpr, And, Imo2025P6.Matilda.x_min, Imo2025P6.px, Imo2025P6.Matilda.x_max, Imo2025P6.Matilda.y_min, Imo2025P6.py, Imo2025P6.Matilda.y_max, Not, Imo2025P6.calc_s, Imo2025P6.calc_t, id, congrArg, Eq.trans, Finset.filter, Fin, Finset.univ, True, congrFun', true_and and 97 more
178 instances, coercions and auxiliary constants left out.
Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.construction_is_valid_partition line 3350 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NeZero, DecidableEq, Imo2025P6.Matilda, HMul.hMul, Imo2025P6.all_black_k, Imo2025P6.Point, Not, Membership.mem, Finset, ExistsUnique, And, Imo2025P6.construct_partition, Imo2025P6.Matilda.mem
Proof uses: Int, Imo2025P6.calc_s, Imo2025P6.calc_t, Imo2025P6.s_t_range, Imo2025P6.M_st, Eq.mpr, Eq, id, Eq.trans, Finset.filter, Fin, Finset.univ, True, congrFun', congrArg, true_and, And.intro, rfl, LT.lt, HSub.hSub and 145 more
160 instances, coercions and auxiliary constants left out.
Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P6.sqrt_kk line 3431 source
theorem Imo2025P6.matilda_solution_general line 3438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, NeZero, NeZero.mk, Imo2025P6.IsMinMatildaCount, HSub.hSub, HAdd.hAdd, HPow.hPow
Proof uses: ne_of_gt, mul_pos, lt_of_lt_of_le, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, id, And.intro, Finset, Imo2025P6.Point, Imo2025P6.Matilda, Imo2025P6.IsValidConfiguration, Finset.card, Exists, And, Eq, Membership.mem, Imo2025P6.px and 49 more
59 instances, coercions and auxiliary constants left out.
Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
determine Imo2025P6.solution_value line 3483 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo2025P6.imo2025_p6 line 3485 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P6.IsMinMatildaCount, OfNat.ofNat, Nat, Imo2025P6.solution_value
Proof uses: id, Imo2025P6.matilda_solution_general, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true
9 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.