awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
iff_of_false (fun hi ↦ hI hi.subset_ground)
      (fun hi ↦ hI (hi.subset_ground.trans_eq hE.symm))

Premises used: LE.le.trans_eq, iff_of_false, Matroid.Indep.subset_ground, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
exact iff_of_false (fun hi ↦ hI hi.subset_ground)
      (fun hi ↦ hI (hi.subset_ground.trans_eq hE.symm))

Premises used: iff_of_false
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
h' : M₁.Indep = M₂.Indep
B : Set α
h_1 : B ⊆ M₁.E
simp_rw : Maximal M₁.Indep B ↔ Maximal M₂.Indep B
⊢ M₁.IsBase B ↔ M₂.IsBase B

Tactic:
simp_rw [isBase_iff_maximal_indep, h']

Premises used: Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
subst : M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)
⊢ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)

Tactic:
subst h
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ : Matroid α
⊢ M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
⊢ M₁ = M₂

Tactic:
ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩

Premises used: Iff.intro, Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
refine_1 : ∀ (I : Set α) (hIE : I ⊆ M₁.E) (hI : M₁.Indep I), M₂.Indep I
refine_2 : ∀ (I : Set α) (hIE : I ⊆ M₁.E) (hI : M₂.Indep I), M₁.Indep I
⊢ M₁ = M₂

Tactic:
refine ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩

Premises used: Iff.intro, Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
refine_1 : ∀ (B : Set α) (hB : M₁.IsBase B) (hIB : I ⊆ B), M₂.Indep I
⊢ M₂.Indep I

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
B : Set α
hB : M₁.IsBase B
hIB : I ⊆ B
⊢ M₂.Indep I

Tactic:
(hM₁ hB).subset hIB

Premises used: Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
B : Set α
hB : M₁.IsBase B
hIB : I ⊆ B
⊢ M₂.Indep I

Tactic:
exact (hM₁ hB).subset hIB

Premises used: Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
refine_2 : ∀ (B : Set α) (hB : M₂.IsBase B) (hIB : I ⊆ B), M₁.Indep I
⊢ M₁.Indep I

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
B : Set α
hB : M₂.IsBase B
hIB : I ⊆ B
⊢ M₁.Indep I

Tactic:
(hM₂ hB).subset hIB

Premises used: Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
B : Set α
hB : M₂.IsBase B
hIB : I ⊆ B
⊢ M₁.Indep I

Tactic:
exact (hM₂ hB).subset hIB

Premises used: Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
inst : M.Finitary
I : Set α
h : ∀ J ⊆ I, J.Finite → M.Indep J
⊢ M.Indep I

Tactic:
Finitary.indep_of_forall_finite I h

Premises used: Matroid.Finitary.indep_of_forall_finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
I : Set α
M : Matroid α
inst : M.Finitary
⊢ M.Indep I ↔ ∀ J ⊆ I, J.Finite → M.Indep J

Tactic:
⟨fun h _ hJI _ ↦ h.subset hJI, Finitary.indep_of_forall_finite I⟩

Premises used: Matroid.Finitary.indep_of_forall_finite, Matroid.Indep.subset, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B B' I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
⊢ M.Indep I

Tactic:
I.finite_or_infinite.elim (hI _ Subset.rfl) (fun h ↦ False.elim ?_)

Premises used: Set.finite_or_infinite, False.elim, Set.Subset.rfl, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B B' I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
refine : ∀ (h : I.Infinite), False
⊢ M.Indep I

Tactic:
refine I.finite_or_infinite.elim (hI _ Subset.rfl) (fun h ↦ False.elim ?_)

Premises used: Set.finite_or_infinite, False.elim, Set.Subset.rfl, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B B' I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
obtain : ∀ (B : Set α) (hB : M.IsBase B), False
⊢ False

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B_1 B' I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
obtain : ∀ (I₀ : Set α) (hI₀I : I₀ ⊆ I) (hI₀fin : I₀.Finite) (hI₀card : I₀.ncard = B.ncard + 1), False
⊢ False

Tactic:
obtain ⟨I₀, hI₀I, hI₀fin, hI₀card⟩ := h.exists_subset_ncard_eq (B.ncard + 1)

Premises used: HAdd.hAdd, Set.Infinite.exists_subset_ncard_eq, Set.ncard, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B_1 B' I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hI₀B' : I₀ ⊆ B'), False
⊢ False

Tactic:
obtain ⟨B', hB', hI₀B'⟩ := (hI _ hI₀I hI₀fin).exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B_1 B'_1 I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
⊢ I₀.ncard ≤ B'.ncard

Tactic:
have hle := ncard_le_ncard hI₀B' hB'.finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B_1 B'_1 I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : I₀.ncard ≤ B'.ncard
⊢ B.ncard < B.ncard

Tactic:
rw [hI₀card, hB'.ncard_eq_ncard_of_isBase hB, Nat.add_one_le_iff] at hle

Premises used: Matroid.IsBase.ncard_eq_ncard_of_isBase, Nat.add_one_le_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B_1 B'_1 I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard < B.ncard
⊢ False

Tactic:
hle.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 : Matroid α
B_1 B'_1 I_1 J D X : Set α
e f : α
M : Matroid α
inst : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard < B.ncard
⊢ False

Tactic:
exact hle.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X

Tactic:
M.maximality

Premises used: Matroid.maximality
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
x : Set α
simp_rw : M.Indep x ↔ ∃ (B : Set α), IsBase B ∧ x ⊆ B
simp_rw₁ : M.Indep x ↔ ∃ (B : Set α), M.IsBase B ∧ x ⊆ B
⊢ Indep x ↔ ∃ (B : Set α), IsBase B ∧ x ⊆ B

Tactic:
simp_rw [hI, hB, M.indep_iff]

Premises used: Matroid.indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
simp_rw : ∃ (B : Set α), M.IsBase B
⊢ ∃ (B : Set α), IsBase B

Tactic:
simp_rw [hB]
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ (B : Set α), M.IsBase B

Tactic:
M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ (B : Set α), M.IsBase B

Tactic:
exact M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (x : Set α), IsBase x = M.IsBase x

Tactic:
simp [hB]
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
simp_rw : ExchangeProperty M.IsBase
⊢ ExchangeProperty IsBase

Tactic:
simp_rw [show IsBase = M.IsBase from funext (by simp [hB])]

Premises used: funext
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ExchangeProperty M.IsBase

Tactic:
M.isBase_exchange

Premises used: Matroid.isBase_exchange
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ExchangeProperty M.IsBase

Tactic:
exact M.isBase_exchange

Premises used: Matroid.isBase_exchange
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (x : Set α), Indep x = M.Indep x

Tactic:
simp [hI]
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
simp_rw : ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
simp_rw [hE, show Indep = M.Indep from funext (by simp [hI])]

Premises used: funext
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X

Tactic:
M.maximality

Premises used: Matroid.maximality
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X

Tactic:
exact M.maximality

Premises used: Matroid.maximality
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
simp_rw : ∀ (B : Set α), M.IsBase B → B ⊆ M.E
⊢ ∀ (B : Set α), IsBase B → B ⊆ E

Tactic:
simp_rw [hE, hB]
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), M.IsBase B → B ⊆ M.E

Tactic:
M.subset_ground

Premises used: Matroid.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M_1 M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), M.IsBase B → B ⊆ M.E

Tactic:
exact M.subset_ground

Premises used: Matroid.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M.Indep I

Tactic:
hI.1.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M.Indep I

Tactic:
hI.1.1.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ I ⊆ X

Tactic:
hI.1.1.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M.IsBasis' I X

Tactic:
hI.1

Premises used: Matroid.IsBasis', And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
hX : X ⊆ M.E
⊢ M.IsBasis I X

Tactic:
⟨hI, hX⟩

Premises used: And.intro, Matroid.IsBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ I ⊆ X

Tactic:
hI.1.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ X ⊆ M.E

Tactic:
hI.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M.IsBasis I X

Tactic:
hI
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
h : X ∩ M.E = X
⊢ M.IsBasis I (X ∩ M.E)

Tactic:
convert! hI
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
h h₁ : X = X
⊢ X ∩ M.E = X

Tactic:
rw [inter_eq_self_of_subset_left hI.subset_ground]

Premises used: Matroid.IsBasis.subset_ground, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ I ⊆ M.E

Tactic:
hI.indep.subset_ground

Premises used: Matroid.Indep.subset_ground, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ I = J

Tactic:
hIJ.antisymm (hI.1.2 ⟨hJ, hJX⟩ hIJ)

Premises used: And.right, And.left, HasSubset.Subset.antisymm, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
inst : M.RankFinite
⊢ I.Finite

Tactic:
hI.indep.finite

Premises used: Matroid.Indep.finite, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
rw :
  ((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
⊢ M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Tactic:
rw [IsBasis, maximal_subset_iff]

Premises used: maximal_subset_iff, Matroid.IsBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
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
mpr₁₀ mpr₁₁ 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
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 α⦄, I ⊆ t → M.Indep t → t ⊆ X → I = t
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₁₇ :
  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
⊢ ((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

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Basic
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
rw₁ 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
⊢ M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
rw [isBasis_iff', and_iff_left hX]

Premises used: and_iff_left, Matroid.isBasis_iff'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hPQ : ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X
h : ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ (y : Set α), x ≤ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)

Tactic:
rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]

Premises used: Matroid.IsBasis', and_iff_left, maximal_iff_maximal_of_imp_of_forall, Matroid.IsBasis, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X

Tactic:
fun I hI ↦ ⟨hI.1, hI.2.trans inter_subset_left⟩

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X

Tactic:
exact fun I hI ↦ ⟨hI.1, hI.2.trans inter_subset_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ (y : Set α), x ≤ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E

Tactic:
fun I hI ↦ ⟨I, rfl.le, hI.1, subset_inter hI.2 hI.1.subset_ground⟩

Premises used: Eq.le, Matroid.Indep.subset_ground, Set.subset_inter, And.right, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ (y : Set α), x ≤ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E

Tactic:
exact fun I hI ↦ ⟨I, rfl.le, hI.1, subset_inter hI.2 hI.1.subset_ground⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
rw : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
rw₁ rw₂ : M.IsBasis I X ↔ M.IsBasis I X
⊢ M.IsBasis' I X ↔ M.IsBasis I X

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, inter_eq_self_of_subset_left hX]

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I X ↔ M.IsBasis' I X ∧ X ⊆ M.E

Tactic:
⟨fun h ↦ ⟨h.isBasis', h.subset_ground⟩, fun h ↦ (isBasis'_iff_isBasis h.2).mp h.1⟩

Premises used: Matroid.IsBasis.subset_ground, Matroid.IsBasis.isBasis', And.right, And.left, Matroid.isBasis'_iff_isBasis, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ M.IsBasis I (X ∩ M.E)

Tactic:
isBasis'_iff_isBasis_inter_ground.mp hIX

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ I = J

Tactic:
hIJ.antisymm (hI.2 ⟨hJ, hJX⟩ hIJ)

Premises used: And.right, HasSubset.Subset.antisymm, And.intro