awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
have neg : ∀ (e : α) (he : e ∈ B \ B') (hBase : M.IsBase (insert e (B' \ {x}))), ∃ e ∈ B \ I, M.Indep (insert e I)
Tactic: obtain ⟨e, he, hBase⟩ := hB'.exchange hB ⟨hxB', hxB⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hInotmax : ¬Maximal M.Indep I
hB : Maximal M.Indep B
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)
have hB₁ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
Tactic: simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax
Cleared hypotheses: hInotmax, hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hInotmax : ¬Maximal M.Indep I
hB : Maximal M.Indep B
hB₁ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)
have hInotmax₁ : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
Tactic: simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax
Cleared hypotheses: hInotmax, hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)
have refine_1 : ∀ (hIb : M.IsBase I), False
Tactic: refine hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
refine_1 : ∀ (hIb : M.IsBase I), False
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)
have refine_2 : M.IsBase B
Tactic: refine hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False
have refine_1 : ∀ (I' : Set α) (hII' : M.Indep I') (hI' : I ⊆ I') (hne : ¬I = I'), False
Tactic: obtain ⟨I', hII', hI', hne⟩ := hInotmax
Cleared hypotheses: hInotmax
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
⊢ M.IsBase B
have by_contra : ∀ (hnb : ¬M.IsBase B), False
Tactic: by_contra hnb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
⊢ False
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B'), False
Tactic: obtain ⟨B', hB'⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
⊢ False
have obtain : ∀ (e : α) (he : e ∈ B' \ B) (h : M.Indep (insert e B)), False
Tactic: obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_isBase hnb hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
⊢ M₁.Indep = M₂.Indep
have h₁ : ∀ (I : Set α), M₁.Indep I ↔ M₂.Indep I
Tactic: ext I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 α
⊢ M₁.Indep I ↔ M₂.Indep I
have pos : ∀ (hI : I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
Tactic: by_cases hI : I ⊆ M₁.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 α
pos : ∀ (hI : I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
⊢ M₁.Indep I ↔ M₂.Indep I
have neg : ∀ (hI : ¬I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
Tactic: by_cases hI : I ⊆ M₁.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
have pos : M₂.Indep I ↔ M₂.Indep I
Tactic: rwa [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ M₁.IsBase B ↔ M₂.IsBase B
have simp_rw : Maximal M₁.Indep B ↔ Maximal M₂.Indep B
Tactic: simp_rw [isBase_iff_maximal_indep, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
have subst : M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)
Tactic: subst h
Cleared hypotheses: M₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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₂
have refine_1 : ∀ (I : Set α) (hIE : I ⊆ M₁.E) (hI : M₁.Indep I), M₂.Indep I
Tactic: refine ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ M₁ = M₂
have refine_2 : ∀ (I : Set α) (hIE : I ⊆ M₁.E) (hI : M₂.Indep I), M₁.Indep I
Tactic: refine ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ M₂.Indep I
have refine_1 : ∀ (B : Set α) (hB : M₁.IsBase B) (hIB : I ⊆ B), M₂.Indep I
Tactic: obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ M₁.Indep I
have refine_2 : ∀ (B : Set α) (hB : M₂.IsBase B) (hIB : I ⊆ B), M₁.Indep I
Tactic: obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
have refine : ∀ (h : I.Infinite), False
Tactic: refine I.finite_or_infinite.elim (hI _ Subset.rfl) (fun h ↦ False.elim ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ False
have obtain : ∀ (B : Set α) (hB : M.IsBase B), False
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ False
have obtain : ∀ (I₀ : Set α) (hI₀I : I₀ ⊆ I) (hI₀fin : I₀.Finite) (hI₀card : I₀.ncard = B.ncard + 1), False
Tactic: obtain ⟨I₀, hI₀I, hI₀fin, hI₀card⟩ := h.exists_subset_ncard_eq (B.ncard + 1)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ False
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hI₀B' : I₀ ⊆ B'), False
Tactic: obtain ⟨B', hB', hI₀B'⟩ := (hI _ hI₀I hI₀fin).exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
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'
⊢ False
have hle : I₀.ncard ≤ B'.ncard
Tactic: have hle := ncard_le_ncard hI₀B' hB'.finite
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (hypothesis)
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
⊢ False
have hle₁ : B.ncard < B.ncard
Tactic: rw [hI₀card, hB'.ncard_eq_ncard_of_isBase hB, Nat.add_one_le_iff] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 ↔ ∃ (B : Set α), IsBase B ∧ x ⊆ B
have simp_rw : M.Indep x ↔ ∃ (B : Set α), IsBase B ∧ x ⊆ B
Tactic: simp_rw [hI, hB, M.indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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
⊢ Indep x ↔ ∃ (B : Set α), IsBase B ∧ x ⊆ B
have simp_rw₁ : M.Indep x ↔ ∃ (B : Set α), M.IsBase B ∧ x ⊆ B
Tactic: simp_rw [hI, hB, M.indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 α), IsBase B
have simp_rw : ∃ (B : Set α), M.IsBase B
Tactic: simp_rw [hB]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 IsBase
have simp_rw : ExchangeProperty M.IsBase
Tactic: simp_rw [show IsBase = M.IsBase from funext (by simp [hB])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 ⊆ E, ExistsMaximalSubsetProperty Indep X
have simp_rw : ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
Tactic: simp_rw [hE, show Indep = M.Indep from funext (by simp [hI])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
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 α), IsBase B → B ⊆ E
have simp_rw : ∀ (B : Set α), M.IsBase B → B ⊆ M.E
Tactic: simp_rw [hE, hB]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M.IsBasis I (X ∩ M.E)
have h : X ∩ M.E = X
Tactic: convert! hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ X ∩ M.E = X
have h : X = X
Tactic: rw [inter_eq_self_of_subset_left hI.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
have 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
Tactic: rw [IsBasis, maximal_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ((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 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
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
⊢ ((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 : (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
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
⊢ ((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 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
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
⊢ ((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 mp₃ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → M.Indep I
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
⊢ ((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 mp₄ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → I ⊆ X
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
⊢ ((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 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
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
⊢ ((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 mp₆ : X ⊆ M.E → (∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) → M.Indep I → I ⊆ X → 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
⊢ ((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) →
        ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ 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
⊢ ((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) → M.Indep I
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
⊢ ((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) → I ⊆ X
Tactic: tauto