Theorem: Matroid.IsoMinor.exists_iso (Matroid/Minor/Iso.lean)

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
⊢ ∃ M₀, ∃ (hM₀ : M₀ ≤m M), ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
obtain ⟨M₀, hM₀, hE, h⟩ := i.exists_minor
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ M₀, ∃ (hM₀ : M₀ ≤m M), ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ M₀, ∃ (hM₀ : M₀ ≤m M), ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
refine ⟨M₀, hM₀,  ?_⟩
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
let e := Equiv.ofInjective _ (Subtype.val_injective.comp (EmbeddingLike.injective i))
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
exact ⟨Iso.mk (e.trans (Equiv.setCongr (by simp [hE, range_comp])))
  fun _ ↦ by simp [h, image_image, e], fun ⟨x,hx⟩ ↦ rfl⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ range (val ∘ ⇑i) = M₀.E
Tactic:
simp [hE, range_comp]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
x✝ : Set ↑N.E
⊢ N.Indep ↑x✝ ↔ M₀.Indep ↑(⇑(e.trans (Equiv.setCongr ⋯)) '' x✝)
Tactic:
simp [h, image_image, e]
State after:
no goals