Theorem: Matroid.encard_ground_eq_sum_encard_lines_through (Matroid/Old/Kung.lean)

State before:
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ M.E.encard = 1 + ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
Tactic:
rw [← encard_diff_add_encard_of_subset (singleton_subset_iff.2 he), add_comm, encard_singleton]
State after:
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ 1 + (M.E \ {e}).encard = 1 + ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard

State before:
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
Tactic:
convert (ENat.tsum_encard_eq_encard_sUnion (M ／ e).parallelClasses.pairwiseDisjoint).symm using 1
State after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = (⋃₀ ↑(M ／ e).parallelClasses).encard

case h.e'_3
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard = ∑' (t : ↑↑(M ／ e).parallelClasses), (↑t).encard

State before:
case h.e'_3
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard = ∑' (t : ↑↑(M ／ e).parallelClasses), (↑t).encard
Tactic:
convert ENat.tsum_comp_eq_tsum_of_equiv (M ／ e).parallelPointEquiv.symm (g := fun x ↦ x.1.encard)
  using 1
State after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard

State before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
Tactic:
rw [← ENat.tsum_comp_eq_tsum_of_equiv (toNonloop he).lineContractPointEquiv]
State after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (x : { P // (M ／ e).Point P }), (↑(⋯.lineContractPointEquiv x) \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard

State before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (x : { P // (M ／ e).Point P }), (↑(⋯.lineContractPointEquiv x) \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
Tactic:
refine tsum_congr (fun ⟨P,hP⟩ ↦ ?_)
State after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
x✝ : { P // (M ／ e).Point P }
P : Set α
hP : (M ／ e).Point P
⊢ (↑(⋯.lineContractPointEquiv ⟨P, hP⟩) \ {e}).encard = (↑((M ／ e).parallelPointEquiv.symm ⟨P, hP⟩)).encard

State before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
x✝ : { P // (M ／ e).Point P }
P : Set α
hP : (M ／ e).Point P
⊢ (↑(⋯.lineContractPointEquiv ⟨P, hP⟩) \ {e}).encard = (↑((M ／ e).parallelPointEquiv.symm ⟨P, hP⟩)).encard
Tactic:
simp [Nonloop.lineContractPointEquiv, cl_singleton_eq he,
  diff_singleton_eq_self (fun heP ↦ (hP.subset_ground heP).2 rfl)]
State after:
no goals

State before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = (⋃₀ ↑(M ／ e).parallelClasses).encard
Tactic:
simp only [contract_elem, Partition.sUnion_eq, contract_nonloop_iff, mem_diff]
State after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = {e_1 | e_1 ∈ M.E ∧ e_1 ∉ M.cl {e}}.encard

State before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = {e_1 | e_1 ∈ M.E ∧ e_1 ∉ M.cl {e}}.encard
Tactic:
congr
State after:
case h.e'_2.e_s.e_a
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ {e} = M.cl {e}

State before:
case h.e'_2.e_s.e_a
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ {e} = M.cl {e}
Tactic:
rw [cl_singleton_eq]
State after:
no goals