internlm/Lean-Github huggingface dataset:
Theorem: Matroid.eq_of_circuit_iff_circuit_forall
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂
Tactic:
have h' : ∀ C, M₁.Circuit C ↔ M₂.Circuit C := by
  exact fun C ↦ (em (C ⊆ M₁.E)).elim (h C)
    (fun hC ↦ iff_of_false (mt Circuit.subset_ground hC)
      (mt Circuit.subset_ground (fun hss ↦ hC (hss.trans_eq hE.symm))))
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂
Theorem: Matroid.eq_of_circuit_iff_circuit_forall
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂
Tactic:
refine' eq_of_indep_iff_indep_forall hE fun I hI ↦ _
Proof state after:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Theorem: Matroid.eq_of_circuit_iff_circuit_forall
Proof state before:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Tactic:
simp_rw [indep_iff_forall_subset_not_circuit hI, h',
  indep_iff_forall_subset_not_circuit (hI.trans_eq hE)]
Proof state after:
no goals
Theorem: Matroid.eq_of_circuit_iff_circuit_forall
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
⊢ ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
Tactic:
exact fun C ↦ (em (C ⊆ M₁.E)).elim (h C)
  (fun hC ↦ iff_of_false (mt Circuit.subset_ground hC)
    (mt Circuit.subset_ground (fun hss ↦ hC (hss.trans_eq hE.symm))))
Proof state after:
no goals
Theorem: Matroid.map_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Circuit C ↔ ∃ C₀, M.Circuit C₀ ∧ C = f '' C₀
Tactic:
simp only [circuit_iff, map_dep_iff, forall_exists_index, and_imp]
Proof state after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) ↔
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀
Theorem: Matroid.map_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) ↔
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) →
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀

case mpr
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ (∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀) →
    (∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C
Theorem: Matroid.map_circuit_iff
Proof state before:
case mpr
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ (∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀) →
    (∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C
Tactic:
rintro ⟨C₀, ⟨h,h'⟩, rfl⟩
Proof state after:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ (∃ D₀, M.Dep D₀ ∧ f '' C₀ = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
Theorem: Matroid.map_circuit_iff
Proof state before:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ (∃ D₀, M.Dep D₀ ∧ f '' C₀ = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
Tactic:
refine ⟨⟨C₀, h, rfl⟩, ?_⟩
Proof state after:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
Theorem: Matroid.map_circuit_iff
Proof state before:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
Tactic:
rintro _ D hD rfl hss
Proof state after:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
D : Set α
hD : M.Dep D
hss : f '' D ⊆ f '' C₀
⊢ f '' D = f '' C₀
Theorem: Matroid.map_circuit_iff
Proof state before:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
D : Set α
hD : M.Dep D
hss : f '' D ⊆ f '' C₀
⊢ f '' D = f '' C₀
Tactic:
rw [h' hD ((hf.image_subset_image_iff hD.subset_ground h.subset_ground).1 hss)]
Proof state after:
no goals
Theorem: Matroid.map_circuit_iff
Proof state before:
case mp
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) →
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀
Tactic:
rintro ⟨⟨C, hC, rfl⟩, h⟩
Proof state after:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
⊢ ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ f '' C = f '' C₀
Theorem: Matroid.map_circuit_iff
Proof state before:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
⊢ ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ f '' C = f '' C₀
Tactic:
refine ⟨C, ⟨hC, fun D hD hDC ↦ ?_⟩, rfl⟩
Proof state after:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ D = C
Theorem: Matroid.map_circuit_iff
Proof state before:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ D = C
Tactic:
rw [← hf.image_eq_image_iff hD.subset_ground hC.subset_ground]
Proof state after:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ f '' D = f '' C
Theorem: Matroid.map_circuit_iff
Proof state before:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ f '' D = f '' C
Tactic:
exact h _ hD rfl (image_subset f hDC)
Proof state after:
no goals
Theorem: Matroid.mapEquiv_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (M.mapEquiv f).Circuit C ↔ M.Circuit (⇑f.symm '' C)
Tactic:
rw [mapEquiv_eq_map, map_circuit_iff]
Proof state after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) ↔ M.Circuit (⇑f.symm '' C)
Theorem: Matroid.mapEquiv_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) ↔ M.Circuit (⇑f.symm '' C)
Tactic:
exact ⟨by rintro ⟨C, hC, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
Proof state after:
no goals
Theorem: Matroid.mapEquiv_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) → M.Circuit (⇑f.symm '' C)
Tactic:
rintro ⟨C, hC, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α ≃ β
C : Set α
hC : M.Circuit C
⊢ M.Circuit (⇑f.symm '' (⇑f '' C))
Theorem: Matroid.mapEquiv_circuit_iff
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α ≃ β
C : Set α
hC : M.Circuit C
⊢ M.Circuit (⇑f.symm '' (⇑f '' C))
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.mapEquiv_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
h : M.Circuit (⇑f.symm '' C)
⊢ C = ⇑f '' (⇑f.symm '' C)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Circuit.cocircuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
⊢ M✶.Cocircuit C
Tactic:
rwa [cocircuit_def, dual_dual]
Proof state after:
no goals
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
revert K
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ {K : Set α}, M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ {K : Set α}, M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
simp_rw [cocircuit_def, circuit_def, ← Set.ext_iff, dep_iff, ← coindep_def, dual_ground,
  coindep_iff_exists', not_and, imp_not_comm (b := (_ ⊆ _)), not_exists, not_and, subset_diff,
  not_and, not_disjoint_iff_nonempty_inter]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ minimals (fun x x_1 => x ⊆ x_1) {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} =
    minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ minimals (fun x x_1 => x ⊆ x_1) {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} =
    minimals (fun x x_1 => x ⊆ x_1) {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
apply (minimals_eq_minimals_of_subset_of_forall _ _).symm
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} ⊆
    {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}

α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ x ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty},
    ∃ y ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}, y ⊆ x
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ x ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty},
    ∃ y ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}, y ⊆ x
Tactic:
refine' fun K hK ↦ ⟨K ∩ M.E, _, inter_subset_left⟩
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ K ∩ M.E ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ K ∩ M.E ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
Tactic:
simp only [mem_setOf_eq, inter_subset_right, forall_true_left, and_true]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ (K ∩ M.E)).Nonempty
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ (K ∩ M.E)).Nonempty
Tactic:
rintro B hB hBE
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (B ∩ (K ∩ M.E)).Nonempty
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (B ∩ (K ∩ M.E)).Nonempty
Tactic:
rw [inter_comm, inter_assoc, inter_eq_self_of_subset_right hBE]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (K ∩ B).Nonempty
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
B : Set α
hB : M.Base B
hBE : B ⊆ M.E
⊢ (K ∩ B).Nonempty
Tactic:
exact hK B hB
Proof state after:
no goals
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E} ⊆
    {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
Tactic:
exact fun K ⟨hK1, hK2⟩ B hB ↦ by rw [inter_comm]; exact hK1 hK2 B hB hB.subset_ground
Proof state after:
no goals
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
x✝ : K ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
B : Set α
hB : M.Base B
hK1 : K ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ K).Nonempty
hK2 : K ⊆ M.E
⊢ (K ∩ B).Nonempty
Tactic:
rw [inter_comm]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
x✝ : K ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
B : Set α
hB : M.Base B
hK1 : K ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ K).Nonempty
hK2 : K ⊆ M.E
⊢ (B ∩ K).Nonempty
Theorem: Matroid.cocircuit_iff_mem_minimals
Proof state before:
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B✝ K : Set α
x✝ : K ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}
B : Set α
hB : M.Base B
hK1 : K ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ K).Nonempty
hK2 : K ⊆ M.E
⊢ (B ∩ K).Nonempty
Tactic:
exact hK1 hK2 B hB hB.subset_ground
Proof state after:
no goals
Theorem: Matroid.cocircuit_iff_mem_minimals_compl_nonspanning
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ¬M.Spanning (M.E \ X)}
Tactic:
convert cocircuit_iff_mem_minimals with K
Proof state after:
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.a
α : Type u_1
M : Matroid α
C C' I X K✝ C₁ C₂ R : Set α
e f x y : α
B K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.Base B → (K ∩ B).Nonempty
Theorem: Matroid.cocircuit_iff_mem_minimals_compl_nonspanning
Proof state before:
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.a
α : Type u_1
M : Matroid α
C C' I X K✝ C₁ C₂ R : Set α
e f x y : α
B K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.Base B → (K ∩ B).Nonempty
Tactic:
simp_rw [spanning_iff_superset_base (S := M.E \ K), not_exists, subset_diff, not_and,
  not_disjoint_iff_nonempty_inter, ← and_imp, and_iff_left_of_imp Base.subset_ground,
    inter_comm K]
Proof state after:
no goals
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial
Tactic:
simp_rw [or_iff_not_imp_left, not_disjoint_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
⊢ (∃ x ∈ C, x ∈ K) → (C ∩ K).Nontrivial
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
⊢ (∃ x ∈ C, x ∈ K) → (C ∩ K).Nontrivial
Tactic:
rintro ⟨e, heC, heK⟩
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ (C ∩ K).Nontrivial
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ (C ∩ K).Nontrivial
Tactic:
simp_rw [nontrivial_iff_ne_singleton <| show e ∈ C ∩ K from ⟨heC, heK⟩]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ C ∩ K ≠ {e}
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ C ∩ K ≠ {e}
Tactic:
intro he
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
⊢ False
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
⊢ False
Tactic:
simp_rw [cocircuit_iff_mem_minimals_compl_nonspanning, mem_minimals_iff_forall_ssubset_not_mem,
  mem_setOf, not_not] at hK
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
⊢ False
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
⊢ False
Tactic:
have' hKe := hK.2 (y := K \ {e}) (diff_singleton_sSubset.2 (he.symm.subset rfl).2)
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False
Tactic:
apply hK.1
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)
Tactic:
rw [spanning_iff_ground_subset_cl]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.cl (M.E \ K)
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.cl (M.E \ K)
Tactic:
nth_rw 1 [← hKe.cl_eq, diff_diff_eq_sdiff_union]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e}) ⊆ M.cl (M.E \ K)

case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E