`Compfiles/Imo2020P4.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

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

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

30 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2020, Problem 4

There is an integer n > 1. There are n² stations on a slope of a mountain, all at different altitudes. Each of two cable car companies, A and B, operates k cable cars; each cable car provides a transfer from one of the stations to a higher one (with no intermediate stops). The k cable cars of A have k different starting points and k different finishing points, and a cable car which starts higher also finishes higher. The same conditions hold for B. We say that two stations are linked by a company if one can start from the lower station and reach the higher one by using one or more cars of that company (no other movements between stations are allowed). Determine the smallest positive integer k for which one can guarantee that there are two stations that are linked by both companies.

Imports (2)

Imported by 1 file

Compfiles.lean

structure Imo2020P4.Car A cable car's starting and finishing points line 40 source
Source documentation
A cable car's starting and finishing points.

standard axioms: propext what this means
Statement uses: Nat
```
structure Car (n : ℕ) : Type where
…
```
structure Imo2020P4.Company The cable cars of a company line 48 source
Source documentation
The cable cars of a company.

standard axioms: propext what this means
Statement uses: Nat
```
structure Company (n k : ℕ) : Type where
…
```
structure Imo2020P4.Company.linkage A linkage between two stations line 56 source
Source documentation
A linkage between two stations.

standard axioms: propext what this means
Statement uses: Nat, Imo2020P4.Company
```
structure Company.linkage {n k : ℕ} (c : Company n k) : Type where
…
```
Mentions: Imo2020P4.Company
def Imo2020P4.Company.linkage.start The first station in a linkage line 63 source
Source documentation
The first station in a linkage.

standard axioms: propext what this means
Statement uses: Nat, Imo2020P4.Company, Imo2020P4.Company.linkage, Fin, HPow.hPow, OfNat.ofNat
Proof uses: Imo2020P4.Car.start, Imo2020P4.Company.cars, List.head, Imo2020P4.Company.linkage.cars, Imo2020P4.Company.linkage.nonempty
5 instances, coercions and auxiliary constants left out.
```
def Company.linkage.start {n k : ℕ} {c : Company n k} (x : c.linkage) : Fin (n ^ 2) :=
…
```
Mentions: Imo2020P4.Company
def Imo2020P4.Company.linkage.finish The last station in a linkage line 67 source
Source documentation
The last station in a linkage.

standard axioms: propext what this means
Statement uses: Nat, Imo2020P4.Company, Imo2020P4.Company.linkage, Fin, HPow.hPow, OfNat.ofNat
Proof uses: Imo2020P4.Car.finish, Imo2020P4.Company.cars, List.getLast, Imo2020P4.Company.linkage.cars, Imo2020P4.Company.linkage.nonempty
5 instances, coercions and auxiliary constants left out.
```
def Company.linkage.finish {n k : ℕ} {c : Company n k} (x : c.linkage) : Fin (n ^ 2) :=
…
```
Mentions: Imo2020P4.Company
def Imo2020P4.Company.linked The property of two stations being linked (in the given order) line 71 source
Source documentation
The property of two stations being linked (in the given order).

standard axioms: propext what this means
Statement uses: Nat, Imo2020P4.Company, Fin, HPow.hPow, OfNat.ofNat
Proof uses: Exists, Imo2020P4.Company.linkage, And, Eq, Imo2020P4.Company.linkage.start, Imo2020P4.Company.linkage.finish
10 instances, coercions and auxiliary constants left out.
```
def Company.linked {n k : ℕ} (c : Company n k) (l h : Fin (n ^ 2)) : Prop :=
…
```
Mentions: Imo2020P4.Company, h
instance Imo2020P4.instFintypeEdgeSetOfFinite Fintype G.edgeSet previously resolved via a noncomputable instance derived from finiteness of the vertex type (as still happens for SetLike types such as ConnectedComponent) line 82 source
Source comment
`Fintype G.edgeSet` previously resolved via a noncomputable instance derived from finiteness of the vertex type (as still happens for `SetLike` types such as `ConnectedComponent`). Recent mathlib only provides a computable instance requiring `[DecidableRel G.Adj]`, so we supply the noncomputable instance locally.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, SimpleGraph, Fintype, Sym2, SimpleGraph.edgeSet
Proof uses: Fintype.ofFinite
3 instances, coercions and auxiliary constants left out.
```
noncomputable instance instFintypeEdgeSetOfFinite {V : Type*} [Finite V] (G : SimpleGraph V) :
    Fintype G.edgeSet := Fintype.ofFinite _
```
lemma Imo2020P4.Sym2.exists_mk line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Sym2, Exists, Eq, Sym2.mk
Proof uses: Membership.mem, Prod.fst, Quot.out, Prod, Sym2.Rel, Sym2.out_fst_mem, Exists.intro, Eq.mp, congrArg, propext, Sym2.mem_iff_exists
2 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.SimpleGraph.sum_card_connectedComponent_eq_card line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Eq, Nat, Finset.sum, SimpleGraph.ConnectedComponent, Finset.univ, Nat.card, Subtype, Membership.mem, Fintype.card
Proof uses: Set.ncard, SimpleGraph.ConnectedComponent.supp, Finset.sum_congr, rfl, Finset, Eq.mpr, id, congrArg, Eq.symm, SetLike.coe_sort_coe, Nat.card_coe_set_eq, Set, Eq.rec, Eq.refl, SetLike, Set.Finite, Set.toFinite, Pairwise, Function.onFun, Disjoint and 10 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.SimpleGraph.sum_card_edgeFinset_toSimpleGraph_connectedComponent_eq_edgeFinset_card line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Eq, Nat, Finset.sum, SimpleGraph.ConnectedComponent, Finset.univ, Finset.card, Sym2, Subtype, Membership.mem, SimpleGraph.edgeFinset, SimpleGraph.ConnectedComponent.toSimpleGraph
Proof uses: Finset, Finset.image, Sym2.map, rfl, Finset.sum_congr, Eq.mpr, id, congrArg, Eq.symm, Finset.card_image_of_injective, Sym2.map.injective, Subtype.val_injective, Set.PairwiseDisjoint, Set, Ne, Function.onFun, Disjoint, Function.onFun.eq_1, Mathlib.Tactic.Contrapose.contrapose₂, Not and 39 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.SimpleGraph.card_connectedComponent_add_card_edge_eq_card_vertex_of_acyclic line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.IsAcyclic, Eq, Nat, HAdd.hAdd, Fintype.card, SimpleGraph.ConnectedComponent, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: Membership.mem, Finset, Finset.univ, Subtype, SimpleGraph.ConnectedComponent.toSimpleGraph, OfNat.ofNat, Nat.card, Eq.mpr, SimpleGraph.edgeSet, id, congrArg, Eq.symm, And.right, SimpleGraph.Connected, Iff.mp, SimpleGraph.IsTree, And, SimpleGraph.isTree_iff_connected_and_card, SimpleGraph.IsAcyclic.isTree_connectedComponent, HAdd and 14 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Imo2020P4.Company.graph line 196 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, SimpleGraph, Fin, HPow.hPow, OfNat.ofNat
Proof uses: SimpleGraph.mk, Exists, Eq, Sym2, Sym2.mk, Imo2020P4.Car.start, Imo2020P4.Company.cars, Imo2020P4.Car.finish
12 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.graph_edgeFinset_card line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, Eq, Finset.card, Sym2, Fin, HPow.hPow, OfNat.ofNat, SimpleGraph.edgeFinset, Imo2020P4.Company.graph
Proof uses: Sym2.mk, Imo2020P4.Car.start, Imo2020P4.Company.cars, Imo2020P4.Car.finish, rfl, Finset, Finset.image, Finset.univ, Finset.ext, Exists, Iff, Membership.mem, Imo2020P4.Sym2.exists_mk, Eq.mpr, And, id, congrArg, propext, Finset.mem_image, Set and 32 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.graph_isAcyclic line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, SimpleGraph.IsAcyclic, Fin, HPow.hPow, OfNat.ofNat, Imo2020P4.Company.graph
Proof uses: SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Ne, List, SimpleGraph.Walk.support, List.nil, SimpleGraph.Walk.support_ne_nil, List.min, Eq, rfl, Membership.mem, LE.le, And, False, Iff.mp, List.min_eq_iff, Set.ncard, SimpleGraph.Subgraph.neighborSet, SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two and 45 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.low_le_of_mem_path line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, Fin, HPow.hPow, OfNat.ofNat, LT.lt, SimpleGraph.Walk, Imo2020P4.Company.graph, SimpleGraph.Walk.IsPath, Membership.mem, List, SimpleGraph.Walk.support, LE.le
Proof uses: Ne, List.nil, SimpleGraph.Walk.support_ne_nil, List.min, Eq, rfl, And, Iff.mp, List.min_eq_iff, SimpleGraph.Walk.getVert, SimpleGraph.Walk.length, Exists, SimpleGraph.Walk.mem_support_iff_exists_getVert, dite, Eq.trans_le, Eq.mp, congrArg, SimpleGraph.Walk.getVert_zero, Not, lt_of_le_of_ne and 49 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.le_high_of_mem_path line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, Fin, HPow.hPow, OfNat.ofNat, LT.lt, SimpleGraph.Walk, Imo2020P4.Company.graph, SimpleGraph.Walk.IsPath, Membership.mem, List, SimpleGraph.Walk.support, LE.le
Proof uses: Ne, List.nil, SimpleGraph.Walk.support_ne_nil, List.max, Eq, rfl, And, Iff.mp, List.max_eq_iff, SimpleGraph.Walk.getVert, SimpleGraph.Walk.length, Exists, SimpleGraph.Walk.mem_support_iff_exists_getVert, dite, LE.le.trans_eq, Eq.symm, Eq.mp, congrArg, SimpleGraph.Walk.getVert_length, Not and 49 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.linked_of_graph_reachable line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, Fin, HPow.hPow, OfNat.ofNat, SimpleGraph.Reachable, Imo2020P4.Company.graph, LT.lt, Imo2020P4.Company.linked
Proof uses: SimpleGraph.Walk, SimpleGraph.Walk.IsPath, Exists, SimpleGraph.Reachable.exists_isPath, SimpleGraph.Walk.rec, SimpleGraph.Walk.nil, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LE.le, id, Eq, implies_congr, Eq.refl, le_refl, SimpleGraph.Adj, SimpleGraph.Walk.cons, Membership.mem, List, SimpleGraph.Walk.support and 55 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.lt_of_linked line 475 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, Fin, HPow.hPow, OfNat.ofNat, Imo2020P4.Company.linked, LT.lt
Proof uses: Imo2020P4.Company.linkage, And, Eq, Imo2020P4.Company.linkage.start, Imo2020P4.Company.linkage.finish, Exists, Eq.mp, congrArg, Imo2020P4.Company.linked.eq_1, List, Ne, List.nil, List.IsChain, Imo2020P4.Car.finish, Imo2020P4.Company.cars, Imo2020P4.Car.start, Imo2020P4.Company.linkage.mk, List.rec, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr and 29 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.aux_succ line 508 source
standard axioms: propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Eq, HAdd.hAdd, HSub.hSub, Membership.mem, Set
Proof uses: Subtype.property, Nat.sub_add_cancel, le_of_lt, Eq.mp, LT.lt, congrArg, propext, Set.mem_Ioi
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.aux_pow line 514 source
standard axioms: propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Eq, HMul.hMul, Membership.mem, Set, HPow.hPow
Proof uses: Eq.mpr, id, congrArg, pow_two, Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.aux_A line 517 source
standard axioms: propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Eq, HSub.hSub, HMul.hMul, Membership.mem, Set
Proof uses: Eq.mpr, id, congrArg, Nat.sub_mul, one_mul, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.aux_B line 520 source
standard axioms: propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Eq, HSub.hSub, HMul.hMul, Membership.mem, Set
Proof uses: Eq.mpr, id, congrArg, Nat.mul_sub, mul_one, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2020P4.constructCompanyA line 523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Imo2020P4.Company, Membership.mem, Set, HSub.hSub, HMul.hMul
Proof uses: Imo2020P4.Company.mk, Fin, Imo2020P4.Car.mk, Fin.cast, HPow.hPow, Imo2020P4.aux_pow, Fin.mkDivMod, HAdd.hAdd, Imo2020P4.aux_succ, Fin.castSucc, Fin.divNat, Imo2020P4.aux_A, Fin.modNat, Fin.succ
28 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
def Imo2020P4.constructCompanyB line 578 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Imo2020P4.Company, Membership.mem, Set, HSub.hSub, HMul.hMul
Proof uses: Imo2020P4.Company.mk, Fin, Imo2020P4.Car.mk, Fin.cast, HPow.hPow, Imo2020P4.aux_pow, Fin.mkDivMod, Fin.divNat, Imo2020P4.aux_B, HAdd.hAdd, Imo2020P4.aux_succ, Fin.castSucc, Fin.modNat, Fin.succ
28 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.cast_modNat_eq_of_linked_constructCompanyA line 633 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Fin, HPow.hPow, Membership.mem, Set, Imo2020P4.Company.linked, HSub.hSub, HMul.hMul, Imo2020P4.constructCompanyA, Eq, Fin.modNat, Fin.cast, Eq.symm, Imo2020P4.aux_pow
Proof uses: Imo2020P4.Company.linkage, And, Imo2020P4.Company.linkage.start, Imo2020P4.Company.linkage.finish, Exists, Eq.mp, congrArg, Imo2020P4.Company.linked.eq_1, List, Ne, List.nil, List.IsChain, Imo2020P4.Car.finish, Imo2020P4.Company.cars, Imo2020P4.Car.start, Imo2020P4.Company.linkage.mk, List.rec, Mathlib.Tactic.Contrapose.contrapose₂, id, Not and 34 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.cast_divNat_eq_of_linked_constructCompanyB line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, Fin, HPow.hPow, Membership.mem, Set, Imo2020P4.Company.linked, HSub.hSub, HMul.hMul, Imo2020P4.constructCompanyB, Eq, Fin.divNat, Fin.cast, Eq.symm, Imo2020P4.aux_pow
Proof uses: Imo2020P4.Company.linkage, And, Imo2020P4.Company.linkage.start, Imo2020P4.Company.linkage.finish, Exists, Eq.mp, congrArg, Imo2020P4.Company.linked.eq_1, List, Ne, List.nil, List.IsChain, Imo2020P4.Car.finish, Imo2020P4.Company.cars, Imo2020P4.Car.start, Imo2020P4.Company.linkage.mk, List.rec, Mathlib.Tactic.Contrapose.contrapose₂, id, Not and 34 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
def Imo2020P4.Company.subCompany line 707 source
standard axioms: propext what this means
Statement uses: Nat, Imo2020P4.Company, LE.le
Proof uses: Imo2020P4.Company.mk, Fin, Imo2020P4.Company.cars, Fin.castLE
5 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2020P4.Company.linked_of_subCompany_linked line 728 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2020P4.Company, LE.le, Fin, HPow.hPow, OfNat.ofNat, Imo2020P4.Company.linked, Imo2020P4.Company.subCompany
Proof uses: Eq.mpr, Exists, Imo2020P4.Company.linkage, And, Eq, Imo2020P4.Company.linkage.start, Imo2020P4.Company.linkage.finish, id, congrArg, Imo2020P4.Company.linked.eq_1, Eq.mp, Exists.intro, Imo2020P4.Company.linkage.mk, List.map, Fin.castLE, Imo2020P4.Company.linkage.cars, Ne, List, List.nil, propext and 19 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
determine Imo2020P4.answer line 759 source
no axioms what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat
Proof uses: HAdd.hAdd, HSub.hSub, HMul.hMul, Membership.mem, Set
14 instances, coercions and auxiliary constants left out.
problem Imo2020P4.imo2020_p4 line 761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Ioi, OfNat.ofNat, IsLeast, Set.ofPred, Imo2020P4.Company, Membership.mem, Set, Exists, Fin, HPow.hPow, And, Imo2020P4.Company.linked, Imo2020P4.answer
Proof uses: Subtype.property, Eq.mpr, HAdd.hAdd, HSub.hSub, HMul.hMul, id, Eq, congrArg, Imo2020P4.answer.eq_1, lowerBounds, IsLeast.eq_1, LE.le, lowerBounds.eq_1, And.intro, Fintype.card, SimpleGraph.ConnectedComponent, Imo2020P4.Company.graph, Finset.card, Sym2, SimpleGraph.edgeFinset and 73 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.