Theorem: Matroid.minor_loopyOn_iff (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M ≤m loopyOn E ↔ M = loopyOn M.E ∧ M.E ⊆ E
Tactic:
refine ⟨fun h ↦ ⟨by obtain ⟨C, D, _, _, _, rfl⟩ := h; simp, h.subset⟩, fun ⟨h, hss⟩ ↦ ?_⟩
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M ≤m loopyOn E

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M ≤m loopyOn E
Tactic:
convert (loopyOn E).restrict_minor hss using 1
State after:
case h.e'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M = loopyOn E ↾ M.E

State before:
case h.e'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M = loopyOn E ↾ M.E
Tactic:
rw [h, loopyOn_ground, loopyOn_restrict]
State after:
no goals

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ≤m loopyOn E
⊢ M = loopyOn M.E
Tactic:
obtain ⟨C, D, _, _, _, rfl⟩ := h
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E C D : Set α
left✝² : C ⊆ (loopyOn E).E
left✝¹ : D ⊆ (loopyOn E).E
left✝ : Disjoint C D
⊢ loopyOn E ／ C ＼ D = loopyOn (loopyOn E ／ C ＼ D).E

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E C D : Set α
left✝² : C ⊆ (loopyOn E).E
left✝¹ : D ⊆ (loopyOn E).E
left✝ : Disjoint C D
⊢ loopyOn E ／ C ＼ D = loopyOn (loopyOn E ／ C ＼ D).E
Tactic:
simp
State after:
no goals