-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma map_closure_eq {β : Type*} (M : Matroid α) (f : α → β) (hf) (X : Set β) :
    (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Proof state:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJ : M.Indep J
hJI : insert (f x) (f '' I) = f '' J
⊢ M.Indep (insert x I)

Tactic:
replace hJ := hJ.map f hf

Result:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
⊢ M.Indep (insert x I)

Proof state:
case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ (∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
    (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e

Tactic:
rintro ⟨x, ⟨hxE, hxi⟩, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
⊢ (∃ x_1 ∈ M.E, f x_1 = f x) ∧ ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x

Proof state:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
⊢ (∃ x_1 ∈ M.E, f x_1 = f x) ∧ ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x

Tactic:
refine ⟨⟨x, hxE, rfl⟩, fun J hJ hJI ↦ ⟨x, hxi ?_, rfl⟩⟩

Result:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJ : M.Indep J
hJI : insert (f x) (f '' I) = f '' J
⊢ M.Indep (insert x I)

Proof state:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ e ∈ (M.map f hf).closure (f '' I) ↔ e ∈ f '' M.closure I

Tactic:
simp only [(hI.map f hf).mem_closure_iff', map_ground, mem_image, map_indep_iff,
  forall_exists_index, and_imp, hI.mem_closure_iff']

Result:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

Proof state:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
⊢ M.Indep (insert x I)

Tactic:
have hrw := image_insert_eq ▸ hJI

Result:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
hrw : f '' insert x I = f '' J
⊢ M.Indep (insert x I)

Proof state:
case mpr.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
hrw : f '' insert x I = f '' J
⊢ M.Indep (insert x I)

Tactic:
rwa [← hrw, map_image_indep_iff (insert_subset hxE hI.subset_ground)] at hJ

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I

Tactic:
refine fun I hI ↦ Set.ext fun e ↦ ?_

Result:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ e ∈ (M.map f hf).closure (f '' I) ↔ e ∈ f '' M.closure I

Proof state:
case mp.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
⊢ x ∈ I

Tactic:
obtain ⟨y, hyI, hfy⟩ := h2 _ hI' image_insert_eq.symm

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : f y = f x
⊢ x ∈ I

Proof state:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) ↔
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

Tactic:
constructor

Result:
case mp
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ (∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
    (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e

Proof state:
case intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
  ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
suffices aux : ∀ ⦃I⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' (M.closure I) by
  obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
  rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
    ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]

Result:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : f y = f x
⊢ x ∈ I

Tactic:
rw [hf.eq_iff (hI.subset_ground hyI) hxE] at hfy

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : y = x
⊢ x ∈ I