-- Mathlib/Data/Matroid/Map.lean
lemma map_comap {f : α → β} (h_range : N.E ⊆ range f) (hf : InjOn f (f ⁻¹' N.E)) :
    (N.comap f).map f hf = N

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : f '' I = f '' I₀
⊢ N.Indep (f '' I)

Tactic:
suffices h : I₀ ⊆ f ⁻¹' N.E by rw [InjOn.image_eq_image_iff hf hI h] at hII₀; rwa [hII₀]

Result:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : f '' I = f '' I₀
⊢ I₀ ⊆ f ⁻¹' N.E

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : f '' I = f '' I₀
h : I₀ ⊆ f ⁻¹' N.E
⊢ N.Indep (f '' I)

Tactic:
rw [InjOn.image_eq_image_iff hf hI h] at hII₀

Result:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : I = I₀
h : I₀ ⊆ f ⁻¹' N.E
⊢ N.Indep (f '' I)

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)

Tactic:
simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]

Result:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ t ⊆ f ⁻¹' N.E, (∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ((N.comap f).map f hf).E = N.E

Tactic:
simpa [image_preimage_eq_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : f '' I = f '' I₀
⊢ I₀ ⊆ f ⁻¹' N.E

Tactic:
exact (subset_preimage_image f I₀).trans <| preimage_mono (f := f) hI₀.subset_ground

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : I = I₀
h : I₀ ⊆ f ⁻¹' N.E
⊢ N.Indep (f '' I)

Tactic:
rwa [hII₀]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).map f hf = N

Tactic:
refine ext_indep (by simpa [image_preimage_eq_iff]) ?_

Result:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ t ⊆ f ⁻¹' N.E, (∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)

Tactic:
refine fun I hI ↦ ⟨fun ⟨I₀, ⟨hI₀, _⟩, hII₀⟩ ↦ ?_, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩

Result:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
I : Set α
hI : I ⊆ f ⁻¹' N.E
x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀
I₀ : Set α
hI₀ : N.Indep (f '' I₀)
right✝ : InjOn f I₀
hII₀ : f '' I = f '' I₀
⊢ N.Indep (f '' I)