internlm/Lean-Github huggingface dataset:
Theorem: Matroid.comap_cl_eq
Proof state before:
case 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
obtain (hxE | hxE) := em' (f x ∈ M.E)
Proof state after:
case intro.intro.intro.h.inl
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∉ M.E
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)

case intro.intro.intro.h.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
obtain (hxI | hxI) := em (x ∈ I)
Proof state after:
case intro.intro.intro.h.inr.inl
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∈ I
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)

case intro.intro.intro.h.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
have hss : insert x I ⊆ (M.comap f).E := insert_subset hxE hI.indep.subset_ground
Proof state after:
case intro.intro.intro.h.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
rw [hI.indep.mem_cl_iff_of_not_mem hxI, ← not_indep_iff hss, comap_indep_iff,
  injOn_insert hxI, not_and, not_and, not_not, iff_true_intro hIinj, true_imp_iff]
Proof state after:
case intro.intro.intro.h.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
obtain (hxI' | hxI') := em (f x ∈ f '' I)
Proof state after:
case intro.intro.intro.h.inr.inr.inl
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
hxI' : f x ∈ f '' I
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)

case intro.intro.intro.h.inr.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
hxI' : f x ∉ f '' I
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr.inr.inr
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
hxI' : f x ∉ f '' I
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
rw [iff_false_intro hxI', imp_false, mem_preimage, image_insert_eq,
  hI'.indep.insert_indep_iff_of_not_mem hxI', mem_diff, and_iff_right hxE, not_not, hI'.cl_eq_cl]
Proof state after:
no goals
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inl
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∉ M.E
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
apply iff_of_false <;> exact (fun h ↦ hxE (by simpa using mem_ground_of_mem_cl h))
Proof state after:
no goals
Theorem: Matroid.comap_cl_eq
Proof 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∉ M.E
h : x ∈ f ⁻¹' M.cl (f '' X)
⊢ f x ∈ M.E
Tactic:
simpa using mem_ground_of_mem_cl h
Proof state after:
no goals
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr.inl
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∈ I
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
exact iff_of_true (mem_cl_of_mem _ hxI hI.indep.subset_ground)
  (mem_cl_of_mem' _ (mem_image_of_mem f (hI.subset hxI))
    (hI'.indep.subset_ground (mem_image_of_mem f hxI)))
Proof state after:
no goals
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro.h.inr.inr.inl
α : 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
hxI' : f x ∈ f '' I
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)
Tactic:
simp [hxI', hxE, mem_cl_of_mem' _ (hI'.subset hxI') hxE]
Proof state after:
no goals
Theorem: Matroid.map_cl_eq
Proof 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
Proof 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)
Theorem: Matroid.map_cl_eq
Proof 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
Proof 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)
Theorem: Matroid.map_cl_eq
Proof 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
Proof 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)
Theorem: Matroid.map_cl_eq
Proof 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
Proof 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))
Theorem: Matroid.map_cl_eq
Proof 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]
Proof 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)
Theorem: Matroid.map_cl_eq
Proof 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
Proof 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)
Theorem: Matroid.map_cl_eq
Proof 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']
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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 ⟨?_, ?_⟩
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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]
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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⟩
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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⟩
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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])
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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]
Proof state after:
no goals
Theorem: Matroid.map_cl_eq
Proof 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
Proof 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))
Theorem: Matroid.map_cl_eq
Proof 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]
Proof state after:
no goals
Theorem: Matroid.map_cl_eq
Proof 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]
Proof 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)
Theorem: Matroid.map_cl_eq
Proof 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
Proof state after:
no goals
Theorem: Matroid.map_cl_eq
Proof 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⟩
Proof 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
Theorem: Matroid.map_cl_eq
Proof 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⟩⟩
Proof 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)