internlm/Lean-Github huggingface dataset:
Theorem: Matroid.map_basis_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 β
hf : InjOn f M.E
I X : Set α
hIX : M.Basis I X
⊢ (M.map f hf).Basis (f '' I) (f '' X)
Tactic:
exact hIX.map hf
Proof state after:
no goals
Theorem: Matroid.map_basis_iff'
Proof state before:
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₀
Tactic:
obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground
Proof state after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ X = f '' X₀
Theorem: Matroid.map_basis_iff'
Proof state before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ X = f '' X₀
Tactic:
obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground
Proof state after:
case refine_1.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 : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) ((fun a => f a) '' X)
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
Theorem: Matroid.map_basis_iff'
Proof state before:
case refine_1.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 : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) ((fun a => f a) '' X)
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
Tactic:
rw [map_basis_iff _ _ hI hX] at h
Proof state after:
case refine_1.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 : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
Theorem: Matroid.map_basis_iff'
Proof state before:
case refine_1.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 : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
Tactic:
exact ⟨I, X, h, rfl, rfl⟩
Proof state after:
no goals
Theorem: Matroid.map_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
⊢ (M.map f hf)✶ = M✶.map f hf
Tactic:
apply eq_of_base_iff_base_forall (by simp)
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 β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.Base B ↔ (M✶.map f hf).Base B)
Theorem: Matroid.map_dual
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 β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.Base B ↔ (M✶.map f hf).Base B)
Tactic:
simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, dual_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
⊢ ∀ a ⊆ M.E, ((M.map f hf).Base (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).Base (f '' a)
Theorem: Matroid.map_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
⊢ ∀ a ⊆ M.E, ((M.map f hf).Base (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).Base (f '' a)
Tactic:
intro B hB
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
⊢ ((M.map f hf).Base (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).Base (f '' B)
Theorem: Matroid.map_dual
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 '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).Base (f '' B)
Tactic:
simp_rw [← hf.image_diff_subset hB, map_image_base_iff diff_subset,
  map_image_base_iff (show B ⊆ M✶.E from hB), dual_base_iff hB, and_iff_left_iff_imp]
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
⊢ M.Base (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B
Theorem: Matroid.map_dual
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.Base (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B
Tactic:
exact fun _ ↦ ⟨B, hB, rfl⟩
Proof state after:
no goals
Theorem: Matroid.map_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
⊢ (M.map f hf)✶.E = (M✶.map f hf).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.map_emptyOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ InjOn f (emptyOn α).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.map_emptyOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ (emptyOn α).map f ⋯ = emptyOn β
Tactic:
simp [← ground_eq_empty_iff]
Proof state after:
no goals
Theorem: Matroid.map_loopyOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
hf : InjOn f (loopyOn E).E
⊢ (loopyOn E).map f hf = loopyOn (f '' E)
Tactic:
simp [eq_loopyOn_iff]
Proof state after:
no goals
Theorem: Matroid.map_freeOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
hf : InjOn f (freeOn E).E
⊢ (freeOn E).map f hf = freeOn (f '' E)
Tactic:
rw [← dual_inj]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
Theorem: Matroid.map_freeOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.mapEmbedding_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Tactic:
rw [mapEmbedding, map_indep_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Theorem: Matroid.mapEmbedding_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Theorem: Matroid.mapEmbedding_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Tactic:
rintro ⟨I, hI, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f
Theorem: Matroid.mapEmbedding_indep_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f
Tactic:
rw [preimage_image_eq _ f.injective]
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f
Theorem: Matroid.mapEmbedding_indep_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f
Tactic:
exact ⟨hI, image_subset_range _ _⟩
Proof state after:
no goals
Theorem: Matroid.mapEmbedding_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
x✝ : M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
h : M.Indep (⇑f ⁻¹' I)
h' : I ⊆ range ⇑f
⊢ I = ⇑f '' (⇑f ⁻¹' I)
Tactic:
rwa [eq_comm, image_preimage_eq_iff]
Proof state after:
no goals
Theorem: Matroid.Indep.mapEmbedding
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : M.Indep I
f : α ↪ β
⊢ (M.mapEmbedding f).Indep (⇑f '' I)
Tactic:
simpa [preimage_image_eq I f.injective]
Proof state after:
no goals
Theorem: Matroid.Base.mapEmbedding
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 : α ↪ β
⊢ (M.mapEmbedding f).Base (⇑f '' B)
Tactic:
rw [Matroid.mapEmbedding, 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 : α ↪ β
⊢ ∃ B₀, M.Base B₀ ∧ ⇑f '' B = ⇑f '' B₀
Theorem: Matroid.Base.mapEmbedding
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 : α ↪ β
⊢ ∃ B₀, M.Base B₀ ∧ ⇑f '' B = ⇑f '' B₀
Tactic:
exact ⟨B, hB, rfl⟩
Proof state after:
no goals
Theorem: Matroid.Basis.mapEmbedding
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 : α ↪ β
⊢ (M.mapEmbedding f).Basis (⇑f '' I) (⇑f '' X)
Tactic:
apply hIX.map
Proof state after:
no goals
Theorem: Matroid.mapEquiv_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set β
⊢ (M.mapEquiv f).Indep I ↔ M.Indep (⇑f.symm '' I)
Tactic:
rw [mapEquiv_eq_map, map_indep_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)
Theorem: Matroid.mapEquiv_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)
Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
Proof state after:
no goals
Theorem: Matroid.mapEquiv_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f.symm '' I)
Tactic:
rintro ⟨I, hI, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' (⇑f '' I))
Theorem: Matroid.mapEquiv_indep_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' (⇑f '' I))
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.mapEquiv_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set β
h : M.Indep (⇑f.symm '' I)
⊢ I = ⇑f '' (⇑f.symm '' I)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.mapEquiv_dep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
⊢ (M.mapEquiv f).Dep D ↔ M.Dep (⇑f.symm '' D)
Tactic:
rw [mapEquiv_eq_map, map_dep_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)
Theorem: Matroid.mapEquiv_dep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)
Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
Proof state after:
no goals
Theorem: Matroid.mapEquiv_dep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) → M.Dep (⇑f.symm '' D)
Tactic:
rintro ⟨I, hI, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' (⇑f '' I))
Theorem: Matroid.mapEquiv_dep_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' (⇑f '' I))
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.mapEquiv_dep_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
h : M.Dep (⇑f.symm '' D)
⊢ D = ⇑f '' (⇑f.symm '' D)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.mapEquiv_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (M.mapEquiv f).Base B ↔ M.Base (⇑f.symm '' B)
Tactic:
rw [mapEquiv_eq_map, map_base_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) ↔ M.Base (⇑f.symm '' B)
Theorem: Matroid.mapEquiv_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) ↔ M.Base (⇑f.symm '' B)
Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
Proof state after:
no goals
Theorem: Matroid.mapEquiv_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) → M.Base (⇑f.symm '' B)
Tactic:
rintro ⟨I, hI, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Base I
⊢ M.Base (⇑f.symm '' (⇑f '' I))
Theorem: Matroid.mapEquiv_base_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Base I
⊢ M.Base (⇑f.symm '' (⇑f '' I))
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.mapEquiv_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
h : M.Base (⇑f.symm '' B)
⊢ B = ⇑f '' (⇑f.symm '' B)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_ground
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ (M.restrictSubtype X).E = univ
Tactic:
simp [restrictSubtype]
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝¹ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I✝ : Set α
M N : Matroid α
I : Set ↑X
⊢ (M.restrictSubtype X).Indep I ↔ M.Indep ↑I
Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_indep_iff_of_subset
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hIX : I ⊆ X
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I
Tactic:
rw [restrictSubtype_indep_iff, image_preimage_eq_iff.2]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val
Theorem: Matroid.restrictSubtype_indep_iff_of_subset
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_inter_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)
Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]
Proof state after:
no goals
Theorem: Matroid.eq_of_restrictSubtype_eq
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ M = N
Tactic:
subst hM
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N
Theorem: Matroid.eq_of_restrictSubtype_eq
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N
Tactic:
refine eq_of_indep_iff_indep_forall (by rw [hN]) (fun I hI ↦ ?_)
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝¹ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I✝ : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I
Theorem: Matroid.eq_of_restrictSubtype_eq
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝¹ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I✝ : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I
Tactic:
rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]
Proof state after:
no goals
Theorem: Matroid.eq_of_restrictSubtype_eq
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M.E = N.E
Tactic:
rw [hN]
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
Tactic:
rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
  ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Theorem: Matroid.restrictSubtype_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic:
exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn, Subset.rfl]⟩
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ MapsTo Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic:
simp [MapsTo]
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_dual
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ SurjOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic:
simp [SurjOn, Subset.rfl]
Proof state after:
no goals
Theorem: Matroid.restrictSubtype_dual'
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E
Tactic:
rw [← hM, restrictSubtype_dual]
Proof state after:
no goals
Theorem: Matroid.Flat.eq_ground_of_spanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat F
h : M.Spanning F
⊢ F = M.E
Tactic:
rw [← hF.cl, h.cl_eq]
Proof state after:
no goals
Theorem: Matroid.Flat.spanning_iff
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat F
⊢ F = M.E → M.Spanning F
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat M.E
⊢ M.Spanning M.E
Theorem: Matroid.Flat.spanning_iff
Proof state before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat M.E
⊢ M.Spanning M.E
Tactic:
exact M.ground_spanning
Proof state after:
no goals
Theorem: Matroid.Flat.iInter
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
⊢ M.Flat (⋂ i, Fs i)
Tactic:
refine' ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ _,
  (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩
Proof state after:
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
⊢ X ⊆ Fs i
Theorem: Matroid.Flat.iInter
Proof state before:
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
⊢ X ⊆ Fs i
Tactic:
obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_basis_of_subset (hI.subset.trans (iInter_subset _ i))
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i
Theorem: Matroid.Flat.iInter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i
Tactic:
refine' subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ _)
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ M.Basis J (Fs i ∪ X)
Theorem: Matroid.Flat.iInter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ M.Basis J (Fs i ∪ X)
Tactic:
convert hIJ.basis_union (hIX.basis_union_of_subset hIJ.indep hJ) using 1
Proof state after:
case h.e'_4
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)