awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
mp :
  ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E →
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
mpr :
  (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E →
    ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E
mp₁ mp₂ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
mp₃ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → M.Indep I
mp₄ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → I ⊆ X
mp₅ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J
mp₆ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → X ⊆ M.E
mpr₁ mpr₂ :
  X ⊆ M.E →
    M.Indep I →
      I ⊆ X →
        (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) →
          ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E
mpr₃ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → M.Indep I
mpr₄ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → I ⊆ X
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
have mpr₅ : X ⊆ M.E →
  M.Indep I →
    I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
mp :
  ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E →
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
mpr :
  (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E →
    ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E
mp₁ mp₂ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
mp₃ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → M.Indep I
mp₄ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → I ⊆ X
mp₅ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J
mp₆ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → X ⊆ M.E
mpr₁ mpr₂ :
  X ⊆ M.E →
    M.Indep I →
      I ⊆ X →
        (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) →
          ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E
mpr₃ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → M.Indep I
mpr₄ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → I ⊆ X
mpr₅ :
  X ⊆ M.E →
    M.Indep I →
      I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
have mpr₆ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → X ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
mp :
  ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E →
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
mpr :
  (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E →
    ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E
mp₁ mp₂ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
mp₃ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → M.Indep I
mp₄ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → I ⊆ X
mp₅ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J
mp₆ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → X ⊆ M.E
mpr₁ mpr₂ :
  X ⊆ M.E →
    M.Indep I →
      I ⊆ X →
        (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) →
          ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E
mpr₃ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → M.Indep I
mpr₄ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → I ⊆ X
mpr₅ :
  X ⊆ M.E →
    M.Indep I →
      I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t
mpr₆ : X ⊆ M.E → M.Indep I → I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → X ⊆ M.E
mp₇ mp₈ mp₉ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J
mpr₇ mpr₈ mpr₉ :
  X ⊆ M.E →
    M.Indep I →
      I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t
mp₁₀ mp₁₁ mp₁₂ :
  X ⊆ M.E →
    (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) →
      M.Indep I → I ⊆ X → ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
have mpr₁₀ : X ⊆ M.E →
  M.Indep I →
    I ⊆ X → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) → ∀ ⦃t : Set α⦄, I ⊆ t → M.Indep t → t ⊆ X → I = t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
have rw : (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E ↔
  M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
Tactic: rw [isBasis_iff', and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
rw :
  (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E ↔
    M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
⊢ M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
have rw₁ : (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ↔
  M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
Tactic: rw [isBasis_iff', and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)
have hPQ : ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X
Tactic: rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hPQ : ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)
have h : ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ (y : Set α), x ≤ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E
Tactic: rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis' I X ↔ M.IsBasis I X
have rw : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
Tactic: rw [isBasis'_iff_isBasis_inter_ground, inter_eq_self_of_subset_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
rw : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
⊢ M.IsBasis' I X ↔ M.IsBasis I X
have rw₁ : M.IsBasis I X ↔ M.IsBasis I X
Tactic: rw [isBasis'_iff_isBasis_inter_ground, inter_eq_self_of_subset_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
have rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
Tactic: rw [IsBasis, and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
⊢ M.IsBasis I X ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
have rw₁ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
Tactic: rw [IsBasis, and_iff_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ M.IsBasis I X
have rw : ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
Tactic: rw [isBasis_iff (by aesop_mat : X ⊆ M.E), and_iff_right hI, and_iff_right hIX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ M.IsBasis I Y
have rw : ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J
Tactic: rw [isBasis_iff (hYX.trans hI.subset_ground), and_iff_right hI.indep, and_iff_right hIY]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.IsBasis I I ↔ M.Indep I
have rw : M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E
Tactic: rw [isBasis_iff', and_iff_right rfl.subset, and_assoc, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis I ∅
have rw : M.IsBasis ∅ ∅
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
⊢ M.Dep Y
have this : X ⊆ M.E
Tactic: have : X ⊆ M.E := hI.subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ M.Dep Y
have rw : ¬M.Indep Y
Tactic: rw [← not_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : X ⊆ M.E
⊢ ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J
have obtain : ∀ (J : Set α) (hJ : I ⊆ J) (hJmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ X) J),
  ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J
Tactic: obtain ⟨J, hJ, hJmax⟩ := M.maximality X hX I hI hIX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ (J : Set α), M.IsBasis' J X ∧ I ⊆ J
have simp_rw : ∃ (J : Set α), M.IsBasis J (X ∩ M.E) ∧ I ⊆ J
Tactic: simp_rw [isBasis'_iff_isBasis_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
have obtain : ∀ (I : Set α) (hI : M.IsBasis I X), ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis X (hXY.trans hY)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
have obtain : ∀ (J : Set α) (hJ : M.IsBasis J Y) (hIJ : I ⊆ J), ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I
have obtain : ∀ (J : Set α) (hJ : M.IsBasis J Y) (hIJ : I ⊆ J), ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I
have refine : J ∩ X ⊆ I
Tactic: refine ⟨J, hJ, subset_antisymm ?_ (subset_inter hIJ hI.subset)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ B ∩ X ⊆ I
have rw : B ∩ X ⊆ B ∩ X
Tactic: rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
    inter_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBasis B M.E ↔ M.IsBase B
have rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
Tactic: rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
⊢ M.IsBasis B M.E ↔ M.IsBase B
have rw₁ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ M.IsBase B
Tactic: rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
rw₁ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ M.IsBase B
⊢ M.IsBasis B M.E ↔ M.IsBase B
have rw₂ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ Maximal M.Indep B
Tactic: rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
rw₁ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ M.IsBase B
rw₂ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ Maximal M.Indep B
⊢ M.IsBasis B M.E ↔ M.IsBase B
have rw₃ : Maximal M.Indep B ∧ B ⊆ M.E ↔ Maximal M.Indep B
Tactic: rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
rw₁ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ M.IsBase B
rw₂ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ Maximal M.Indep B
rw₃ : Maximal M.Indep B ∧ B ⊆ M.E ↔ Maximal M.Indep B
⊢ M.IsBasis B M.E ↔ M.IsBase B
have rw₄ : Maximal M.Indep B ↔ Maximal M.Indep B
Tactic: rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
have rw : ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
Tactic: rw [IsBasis, maximal_iff_forall_insert (fun I J hI hIJ ↦ ⟨hI.1.subset hIJ, hIJ.trans hI.2⟩)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
have simp : (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Tactic: simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, mem_diff, and_imp,
    Dep, hI.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I
have simp_rw : e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
Tactic: simp_rw [hI.isBasis_iff_forall_insert_dep (subset_insert _ _), dep_iff, insert_subset_iff,
    and_iff_left hI.subset_ground, mem_diff, mem_insert_iff, or_and_right, and_not_self,
    or_false, and_imp, forall_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
have mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
Tactic: tauto