awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
have h : ∀ (heX : e ∉ X), e ∈ B'
Tactic: refine ⟨by_contra (fun heX ↦ heB'' (hB''₁ ⟨?_, heI⟩)), ⟨B'', hB'', ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
h : ∀ (heX : e ∉ X), e ∈ B'
⊢ e ∈ X ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
have h₁ : Disjoint (insert e I) B''
Tactic: refine ⟨by_contra (fun heX ↦ heB'' (hB''₁ ⟨?_, heI⟩)), ⟨B'', hB'', ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint (insert e I) B''
have h : Disjoint I B''
Tactic: rw [← union_singleton, disjoint_union_left, disjoint_singleton_left, and_iff_left heB'']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
have obtain : ∀ (I : Set α) (hI : M.IsBasis I (M.E \ X)),
  ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis (M.E \ X)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
I : Set α
hI : M.IsBasis I (M.E \ X)
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hIB' : I ⊆ B') (hB'IB : B' ⊆ I ∪ B),
  ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
Tactic: obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_isBase_subset_union_isBase hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
have hI₁ : M.IsBasis (B' \ X) (M.E \ X)
Tactic: obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)
Cleared hypotheses: I, hI, hIB', hB'IB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
hI₁ : M.IsBasis (B' \ X) (M.E \ X)
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
have hIB'₁ : B' \ X ⊆ B'
Tactic: obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)
Cleared hypotheses: I, hI, hIB', hB'IB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
hI₁ : M.IsBasis (B' \ X) (M.E \ X)
hIB'₁ : B' \ X ⊆ B'
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
have hB'IB₁ : B' ⊆ B' \ X ∪ B
Tactic: obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)
Cleared hypotheses: I, hI, hIB', hB'IB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      ((J ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint J B) ∧ J ⊆ X) ∧
        ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → J ⊆ t → t ⊆ J
have refine_1 : I' ⊆ X \ B' ∩ M.E
Tactic: refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
refine_1 : I' ⊆ X \ B' ∩ M.E
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      ((J ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint J B) ∧ J ⊆ X) ∧
        ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → J ⊆ t → t ⊆ J
have refine_2 : ∃ (B : Set α), M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B
Tactic: refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
refine_1 : I' ⊆ X \ B' ∩ M.E
refine_2 : ∃ (B : Set α), M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      ((J ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint J B) ∧ J ⊆ X) ∧
        ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → J ⊆ t → t ⊆ J
have refine_3 : X \ B' ∩ M.E ⊆ X
Tactic: refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
refine_1 : I' ⊆ X \ B' ∩ M.E
refine_2 : ∃ (B : Set α), M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B
refine_3 : X \ B' ∩ M.E ⊆ X
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      ((J ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint J B) ∧ J ⊆ X) ∧
        ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → J ⊆ t → t ⊆ J
have refine_4 : ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E
Tactic: refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B' ∩ M.E
have refine_1 : Disjoint I' B'
Tactic: rw [subset_inter_iff, and_iff_left hI'E, subset_diff, and_iff_right hI'X]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E
have refine_4 : ∀ ⦃t : Set α⦄,
  t ⊆ M.E → ∀ (x : Set α), M.IsBase x → Disjoint t x → t ⊆ X → X \ B' ∩ M.E ⊆ t → (t ⊆ X ∧ Disjoint t B') ∧ t ⊆ M.E
Tactic: simp only [subset_inter_iff, subset_diff, and_imp, forall_exists_index]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∀ ⦃t : Set α⦄,
    t ⊆ M.E → ∀ (x : Set α), M.IsBase x → Disjoint t x → t ⊆ X → X \ B' ∩ M.E ⊆ t → (t ⊆ X ∧ Disjoint t B') ∧ t ⊆ M.E
have refine_4 : ∀ (J : Set α) (hJE : J ⊆ M.E) (B'' : Set α) (hB'' : M.IsBase B'') (hdj : Disjoint J B'') (hJX : J ⊆ X)
  (hXJ : X \ B' ∩ M.E ⊆ J), Disjoint J B'
Tactic: refine fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ X ∪ B' \ X ⊆ B'
have rw : X \ B' ∩ B'' ⊆ J
Tactic: rw [union_subset_iff, and_iff_left diff_subset, ← union_diff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, diff_eq, ← inter_assoc,
        ← diff_eq, diff_subset_comm, diff_eq, inter_assoc, ← diff_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ Disjoint J B'
have hI' : B'' ∩ X ∪ B' \ X ⊆ B'
Tactic: have hI' : (B'' ∩ X) ∪ (B' \ X) ⊆ B' := by
      rw [union_subset_iff, and_iff_left diff_subset, ← union_diff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, diff_eq, ← inter_assoc,
        ← diff_eq, diff_subset_comm, diff_eq, inter_assoc, ← diff_eq, inter_comm]
      exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
⊢ Disjoint J B'
have refine_4 : ∀ (B₁ : Set α) (hB₁ : M.IsBase B₁) (hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁) (hB₁I : B₁ ⊆ B'' ∩ X ∪ B' \ X ∪ B''), Disjoint J B'
Tactic: obtain ⟨B₁, hB₁, hI'B₁, hB₁I⟩ := (hB'.indep.subset hI').exists_isBase_subset_union_isBase hB''
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∩ X ∪ B' \ X ∪ B''
⊢ Disjoint J B'
have hB₁I₁ : B₁ ⊆ B'' ∪ B' \ X
Tactic: rw [union_comm, ← union_assoc, union_eq_self_of_subset_right inter_subset_left] at hB₁I
Cleared hypotheses: hB₁I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
⊢ B₁ = B'
have refine : ∀ (e : α) (he : e ∈ B₁), e ∈ B'
Tactic: refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
⊢ e ∈ B'
have heB'' : e ∈ B''
Tactic: refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
⊢ e ∈ B'
have refine : ∀ (heX : e ∉ X), e ∈ B' \ X
Tactic: refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
heX : e ∉ X
⊢ e ∈ B' \ X
have refine : M.Indep (insert e (B' \ X))
Tactic: refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
⊢ Disjoint J B'
have refine_4 : ∀ (hB' : M.IsBase B₁) (hI : M.IsBasis (B₁ \ X) (M.E \ X)) (hIB' : B₁ \ X ⊆ B₁) (hB'IB : B₁ ⊆ B₁ \ X ∪ B)
  (hXJ : X \ B₁ ∩ M.E ⊆ J) (hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁) (hB₁I : B₁ ⊆ B'' ∪ B₁ \ X), Disjoint J B₁
Tactic: obtain rfl : B₁ = B' := by
      refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
      refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
      refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
      refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
      exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))
Cleared hypotheses: B', hB', hI, hIB', hB'IB, hXJ, hI', hI'B₁, hB₁I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
⊢ Disjoint J B₁
have refine_4 : ∀ (hdj' : ¬Disjoint J B₁), False
Tactic: by_contra hdj'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
⊢ False
have refine_4 : ∀ (e : α) (heJ : e ∈ J) (heB' : e ∈ B₁), False
Tactic: obtain ⟨e, heJ, heB'⟩ := not_disjoint_iff.mp hdj'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
⊢ False
have refine_4 : ∀ (heB'' : e ∈ B''), False
Tactic: obtain (heB'' | ⟨-, heX⟩) := hB₁I heB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
refine_4 : ∀ (heB'' : e ∈ B''), False
⊢ False
have refine_4₁ : ∀ (heX : e ∉ X), False
Tactic: obtain (heB'' | ⟨-, heX⟩) := hB₁I heB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B X : Set α
M : Matroid α
tauto tauto₁ tauto₂ : ∀ (I : Set α), (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) → I ⊆ M.E
⊢ ∀ (I : Set α), (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) → I ⊆ M.E
have tauto₃ : ∀ (I : Set α) ⦃a : α⦄, I ⊆ M.E → ∀ (w : Set α), M.IsBase w → Disjoint I w → a ∈ I → a ∈ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M✶.Indep I ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
have rw : (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
Tactic: rw [dual_indep_iff_exists', and_iff_right hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
rw : (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
⊢ M✶.Indep I ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
have rw₁ : (∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
Tactic: rw [dual_indep_iff_exists', and_iff_right hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
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
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have 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
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
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
have 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
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]