awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M✶.IsCocircuit C ↔ M.IsCircuit C
have rw : M✶✶.IsCircuit C ↔ M.IsCircuit C
Tactic: rw [isCocircuit_def, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : M✶✶.IsCircuit C ↔ M.IsCircuit C
⊢ M✶.IsCocircuit C ↔ M.IsCircuit C
have rw₁ : M.IsCircuit C ↔ M.IsCircuit C
Tactic: rw [isCocircuit_def, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
have h : ∀ (x : Set α), M✶.Dep x ↔ (∀ (B : Set α), M.IsBase B → (x ∩ B).Nonempty) ∧ x ⊆ M.E
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K
have aux : M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
Tactic: have aux : M✶.Dep = fun X ↦ (∀ B, M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E := by
    ext; apply dual_dep_iff_forall
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K
have rw : Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
  Minimal (fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K
Tactic: rw [isCocircuit_def, isCircuit_def, aux, iff_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K
have refine : ∀ (X : Set α) (hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) (B : Set α) (hB : M.IsBase B), (X ∩ M.E ∩ B).Nonempty
Tactic: refine minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1) fun X hX ↦
    ⟨X ∩ M.E, inter_subset_left, fun B hB ↦ ?_, inter_subset_right⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ M.E ∩ B).Nonempty
have rw : (X ∩ B).Nonempty
Tactic: rw [inter_assoc, inter_eq_self_of_subset_right hB.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X)) K
have h : ∀ (K : Set α), ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: convert! isCocircuit_iff_minimal with K
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h : (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: rw [spanning_iff_exists_isBase_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h₁ : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₁ : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h₂ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → ¬Disjoint x K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₁ : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₂ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → ¬Disjoint x K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h₃ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₁ : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₂ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → ¬Disjoint x K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₃ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h₄ : (∀ (x : Set α), M.IsBase x ∧ x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₁ : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₂ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → ¬Disjoint x K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₃ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₄ : (∀ (x : Set α), M.IsBase x ∧ x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
have h₅ : (∀ (x : Set α), M.IsBase x → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Tactic: simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ M.IsCocircuit (M.E \ M.closure (B \ {e}))
have rw : ¬M.Spanning (B \ {e}) ∧
  ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
Tactic: rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_subset_iff,
    diff_diff_cancel_left (M.closure_subset_ground _),
    closure_spanning_iff (diff_subset.trans hB.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ ¬M.Spanning (B \ {e}) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
have hB' : Minimal M.Spanning B
Tactic: have hB' := (isBase_iff_minimal_spanning.1 hB)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
⊢ ¬M.Spanning (B \ {e}) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
have refine : ∀ (X : Set α) (hX : ¬M.Spanning (M.E \ X)) (hXss : X ⊆ M.E \ M.closure (B \ {e})), M.E \ M.closure (B \ {e}) ⊆ X
Tactic: refine ⟨fun hsp ↦ hB'.notMem_of_prop_diff_singleton hsp he, fun X hX hXss ↦ hXss.antisymm' ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
⊢ M.E \ M.closure (B \ {e}) ⊆ X
have rw : M.E \ X ⊆ M.closure (B \ {e})
Tactic: rw [diff_subset_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
⊢ M.E \ X ⊆ M.closure (B \ {e})
have refine : ∀ (f : α) (hf : f ∈ M.E \ X) (fcl : f ∉ M.closure (B \ {e})), M.Spanning (M.E \ X)
Tactic: refine fun f hf ↦ by_contra fun fcl ↦ hX ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.Spanning (M.E \ X)
have rw : ∀ (hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))) (f : α) (hf : f ∈ M.E \ X) (fcl : f ∉ M.closure (B \ {e})),
  M.Spanning (M.E \ X)
Tactic: rw [subset_diff] at hXss
Cleared hypotheses: hXss, f, hf, fcl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.Spanning (M.E \ X)
have refine : M.closure (B \ {e}) ⊆ M.E \ X
Tactic: refine hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (diff_subset.trans hB.subset_ground)).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.closure (B \ {e}) ⊆ M.E \ X
have rw : M.closure (B \ {e}) ⊆ M.E
Tactic: rw [subset_diff, and_iff_left hXss.2.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.Spanning (M.E \ X)
have suffices : M.IsBase (insert f (B \ {e}))
Tactic: suffices hsp : M.IsBase (insert f (B \ {e})) by
    refine hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (diff_subset.trans hB.subset_ground)).trans ?_
    rw [subset_diff, and_iff_left hXss.2.symm]
    apply closure_subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K
have rw : Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K
Tactic: rw [isCocircuit_iff_minimal_compl_nonspanning]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
⊢ False
have heC : e ∈ C
Tactic: have heC : e ∈ C := (he.symm.subset rfl).1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
heC : e ∈ C
⊢ False
have hK₁ : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
Tactic: simp_rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_iff_forall_ssubset, not_not] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
⊢ False
have hKe : M.Spanning (M.E \ (K \ {e}))
Tactic: have' hKe := hK.2 (t := K \ {e}) (diff_singleton_ssubset.2 (he.symm.subset rfl).2)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False
have apply : M.Spanning (M.E \ K)
Tactic: apply hK.1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)
have rw : M.E ⊆ M.closure (M.E \ K)
Tactic: rw [spanning_iff_ground_subset_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.closure (M.E \ K)
have nth_rw : M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)
Tactic: nth_rw 1 [← hKe.closure_eq, diff_diff_eq_sdiff_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
nth_rw : M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)
⊢ M.E ⊆ M.closure (M.E \ K)
have nth_rw₁ : {e} ⊆ M.E
Tactic: nth_rw 1 [← hKe.closure_eq, diff_diff_eq_sdiff_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)
have refine : M.closure (M.E \ K ∪ {e} ∪ C) ⊆ M.closure (M.E \ K)
Tactic: refine (M.closure_subset_closure (subset_union_left (t := C))).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e} ∪ C) ⊆ M.closure (M.E \ K)
have rw : C \ {e} ⊆ M.E \ K
Tactic: rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← closure_union_congr_right
      (hC.closure_diff_singleton_eq e), union_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ {e} ⊆ M.E \ K
have rw : C \ K ⊆ M.E \ K
Tactic: rw [← he, diff_self_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E
have rw : C ∩ K ⊆ M.E
Tactic: rw [← he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
hCK : (C ∩ K).Nonempty
⊢ (C ∩ K).Nontrivial
have obtain : ∀ (e : α) (heCK : e ∈ C ∩ K), (C ∩ K).Nontrivial
Tactic: obtain ⟨e, heCK⟩ := hCK
Cleared hypotheses: hCK
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ (C ∩ K).Nontrivial
have rw : C ∩ K ≠ {e}
Tactic: rw [nontrivial_iff_ne_singleton heCK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial
have rw : (C ∩ K).Nonempty → (C ∩ K).Nontrivial
Tactic: rw [or_iff_not_imp_left, disjoint_iff_inter_eq_empty, ← ne_eq, ← nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M✶.RankPos ↔ ∃ (C : Set α), M.IsCircuit C
have rw : (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C
Tactic: rw [rankPos_iff, dual_isBase_iff, diff_empty, not_iff_comm, not_exists,
    ← ground_indep_iff_isBase, indep_iff_forall_subset_not_isCircuit]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.RankPos ↔ ∃ (K : Set α), M.IsCocircuit K
have rw : M✶✶.RankPos ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
Tactic: rw [← dual_dual M, dual_rankPos_iff_exists_isCircuit, dual_dual M]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M✶✶.RankPos ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
⊢ M.RankPos ↔ ∃ (K : Set α), M.IsCocircuit K
have rw₁ : (∃ (C : Set α), M✶.IsCircuit C) ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
Tactic: rw [← dual_dual M, dual_rankPos_iff_exists_isCircuit, dual_dual M]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M✶✶.RankPos ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
rw₁ : (∃ (C : Set α), M✶.IsCircuit C) ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
⊢ M.RankPos ↔ ∃ (K : Set α), M.IsCocircuit K
have rw₂ : (∃ (C : Set α), M✶.IsCircuit C) ↔ ∃ (K : Set α), M.IsCocircuit K
Tactic: rw [← dual_dual M, dual_rankPos_iff_exists_isCircuit, dual_dual M]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ M.IsCocircuit (M.fundCocircuit e B)
have apply : e ∈ M✶.closure (M.E \ B)
Tactic: apply hB.compl_isBase_dual.indep.fundCircuit_isCircuit _ (by simp [he])
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.closure (M.E \ B)
have rw : e ∈ M.E
Tactic: rw [hB.compl_isBase_dual.closure_eq, dual_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B = {e}
have refine : M.fundCocircuit e B ∩ B ⊆ {e}
Tactic: refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocircuit _ _, he⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B ⊆ {e}
have refine : insert e (M.E \ B) ∩ B ⊆ {e}
Tactic: refine (inter_subset_inter_left _ (M.fundCocircuit_subset_insert_compl _ _)).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}
have rwa : M✶.fundCircuit e (M✶.E \ X) = {e}
Tactic: rwa [fundCocircuit, fundCircuit_eq_of_notMem_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
rwa : M✶.fundCircuit e (M✶.E \ X) = {e}
⊢ M.fundCocircuit e X = {e}
have rwa₁ : Eq (α := Set α) {e} {e}
Tactic: rwa [fundCocircuit, fundCircuit_eq_of_notMem_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
rwa : M✶.fundCircuit e (M✶.E \ X) = {e}
rwa₁ : Eq (α := Set α) {e} {e}
⊢ M.fundCocircuit e X = {e}
have rwa₂ : e ∉ M✶.E
Tactic: rwa [fundCocircuit, fundCircuit_eq_of_notMem_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
⊢ M.fundCocircuit e X = {e}
have pos : ∀ (he : e ∈ M.E), M.fundCocircuit e X = {e}
Tactic: by_cases he : e ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
pos : ∀ (he : e ∈ M.E), M.fundCocircuit e X = {e}
⊢ M.fundCocircuit e X = {e}
have neg : ∀ (he : e ∉ M.E), M.fundCocircuit e X = {e}
Tactic: by_cases he : e ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M.fundCocircuit e X = {e}
have pos : e ∈ M✶.E \ X
Tactic: rw [fundCocircuit, fundCircuit_eq_of_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}
have neg : Eq (α := Set α) {e} {e}
Tactic: rw [fundCocircuit_eq_of_notMem_ground _ he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}
Tactic: obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}
have refine : M.fundCocircuit e B ∩ I = {e}
Tactic: refine ⟨M.fundCocircuit e B, fundCocircuit_isCocircuit (hIB heI) hB, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I = {e}
have rw : M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B
Tactic: rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
    (mem_fundCocircuit _ _ _), singleton_subset_iff, and_iff_left heI,
    ← M.fundCocircuit_inter_eq (hIB heI)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
⊢ e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B
have suffices : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'
Tactic: suffices aux : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f},
      e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B' from
    ⟨fun h ↦ aux hB h, fun h ↦ aux hB.compl_isBase_dual <| by
      simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]⟩