Theorem: Matroid.comap_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 : α → β
X : Set α
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Tactic:
obtain ⟨I, hI⟩ := (M.comap f).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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
⊢ (M.comap f).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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Tactic:
obtain ⟨hI', -, hIinj⟩ := comap_basis'_iff.1 hI
State after:
case 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)

State before:
case 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Tactic:
rw [← hI.cl_eq_cl]
State after:
case 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl I = f ⁻¹' M.cl (f '' X)

State before:
case 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 : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl I = f ⁻¹' M.cl (f '' X)
Tactic:
ext x
State after:
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)

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)
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)

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)
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)

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
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)

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]
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)

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)
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)

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]
State after:
no goals

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))
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 : α → β
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
State after:
no goals

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)))
State after:
no goals

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]
State after:
no goals