[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
ht : IsTrail p
x : V
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ u ≠ v → x ≠ u ∧ x ≠ v
[PROOFSTEP]
induction' p with u u v w huv p ih
[GOAL]
case nil
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v : V
p : Walk G u✝ v
ht✝ : IsTrail p
x u : V
ht : IsTrail Walk.nil
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges Walk.nil)) ↔ u ≠ u → x ≠ u ∧ x ≠ u
[PROOFSTEP]
simp
[GOAL]
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ih : IsTrail p → (Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w)
ht : IsTrail (cons huv p)
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges (cons huv p))) ↔ u ≠ w → x ≠ u ∧ x ≠ w
[PROOFSTEP]
rw [cons_isTrail_iff] at ht
[GOAL]
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ih : IsTrail p → (Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w)
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges (cons huv p))) ↔ u ≠ w → x ≠ u ∧ x ≠ w
[PROOFSTEP]
specialize ih ht.1
[GOAL]
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges (cons huv p))) ↔ u ≠ w → x ≠ u ∧ x ≠ w
[PROOFSTEP]
simp only [List.countp_cons, Ne.def, edges_cons, Sym2.mem_iff]
[GOAL]
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + if decide (x = u ∨ x = v) = true then 1 else 0) ↔
    ¬u = w → ¬x = u ∧ ¬x = w
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
h : decide (x = u ∨ x = v) = true
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + 1) ↔ ¬u = w → ¬x = u ∧ ¬x = w
[PROOFSTEP]
rw [decide_eq_true_eq] at h
[GOAL]
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
h : x = u ∨ x = v
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + 1) ↔ ¬u = w → ¬x = u ∧ ¬x = w
[PROOFSTEP]
obtain (rfl | rfl) := h
[GOAL]
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v✝ : V
p✝ : Walk G u v✝
ht✝ : IsTrail p✝
x v w : V
p : Walk G v w
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
huv : Adj G x v
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (x, v) ∈ edges p
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + 1) ↔ ¬x = w → ¬x = x ∧ ¬x = w
[PROOFSTEP]
rw [Nat.even_add_one, ih]
[GOAL]
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v✝ : V
p✝ : Walk G u v✝
ht✝ : IsTrail p✝
x v w : V
p : Walk G v w
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
huv : Adj G x v
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (x, v) ∈ edges p
⊢ ¬(v ≠ w → x ≠ v ∧ x ≠ w) ↔ ¬x = w → ¬x = x ∧ ¬x = w
[PROOFSTEP]
simp only [huv.ne, imp_false, Ne.def, not_false_iff, true_and_iff, not_forall, Classical.not_not, exists_prop,
  eq_self_iff_true, not_true, false_and_iff, and_iff_right_iff_imp]
[GOAL]
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v✝ : V
p✝ : Walk G u v✝
ht✝ : IsTrail p✝
x v w : V
p : Walk G v w
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
huv : Adj G x v
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (x, v) ∈ edges p
⊢ x = w → ¬v = w
[PROOFSTEP]
rintro rfl rfl
[GOAL]
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v✝ : V
p✝ : Walk G u v✝
ht✝ : IsTrail p✝
v : V
huv : Adj G v v
p : Walk G v v
ih : Even (List.countp (fun e => decide (v ∈ e)) (edges p)) ↔ v ≠ v → v ≠ v ∧ v ≠ v
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v) ∈ edges p
⊢ False
[PROOFSTEP]
exact G.loopless _ huv
[GOAL]
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v : V
p✝ : Walk G u✝ v
ht✝ : IsTrail p✝
x u w : V
huv : Adj G u x
p : Walk G x w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ x ≠ w → x ≠ x ∧ x ≠ w
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + 1) ↔ ¬u = w → ¬x = u ∧ ¬x = w
[PROOFSTEP]
rw [Nat.even_add_one, ih, ← not_iff_not]
[GOAL]
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v : V
p✝ : Walk G u✝ v
ht✝ : IsTrail p✝
x u w : V
huv : Adj G u x
p : Walk G x w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ x ≠ w → x ≠ x ∧ x ≠ w
⊢ ¬¬(x ≠ w → x ≠ x ∧ x ≠ w) ↔ ¬(¬u = w → ¬x = u ∧ ¬x = w)
[PROOFSTEP]
simp only [huv.ne.symm, Ne.def, eq_self_iff_true, not_true, false_and_iff, not_forall, not_false_iff, exists_prop,
  and_true_iff, Classical.not_not, true_and_iff, iff_and_self]
[GOAL]
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v : V
p✝ : Walk G u✝ v
ht✝ : IsTrail p✝
x u w : V
huv : Adj G u x
p : Walk G x w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ x ≠ w → x ≠ x ∧ x ≠ w
⊢ x = w → ¬u = w
[PROOFSTEP]
rintro rfl
[GOAL]
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v : V
p✝ : Walk G u✝ v
ht✝ : IsTrail p✝
x u : V
huv : Adj G u x
p : Walk G x x
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ x ≠ x → x ≠ x ∧ x ≠ x
⊢ ¬u = x
[PROOFSTEP]
exact huv.ne
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
h : ¬decide (x = u ∨ x = v) = true
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + 0) ↔ ¬u = w → ¬x = u ∧ ¬x = w
[PROOFSTEP]
rw [decide_eq_true_eq, not_or] at h
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ v ≠ w → x ≠ v ∧ x ≠ w
h : ¬x = u ∧ ¬x = v
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p) + 0) ↔ ¬u = w → ¬x = u ∧ ¬x = w
[PROOFSTEP]
simp only [h.1, h.2, not_false_iff, true_and_iff, add_zero, Ne.def] at ih ⊢
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
h : ¬x = u ∧ ¬x = v
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = w → ¬x = w
⊢ Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬u = w → ¬x = w
[PROOFSTEP]
rw [ih]
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
h : ¬x = u ∧ ¬x = v
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = w → ¬x = w
⊢ ¬v = w → ¬x = w ↔ ¬u = w → ¬x = w
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
h : ¬x = u ∧ ¬x = v
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = w → ¬x = w
⊢ (¬v = w → ¬x = w) → ¬u = w → ¬x = w
[PROOFSTEP]
rintro h' h'' rfl
[GOAL]
case neg.mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v : V
huv : Adj G u v
h : ¬x = u ∧ ¬x = v
p : Walk G v x
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = x → ¬x = x
h' : ¬v = x → ¬x = x
h'' : ¬u = x
⊢ False
[PROOFSTEP]
simp only [imp_false, eq_self_iff_true, not_true, Classical.not_not] at h'
[GOAL]
case neg.mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v : V
huv : Adj G u v
h : ¬x = u ∧ ¬x = v
p : Walk G v x
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = x → ¬x = x
h'' : ¬u = x
h' : v = x
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
case neg.mp.refl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v : V
p✝ : Walk G u✝ v
ht✝ : IsTrail p✝
x u : V
h'' : ¬u = x
huv : Adj G u x
h : ¬x = u ∧ ¬x = x
p : Walk G x x
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬x = x → ¬x = x
⊢ False
[PROOFSTEP]
simp only [not_true, and_false, false_and] at h
[GOAL]
case neg.mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v w : V
huv : Adj G u v
p : Walk G v w
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
h : ¬x = u ∧ ¬x = v
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = w → ¬x = w
⊢ (¬u = w → ¬x = w) → ¬v = w → ¬x = w
[PROOFSTEP]
rintro h' h'' rfl
[GOAL]
case neg.mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v : V
huv : Adj G u v
h : ¬x = u ∧ ¬x = v
p : Walk G v x
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = x → ¬x = x
h' : ¬u = x → ¬x = x
h'' : ¬v = x
⊢ False
[PROOFSTEP]
simp only [imp_false, eq_self_iff_true, not_true, Classical.not_not] at h'
[GOAL]
case neg.mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u✝ v✝ : V
p✝ : Walk G u✝ v✝
ht✝ : IsTrail p✝
x u v : V
huv : Adj G u v
h : ¬x = u ∧ ¬x = v
p : Walk G v x
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = x → ¬x = x
h'' : ¬v = x
h' : u = x
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
case neg.mpr.refl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v✝ : V
p✝ : Walk G u v✝
ht✝ : IsTrail p✝
x v : V
p : Walk G v x
ih : Even (List.countp (fun e => decide (x ∈ e)) (edges p)) ↔ ¬v = x → ¬x = x
h'' : ¬v = x
huv : Adj G x v
h : ¬x = x ∧ ¬x = v
ht : IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (x, v) ∈ edges p
⊢ False
[PROOFSTEP]
simp only [not_true, and_false, false_and] at h
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail p
[PROOFSTEP]
rw [isTrail_def, List.nodup_iff_count_le_one]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ ∀ (a : Sym2 V), List.count a (edges p) ≤ 1
[PROOFSTEP]
intro e
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ List.count e (edges p) ≤ 1
[PROOFSTEP]
by_cases he : e ∈ p.edges
[GOAL]
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : e ∈ edges p
⊢ List.count e (edges p) ≤ 1
[PROOFSTEP]
exact (h e (edges_subset_edgeSet _ he)).le
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : ¬e ∈ edges p
⊢ List.count e (edges p) ≤ 1
[PROOFSTEP]
simp [he]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : e ∈ edgeSet G
⊢ e ∈ edges p
[PROOFSTEP]
simpa using (h e he).ge
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ e ∈ IsTrail.edgesFinset (_ : IsTrail p) ↔ e ∈ edgeSet G
[PROOFSTEP]
simp only [Finset.mem_mk, Multiset.mem_coe, h.mem_edges_iff]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ IsEulerian p ↔ IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ IsEulerian p → IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
[PROOFSTEP]
intro h
[GOAL]
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
[PROOFSTEP]
exact ⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩
[GOAL]
case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ (IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p) → IsEulerian p
[PROOFSTEP]
rintro ⟨h, hl⟩
[GOAL]
case mpr.intro
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsTrail p
hl : ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
⊢ IsEulerian p
[PROOFSTEP]
exact h.isEulerian_of_forall_mem hl
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail.edgesFinset (_ : IsTrail p) = edgeFinset G
[PROOFSTEP]
ext e
[GOAL]
case a
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ e ∈ IsTrail.edgesFinset (_ : IsTrail p) ↔ e ∈ edgeFinset G
[PROOFSTEP]
simp [h.mem_edges_iff]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (degree G x) ↔ u ≠ v → x ≠ u ∧ x ≠ v
[PROOFSTEP]
convert ht.isTrail.even_countp_edges_iff x
[GOAL]
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ degree G x = List.countp (fun e => decide (x ∈ e)) (edges p)
[PROOFSTEP]
rw [← Multiset.coe_countp, Multiset.countp_eq_card_filter, ← card_incidenceFinset_eq_degree]
[GOAL]
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Finset.card (incidenceFinset G x) = ↑Multiset.card (Multiset.filter (fun e => x ∈ e) ↑(edges p))
[PROOFSTEP]
change Multiset.card _ = _
[GOAL]
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ↑Multiset.card (incidenceFinset G x).val = ↑Multiset.card (Multiset.filter (fun e => x ∈ e) ↑(edges p))
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (incidenceFinset G x).val = Multiset.filter (fun e => x ∈ e) ↑(edges p)
[PROOFSTEP]
convert_to _ = (ht.isTrail.edgesFinset.filter (Membership.mem x)).val
[GOAL]
case h.e'_1.h.e'_3.h.e_6.h.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (incidenceFinset G x).val = (Finset.filter (Membership.mem x) (IsTrail.edgesFinset (_ : IsTrail p))).val
[PROOFSTEP]
have : Fintype G.edgeSet := fintypeEdgeSet ht
[GOAL]
case h.e'_1.h.e'_3.h.e_6.h.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : Fintype ↑(edgeSet G)
⊢ (incidenceFinset G x).val = (Finset.filter (Membership.mem x) (IsTrail.edgesFinset (_ : IsTrail p))).val
[PROOFSTEP]
rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
s : Finset V
h : s = Finset.filter (fun v => Odd (degree G v)) Finset.univ
⊢ Finset.card s = 0 ∨ Finset.card s = 2
[PROOFSTEP]
subst s
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Finset.card (Finset.filter (fun v => Odd (degree G v)) Finset.univ) = 0 ∨
    Finset.card (Finset.filter (fun v => Odd (degree G v)) Finset.univ) = 2
[PROOFSTEP]
simp only [Nat.odd_iff_not_even, Finset.card_eq_zero]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬Even (degree G v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v => ¬Even (degree G v)) Finset.univ) = 2
[PROOFSTEP]
simp only [ht.even_degree_iff, Ne.def, not_forall, not_and, Classical.not_not, exists_prop]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
[PROOFSTEP]
obtain rfl | hn := eq_or_ne u v
[GOAL]
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : Walk G u u
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ) = 2
[PROOFSTEP]
left
[GOAL]
case inl.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : Walk G u u
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅
[PROOFSTEP]
simp
[GOAL]
case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
[PROOFSTEP]
right
[GOAL]
case inr.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
hn : u ≠ v
⊢ Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
[PROOFSTEP]
convert_to _ = ({ u, v } : Finset V).card
[GOAL]
case h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
hn : u ≠ v
⊢ 2 = Finset.card {u, v}
[PROOFSTEP]
simp [hn]
[GOAL]
case inr.h.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
hn : u ≠ v
⊢ Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = Finset.card {u, v}
[PROOFSTEP]
congr
[GOAL]
case inr.h.convert_2.e_s
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = {u, v}
[PROOFSTEP]
ext x
[GOAL]
case inr.h.convert_2.e_s.a
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
hn : u ≠ v
x : V
⊢ x ∈ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ ↔ x ∈ {u, v}
[PROOFSTEP]
simp [hn, imp_iff_not_or]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Fintype.card ↑{v | Odd (degree G v)} = 0 ∨ Fintype.card ↑{v | Odd (degree G v)} = 2
[PROOFSTEP]
rw [← Set.toFinset_card]
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Finset.card (Set.toFinset {v | Odd (degree G v)}) = 0 ∨ Finset.card (Set.toFinset {v | Odd (degree G v)}) = 2
[PROOFSTEP]
apply IsEulerian.card_filter_odd_degree ht
[GOAL]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Set.toFinset {v | Odd (degree G v)} = Finset.filter (fun v => Odd (degree G v)) Finset.univ
[PROOFSTEP]
ext v
[GOAL]
case a
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v✝ : V
p : Walk G u v✝
ht : IsEulerian p
v : V
⊢ v ∈ Set.toFinset {v | Odd (degree G v)} ↔ v ∈ Finset.filter (fun v => Odd (degree G v)) Finset.univ
[PROOFSTEP]
simp


[GOAL]
x : ℤ
⊢ IsUnit x ↔ |x| = 1
[PROOFSTEP]
rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, coe_nat_inj']
[GOAL]
a : ℤ
ha : IsUnit a
⊢ a ^ 2 = 1
[PROOFSTEP]
rw [sq, isUnit_mul_self ha]
[GOAL]
u : ℤˣ
⊢ u ^ 2 = 1
[PROOFSTEP]
rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]
[GOAL]
u : ℤˣ
⊢ u * u = 1
[PROOFSTEP]
rw [← sq, units_sq]
[GOAL]
u : ℤˣ
⊢ u⁻¹ = u
[PROOFSTEP]
rw [inv_eq_iff_mul_eq_one, units_mul_self]
[GOAL]
u : ℤˣ
⊢ ↑u * ↑u = 1
[PROOFSTEP]
rw [← Units.val_mul, units_mul_self, Units.val_one]
[GOAL]
n : ℕ
⊢ 0 < |(-1)|
[PROOFSTEP]
simp
[GOAL]
u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ (n % 2)
[PROOFSTEP]
conv =>
  lhs
  rw [← Nat.mod_add_div n 2]; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
[PROOFSTEP]
  lhs
  rw [← Nat.mod_add_div n 2]; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
[PROOFSTEP]
  lhs
  rw [← Nat.mod_add_div n 2]; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
[PROOFSTEP]
lhs
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n
[PROOFSTEP]
rw [← Nat.mod_add_div n 2]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ (n % 2 + 2 * (n / 2))
[PROOFSTEP]
rw [pow_add, pow_mul, units_sq, one_pow, mul_one]


[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ ¬Adj ⊥ v w → Fintype.card ↑(commonNeighbors ⊥ v w) = 0
[PROOFSTEP]
simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ ↔ a✝ ∈ ∅
[PROOFSTEP]
simp [mem_commonNeighbors]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ Fintype.card ↑(commonNeighbors ⊤ v w) = Fintype.card V - 2
[PROOFSTEP]
rw [card_commonNeighbors_top]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ v ≠ w
[PROOFSTEP]
exact h
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
[PROOFSTEP]
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) + Fintype.card ↑(commonNeighbors G v w) =
    2 * k - Fintype.card ↑(commonNeighbors G v w) + Fintype.card ↑(commonNeighbors G v w)
[PROOFSTEP]
rw [Nat.sub_add_cancel, ← Set.toFinset_card]
  -- porting note: Set.toFinset_inter needs workaround to use unification to solve for one of the
    -- instance arguments:
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) + Finset.card (Set.toFinset (commonNeighbors G v w)) = 2 * k
[PROOFSTEP]
simp [commonNeighbors, @Set.toFinset_inter _ _ _ _ _ _ (_), ← neighborFinset_def, Finset.card_union_add_card_inter,
  card_neighborFinset_eq_degree, h.regular.degree_eq, two_mul]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ 2 * k
[PROOFSTEP]
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ degree G v ≤ 2 * k
[PROOFSTEP]
simp [h.regular.degree_eq, two_mul]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
hne : v ≠ w
ha : ¬Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - μ
[PROOFSTEP]
rw [← h.of_not_adj v w hne ha]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
hne : v ≠ w
ha : ¬Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
[PROOFSTEP]
apply h.card_neighborFinset_union_eq
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - ℓ
[PROOFSTEP]
rw [← h.of_adj v w ha]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
[PROOFSTEP]
apply h.card_neighborFinset_union_eq
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
⊢ (neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w}) =
    ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ a✝ ∈ (neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w}) ↔
    a✝ ∈ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ ¬a✝ ∈ (neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w}) ↔
    ¬a✝ ∈ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})
[PROOFSTEP]
simp [imp_iff_not_or, or_assoc, or_comm, or_left_comm]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
⊢ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v}) = (neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ a✝ ∈ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v}) ↔
    a✝ ∈ (neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ
[PROOFSTEP]
simp only [and_imp, mem_union, mem_sdiff, mem_compl, and_iff_left_iff_imp, mem_neighborFinset, mem_inter, mem_singleton]
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ ¬Adj G v a✝ → ¬Adj G w a✝ → ¬(a✝ = w ∨ a✝ = v)
[PROOFSTEP]
rintro hnv hnw (rfl | rfl)
[GOAL]
case a.inl
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v a✝ : V
hnv : ¬Adj G v a✝
h : Adj G v a✝
hnw : ¬Adj G a✝ a✝
⊢ False
[PROOFSTEP]
exact hnv h
[GOAL]
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ False
[PROOFSTEP]
apply hnw
[GOAL]
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ Adj G w a✝
[PROOFSTEP]
rwa [adj_comm]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree Gᶜ (n - k - 1)
[PROOFSTEP]
rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree Gᶜ (Fintype.card V - 1 - k)
[PROOFSTEP]
exact h.regular.compl
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : Adj Gᶜ v w
⊢ Fintype.card ↑(commonNeighbors Gᶜ v w) = n - (2 * k - μ) - 2
[PROOFSTEP]
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl, Set.toFinset_diff,
  Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : Adj Gᶜ v w
⊢ Finset.card ((neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w})) = n - (2 * k - μ) - 2
[PROOFSTEP]
simp_rw [compl_neighborFinset_sdiff_inter_eq]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : Adj Gᶜ v w
⊢ Finset.card (((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
[PROOFSTEP]
have hne : v ≠ w := ne_of_adj _ ha
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : Adj Gᶜ v w
hne : v ≠ w
⊢ Finset.card (((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
[PROOFSTEP]
rw [compl_adj] at ha
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ Finset.card (((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
[PROOFSTEP]
rw [card_sdiff, ← insert_eq, card_insert_of_not_mem, card_singleton, ← Finset.compl_union]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w)ᶜ - (1 + 1) = n - (2 * k - μ) - 2
[PROOFSTEP]
rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ ¬w ∈ {v}
[PROOFSTEP]
simp only [hne.symm, not_false_iff, mem_singleton]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ
[PROOFSTEP]
intro u
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
u : V
⊢ u ∈ {w} ∪ {v} → u ∈ (neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ
[PROOFSTEP]
simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
u : V
⊢ u = w ∨ u = v → ¬Adj G v u ∧ ¬Adj G w u
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬Adj G v u
hne : v ≠ u
⊢ ¬Adj G v u ∧ ¬Adj G u u
[PROOFSTEP]
simpa [adj_comm] using ha.2
[GOAL]
case inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬Adj G u w
hne : u ≠ w
⊢ ¬Adj G u u ∧ ¬Adj G w u
[PROOFSTEP]
simpa [adj_comm] using ha.2
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Adj Gᶜ v w
⊢ Fintype.card ↑(commonNeighbors Gᶜ v w) = n - (2 * k - ℓ)
[PROOFSTEP]
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl, Set.toFinset_diff,
  Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Adj Gᶜ v w
⊢ Finset.card ((neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w})) = n - (2 * k - ℓ)
[PROOFSTEP]
simp only [not_and, Classical.not_not, compl_adj] at hna
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
⊢ Finset.card ((neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w})) = n - (2 * k - ℓ)
[PROOFSTEP]
have h2' := hna hn
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
h2' : Adj G v w
⊢ Finset.card ((neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w})) = n - (2 * k - ℓ)
[PROOFSTEP]
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
h2' : Adj G v w
⊢ Finset.card ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) = n - (2 * k - ℓ)
[PROOFSTEP]
rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
hn : 0 < n
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
[PROOFSTEP]
rw [← h.card, Fintype.card_pos_iff] at hn
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
hn : Nonempty V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
[PROOFSTEP]
obtain ⟨v⟩ := hn
[GOAL]
case intro
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
[PROOFSTEP]
convert card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
[GOAL]
case h.e'_2.h.e'_5
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ k = Finset.card (neighborFinset G v)
[PROOFSTEP]
simp [h.regular v]
[GOAL]
case h.e'_3.h.e'_5
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ n - k - 1 = Finset.card (neighborFinset Gᶜ v)
[PROOFSTEP]
simp [h.compl.regular v]
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ ∀ (a : V), a ∈ neighborFinset G v → Finset.card (bipartiteAbove G.Adj (neighborFinset Gᶜ v) a) = k - ℓ - 1
[PROOFSTEP]
intro w hw
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : w ∈ neighborFinset G v
⊢ Finset.card (bipartiteAbove G.Adj (neighborFinset Gᶜ v) w) = k - ℓ - 1
[PROOFSTEP]
rw [mem_neighborFinset] at hw
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
⊢ Finset.card (bipartiteAbove G.Adj (neighborFinset Gᶜ v) w) = k - ℓ - 1
[PROOFSTEP]
simp_rw [bipartiteAbove, show G.Adj w = fun a => G.Adj w a by rfl, ← mem_neighborFinset, filter_mem_eq_inter]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
⊢ Adj G w = fun a => Adj G w a
[PROOFSTEP]
rfl
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
⊢ Finset.card (neighborFinset Gᶜ v ∩ neighborFinset G w) = k - ℓ - 1
[PROOFSTEP]
have s : { v } ⊆ G.neighborFinset w \ G.neighborFinset v :=
  by
  rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
  exact ⟨hw.symm, G.not_mem_neighborFinset_self v⟩
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
⊢ {v} ⊆ neighborFinset G w \ neighborFinset G v
[PROOFSTEP]
rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
⊢ Adj G w v ∧ ¬v ∈ neighborFinset G v
[PROOFSTEP]
exact ⟨hw.symm, G.not_mem_neighborFinset_self v⟩
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset Gᶜ v ∩ neighborFinset G w) = k - ℓ - 1
[PROOFSTEP]
rw [inter_comm, neighborFinset_compl, inter_sdiff, ← sdiff_eq_inter_compl, card_sdiff s, card_singleton, ←
  sdiff_inter_self_left, card_sdiff (by apply inter_subset_left)]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ neighborFinset G w ∩ neighborFinset G v ⊆ neighborFinset G w
[PROOFSTEP]
apply inter_subset_left
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset G w) - Finset.card (neighborFinset G w ∩ neighborFinset G v) - 1 = k - ℓ - 1
[PROOFSTEP]
congr
[GOAL]
case intro.convert_3.e_a.e_a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset G w) = k
[PROOFSTEP]
simp [h.regular w]
[GOAL]
case intro.convert_3.e_a.e_a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset G w ∩ neighborFinset G v) = ℓ
[PROOFSTEP]
simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw, ← Set.toFinset_card]
[GOAL]
case intro.convert_3.e_a.e_a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (Set.toFinset (neighborSet G v ∩ neighborSet G w)) = Finset.card (Set.toFinset (commonNeighbors G v w))
[PROOFSTEP]
congr!
[GOAL]
case intro.convert_4
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ ∀ (b : V), b ∈ neighborFinset Gᶜ v → Finset.card (bipartiteBelow G.Adj (neighborFinset G v) b) = μ
[PROOFSTEP]
intro w hw
[GOAL]
case intro.convert_4
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : w ∈ neighborFinset Gᶜ v
⊢ Finset.card (bipartiteBelow G.Adj (neighborFinset G v) w) = μ
[PROOFSTEP]
simp_rw [neighborFinset_compl, mem_sdiff, mem_compl, mem_singleton, mem_neighborFinset, ← Ne.def] at hw
[GOAL]
case intro.convert_4
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : ¬Adj G v w ∧ w ≠ v
⊢ Finset.card (bipartiteBelow G.Adj (neighborFinset G v) w) = μ
[PROOFSTEP]
simp_rw [bipartiteBelow, adj_comm, ← mem_neighborFinset, filter_mem_eq_inter, neighborFinset_def, ← Set.toFinset_inter,
  ← h.of_not_adj v w hw.2.symm hw.1, ← Set.toFinset_card]
[GOAL]
case intro.convert_4
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hw : ¬Adj G v w ∧ w ≠ v
⊢ Finset.card (Set.toFinset (neighborSet G v ∩ neighborSet G w)) = Finset.card (Set.toFinset (commonNeighbors G v w))
[PROOFSTEP]
congr!
[GOAL]
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
⊢ adjMatrix α G ^ 2 = k • 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ
[PROOFSTEP]
ext v w
[GOAL]
case a.h
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
⊢ (adjMatrix α G ^ 2) v w = (k • 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w
[PROOFSTEP]
simp only [adjMatrix_pow_apply_eq_card_walk, Set.coe_setOf, Matrix.add_apply, Matrix.smul_apply, adjMatrix_apply,
  compl_adj]
[GOAL]
case a.h
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
⊢ ↑(Fintype.card { x // Walk.length x = 2 }) =
    (k • OfNat.ofNat 1 v w + ℓ • if Adj G v w then 1 else 0) + μ • if v ≠ w ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
rw [Fintype.card_congr (G.walkLengthTwoEquivCommonNeighbors v w)]
[GOAL]
case a.h
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • OfNat.ofNat 1 v w + ℓ • if Adj G v w then 1 else 0) + μ • if v ≠ w ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
obtain rfl | hn := eq_or_ne v w
[GOAL]
case a.h.inl
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v : V
⊢ ↑(Fintype.card ↑(commonNeighbors G v v)) =
    (k • OfNat.ofNat 1 v v + ℓ • if Adj G v v then 1 else 0) + μ • if v ≠ v ∧ ¬Adj G v v then 1 else 0
[PROOFSTEP]
rw [← Set.toFinset_card]
[GOAL]
case a.h.inl
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v : V
⊢ ↑(Finset.card (Set.toFinset (commonNeighbors G v v))) =
    (k • OfNat.ofNat 1 v v + ℓ • if Adj G v v then 1 else 0) + μ • if v ≠ v ∧ ¬Adj G v v then 1 else 0
[PROOFSTEP]
simp [commonNeighbors, ← neighborFinset_def, h.regular v]
[GOAL]
case a.h.inr
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • OfNat.ofNat 1 v w + ℓ • if Adj G v w then 1 else 0) + μ • if v ≠ w ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn]
[GOAL]
case a.h.inr
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • 0 + ℓ • if Adj G v w then 1 else 0) + μ • if True ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
by_cases ha : G.Adj v w
[GOAL]
case pos
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • 0 + ℓ • if Adj G v w then 1 else 0) + μ • if True ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one]
[GOAL]
case neg
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • 0 + ℓ • if Adj G v w then 1 else 0) + μ • if True ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one]
[GOAL]
case pos
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) = ↑ℓ
[PROOFSTEP]
rw [h.of_adj v w ha]
[GOAL]
case neg
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) = ↑μ
[PROOFSTEP]
rw [h.of_not_adj v w hn ha]


[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ toEdge h { val := v, property := hv } = { val := Quotient.mk (Sym2.Rel.setoid V) (v, w), property := hvw }
[PROOFSTEP]
simp only [IsMatching.toEdge, Subtype.mk_eq_mk]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, Exists.choose (_ : ∃! w, Adj M (↑{ val := v, property := hv }) w)) =
    Quotient.mk (Sym2.Rel.setoid V) (v, w)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_snd
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ Exists.choose (_ : ∃! w, Adj M (↑{ val := v, property := hv }) w) = w
[PROOFSTEP]
exact ((h (M.edge_vert hvw)).choose_spec.2 w hvw).symm
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
⊢ Function.Surjective (toEdge h)
[PROOFSTEP]
rintro ⟨e, he⟩
[GOAL]
case mk
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
e : Sym2 V
he : e ∈ edgeSet M
⊢ ∃ a, toEdge h a = { val := e, property := he }
[PROOFSTEP]
refine Sym2.ind (fun x y he => ?_) e he
[GOAL]
case mk
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
e : Sym2 V
he✝ : e ∈ edgeSet M
x y : V
he : Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet M
⊢ ∃ a, toEdge h a = { val := Quotient.mk (Sym2.Rel.setoid V) (x, y), property := he }
[PROOFSTEP]
exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj _ he⟩
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
v w : V
h : IsMatching M
hv : v ∈ M.verts
hw : w ∈ M.verts
ha : Adj M v w
⊢ toEdge h { val := v, property := hv } = toEdge h { val := w, property := hw }
[PROOFSTEP]
rw [h.toEdge_eq_of_adj hv ha, h.toEdge_eq_of_adj hw (M.symm ha), Subtype.mk_eq_mk, Sym2.eq_swap]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
⊢ support M = M.verts
[PROOFSTEP]
refine M.support_subset_verts.antisymm fun v hv => ?_
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
⊢ v ∈ support M
[PROOFSTEP]
obtain ⟨w, hvw, -⟩ := h hv
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
w : V
hvw : Adj M v w
⊢ v ∈ support M
[PROOFSTEP]
exact ⟨_, hvw⟩
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : (v : V) → Fintype ↑(neighborSet M v)
⊢ IsMatching M ↔ ∀ (v : V), v ∈ M.verts → degree M v = 1
[PROOFSTEP]
simp only [degree_eq_one_iff_unique_adj, IsMatching]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h : IsMatching M
⊢ Even (Finset.card (Set.toFinset M.verts))
[PROOFSTEP]
classical
rw [isMatching_iff_forall_degree] at h
use M.coe.edgeFinset.card
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  -- Porting note: `SimpleGraph.Subgraph.coe_degree` does not trigger because it uses
    -- instance arguments instead of implicit arguments for the first `Fintype` argument.
    -- Using a `convert_to` to swap out the `Fintype` instance to the "right" one.
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
simp [h, Finset.card_univ]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h : IsMatching M
⊢ Even (Finset.card (Set.toFinset M.verts))
[PROOFSTEP]
rw [isMatching_iff_forall_degree] at h
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Even (Finset.card (Set.toFinset M.verts))
[PROOFSTEP]
use M.coe.edgeFinset.card
[GOAL]
case h
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Finset.card (Set.toFinset M.verts) =
    Finset.card (edgeFinset (Subgraph.coe M)) + Finset.card (edgeFinset (Subgraph.coe M))
[PROOFSTEP]
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  -- Porting note: `SimpleGraph.Subgraph.coe_degree` does not trigger because it uses
    -- instance arguments instead of implicit arguments for the first `Fintype` argument.
    -- Using a `convert_to` to swap out the `Fintype` instance to the "right" one.
[GOAL]
case h
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Finset.card (Set.toFinset M.verts) = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v
[PROOFSTEP]
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
[GOAL]
case h.convert_2
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Finset.card (Set.toFinset M.verts) = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v
[PROOFSTEP]
simp [h, Finset.card_univ]
[GOAL]
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M ↔ ∀ (v : V), ∃! w, Adj M v w
[PROOFSTEP]
refine' ⟨_, fun hm => ⟨fun v _ => hm v, fun v => _⟩⟩
[GOAL]
case refine'_1
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M → ∀ (v : V), ∃! w, Adj M v w
[PROOFSTEP]
rintro ⟨hm, hs⟩ v
[GOAL]
case refine'_1.intro
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : IsMatching M
hs : IsSpanning M
v : V
⊢ ∃! w, Adj M v w
[PROOFSTEP]
exact hm (hs v)
[GOAL]
case refine'_2
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : ∀ (v : V), ∃! w, Adj M v w
v : V
⊢ v ∈ M.verts
[PROOFSTEP]
obtain ⟨w, hw, -⟩ := hm v
[GOAL]
case refine'_2.intro.intro
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : ∀ (v : V), ∃! w, Adj M v w
v w : V
hw : Adj M v w
⊢ v ∈ M.verts
[PROOFSTEP]
exact M.edge_vert hw
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : (v : V) → Fintype ↑(neighborSet M v)
⊢ IsPerfectMatching M ↔ ∀ (v : V), degree M v = 1
[PROOFSTEP]
simp [degree_eq_one_iff_unique_adj, isPerfectMatching_iff]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype V
h : IsPerfectMatching M
⊢ Even (Fintype.card V)
[PROOFSTEP]
classical simpa only [h.2.card_verts] using IsMatching.even_card h.1
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype V
h : IsPerfectMatching M
⊢ Even (Fintype.card V)
[PROOFSTEP]
simpa only [h.2.card_verts] using IsMatching.even_card h.1


[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
⊢ ↑(hallMatchingsOn t ι')
[PROOFSTEP]
refine' ⟨fun i => f.val ⟨i, h i.property⟩, _⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
⊢ (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) ∈ hallMatchingsOn t ι'
[PROOFSTEP]
cases' f.property with hinj hc
[GOAL]
case intro
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Function.Injective ↑f
hc : ∀ (x : { x // x ∈ ι'' }), ↑f x ∈ t ↑x
⊢ (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) ∈ hallMatchingsOn t ι'
[PROOFSTEP]
refine' ⟨_, fun i => hc ⟨i, h i.property⟩⟩
[GOAL]
case intro
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Function.Injective ↑f
hc : ∀ (x : { x // x ∈ ι'' }), ↑f x ∈ t ↑x
⊢ Function.Injective fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }
[PROOFSTEP]
rintro ⟨i, hi⟩ ⟨j, hj⟩ hh
[GOAL]
case intro.mk.mk
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Function.Injective ↑f
hc : ∀ (x : { x // x ∈ ι'' }), ↑f x ∈ t ↑x
i : ι
hi : i ∈ ι'
j : ι
hj : j ∈ ι'
hh :
  (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) { val := i, property := hi } =
    (fun i => ↑f { val := ↑i, property := (_ : ↑i ∈ ι'') }) { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
[PROOFSTEP]
simpa only [Subtype.mk_eq_mk] using hinj hh
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ Nonempty ↑(hallMatchingsOn t ι')
[PROOFSTEP]
classical
refine' ⟨Classical.indefiniteDescription _ _⟩
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
intro s'
convert h (s'.image (↑)) using 1
simp only [card_image_of_injective s' Subtype.coe_injective]
rw [image_biUnion]
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ Nonempty ↑(hallMatchingsOn t ι')
[PROOFSTEP]
refine' ⟨Classical.indefiniteDescription _ _⟩
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ ∃ x, x ∈ hallMatchingsOn t ι'
[PROOFSTEP]
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
⊢ ∀ (s : Finset { x // x ∈ ι' }), card s ≤ card (Finset.biUnion s fun i => t ↑i)
[PROOFSTEP]
intro s'
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card s' ≤ card (Finset.biUnion s' fun i => t ↑i)
[PROOFSTEP]
convert h (s'.image (↑)) using 1
[GOAL]
case h.e'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card s' = card (image Subtype.val s')
case h.e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card (Finset.biUnion s' fun i => t ↑i) = card (Finset.biUnion (image Subtype.val s') t)
[PROOFSTEP]
simp only [card_image_of_injective s' Subtype.coe_injective]
[GOAL]
case h.e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ card (Finset.biUnion s' fun i => t ↑i) = card (Finset.biUnion (image Subtype.val s') t)
[PROOFSTEP]
rw [image_biUnion]
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')
[PROOFSTEP]
classical
rw [hallMatchingsOn]
let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
  rintro f i
  refine' ⟨f.val i, _⟩
  rw [mem_biUnion]
  exact ⟨i, i.property, f.property.2 i⟩
apply Finite.of_injective g
intro f f' h
ext a
rw [Function.funext_iff] at h
simpa using h a
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')
[PROOFSTEP]
rw [hallMatchingsOn]
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑{f | Function.Injective f ∧ ∀ (x : { x // x ∈ ι' }), f x ∈ t ↑x}
[PROOFSTEP]
let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
  rintro f i
  refine' ⟨f.val i, _⟩
  rw [mem_biUnion]
  exact ⟨i, i.property, f.property.2 i⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t }
[PROOFSTEP]
rintro f i
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : { x // x ∈ ι' }
⊢ { x // x ∈ Finset.biUnion ι' t }
[PROOFSTEP]
refine' ⟨f.val i, _⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : { x // x ∈ ι' }
⊢ ↑f i ∈ Finset.biUnion ι' t
[PROOFSTEP]
rw [mem_biUnion]
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : { x // x ∈ ι' }
⊢ ∃ a, a ∈ ι' ∧ ↑f i ∈ t a
[PROOFSTEP]
exact ⟨i, i.property, f.property.2 i⟩
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
⊢ Finite ↑{f | Function.Injective f ∧ ∀ (x : { x // x ∈ ι' }), f x ∈ t ↑x}
[PROOFSTEP]
apply Finite.of_injective g
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
⊢ Function.Injective g
[PROOFSTEP]
intro f f' h
[GOAL]
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
⊢ f = f'
[PROOFSTEP]
ext a
[GOAL]
case a.h
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
a : { x // x ∈ ι' }
⊢ ↑f a = ↑f' a
[PROOFSTEP]
rw [Function.funext_iff] at h
[GOAL]
case a.h
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → { x // x ∈ ι' } → { x // x ∈ Finset.biUnion ι' t } :=
  fun f i => { val := ↑f i, property := (_ : ↑f i ∈ Finset.biUnion ι' t) }
f f' : ↑(hallMatchingsOn t ι')
h : ∀ (a : { x // x ∈ ι' }), g f a = g f' a
a : { x // x ∈ ι' }
⊢ ↑f a = ↑f' a
[PROOFSTEP]
simpa using h a
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
intro h
[GOAL]
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
  hallMatchingsOn.nonempty t h ι'.unop
[GOAL]
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
classical
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') :=
  by
  intro ι'
  rw [hallMatchingsFunctor]
  infer_instance
    -- Apply the compactness argument
obtain ⟨u, hu⟩ :=
  nonempty_sections_of_finite_inverse_system
    (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
refine' ⟨_, _, _⟩
·
  -- Build the matching function from the sectionexact fun i =>
    (u (Opposite.op ({ i } : Finset ι))).val ⟨i, by simp only [Opposite.unop_op, mem_singleton]⟩
·
  -- Show that it is injective
  intro i i'
  have subi : ({ i } : Finset ι) ⊆ { i, i' } := by simp
  have subi' : ({ i' } : Finset ι) ⊆ { i, i' } := by simp
  rw [← Finset.le_iff_subset] at subi subi'
  simp only
  rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
  let uii' := u (Opposite.op ({ i, i' } : Finset ι))
  exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
·
  -- Show that it maps each index to the corresponding finite set
  intro i
  apply (u (Opposite.op ({ i } : Finset ι))).property.2
[GOAL]
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') :=
  by
  intro ι'
  rw [hallMatchingsFunctor]
  infer_instance
    -- Apply the compactness argument
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
[PROOFSTEP]
intro ι'
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite ((hallMatchingsFunctor t).obj ι')
[PROOFSTEP]
rw [hallMatchingsFunctor]
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ((CategoryTheory.Functor.mk
          { obj := fun ι' => ↑(hallMatchingsOn t ι'.unop),
            map := fun {ι' ι''} g f => hallMatchingsOn.restrict t (_ : ι''.unop ≤ ι'.unop) f }).obj
      ι')
[PROOFSTEP]
infer_instance
  -- Apply the compactness argument
[GOAL]
case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
obtain ⟨u, hu⟩ :=
  nonempty_sections_of_finite_inverse_system
    (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
[GOAL]
case mp.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case mp.intro.refine'_1
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
⊢ ι → α
[PROOFSTEP]
exact fun i => (u (Opposite.op ({ i } : Finset ι))).val ⟨i, by simp only [Opposite.unop_op, mem_singleton]⟩
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ i ∈ (Opposite.op {i}).unop
[PROOFSTEP]
simp only [Opposite.unop_op, mem_singleton]
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
⊢ Function.Injective fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }
[PROOFSTEP]
intro i i'
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
have subi : ({ i } : Finset ι) ⊆ { i, i' } := by simp
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
⊢ {i} ⊆ {i, i'}
[PROOFSTEP]
simp
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
have subi' : ({ i' } : Finset ι) ⊆ { i, i' } := by simp
[GOAL]
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
⊢ {i'} ⊆ {i, i'}
[PROOFSTEP]
simp
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
rw [← Finset.le_iff_subset] at subi subi'
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i =
      (fun i => ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) }) i' →
    i = i'
[PROOFSTEP]
simp only
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) } =
      ↑(u (Opposite.op {i'})) { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
[PROOFSTEP]
rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
⊢ ↑((hallMatchingsFunctor t).map (homOfLE subi).op (u (Opposite.op {i, i'}))) { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'})))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
[PROOFSTEP]
let uii' := u (Opposite.op ({ i, i' } : Finset ι))
[GOAL]
case mp.intro.refine'_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i i' : ι
subi : {i} ≤ {i, i'}
subi' : {i'} ≤ {i, i'}
uii' : (hallMatchingsFunctor t).obj (Opposite.op {i, i'}) := u (Opposite.op {i, i'})
⊢ ↑((hallMatchingsFunctor t).map (homOfLE subi).op (u (Opposite.op {i, i'}))) { val := i, property := (_ : i ∈ {i}) } =
      ↑((hallMatchingsFunctor t).map (homOfLE subi').op (u (Opposite.op {i, i'})))
        { val := i', property := (_ : i' ∈ {i'}) } →
    i = i'
[PROOFSTEP]
exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
[GOAL]
case mp.intro.refine'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
⊢ ∀ (x : ι), ↑(u (Opposite.op {x})) { val := x, property := (_ : x ∈ {x}) } ∈ t x
[PROOFSTEP]
intro i
[GOAL]
case mp.intro.refine'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ Functor.sections (hallMatchingsFunctor t)
i : ι
⊢ ↑(u (Opposite.op {i})) { val := i, property := (_ : i ∈ {i}) } ∈ t i
[PROOFSTEP]
apply (u (Opposite.op ({ i } : Finset ι))).property.2
[GOAL]
case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
[PROOFSTEP]
rintro ⟨f, hf₁, hf₂⟩ s
[GOAL]
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ card s ≤ card (Finset.biUnion s t)
[PROOFSTEP]
rw [← Finset.card_image_of_injective s hf₁]
[GOAL]
case mpr.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ card (image f s) ≤ card (Finset.biUnion s t)
[PROOFSTEP]
apply Finset.card_le_of_subset
[GOAL]
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ image f s ⊆ Finset.biUnion s t
[PROOFSTEP]
intro
[GOAL]
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ a✝ ∈ image f s → a✝ ∈ Finset.biUnion s t
[PROOFSTEP]
rw [Finset.mem_image, Finset.mem_biUnion]
[GOAL]
case mpr.intro.intro.a
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a✝ : α
⊢ (∃ a, a ∈ s ∧ f a = a✝) → ∃ a, a ∈ s ∧ a✝ ∈ t a
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case mpr.intro.intro.a.intro.intro
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a, a ∈ s ∧ f x ∈ t a
[PROOFSTEP]
exact ⟨x, hx, hf₂ x⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
⊢ Fintype ↑(Rel.image r ↑A)
[PROOFSTEP]
have h : Rel.image r A = (A.biUnion fun a => (Rel.image r { a }).toFinset : Set β) :=
  by
  ext
    -- Porting note: added `Set.mem_toFinset`
  simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
⊢ Rel.image r ↑A = ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
[PROOFSTEP]
ext
  -- Porting note: added `Set.mem_toFinset`
[GOAL]
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
x✝ : β
⊢ x✝ ∈ Rel.image r ↑A ↔ x✝ ∈ ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
[PROOFSTEP]
simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
h : Rel.image r ↑A = ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
⊢ Fintype ↑(Rel.image r ↑A)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
A : Finset α
h : Rel.image r ↑A = ↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
⊢ Fintype ↑↑(Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))
[PROOFSTEP]
apply FinsetCoe.fintype
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
let r' a := (Rel.image r { a }).toFinset
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h : ∀ A : Finset α, Fintype.card (Rel.image r A) = (A.biUnion r').card :=
  by
  intro A
  rw [← Set.toFinset_card]
  apply congr_arg
  ext b
  simp [Rel.image, (Set.mem_toFinset)]
    -- Porting note: added `Set.mem_toFinset`
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
⊢ ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
[PROOFSTEP]
intro A
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
⊢ card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
[PROOFSTEP]
rw [← Set.toFinset_card]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
⊢ Finset.card (Set.toFinset (Rel.image r ↑A)) = Finset.card (Finset.biUnion A r')
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
⊢ Set.toFinset (Rel.image r ↑A) = Finset.biUnion A r'
[PROOFSTEP]
ext b
[GOAL]
case h.a
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
A : Finset α
b : β
⊢ b ∈ Set.toFinset (Rel.image r ↑A) ↔ b ∈ Finset.biUnion A r'
[PROOFSTEP]
simp [Rel.image, (Set.mem_toFinset)]
  -- Porting note: added `Set.mem_toFinset`
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
[PROOFSTEP]
simp [Rel.image, (Set.mem_toFinset)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
simp only [h, h']
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq β
r : α → β → Prop
inst✝ : (a : α) → Fintype ↑(Rel.image r {a})
r' : α → Finset β := fun a => Set.toFinset (Rel.image r {a})
h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = Finset.card (Finset.biUnion A r')
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (Finset.biUnion A fun a => Set.toFinset (Rel.image r {a}))) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ Set.toFinset (Rel.image r {x})
[PROOFSTEP]
apply Finset.all_card_le_biUnion_card_iff_exists_injective
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
haveI := Classical.decEq β
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
let r' a := univ.filter fun b => r a b
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h : ∀ A : Finset α, (univ.filter fun b : β => ∃ a ∈ A, r a b) = A.biUnion r' :=
  by
  intro A
  ext b
  simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
⊢ ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
[PROOFSTEP]
intro A
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
⊢ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
[PROOFSTEP]
ext b
[GOAL]
case a
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
A : Finset α
b : β
⊢ b ∈ filter (fun b => ∃ a, a ∈ A ∧ r a b) univ ↔ b ∈ Finset.biUnion A r'
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (filter (fun b => ∃ a, a ∈ A ∧ r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
[PROOFSTEP]
simp_rw [h, h']
[GOAL]
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
this : DecidableEq β
r' : α → Finset β := fun a => filter (fun b => r a b) univ
h : ∀ (A : Finset α), filter (fun b => ∃ a, a ∈ A ∧ r a b) univ = Finset.biUnion A r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), Finset.card A ≤ Finset.card (Finset.biUnion A fun a => filter (fun b => r a b) univ)) ↔
    ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ filter (fun b => r x b) univ
[PROOFSTEP]
apply Finset.all_card_le_biUnion_card_iff_exists_injective


[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v : V
⊢ partOfVertex P v ∈ P.parts
[PROOFSTEP]
obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1
[GOAL]
case intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
h : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
⊢ partOfVertex P v ∈ P.parts
[PROOFSTEP]
exact h
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v : V
⊢ v ∈ partOfVertex P v
[PROOFSTEP]
obtain ⟨⟨h1, h2⟩, _h3⟩ := (P.isPartition.2 v).choose_spec
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
_h3 : ∀ (y : Set V), (fun b => ∃! x, v ∈ b) y → y = Exists.choose (_ : ∃! b x, v ∈ b)
h1 : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
h2 :
  (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) h1 ∧
    ∀ (y : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts), (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) y → y = h1
⊢ v ∈ partOfVertex P v
[PROOFSTEP]
exact h2.1
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
⊢ partOfVertex P v ≠ partOfVertex P w
[PROOFSTEP]
intro hn
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
⊢ False
[PROOFSTEP]
have hw := P.mem_partOfVertex w
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P w
⊢ False
[PROOFSTEP]
rw [← hn] at hw
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P v
⊢ False
[PROOFSTEP]
exact P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v✝ w✝ : V
hvw : Adj G v✝ w✝
⊢ (fun v => { val := partOfVertex P v, property := (_ : partOfVertex P v ∈ P.parts) }) v✝ ≠
    (fun v => { val := partOfVertex P v, property := (_ : partOfVertex P v ∈ P.parts) }) w✝
[PROOFSTEP]
rw [Ne.def, Subtype.mk_eq_mk]
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v✝ w✝ : V
hvw : Adj G v✝ w✝
⊢ ¬partOfVertex P v✝ = partOfVertex P w✝
[PROOFSTEP]
exact P.partOfVertex_ne_of_adj hvw
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
⊢ ∀ (s : Set V), s ∈ colorClasses C → IsAntichain G.Adj s
[PROOFSTEP]
rintro s ⟨c, rfl⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
c : V
⊢ IsAntichain G.Adj {x | Setoid.Rel (Setoid.ker ↑C) x c}
[PROOFSTEP]
apply C.color_classes_independent
[GOAL]
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n ↔ Colorable G n
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n → Colorable G n
[PROOFSTEP]
rintro ⟨P, hf, hc⟩
[GOAL]
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
⊢ Colorable G n
[PROOFSTEP]
have : Fintype P.parts := hf.fintype
[GOAL]
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
this : Fintype ↑P.parts
⊢ Colorable G n
[PROOFSTEP]
rw [Set.Finite.card_toFinset hf] at hc
[GOAL]
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ Colorable G n
[PROOFSTEP]
apply P.to_colorable.mono hc
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Colorable G n → Partitionable G n
[PROOFSTEP]
rintro ⟨C⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Partitionable G n
[PROOFSTEP]
refine' ⟨C.toPartition, C.colorClasses_finite, le_trans _ (Fintype.card_fin n).le⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Finset.card (Set.Finite.toFinset (_ : Set.Finite (Coloring.colorClasses C))) ≤ Fintype.card (Fin n)
[PROOFSTEP]
generalize_proofs h
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
[PROOFSTEP]
haveI : Fintype C.colorClasses := C.colorClasses_finite.fintype
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
[PROOFSTEP]
rw [h.card_toFinset]
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Fintype.card ↑(Coloring.colorClasses C) ≤ Fintype.card (Fin n)
[PROOFSTEP]
exact C.card_colorClasses_le