Theorem: Matroid.flat_map_iff (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ (M.map f hf).Flat F ↔ ∃ F₀, M.Flat F₀ ∧ F = f '' F₀
Tactic:
simp only [flat_iff_cl_self, map_cl_eq]
State after:
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ f '' M.cl (f ⁻¹' F) = F ↔ ∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀

State before:
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ f '' M.cl (f ⁻¹' F) = F ↔ ∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀
Tactic:
refine ⟨fun h ↦ ⟨M.cl (f ⁻¹' F), by simp, h.symm⟩, ?_⟩
State after:
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ (∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀) → f '' M.cl (f ⁻¹' F) = F

State before:
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
⊢ (∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀) → f '' M.cl (f ⁻¹' F) = F
Tactic:
rintro ⟨F, hF, rfl⟩
State after:
case intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ f '' M.cl (f ⁻¹' (f '' F)) = f '' F

State before:
case intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ f '' M.cl (f ⁻¹' (f '' F)) = f '' F
Tactic:
rw [← cl_inter_ground, hf.preimage_image_inter, hF]
State after:
case intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ F ⊆ M.E

State before:
case intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ F ⊆ M.E
Tactic:
exact hF.symm.subset.trans <| M.cl_subset_ground _
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set β
h : f '' M.cl (f ⁻¹' F) = F
⊢ M.cl (M.cl (f ⁻¹' F)) = M.cl (f ⁻¹' F)
Tactic:
simp
State after:
no goals