`Compfiles/Usa2022P6.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

54 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2022, Problem 6

There are 2022 users on a social network called Mathbook, and some of them are Mathbook-friends. (On Mathbook, friendship is always mutual and permanent.) Starting now, Mathbook will only allow a new friendship to be formed between two users if they have at least two friends in common. What is the minimum number of friendships that must already exist so that every user could eventually become friends with every other user?

Imports (7)

Imported by 1 file

Compfiles.lean

structure Usa2022P6.CanAdd A new friendship may be formed between u and v: they are distinct, not yet friends, and have at least two common friends line 44 source
Source documentation
A new friendship may be formed between u and v: they are distinct, not yet friends, and have at least two common friends.

no axioms what this means
Statement uses: SimpleGraph
```
structure CanAdd (G : SimpleGraph V) (u v : V) : Prop where
…
```
inductive Usa2022P6.Reachable Reachable G H means that the graph H can be obtained from G by a sequence of legal moves (each adding one friendship between users with two common friends) line 51 source
Source documentation
Reachable G H means that the graph H can be obtained from G by a sequence of legal moves (each adding one friendship between users with two common friends).

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph
```
inductive Reachable : SimpleGraph V → SimpleGraph V → Prop
  | refl (G : SimpleGraph V) : Reachable G G
  | step {G H : SimpleGraph V} {u v : V} (h : Reachable G H) (hc : CanAdd H u v) :
      Reachable G (H ⊔ SimpleGraph.edge u v)

/-- The graph `G` can be completed so that every user becomes friends with every
other user. -/
```
Mentions: h, Usa2022P6.CanAdd
def Usa2022P6.Completable The graph G can be completed so that every user becomes friends with every other user line 58 source
Source documentation
The graph G can be completed so that every user becomes friends with every other user.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph
Proof uses: Usa2022P6.Reachable, Top.top
4 instances, coercions and auxiliary constants left out.
```
def Completable (G : SimpleGraph V) : Prop := Reachable G ⊤
…
```
Mentions: Usa2022P6.Reachable
lemma Usa2022P6.reachable_trans line 61 source
standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Usa2022P6.Reachable
Proof uses: Usa2022P6.Reachable.rec, Usa2022P6.CanAdd, Usa2022P6.Reachable.step

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.reachable_le line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Usa2022P6.Reachable, LE.le
Proof uses: Usa2022P6.Reachable.rec, le_refl, Usa2022P6.CanAdd, le_trans, Max.max, SimpleGraph.edge, le_sup_left
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.reachable_sup_left line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Usa2022P6.Reachable, Max.max
Proof uses: Usa2022P6.Reachable.rec, Usa2022P6.Reachable.refl, Usa2022P6.CanAdd, dite, SimpleGraph.edge, SimpleGraph.Adj, Classical.propDecidable, LE.le, Iff.mpr, Or, Eq, SimpleGraph.edge_le_iff, Or.inr, Eq.mpr, id, congrArg, Eq.symm, sup_assoc, sup_eq_left, Not and 9 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.completable_mono line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, LE.le, Usa2022P6.Completable
Proof uses: Usa2022P6.Reachable, Max.max, Top.top, Usa2022P6.reachable_sup_left, Eq.mp, congrArg, sup_of_le_right, le_top, sup_of_le_left
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.reachable_eq_of_no_canAdd If no legal move is possible from G, then any graph reachable from G is G itself line 101 source
Source documentation
If no legal move is possible from G, then any graph reachable from G is G itself.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Usa2022P6.Reachable, Not, Usa2022P6.CanAdd, Eq
Proof uses: Usa2022P6.Reachable.rec, Eq.refl, absurd, Max.max, SimpleGraph.edge, Eq.rec
1 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_eq_of_no_canAdd {G H : SimpleGraph V} (h : Reachable G H)
    (hno : ∀ u v : V, ¬ CanAdd G u v) : H = G := by
…
```
Mentions: h, Usa2022P6.Reachable, Usa2022P6.CanAdd
lemma Usa2022P6.reachable_add_edge_of_common Adding a single friendship between two users with two distinct common friends is a legal move (or a no-op if they are already friends) line 112 source
Source documentation
Adding a single friendship between two users with two distinct common friends is a legal move (or a no-op if they are already friends).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Ne, SimpleGraph.Adj, Usa2022P6.Reachable, Max.max, SimpleGraph.edge
Proof uses: dite, Classical.propDecidable, Eq.mpr, id, Eq, congrArg, Iff.mpr, LE.le, sup_eq_left, Or, SimpleGraph.edge_le_iff, Or.inr, Usa2022P6.Reachable.refl, Not, Usa2022P6.Reachable.step, Usa2022P6.CanAdd.mk, Exists.intro, Exists, And, And.intro
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_add_edge_of_common {G : SimpleGraph V} {u v p q : V} (huv : u ≠ v)
    (hpq : p ≠ q) (hup : G.Adj u p) (hvp : G.Adj v p) (huq : G.Adj u q)
    (hvq : G.Adj v q) :
    Reachable G (G ⊔ SimpleGraph.edge u v) := by
…
```
Mentions: Usa2022P6.Reachable
def Usa2022P6.Sym2.toFinsetV The vertex set of an element of Sym2 V, as a Finset line 124 source
Source documentation
The vertex set of an element of Sym2 V, as a Finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Sym2, Finset
Proof uses: Equiv, Subtype, Eq, Sym2.lift, Subtype.mk, Insert.insert, Singleton.singleton
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Sym2.toFinsetV (e : Sym2 V) : Finset V :=
…
```
lemma Usa2022P6.Sym2.toFinsetV_mk line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Eq, Finset, Usa2022P6.Sym2.toFinsetV, Sym2.mk, Insert.insert, Singleton.singleton
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa2022P6.Sym2.mem_toFinsetV line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Sym2, Iff, Membership.mem, Finset, Usa2022P6.Sym2.toFinsetV
Proof uses: Sym2.inductionOn, of_eq_true, Sym2.mk, Eq.trans, Or, Eq, True, congr, congrArg, Insert.insert, Singleton.singleton, iff_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.Sym2.toFinsetV_eq line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Sym2, Eq, Finset, Usa2022P6.Sym2.toFinsetV, Insert.insert, Singleton.singleton, Ne, Sym2.mk
Proof uses: Sym2.inductionOn, Or, Membership.mem, Eq.rec, of_eq_true, Eq.trans, True, congr, congrArg, eq_self, true_or, Eq.symm, Eq.mp, Usa2022P6.Sym2.toFinsetV_mk, or_true, Eq.mpr, And, id, propext, Sym2.eq_iff and 5 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
def Usa2022P6.completeOn The complete graph on the finite set S of vertices, seen as a graph on V line 172 source
Source documentation
The complete graph on the finite set S of vertices, seen as a graph on V.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, SimpleGraph
Proof uses: SimpleGraph.mk, And, Membership.mem, Ne
4 instances, coercions and auxiliary constants left out.
```
def completeOn (S : Finset V) : SimpleGraph V where
…
```
Mentions: S
structure Usa2022P6.Cover Documented declaration: Cover line 183 source
Source documentation
A cover of G' relative to the original graph G: a finite collection C of cliques of G' together with a labeling ℓ assigning to every edge of G' a clique containing its endpoints, such that every clique K "owns" at least 3|K|/2 - 2 edges of the original graph G (this is the quantity θ(K) appearing in theta_bound). This is the data maintained by the clique-merging algorithm used in the lower bound proof.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj
```
structure Cover (G G' : SimpleGraph V) [DecidableRel G.Adj] where
…
```
def Usa2022P6.initialCover The initial cover of G: one K₂ per edge line 195 source
Source documentation
The initial cover of G: one K₂ per edge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Usa2022P6.Cover
Proof uses: Usa2022P6.Cover.mk, Finset.image, Sym2, Finset, Usa2022P6.Sym2.toFinsetV, SimpleGraph.edgeFinset
9 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
def initialCover (G : SimpleGraph V) [DecidableRel G.Adj] : Cover G G where
…
```
Mentions: Usa2022P6.Cover
lemma Usa2022P6.card_biUnion_toFinsetV_ge Any family F of at most three of the four edges of the 4-cycle abcd has at least |F| + 1 distinct endpoints line 246 source
Source documentation
Any family F of at most three of the four edges of the 4-cycle abcd has at least |F| + 1 distinct endpoints.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Ne, SimpleGraph.Adj, Finset, Sym2, LE.le, Insert.insert, Sym2.mk, Singleton.singleton, Finset.Nonempty, Nat, Finset.card, OfNat.ofNat, HAdd.hAdd, Finset.biUnion, Usa2022P6.Sym2.toFinsetV
Proof uses: SimpleGraph.Adj.ne, Ne.symm, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, Sym2.Rel, Prod.mk, Or, Prod, Prod.swap, congr, And, Prod.mk.injEq, eq_false, and_self, eq_self and 70 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 214 steps (first 200 of 214)
Open to load the checked before-and-after goal states.
```
lemma card_biUnion_toFinsetV_ge {G' : SimpleGraph V} {a b c d : V}
    (hac : a ≠ c) (hbd : b ≠ d)
    (hab : G'.Adj a b) (hbc : G'.Adj b c) (hcd : G'.Adj c d) (hda : G'.Adj d a)
    {F : Finset (Sym2 V)} (hsub : F ⊆ {s(a, b), s(b, c), s(c, d), s(d, a)})
    (hne : F.Nonempty) (hcard : F.card ≤ 3) :
    F.card + 1 ≤ (F.biUnion Sym2.toFinsetV).card := by
…
```
Mentions: Usa2022P6.Sym2.toFinsetV
lemma Usa2022P6.Cover.merge Documented declaration: merge line 425 source
Source documentation
One merge step of the clique-cover algorithm: if the four edges of some 4-cycle abcd in G' do not all carry the same label, we may add all missing edges inside the union V' of the (two to four) cliques labeling those edges and merge those cliques into a single clique V', obtaining a new valid cover with strictly fewer cliques.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Usa2022P6.Cover, Ne, Not, And, Eq, Finset, Usa2022P6.Cover.ℓ, Sym2.mk, Exists, LE.le, LT.lt, Nat, Finset.card, Usa2022P6.Cover.C
Proof uses: Sym2, rfl, Insert.insert, Singleton.singleton, Finset.biUnion, id, SimpleGraph.Adj.ne, Ne.symm, Membership.mem, Set, SimpleGraph.edgeSet, Eq.mpr, congrArg, Usa2022P6.Cover.label_mem, Finset.mem_insert_self, of_eq_true, Eq.trans, Or, True, congr and 114 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 478 steps (first 200 of 478)
Open to load the checked before-and-after goal states.
```
lemma Cover.merge {G G' : SimpleGraph V} [DecidableRel G.Adj] (cov : Cover G G')
    {a b c d : V} (hac : a ≠ c) (hbd : b ≠ d)
    (hab : G'.Adj a b) (hbc : G'.Adj b c) (hcd : G'.Adj c d) (hda : G'.Adj d a)
    (hdiff : ¬ (cov.ℓ s(a, b) = cov.ℓ s(b, c) ∧ cov.ℓ s(b, c) = cov.ℓ s(c, d) ∧
      cov.ℓ s(c, d) = cov.ℓ s(d, a))) :
    ∃ (G'' : SimpleGraph V) (cov' : Cover G G''), G' ≤ G'' ∧ cov'.C.card < cov.C.card := by
…
```
Mentions: Usa2022P6.Cover
lemma Usa2022P6.exists_terminal_cover Documented declaration: exists_terminal_cover line 832 source
Source documentation
Running the merge algorithm of Cover.merge, starting from any cover, yields a cover in which the four edges of every 4-cycle abcd with a ≠ c and b ≠ d all carry the same label.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Usa2022P6.Cover, LE.le, Finset.card, Finset, Usa2022P6.Cover.C, Exists, And, Ne, Eq, Usa2022P6.Cover.ℓ, Sym2.mk
Proof uses: Nat.recAux, OfNat.ofNat, dite, Classical.propDecidable, Exists.intro, And.intro, le_refl, Not, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, And.left, And.right, LT.lt, Usa2022P6.Cover.merge and 2 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma exists_terminal_cover (G : SimpleGraph V) [DecidableRel G.Adj] :
    ∀ (n : ℕ) (G' : SimpleGraph V) (cov : Cover G G'), cov.C.card ≤ n →
    ∃ (G'' : SimpleGraph V) (cov' : Cover G G''), G' ≤ G'' ∧
      ∀ (a b c d : V), a ≠ c → b ≠ d →
        G''.Adj a b → G''.Adj b c → G''.Adj c d → G''.Adj d a →
        cov'.ℓ s(a, b) = cov'.ℓ s(b, c) ∧ cov'.ℓ s(b, c) = cov'.ℓ s(c, d) ∧
        cov'.ℓ s(c, d) = cov'.ℓ s(d, a) := by
…
```
Mentions: Usa2022P6.Cover
lemma Usa2022P6.lower_bound_of_terminal Documented declaration: lower_bound_of_terminal line 872 source
Source documentation
If a cover of G' relative to G assigns the same label to the four edges of every 4-cycle, and G' is completable, then the original graph G on n vertices satisfies 3n ≤ 2·e(G) + 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Usa2022P6.Cover, LE.le, Nat, OfNat.ofNat, Fintype.card, Ne, And, Eq, Finset, Usa2022P6.Cover.ℓ, Sym2.mk, Usa2022P6.Completable, HMul.hMul, HAdd.hAdd, Finset.card and 2 more
Proof uses: Not, Usa2022P6.CanAdd, False, Exists, SimpleGraph.Adj.symm, Membership.mem, Set, SimpleGraph.edgeSet, Usa2022P6.Cover.label_sub, Eq.mpr, Or, id, congrArg, propext, Sym2.mem_iff, Or.inl, rfl, Or.inr, Usa2022P6.Cover.clique, Usa2022P6.Cover.label_mem and 40 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 121 steps
Open to load the checked before-and-after goal states.
```
lemma lower_bound_of_terminal {G G' : SimpleGraph V} [DecidableRel G.Adj]
    (cov : Cover G G') (hn : 4 ≤ Fintype.card V)
    (hterm : ∀ (a b c d : V), a ≠ c → b ≠ d →
      G'.Adj a b → G'.Adj b c → G'.Adj c d → G'.Adj d a →
      cov.ℓ s(a, b) = cov.ℓ s(b, c) ∧ cov.ℓ s(b, c) = cov.ℓ s(c, d) ∧
      cov.ℓ s(c, d) = cov.ℓ s(d, a))
    (hcomp : Completable G') :
    3 * Fintype.card V ≤ 2 * G.edgeFinset.card + 4 := by
…
```
Mentions: Usa2022P6.Cover, Usa2022P6.Completable
theorem Usa2022P6.lower_bound Lower bound: any completable graph on 2022 vertices has at least 3031 edges line 986 source
Source documentation
Lower bound: any completable graph on 2022 vertices has at least 3031 edges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, Usa2022P6.Completable, LE.le, HMul.hMul, HAdd.hAdd, Set.ncard, Sym2, SimpleGraph.edgeSet
Proof uses: Eq.mpr, Finset, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj, id, Eq, congrArg, Set, Eq.symm, SimpleGraph.coe_edgeFinset, Finset.card, Set.ncard_coe_finset, Exists, Usa2022P6.Cover, And, Ne, Usa2022P6.Cover.ℓ, Sym2.mk, Usa2022P6.exists_terminal_cover and 12 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound (G : SimpleGraph (Fin 2022)) (hcomp : Completable G) :
    3 * 2022 ≤ 2 * G.edgeSet.ncard + 4 := by
…
```
Mentions: Usa2022P6.Completable
def Usa2022P6.xi The i-th "even" vertex 2i + 2 of the construction line 1001 source
Source documentation
The i-th "even" vertex 2i + 2 of the construction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: Fin.mk, HAdd.hAdd, HMul.hMul
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def xi (i : Fin 1010) : Fin 2022 := ⟨2 * i.val + 2, by lia⟩
```
def Usa2022P6.yi The i-th "odd" vertex 2i + 3 of the construction line 1004 source
Source documentation
The i-th "odd" vertex 2i + 3 of the construction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: Fin.mk, HAdd.hAdd, HMul.hMul
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def yi (i : Fin 1010) : Fin 2022 := ⟨2 * i.val + 3, by lia⟩
```
lemma Usa2022P6.xi_val line 1006 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Usa2022P6.xi, HAdd.hAdd, HMul.hMul
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Usa2022P6.yi_val line 1008 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, Usa2022P6.yi, HAdd.hAdd, HMul.hMul
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Usa2022P6.fin0_val line 1010 source
standard axioms: propext what this means
Statement uses: Eq, Nat, OfNat.ofNat, Fin
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.fin1_val line 1012 source
standard axioms: propext what this means
Statement uses: Eq, Nat, OfNat.ofNat, Fin
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.ne0x line 1014 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.xi
Proof uses: Eq, congr_arg, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.xi_val, Usa2022P6.fin0_val
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.ne1x line 1020 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.xi
Proof uses: Eq, congr_arg, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.xi_val, Usa2022P6.fin1_val
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.ne0y line 1026 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.yi
Proof uses: Eq, congr_arg, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.yi_val, Usa2022P6.fin0_val
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.ne1y line 1032 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.yi
Proof uses: Eq, congr_arg, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.yi_val, Usa2022P6.fin1_val
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.nexy line 1038 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.xi, Usa2022P6.yi
Proof uses: Eq, congr_arg, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.yi_val, Usa2022P6.xi_val
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.xex line 1044 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.xi
Proof uses: Eq, congr_arg, Fin.eq_of_val_eq, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.xi_val
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.yey line 1050 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.yi
Proof uses: Eq, congr_arg, Fin.eq_of_val_eq, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.yi_val
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.xey line 1056 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Usa2022P6.xi, Usa2022P6.yi
Proof uses: Eq, congr_arg, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Usa2022P6.yi_val, Usa2022P6.xi_val
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa2022P6.constrEdges Documented declaration: constrEdges line 1065 source
Source documentation
The edge set of the construction: the edge 0-1 together with, for each i < 1010, the three further edges 1-xᵢ, xᵢ-yᵢ, yᵢ-0 of a 4-cycle 0-1-xᵢ-yᵢ-0 sharing the edge 0-1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Sym2, Fin, OfNat.ofNat, Nat
Proof uses: Union.union, Singleton.singleton, Sym2.mk, Finset.biUnion, Finset.univ, Insert.insert, Usa2022P6.xi, Usa2022P6.yi
10 instances, coercions and auxiliary constants left out.
```
def constrEdges : Finset (Sym2 (Fin 2022)) :=
…
```
def Usa2022P6.constrGraph The graph of the construction line 1070 source
Source documentation
The graph of the construction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.fromEdgeSet, Finset, Sym2, Usa2022P6.constrEdges
4 instances, coercions and auxiliary constants left out.
```
def constrGraph : SimpleGraph (Fin 2022) := SimpleGraph.fromEdgeSet ↑constrEdges
```
Mentions: Usa2022P6.constrEdges
instance Usa2022P6.(instance at line 1072) line 1072 source
lemma Usa2022P6.adj01 line 1075 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph.Adj, Fin, OfNat.ofNat, Nat, Usa2022P6.constrGraph
Proof uses: And.intro, Sym2.ToRel, Finset, Sym2, Usa2022P6.constrEdges, Ne, Eq.mpr, Membership.mem, Set, Sym2.mk, id, Eq, congrArg, propext, Sym2.toRel_prop, Union.union, Singleton.singleton, Finset.biUnion, Finset.univ, Insert.insert and 14 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.adj1x line 1080 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, SimpleGraph.Adj, Usa2022P6.constrGraph, Usa2022P6.xi
Proof uses: And.intro, Sym2.ToRel, Finset, Sym2, Usa2022P6.constrEdges, Ne, Eq.mpr, Membership.mem, Set, Sym2.mk, id, Eq, congrArg, propext, Sym2.toRel_prop, Union.union, Singleton.singleton, Finset.biUnion, Finset.univ, Insert.insert and 13 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.adjxy line 1085 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, SimpleGraph.Adj, Usa2022P6.constrGraph, Usa2022P6.xi, Usa2022P6.yi
Proof uses: And.intro, Sym2.ToRel, Finset, Sym2, Usa2022P6.constrEdges, Ne, Eq.mpr, Membership.mem, Set, Sym2.mk, id, Eq, congrArg, propext, Sym2.toRel_prop, Union.union, Singleton.singleton, Finset.biUnion, Finset.univ, Insert.insert and 13 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.adjy0 line 1090 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, SimpleGraph.Adj, Usa2022P6.constrGraph, Usa2022P6.yi
Proof uses: And.intro, Sym2.ToRel, Finset, Sym2, Usa2022P6.constrEdges, Ne, Eq.mpr, Membership.mem, Set, Sym2.mk, id, Eq, congrArg, propext, Sym2.toRel_prop, Union.union, Singleton.singleton, Finset.biUnion, Finset.univ, Insert.insert and 15 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.phase1 Phase 1 of the completion: for each i, add the friendships 0-xᵢ and 1-yᵢ (each has two common friends) line 1098 source
Source documentation
Phase 1 of the completion: for each i, add the friendships 0-xᵢ and 1-yᵢ (each has two common friends).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, Exists, SimpleGraph, And, Usa2022P6.Reachable, Usa2022P6.constrGraph, LE.le, Membership.mem, SimpleGraph.Adj, Usa2022P6.xi, Usa2022P6.yi
Proof uses: Finset.induction, Exists.intro, EmptyCollection.emptyCollection, And.intro, Usa2022P6.Reachable.refl, le_refl, False.elim, Eq.mp, False, Not, Insert.insert, Usa2022P6.adj01, SimpleGraph.Adj.symm, Usa2022P6.adj1x, Usa2022P6.adjy0, Usa2022P6.adjxy, Max.max, SimpleGraph.edge, Usa2022P6.reachable_add_edge_of_common, Usa2022P6.ne0x and 18 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma phase1 (T : Finset (Fin 1010)) :
    ∃ H : SimpleGraph (Fin 2022), Reachable constrGraph H ∧ constrGraph ≤ H ∧
      ∀ i ∈ T, H.Adj 0 (xi i) ∧ H.Adj 1 (yi i) := by
…
```
Mentions: Usa2022P6.Reachable, Usa2022P6.constrGraph, Usa2022P6.xi, Usa2022P6.yi
lemma Usa2022P6.reachable_connect_vertex Documented declaration: reachable_connect_vertex line 1132 source
Source documentation
If x is friends with both 0 and 1, we may successively make x friends with every vertex of a set T ∌ x of vertices all of which are also friends with both 0 and 1 (the pair 0, 1 always serves as the two common friends).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, SimpleGraph.Adj, Finset, Not, Membership.mem, And, Exists, Usa2022P6.Reachable, LE.le
Proof uses: Finset.induction, EmptyCollection.emptyCollection, Exists.intro, And.intro, Usa2022P6.Reachable.refl, le_refl, False.elim, Eq.mp, False, Insert.insert, Finset.mem_insert_of_mem, Ne, Eq, Eq.rec, Finset.mem_insert_self, Eq.symm, And.left, And.right, Max.max, SimpleGraph.edge and 19 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_connect_vertex {H : SimpleGraph (Fin 2022)} {x : Fin 2022}
    (hx0 : H.Adj x 0) (hx1 : H.Adj x 1) (T : Finset (Fin 2022))
    (hxT : x ∉ T) (hT : ∀ v ∈ T, H.Adj v 0 ∧ H.Adj v 1) :
    ∃ H' : SimpleGraph (Fin 2022), Reachable H H' ∧ H ≤ H' ∧ ∀ v ∈ T, H'.Adj x v := by
…
```
Mentions: Usa2022P6.Reachable
lemma Usa2022P6.reachable_complete_aux If every vertex of T is friends with both 0 and 1, we may make T into a clique line 1157 source
Source documentation
If every vertex of T is friends with both 0 and 1, we may make T into a clique.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, Finset, Membership.mem, And, SimpleGraph.Adj, Exists, Usa2022P6.Reachable, LE.le, Ne
Proof uses: Finset.induction, EmptyCollection.emptyCollection, Exists.intro, And.intro, Usa2022P6.Reachable.refl, le_refl, False.elim, Eq.mp, False, Not, Insert.insert, Finset.mem_insert_of_mem, And.left, Finset.mem_insert_self, And.right, Usa2022P6.reachable_connect_vertex, Usa2022P6.reachable_trans, le_trans, Eq, Or and 6 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_complete_aux {H : SimpleGraph (Fin 2022)} (T : Finset (Fin 2022))
    (hT : ∀ v ∈ T, H.Adj v 0 ∧ H.Adj v 1) :
    ∃ H' : SimpleGraph (Fin 2022), Reachable H H' ∧ H ≤ H' ∧
      ∀ u ∈ T, ∀ w ∈ T, u ≠ w → H'.Adj u w := by
…
```
Mentions: Usa2022P6.Reachable
lemma Usa2022P6.hnb After phase 1, every vertex other than 0 and 1 is of the form xᵢ or yᵢ and is friends with both 0 and 1 line 1181 source
Source documentation
After phase 1, every vertex other than 0 and 1 is of the form xᵢ or yᵢ and is friends with both 0 and 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat, LE.le, Usa2022P6.constrGraph, Membership.mem, Finset, Finset.univ, And, SimpleGraph.Adj, Usa2022P6.xi, Usa2022P6.yi, Not, Insert.insert, Singleton.singleton
Proof uses: Eq, Eq.mp, Eq.trans, Or, congrArg, Decidable.byContradiction, LT.lt, False, Fin.eq_of_val_eq, Eq.mpr, id, Usa2022P6.fin0_val, Eq.refl, Usa2022P6.fin1_val, HDiv.hDiv, HSub.hSub, rfl, HAdd.hAdd, HMul.hMul, Fin.mk and 9 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma hnb {H₁ : SimpleGraph (Fin 2022)} (hle : constrGraph ≤ H₁)
    (hconn : ∀ i ∈ (Finset.univ : Finset (Fin 1010)), H₁.Adj 0 (xi i) ∧ H₁.Adj 1 (yi i))
    (v : Fin 2022) (hv : v ∉ ({0, 1} : Finset (Fin 2022))) :
    H₁.Adj v 0 ∧ H₁.Adj v 1 := by
…
```
Mentions: Usa2022P6.constrGraph, Usa2022P6.xi, Usa2022P6.yi
lemma Usa2022P6.constr_completable The graph of the construction is completable: after phase 1, complete the remaining 2020 vertices to a clique using 0, 1 as common friends line 1209 source
Source documentation
The graph of the construction is completable: after phase 1, complete the remaining 2020 vertices to a clique using 0, 1 as common friends.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2022P6.Completable, Fin, OfNat.ofNat, Nat, Usa2022P6.constrGraph
Proof uses: SimpleGraph, And, Usa2022P6.Reachable, LE.le, Membership.mem, Finset, Finset.univ, SimpleGraph.Adj, Usa2022P6.xi, Usa2022P6.yi, Exists, Usa2022P6.phase1, SDiff.sdiff, Insert.insert, Singleton.singleton, Ne, Usa2022P6.reachable_complete_aux, Usa2022P6.hnb, And.right, Not and 26 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma constr_completable : Completable constrGraph := by
…
```
Mentions: Usa2022P6.Completable, Usa2022P6.constrGraph
lemma Usa2022P6.constr_edgeSet All edges of the construction are non-diagonal, so its edge set is exactly constrEdges line 1245 source
Source documentation
All edges of the construction are non-diagonal, so its edge set is exactly constrEdges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Sym2, Fin, OfNat.ofNat, Nat, SimpleGraph.edgeSet, Usa2022P6.constrGraph, Finset, Usa2022P6.constrEdges
Proof uses: SDiff.sdiff, Sym2.diagSet, Eq.mpr, SimpleGraph.fromEdgeSet, id, congrArg, SimpleGraph, rfl, SimpleGraph.edgeSet_fromEdgeSet, Disjoint, propext, sdiff_eq_self_iff_disjoint, Membership.mem, Not, Set.disjoint_left, Sym2.mk, Exists, And, Finset.univ, Insert.insert and 28 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma constr_edgeSet : constrGraph.edgeSet = ↑constrEdges := by
…
```
Mentions: Usa2022P6.constrEdges
lemma Usa2022P6.constr_edgeFinset line 1266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Sym2, Fin, OfNat.ofNat, Nat, SimpleGraph.edgeFinset, Usa2022P6.constrGraph, Usa2022P6.constrEdges
Proof uses: Iff.mp, Set, Finset.coe_inj, Eq.mpr, SimpleGraph.edgeSet, id, congrArg, SimpleGraph.coe_edgeFinset, Usa2022P6.constr_edgeSet, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P6.sym2_ne_of_fst If the first endpoint of s(a, b) differs from both endpoints of s(c, d), the two edges are distinct line 1272 source
Source documentation
If the first endpoint of s(a, b) differs from both endpoints of s(c, d), the two edges are distinct.

standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Sym2, Sym2.mk
Proof uses: Eq, And, Or, False, Eq.mp, congrArg, propext, Sym2.eq_iff
4 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sym2_ne_of_fst {a b c d : Fin 2022} (hac : a ≠ c) (had : a ≠ d) :
    s(a, b) ≠ s(c, d) := by
…
```
lemma Usa2022P6.sym2_ne_of_snd If the second endpoint of s(a, b) differs from both endpoints of s(c, d), the two edges are distinct line 1282 source
Source documentation
If the second endpoint of s(a, b) differs from both endpoints of s(c, d), the two edges are distinct.

standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Sym2, Sym2.mk
Proof uses: Eq, And, Or, False, Eq.mp, congrArg, propext, Sym2.eq_iff
4 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sym2_ne_of_snd {a b c d : Fin 2022} (hbc : b ≠ c) (hbd : b ≠ d) :
    s(a, b) ≠ s(c, d) := by
…
```
lemma Usa2022P6.constr_edge_ncard The construction has exactly 3031 friendships line 1291 source
Source documentation
The construction has exactly 3031 friendships.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Set.ncard, Sym2, Fin, OfNat.ofNat, SimpleGraph.edgeSet, Usa2022P6.constrGraph
Proof uses: Eq.mpr, Finset, SimpleGraph.edgeFinset, id, congrArg, Set, Eq.symm, SimpleGraph.coe_edgeFinset, Finset.card, Set.ncard_coe_finset, Usa2022P6.constrEdges, Usa2022P6.constr_edgeFinset, Insert.insert, Sym2.mk, Usa2022P6.xi, Usa2022P6.yi, Singleton.singleton, HAdd.hAdd, Finset.card_insert_of_notMem, Not and 49 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma constr_edge_ncard : constrGraph.edgeSet.ncard = 3031 := by
…
```
determine Usa2022P6.answer line 1346 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa2022P6.usa2022_p6 line 1348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, SimpleGraph, Fin, OfNat.ofNat, And, Usa2022P6.Completable, Eq, Set.ncard, Sym2, SimpleGraph.edgeSet, Usa2022P6.answer
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Usa2022P6.constrGraph, Usa2022P6.constr_completable, Usa2022P6.constr_edge_ncard, LE.le, HMul.hMul, HAdd.hAdd, Usa2022P6.lower_bound, id
12 instances, coercions and auxiliary constants left out.

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