awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₅ : M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
rw₅ : M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₆ : M.closure (M.closure (insert f (M.closure (insert e X)))) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
rw₅ : M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
rw₆ : M.closure (M.closure (insert f (M.closure (insert e X)))) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₇ : M.closure (M.closure (M.closure (insert e X))) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
rw₅ : M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
rw₆ : M.closure (M.closure (insert f (M.closure (insert e X)))) = M.closure (insert e X)
rw₇ : M.closure (M.closure (M.closure (insert e X))) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₈ : M.closure (M.closure (insert e X)) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
rw₅ : M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
rw₆ : M.closure (M.closure (insert f (M.closure (insert e X)))) = M.closure (insert e X)
rw₇ : M.closure (M.closure (M.closure (insert e X))) = M.closure (insert e X)
rw₈ : M.closure (M.closure (insert e X)) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₉ : M.closure (insert e X) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
⊢ M.closure (X \ Y) = M.closure X
have rw : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y ∪ X ∩ Y)
Tactic: rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
rw : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y ∪ X ∩ Y)
⊢ M.closure (X \ Y) = M.closure X
have rw₁ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y) ∪ X ∩ Y)
Tactic: rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
rw : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y ∪ X ∩ Y)
rw₁ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y) ∪ X ∩ Y)
⊢ M.closure (X \ Y) = M.closure X
have rw₂ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y))
Tactic: rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
rw : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y ∪ X ∩ Y)
rw₁ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y) ∪ X ∩ Y)
rw₂ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y))
⊢ M.closure (X \ Y) = M.closure X
have rw₃ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y)
Tactic: rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
rw : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y ∪ X ∩ Y)
rw₁ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y) ∪ X ∩ Y)
rw₂ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y))
rw₃ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y)
⊢ M.closure (X \ Y) = M.closure X
have rw₄ : M.closure (X \ Y) = M.closure (X \ Y)
Tactic: rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x : Set α
h_1 : x ⊆ M₁.E
⊢ M₁.Indep x ↔ M₂.Indep x
have simp_rw : (∀ ⦃e : α⦄, e ∈ x → M₁.closure (x \ {e}) ≠ M₁.closure x) ↔ ∀ ⦃e : α⦄, e ∈ x → M₂.closure (x \ {e}) ≠ M₂.closure x
Tactic: simp_rw [indep_iff_forall_closure_diff_ne, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.closure S = M.E
have rw : M.closure S = M.E ∧ S ⊆ M.E ↔ M.closure S = M.E
Tactic: rw [spanning_iff, and_iff_left hS]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure S = M.E ∧ S ⊆ M.E ↔ M.closure S = M.E
⊢ M.Spanning S ↔ M.closure S = M.E
have rw₁ : M.closure S = M.E ↔ M.closure S = M.E
Tactic: rw [spanning_iff, and_iff_left hS]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning (M.closure S) ↔ M.Spanning S
have rw : M.closure (M.closure S) = M.E ↔ M.Spanning S
Tactic: rw [spanning_iff_closure_eq, closure_closure, ← spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure (M.closure S) = M.E ↔ M.Spanning S
⊢ M.Spanning (M.closure S) ↔ M.Spanning S
have rw₁ : M.closure S = M.E ↔ M.Spanning S
Tactic: rw [spanning_iff_closure_eq, closure_closure, ← spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure (M.closure S) = M.E ↔ M.Spanning S
rw₁ : M.closure S = M.E ↔ M.Spanning S
⊢ M.Spanning (M.closure S) ↔ M.Spanning S
have rw₂ : M.Spanning S ↔ M.Spanning S
Tactic: rw [spanning_iff_closure_eq, closure_closure, ← spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.E ⊆ M.closure S
have rw : M.closure S = M.E ↔ M.E ⊆ M.closure S
Tactic: rw [spanning_iff_closure_eq, subset_antisymm_iff, and_iff_right (closure_subset_ground _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure S = M.E ↔ M.E ⊆ M.closure S
⊢ M.Spanning S ↔ M.E ⊆ M.closure S
have rw₁ : M.closure S ⊆ M.E ∧ M.E ⊆ M.closure S ↔ M.E ⊆ M.closure S
Tactic: rw [spanning_iff_closure_eq, subset_antisymm_iff, and_iff_right (closure_subset_ground _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure S = M.E ↔ M.E ⊆ M.closure S
rw₁ : M.closure S ⊆ M.E ∧ M.E ⊆ M.closure S ↔ M.E ⊆ M.closure S
⊢ M.Spanning S ↔ M.E ⊆ M.closure S
have rw₂ : M.E ⊆ M.closure S ↔ M.E ⊆ M.closure S
Tactic: rw [spanning_iff_closure_eq, subset_antisymm_iff, and_iff_right (closure_subset_ground _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.Spanning S ↔ M.closure S ⊂ M.E
have rw : ¬M.closure S = M.E → True
Tactic: rw [spanning_iff_closure_eq, ssubset_iff_subset_ne, iff_and_self,
    iff_true_intro (M.closure_subset_ground _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.E ⊆ M.closure T
have rw : M.closure S ⊆ M.closure T
Tactic: rw [← hS.closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.closure T = M.E
have rw : M.Spanning (T ∩ M.E)
Tactic: rw [← closure_inter_ground, ← spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
⊢ M.Spanning S ↔ (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E
have refine : ∀ (h : M.Spanning S), ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
Tactic: refine ⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
have obtain : ∀ (B : Set α) (hB : M.IsBasis B S), ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
Tactic: obtain ⟨B, hB⟩ := M.exists_isBasis S
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
have hB' : M.IsBasis B (M.closure S)
Tactic: have hB' := hB.isBasis_closure_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B (M.closure S)
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
have hB'₁ : M.IsBase B
Tactic: rw [h.closure_eq, isBasis_ground_iff] at hB'
Cleared hypotheses: hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
have rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
Tactic: rw [spanning_iff_exists_isBase_subset', and_iff_left hS]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
⊢ M.Spanning S ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
have rw₁ : (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
Tactic: rw [spanning_iff_exists_isBase_subset', and_iff_left hS]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
have rwa : ∀ (hS : ∃ (B : Set α), M.IsBase B ∧ B ⊆ S), ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
Tactic: rwa [spanning_iff_exists_isBase_subset] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)
have rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I) ↔ M.Spanning (M.E \ I)
Tactic: rw [coindep_iff_exists, spanning_iff_exists_isBase_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I) ↔ M.Spanning (M.E \ I)
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)
have rw₁ : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I
Tactic: rw [coindep_iff_exists, spanning_iff_exists_isBase_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)
have rw : M.Spanning S ↔ M.Spanning (M.E \ (M.E \ S))
Tactic: rw [coindep_iff_compl_spanning, diff_diff_cancel_left hS]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.Spanning S ↔ M.Spanning (M.E \ (M.E \ S))
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)
have rw₁ : M.Spanning S ↔ M.Spanning S
Tactic: rw [coindep_iff_compl_spanning, diff_diff_cancel_left hS]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E
have rw : M.Spanning (M.E \ X) ↔ M.closure (M.E \ X) = M.E
Tactic: rw [coindep_iff_compl_spanning, spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
rw : M.Spanning (M.E \ X) ↔ M.closure (M.E \ X) = M.E
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E
have rw₁ : M.closure (M.E \ X) = M.E ↔ M.closure (M.E \ X) = M.E
Tactic: rw [coindep_iff_compl_spanning, spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
⊢ M.IsBase I
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hBI : B ⊆ I), M.IsBase I
Tactic: obtain ⟨B, hB, hBI⟩ := hIs.exists_isBase_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.Spanning I ↔ M.Spanning X
have rw : M.closure I = M.E ↔ M.Spanning X
Tactic: rw [spanning_iff_closure_eq, spanning_iff_closure_eq, hIX.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
rw : M.closure I = M.E ↔ M.Spanning X
⊢ M.Spanning I ↔ M.Spanning X
have rw₁ : M.closure I = M.E ↔ M.closure X = M.E
Tactic: rw [spanning_iff_closure_eq, spanning_iff_closure_eq, hIX.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
rw : M.closure I = M.E ↔ M.Spanning X
rw₁ : M.closure I = M.E ↔ M.closure X = M.E
⊢ M.Spanning I ↔ M.Spanning X
have rw₂ : M.closure X = M.E ↔ M.closure X = M.E
Tactic: rw [spanning_iff_closure_eq, spanning_iff_closure_eq, hIX.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S
have rw : M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S
Tactic: rw [isBase_restrict_iff', isBasis'_iff_isBasis]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S
have refine_1 : ∀ (h : M.IsBasis B S), M.IsBase B
Tactic: refine ⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
refine_1 : ∀ (h : M.IsBasis B S), M.IsBase B
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S
have refine_2 : ∀ (h : M.IsBase B ∧ B ⊆ S), S ⊆ M.closure B
Tactic: refine ⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B
have refine_2 : S ⊆ M.E
Tactic: rw [h.1.closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
⊢ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B ∧ B ⊆ S
have obtain : ∀ (B : Set α) (hB : M.IsBasis B S ∧ I ⊆ B), ∃ (B : Set α), M.IsBase B ∧ I ⊆ B ∧ B ⊆ S
Tactic: obtain ⟨B, hB⟩ := hI.subset_isBasis_of_subset hIS
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
N : Matroid α
hR : N ≤r M
hN : M.Spanning N.E
⊢ N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hN : M.Spanning (M ↾ R).E), (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
Tactic: obtain ⟨R, hR : R ⊆ M.E, rfl⟩ := hR
Cleared hypotheses: N, hR, hN
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
⊢ (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
have rw : M.IsBase B ∧ B ⊆ R ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
Tactic: rw [Spanning.isBase_restrict_iff (show M.Spanning R from hN), restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
rw : M.IsBase B ∧ B ⊆ R ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
have rw₁ : M.IsBase B ∧ B ⊆ R ↔ M.IsBase B ∧ B ⊆ R
Tactic: rw [Spanning.isBase_restrict_iff (show M.Spanning R from hN), restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning
have h₁ : ∀ (S : Set α), M.Spanning S ↔ M'.Spanning S
Tactic: ext S
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S
have rw : M'.Spanning S ↔ M'.Spanning S
Tactic: rw [hsp _ hSE]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M = M'
have hsp' : M.Spanning = M'.Spanning
Tactic: have hsp' : M.Spanning = M'.Spanning := by
    ext S
    refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE])
      (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
      (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'
have rw : ∀ ⦃I : Set α⦄, I ⊆ M.E → (M✶.Indep I ↔ M'✶.Indep I)
Tactic: rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I
have rw : M.Coindep I ↔ M'✶.Indep I
Tactic: rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]