internlm/Lean-Github huggingface dataset:
Theorem: Matroid.map_base_iff
Proof state before:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : f '' B₀ ⊆ f '' I
⊢ f '' B₀ = f '' I
Tactic:
rw [hf.image_subset_image_iff hB.subset_ground hI'.subset_ground] at hB₀I
Proof state after:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : B₀ ⊆ I
⊢ f '' B₀ = f '' I
Theorem: Matroid.map_base_iff
Proof state before:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : B₀ ⊆ I
⊢ f '' B₀ = f '' I
Tactic:
rw [hB.eq_of_subset_indep hI' hB₀I]
Proof state after:
no goals
Theorem: Matroid.map_base_iff
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
x✝ : (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
h : ∃ I₀, M.Indep I₀ ∧ B = f '' I₀
hB : ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
⊢ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
Tactic:
obtain ⟨B₀, hB₀, rfl⟩ := h
Proof state after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
⊢ ∃ B₀_1, M.Base B₀_1 ∧ f '' B₀ = f '' B₀_1
Theorem: Matroid.map_base_iff
Proof state before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
⊢ ∃ B₀_1, M.Base B₀_1 ∧ f '' B₀ = f '' B₀_1
Tactic:
refine ⟨_, hB₀.base_of_maximal fun J hJ hB₀J ↦ ?_, rfl⟩
Proof state after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J
Theorem: Matroid.map_base_iff
Proof state before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J
Tactic:
specialize hB (f '' J) ((map_image_indep_iff hJ.subset_ground).2 hJ) (image_subset _ hB₀J)
Proof state after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
hB : f '' B₀ = f '' J
⊢ B₀ = J
Theorem: Matroid.map_base_iff
Proof state before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
hB : f '' B₀ = f '' J
⊢ B₀ = J
Tactic:
rwa [hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground] at hB
Proof state after:
no goals
Theorem: Matroid.Base.map
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Base (f '' B)
Tactic:
rw [map_base_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
Theorem: Matroid.Base.map
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
Tactic:
exact ⟨B, hB, rfl⟩
Proof state after:
no goals
Theorem: Matroid.map_dep_iff
Proof 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]
Proof 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₀
Theorem: Matroid.map_dep_iff
Proof 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
Proof 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
Theorem: Matroid.map_dep_iff
Proof 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⟩
Proof 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₀
Theorem: Matroid.map_dep_iff
Proof 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⟩⟩
Proof 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
Theorem: Matroid.map_dep_iff
Proof 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
Proof 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
Theorem: Matroid.map_dep_iff
Proof 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
Proof 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
Theorem: Matroid.map_dep_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.map_dep_iff
Proof 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⟩
Proof 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
Theorem: Matroid.map_dep_iff
Proof 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⟩
Proof state after:
no goals
Theorem: Matroid.map_image_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.map f hf).Base (f '' B) ↔ M.Base B
Tactic:
rw [map_base_iff]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀) ↔ M.Base B
Theorem: Matroid.map_image_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀) ↔ M.Base B
Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : f '' B = f '' J
⊢ M.Base B
Theorem: Matroid.map_image_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : f '' B = f '' J
⊢ M.Base B
Tactic:
rw [hf.image_eq_image_iff hB hJ.subset_ground] at hIJ
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : B = J
⊢ M.Base B
Theorem: Matroid.map_image_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : B = J
⊢ M.Base B
Tactic:
rwa [hIJ]
Proof state after:
no goals
Theorem: Matroid.Basis.map
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Basis (f '' I) (f '' X)
Tactic:
refine (hIX.indep.map f hf).basis_of_forall_insert (image_subset _ hIX.subset) ?_
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
⊢ ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))
Theorem: Matroid.Basis.map
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
⊢ ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))
Tactic:
rintro _ ⟨⟨e,he,rfl⟩, he'⟩
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
Tactic:
have hss := insert_subset (hIX.subset_ground he) hIX.indep.subset_ground
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))
Tactic:
rw [← not_indep_iff (by simpa [← image_insert_eq] using image_subset f hss)]
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))
Tactic:
simp only [map_indep_iff, not_exists, not_and]
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x
Tactic:
intro J hJ hins
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ False
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ False
Tactic:
rw [← image_insert_eq, hf.image_eq_image_iff hss hJ.subset_ground] at hins
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ False
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ False
Tactic:
obtain rfl := hins
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
hJ : M.Indep (insert e I)
⊢ False
Theorem: Matroid.Basis.map
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
hJ : M.Indep (insert e I)
⊢ False
Tactic:
exact he' (mem_image_of_mem f (hIX.mem_of_insert_indep he hJ))
Proof state after:
no goals
Theorem: Matroid.Basis.map
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ insert (f e) (f '' I) ⊆ (M.map f hf).E
Tactic:
simpa [← image_insert_eq] using image_subset f hss
Proof state after:
no goals
Theorem: Matroid.map_basis_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
⊢ (M.map f hf).Basis (f '' I) (f '' X) ↔ M.Basis I X
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map hf⟩
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
⊢ M.Basis I X
Theorem: Matroid.map_basis_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
⊢ M.Basis I X
Tactic:
obtain ⟨I', hI', hII'⟩ := map_indep_iff.1 h.indep
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.Basis I X
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.Basis I X
Tactic:
rw [hf.image_eq_image_iff hI hI'.subset_ground] at hII'
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.Basis I X
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.Basis I X
Tactic:
obtain rfl := hII'
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.Basis I X
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.Basis I X
Tactic:
have hss := (hf.image_subset_image_iff hI hX).1 h.subset
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.Basis I X
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.Basis I X
Tactic:
refine hI'.basis_of_maximal_subset hss (fun J hJ hIJ hJX ↦ ?_)
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ J ⊆ I
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ J ⊆ I
Tactic:
have hIJ' := h.eq_of_subset_indep (hJ.map f hf) (image_subset f hIJ) (image_subset f hJX)
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : f '' I = f '' J
⊢ J ⊆ I
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : f '' I = f '' J
⊢ J ⊆ I
Tactic:
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ'
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : I = J
⊢ J ⊆ I
Theorem: Matroid.map_basis_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).Basis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : I = J
⊢ J ⊆ I
Tactic:
exact hIJ'.symm.subset
Proof state after:
no goals
Theorem: Matroid.map_basis_iff'
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (M.map f hf).Basis I X ↔ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).Basis I X
Theorem: Matroid.map_basis_iff'
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).Basis I X
Tactic:
rintro ⟨I, X, hIX, rfl, rfl⟩
Proof state after:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I X : Set α
hIX : M.Basis I X
⊢ (M.map f hf).Basis (f '' I) (f '' X)