Theorem: Matroid.map_dep_iff (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ (M.map f hf).Dep D ↔ ∃ D₀, M.Dep D₀ ∧ D = f '' D₀
Tactic:
simp only [Dep, map_indep_iff, not_exists, not_and, map_ground, subset_image_iff]
State after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔ ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔ ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) → ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀

case mpr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ (∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀) → (∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D

State before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ (∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀) → (∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D
Tactic:
rintro ⟨D₀, ⟨hD₀, hD₀E⟩, rfl⟩
State after:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀

State before:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀
Tactic:
refine ⟨fun I hI h_eq ↦ ?_, ⟨_, hD₀E, rfl⟩⟩
State after:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ False

State before:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ False
Tactic:
rw [hf.image_eq_image_iff hD₀E hI.subset_ground] at h_eq
State after:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : D₀ = I
⊢ False

State before:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : D₀ = I
⊢ False
Tactic:
subst h_eq
State after:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
hI : M.Indep D₀
⊢ False

State before:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
hI : M.Indep D₀
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case mp
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) → ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
Tactic:
rintro ⟨h, D₀, hD₀E, rfl⟩
State after:
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀E : D₀ ⊆ M.E
h : ∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x
⊢ ∃ D₀_1, (¬M.Indep D₀_1 ∧ D₀_1 ⊆ M.E) ∧ f '' D₀ = f '' D₀_1

State before:
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀E : D₀ ⊆ M.E
h : ∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x
⊢ ∃ D₀_1, (¬M.Indep D₀_1 ∧ D₀_1 ⊆ M.E) ∧ f '' D₀ = f '' D₀_1
Tactic:
exact ⟨D₀, ⟨fun hd ↦ h _ hd rfl, hD₀E⟩, rfl⟩
State after:
no goals