Theorem: Matroid.Nonloop.point_count_contract_eq (Matroid/Points.lean)

State before:
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ sorryAx ℕ∞ true = {L | M.Line L ∧ e ∈ L}.encard
Tactic:
rw [point_count_eq_num_points]
State after:
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ {P | ?m.6317.Point P}.encard = {L | M.Line L ∧ e ∈ L}.encard

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314

State before:
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ {P | ?m.6317.Point P}.encard = {L | M.Line L ∧ e ∈ L}.encard

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Tactic:
apply encard_congr
State after:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ ↑{P | ?m.6317.Point P} ≃ ↑{L | M.Line L ∧ e ∈ L}

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314

State before:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ ↑{P | ?m.6317.Point P} ≃ ↑{L | M.Line L ∧ e ∈ L}

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Tactic:
simp only [coe_setOf]
State after:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ { P // ?m.6317.Point P } ≃ { L // M.Line L ∧ e ∈ L }

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314

State before:
case e
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ { P // ?m.6317.Point P } ≃ { L // M.Line L ∧ e ∈ L }

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Matroid ?m.6315

α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ Type ?u.6314
Tactic:
convert he.contract_flat_equiv 1 using 2
State after:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ (fun L => M.Line L ∧ e ∈ L) = fun F => M.Flat F ∧ M.er F = ↑1 + 1 ∧ e ∈ F

State before:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ (fun L => M.Line L ∧ e ∈ L) = fun F => M.Flat F ∧ M.er F = ↑1 + 1 ∧ e ∈ F
Tactic:
ext L
State after:
case h.e'_2.h.e'_2.h.a
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
L : Set α
⊢ M.Line L ∧ e ∈ L ↔ M.Flat L ∧ M.er L = ↑1 + 1 ∧ e ∈ L

State before:
case h.e'_2.h.e'_2.h.a
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
L : Set α
⊢ M.Line L ∧ e ∈ L ↔ M.Flat L ∧ M.er L = ↑1 + 1 ∧ e ∈ L
Tactic:
simp [Line, and_assoc, one_add_one_eq_two]
State after:
no goals