awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw₃ : I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
Tactic: simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₃ :
  I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw₄ : I ⊆ M.E → ((I ⊆ M.E → ¬∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
Tactic: simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₃ :
  I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₄ :
  I ⊆ M.E → ((I ⊆ M.E → ¬∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw₅ : I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), ¬(M.IsBase x ∧ Disjoint I x)) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
Tactic: simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₃ :
  I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₄ :
  I ⊆ M.E → ((I ⊆ M.E → ¬∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₅ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), ¬(M.IsBase x ∧ Disjoint I x)) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw₆ : I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → ¬Disjoint I x) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
Tactic: simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₃ :
  I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₄ :
  I ⊆ M.E → ((I ⊆ M.E → ¬∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₅ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), ¬(M.IsBase x ∧ Disjoint I x)) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₆ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → ¬Disjoint I x) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw₇ : I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty) ↔ ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty)
Tactic: simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₃ :
  I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₄ :
  I ⊆ M.E → ((I ⊆ M.E → ¬∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₅ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), ¬(M.IsBase x ∧ Disjoint I x)) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₆ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → ¬Disjoint I x) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₇ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty) ↔ ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty)
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw₈ : I ⊆ M.E → I ⊆ M.E ∨ ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty
Tactic: simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B)
have rw : (M✶.Indep B ∧ ∀ ⦃t : Set α⦄, M✶.Indep t → B ⊆ t → B = t) ↔
  (B ⊆ M.E ∧ ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) → B ⊆ t → B = t
Tactic: rw [isBase_compl_iff_maximal_disjoint_isBase, isBase_iff_maximal_indep, maximal_subset_iff,
    maximal_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
have rw : M.IsBase (M.E \ B) ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
Tactic: rw [dual_isBase_iff, and_iff_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
rw : M.IsBase (M.E \ B) ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
have rw₁ : M.IsBase (M.E \ B) ↔ M.IsBase (M.E \ B)
Tactic: rw [dual_isBase_iff, and_iff_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ Eq.{u_1 + 1} (α := Set (Set α)) {B : Set α | M✶.IsBase B} ((fun (X : Set α) ↦ M.E \ X) '' {B : Set α | M.IsBase B})
have h : ∀ (B : Set α),
  Membership.mem (γ := Set (Set α)) {B : Set α | M✶.IsBase B} B ↔
    Membership.mem (γ := Set (Set α)) ((fun (X : Set α) ↦ M.E \ X) '' {B : Set α | M.IsBase B}) B
Tactic: ext B
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ Membership.mem (γ := Set (Set α)) {B : Set α | M✶.IsBase B} B ↔
    Membership.mem (γ := Set (Set α)) ((fun (X : Set α) ↦ M.E \ X) '' {B : Set α | M.IsBase B}) B
have h : M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B
Tactic: simp only [mem_setOf_eq, mem_image, dual_isBase_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B
have h : (∃ (x : Set α), M.IsBase x ∧ M.E \ x = B) → ∀ (B' : Set α) (hB' : M.IsBase B') (h : M.E \ B' = B), M.IsBase (M.E \ B)
Tactic: refine ⟨fun h ↦ ⟨_, h.1, diff_diff_cancel_left h.2⟩,
    fun ⟨B', hB', h⟩ ↦ ⟨?_,h.symm.trans_subset diff_subset⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h_1 : ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B
B' : Set α
hB' : M.IsBase B'
h : M.E \ B' = B
⊢ M.IsBase (M.E \ B)
have h₁ : M.IsBase (M.E \ (M.E \ B'))
Tactic: rwa [← h, diff_diff_cancel_left hB'.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶✶.IsBase B ↔ M.IsBase B
have rw : M✶.IsBase (M✶.E \ B) ↔ M.IsBase B
Tactic: rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
rw : M✶.IsBase (M✶.E \ B) ↔ M.IsBase B
⊢ M✶✶.IsBase B ↔ M.IsBase B
have rw₁ : M.IsBase (M.E \ (M✶.E \ B)) ↔ M.IsBase B
Tactic: rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
rw : M✶.IsBase (M✶.E \ B) ↔ M.IsBase B
rw₁ : M.IsBase (M.E \ (M✶.E \ B)) ↔ M.IsBase B
⊢ M✶✶.IsBase B ↔ M.IsBase B
have rw₂ : M.IsBase (M.E \ (M.E \ B)) ↔ M.IsBase B
Tactic: rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
rw : M✶.IsBase (M✶.E \ B) ↔ M.IsBase B
rw₁ : M.IsBase (M.E \ (M✶.E \ B)) ↔ M.IsBase B
rw₂ : M.IsBase (M.E \ (M.E \ B)) ↔ M.IsBase B
⊢ M✶✶.IsBase B ↔ M.IsBase B
have rw₃ : M.IsBase B ↔ M.IsBase B
Tactic: rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶
have rw : M₁✶ = M₂✶✶ ↔ M₂ = M₁✶
Tactic: rw [← dual_inj, dual_dual, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
rw : M₁✶ = M₂✶✶ ↔ M₂ = M₁✶
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶
have rw₁ : M₁✶ = M₂ ↔ M₂ = M₁✶
Tactic: rw [← dual_inj, dual_dual, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
rw : M₁✶ = M₂✶✶ ↔ M₂ = M₁✶
rw₁ : M₁✶ = M₂ ↔ M₂ = M₁✶
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶
have rw₂ : M₂ = M₁✶ ↔ M₂ = M₁✶
Tactic: rw [← dual_inj, dual_dual, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase B
⊢ M✶.IsBase (M.E \ B)
have rwa : M.IsBase (M.E \ (M.E \ B))
Tactic: rwa [dual_isBase_iff, diff_diff_cancel_left h.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
have refine_1 : M✶.Indep (M.E \ B ∩ (M.E \ X))
Tactic: refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
refine_1 : M✶.Indep (M.E \ B ∩ (M.E \ X))
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
have refine_2 : ∀ (e : α) (he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))), M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
Tactic: refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))
have refine_1 : ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ B ∩ (M.E \ X)) B_1
Tactic: rw [dual_indep_iff_exists]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
have he₁ : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
Tactic: simp only [diff_inter_self_eq_diff, mem_diff, not_and, not_not, imp_iff_right he.1.1] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
have refine_2 : ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty
Tactic: simp_rw [dual_dep_iff_forall, insert_subset_iff, and_iff_right he.1.1,
    and_iff_left (inter_subset_left.trans diff_subset)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty
have refine_2 : ∀ (B' : Set α) (hB' : M.IsBase B') (hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty), False
Tactic: refine fun B' hB' ↦ by_contra (fun hem ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty
⊢ False
have hem₁ : B' ⊆ B ∪ X ∧ e ∉ B'
Tactic: rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, diff_inter_diff,
    union_inter_distrib_right, union_empty_iff, singleton_inter_eq_empty, diff_eq,
    inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← diff_eq,
    diff_eq_empty] at hem
Cleared hypotheses: hem
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
⊢ False
have refine_2 : ∀ (f : α) (hfb : f ∈ B' \ B) (hBf : M.IsBase (insert f (B \ {e}))), False
Tactic: obtain ⟨f, hfb, hBf⟩ := hB.exchange hB' ⟨he.2, hem.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ M.Indep (insert f (B ∩ X))
have refine : B ∩ X ⊆ B \ {e}
Tactic: refine hBf.indep.subset (insert_subset_insert ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ B ∩ X ⊆ B \ {e}
have simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
Tactic: simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
⊢ B ∩ X ⊆ B \ {e}
have simp_rw₁ : Disjoint (B ∩ X) {e}
Tactic: simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
simp_rw₁ : Disjoint (B ∩ X) {e}
⊢ B ∩ X ⊆ B \ {e}
have simp_rw₂ : e ∉ B ∩ X
Tactic: simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
simp_rw₁ : Disjoint (B ∩ X) {e}
simp_rw₂ : e ∉ B ∩ X
⊢ B ∩ X ⊆ B \ {e}
have simp_rw₃ : ¬(e ∈ B ∧ e ∈ X)
Tactic: simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
simp_rw₁ : Disjoint (B ∩ X) {e}
simp_rw₂ : e ∉ B ∩ X
simp_rw₃ : ¬(e ∈ B ∧ e ∈ X)
⊢ B ∩ X ⊆ B \ {e}
have simp_rw₄ : ¬(e ∈ B ∧ False)
Tactic: simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
simp_rw₁ : Disjoint (B ∩ X) {e}
simp_rw₂ : e ∉ B ∩ X
simp_rw₃ : ¬(e ∈ B ∧ e ∈ X)
simp_rw₄ : ¬(e ∈ B ∧ False)
⊢ B ∩ X ⊆ B \ {e}
have simp_rw₅ : ¬False
Tactic: simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ False
have hi : M.Indep (insert f (B ∩ X))
Tactic: have hi : M.Indep (insert f (B ∩ X)) := by
    refine hBf.indep.subset (insert_subset_insert ?_)
    simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
⊢ M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
have refine : ∀ (h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)), M.IsBasis (B ∩ X) X
Tactic: refine ⟨hB.compl_inter_isBasis_of_inter_isBasis, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase B ↔ M✶.IsBase (M.E \ B)
have rw : M.IsBase B ↔ M.IsBase (M.E \ (M.E \ B))
Tactic: rw [dual_isBase_iff, diff_diff_cancel_left hB]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
rw : M.IsBase B ↔ M.IsBase (M.E \ (M.E \ B))
⊢ M.IsBase B ↔ M✶.IsBase (M.E \ B)
have rw₁ : M.IsBase B ↔ M.IsBase B
Tactic: rw [dual_isBase_iff, diff_diff_cancel_left hB]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
h : M✶.RankPos
⊢ ¬M.IsBase M.E
have rwa : ∀ (h : ¬M✶.IsBase ∅), ¬M.IsBase M.E
Tactic: rwa [rankPos_iff, dual_isBase_iff, diff_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
h : M✶.RankPos
rwa : ∀ (h : ¬M✶.IsBase ∅), ¬M.IsBase M.E
⊢ ¬M.IsBase M.E
have rwa₁ : ∀ (h : ¬M.IsBase (M.E \ ∅)), ¬M.IsBase M.E
Tactic: rwa [rankPos_iff, dual_isBase_iff, diff_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
h : M✶.RankPos
rwa : ∀ (h : ¬M✶.IsBase ∅), ¬M.IsBase M.E
rwa₁ : ∀ (h : ¬M.IsBase (M.E \ ∅)), ¬M.IsBase M.E
⊢ ¬M.IsBase M.E
have rwa₂ : ∀ (h : ¬M.IsBase M.E), ¬M.IsBase M.E
Tactic: rwa [rankPos_iff, dual_isBase_iff, diff_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
⊢ I ⊂ M.E
have obtain : ∀ (B : Set α) (hB : M.IsBase B ∧ I ⊆ B), I ⊂ M.E
Tactic: obtain ⟨B, hB⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.Coindep X ↔ M.Indep X
have rw : M✶✶.Indep X ↔ M.Indep X
Tactic: rw [Coindep, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M✶✶.Indep X ↔ M.Indep X
⊢ M✶.Coindep X ↔ M.Indep X
have rw₁ : M.Indep X ↔ M.Indep X
Tactic: rw [Coindep, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
have simp_rw : X ⊆ M.E → ((∃ (B : Set α), M.IsBase B ∧ Disjoint X B) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)
Tactic: simp_rw [Coindep, dual_indep_iff_exists', and_comm (a := _ ⊆ _), and_congr_left_iff, subset_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Coindep X ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
have rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
Tactic: rw [coindep_iff_exists', and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
⊢ M.Coindep X ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
have rw₁ : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
Tactic: rw [coindep_iff_exists', and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E \ B
have simp_rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B
Tactic: simp_rw [coindep_iff_exists', subset_diff]