Theorem: Matroid.Iso.setOf_prop_eq (Matroid/Old/_Equiv.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
⊢ setOf PN = image ↑e.toPartialEquiv '' setOf PM
Tactic:
refine' Set.ext (fun Y ↦ ⟨fun h ↦ _, _⟩)
State after:
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ setOf PN
⊢ Y ∈ image ↑e.toPartialEquiv '' setOf PM

case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
⊢ Y ∈ image ↑e.toPartialEquiv '' setOf PM → Y ∈ setOf PN

State before:
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
⊢ Y ∈ image ↑e.toPartialEquiv '' setOf PM → Y ∈ setOf PN
Tactic:
intro h
State after:
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ image ↑e.toPartialEquiv '' setOf PM
⊢ Y ∈ setOf PN

State before:
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ image ↑e.toPartialEquiv '' setOf PM
⊢ Y ∈ setOf PN
Tactic:
obtain ⟨X, hX, rfl⟩ := h
State after:
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
X : Set α
hX : X ∈ setOf PM
⊢ ↑e.toPartialEquiv '' X ∈ setOf PN

State before:
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X✝ Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
X : Set α
hX : X ∈ setOf PM
⊢ ↑e.toPartialEquiv '' X ∈ setOf PN
Tactic:
exact hMN hX
State after:
no goals

State before:
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ setOf PN
⊢ Y ∈ image ↑e.toPartialEquiv '' setOf PM
Tactic:
refine' ⟨e.symm '' Y, hNM h, _⟩
State after:
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ setOf PN
⊢ ↑e.toPartialEquiv '' (↑e.symm.toPartialEquiv '' Y) = Y

State before:
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y✝ : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ setOf PN
⊢ ↑e.toPartialEquiv '' (↑e.symm.toPartialEquiv '' Y) = Y
Tactic:
rw [symm_apply, image_symm_image_of_subset_target _ ((hN h).trans_eq e.target_eq.symm)]
State after:
no goals