Theorem: Matroid.map_cl_eq (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
Tactic:
clear X
State after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
Tactic:
intro X hX
State after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
hX : X ⊆ f '' M.E
⊢ (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
hX : X ⊆ f '' M.E
⊢ (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
Tactic:
obtain ⟨I, hI⟩ := (M.map f hf).exists_basis X
State after:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
hX : X ⊆ f '' M.E
I : Set β
hI : (M.map f hf).Basis I X
⊢ (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)

State before:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
hX : X ⊆ f '' M.E
I : Set β
hI : (M.map f hf).Basis I X
⊢ (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
Tactic:
obtain ⟨I, X, hI', rfl, rfl⟩ := (map_basis_iff').1 hI
State after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
⊢ (M.map f hf).cl (f '' X) = f '' M.cl (f ⁻¹' (f '' X))

State before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
⊢ (M.map f hf).cl (f '' X) = f '' M.cl (f ⁻¹' (f '' X))
Tactic:
rw [eq_comm, ← cl_inter_ground, hf.preimage_image_inter hI'.subset_ground,
  ← hI.cl_eq_cl, ← hI'.cl_eq_cl]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
⊢ f '' M.cl I = (M.map f hf).cl (f '' I)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
⊢ f '' M.cl I = (M.map f hf).cl (f '' I)
Tactic:
ext e
State after:
case intro.intro.intro.intro.intro.h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : β
⊢ e ∈ f '' M.cl I ↔ e ∈ (M.map f hf).cl (f '' I)

State before:
case intro.intro.intro.intro.intro.h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : β
⊢ e ∈ f '' M.cl I ↔ e ∈ (M.map f hf).cl (f '' I)
Tactic:
simp only [mem_image, hI.indep.mem_cl_iff', map_ground, map_indep_iff, forall_exists_index,
  and_imp, hI'.indep.mem_cl_iff']
State after:
case intro.intro.intro.intro.intro.h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
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

State before:
case intro.intro.intro.intro.intro.h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
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:
refine ⟨?_, ?_⟩
State after:
case intro.intro.intro.intro.intro.h.refine_1
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
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

case intro.intro.intro.intro.intro.h.refine_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' 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) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

State before:
case intro.intro.intro.intro.intro.h.refine_1
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
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

case intro.intro.intro.intro.intro.h.refine_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' 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) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
Tactic:
. rintro ⟨e, ⟨heE, hind⟩, rfl⟩
  refine ⟨⟨e, heE, rfl⟩, fun J hJ hins ↦ ⟨e, hind ?_, rfl⟩⟩
  rw [← image_insert_eq,
    hf.image_eq_image_iff (insert_subset heE hI'.indep.subset_ground) hJ.subset_ground] at hins
  rwa [hins]
State after:
case intro.intro.intro.intro.intro.h.refine_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' 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) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

State before:
case intro.intro.intro.intro.intro.h.refine_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' 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) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e
Tactic:
rintro ⟨⟨x, hx, rfl⟩, h⟩
State after:
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ x_1, (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x

State before:
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ x_1, (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x
Tactic:
refine ⟨x, ⟨hx, fun hind ↦ ?_⟩, rfl⟩
State after:
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
⊢ x ∈ I

State before:
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
⊢ x ∈ I
Tactic:
obtain ⟨x', hx', h_eq⟩ := h _ hind (by rw [image_insert_eq])
State after:
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
x' : α
hx' : x' ∈ I
h_eq : f x' = f x
⊢ x ∈ I

State before:
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
x' : α
hx' : x' ∈ I
h_eq : f x' = f x
⊢ x ∈ I
Tactic:
rwa [← hf (hI'.indep.subset_ground hx') hx h_eq]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
Tactic:
convert h' (X ∩ f '' M.E) inter_subset_right using 1
State after:
case h.e'_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ (M.map f hf).cl X = (M.map f hf).cl (X ∩ f '' M.E)

case h.e'_3
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ f '' M.cl (f ⁻¹' X) = f '' M.cl (f ⁻¹' (X ∩ f '' M.E))

State before:
case h.e'_3
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ f '' M.cl (f ⁻¹' X) = f '' M.cl (f ⁻¹' (X ∩ f '' M.E))
Tactic:
rw [preimage_inter, eq_comm, ← cl_inter_ground, inter_assoc, hf.preimage_image_inter Subset.rfl,
  cl_inter_ground]
State after:
no goals

State before:
case h.e'_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ (M.map f hf).cl X = (M.map f hf).cl (X ∩ f '' M.E)
Tactic:
rw [← cl_inter_ground]
State after:
case h.e'_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ (M.map f hf).cl (X ∩ (M.map f hf).E) = (M.map f hf).cl (X ∩ f '' M.E)

State before:
case h.e'_2
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ (M.map f hf).cl (X ∩ (M.map f hf).E) = (M.map f hf).cl (X ∩ f '' M.E)
Tactic:
rfl
State after:
no goals

State before:
case intro.intro.intro.intro.intro.h.refine_1
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
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 ⟨e, ⟨heE, hind⟩, rfl⟩
State after:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
⊢ (∃ x ∈ M.E, f x = f e) ∧ ∀ (x : Set α), M.Indep x → insert (f e) (f '' I) = f '' x → ∃ x ∈ I, f x = f e

State before:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
⊢ (∃ x ∈ M.E, f x = f e) ∧ ∀ (x : Set α), M.Indep x → insert (f e) (f '' I) = f '' x → ∃ x ∈ I, f x = f e
Tactic:
refine ⟨⟨e, heE, rfl⟩, fun J hJ hins ↦ ⟨e, hind ?_, rfl⟩⟩
State after:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ M.Indep (insert e I)

State before:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ M.Indep (insert e I)
Tactic:
rw [← image_insert_eq,
  hf.image_eq_image_iff (insert_subset heE hI'.indep.subset_ground) hJ.subset_ground] at hins
State after:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ M.Indep (insert e I)

State before:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ M.Indep (insert e I)
Tactic:
rwa [hins]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
⊢ insert (f x) (f '' I) = f '' insert x I
Tactic:
rw [image_insert_eq]
State after:
no goals