awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
⊢ ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
have refine : ∀ {I J : Set α} (hI : Indep I) (hJ : Indep J) (hIJ : I.encard < J.encard), I.ncard < J.ncard
Tactic: refine fun {I J} hI hJ hIJ ↦ indep_aug hI hJ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I J : Set α
hI : Indep I
hJ : Indep J
hIJ : I.encard < J.encard
⊢ I.ncard < J.ncard
have rwa : LT.lt (α := ℕ∞) (↑I.ncard : ℕ∞) (↑J.ncard : ℕ∞)
Tactic: rwa [← Nat.cast_lt (α := ℕ∞), (hE.subset (subset_ground hJ)).cast_ncard_eq,
        (hE.subset (subset_ground hI)).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I J : Set α
hI : Indep I
hJ : Indep J
hIJ : I.encard < J.encard
rwa : LT.lt (α := ℕ∞) (↑I.ncard : ℕ∞) (↑J.ncard : ℕ∞)
⊢ I.ncard < J.ncard
have rwa₁ : (↑I.ncard : ℕ∞) < J.encard
Tactic: rwa [← Nat.cast_lt (α := ℕ∞), (hE.subset (subset_ground hJ)).cast_ncard_eq,
        (hE.subset (subset_ground hI)).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ (↑E.ncard : ℕ∞)
have rw : I.encard ≤ E.encard
Tactic: rw [hE.cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : I.ncard < J.ncard
⊢ ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)
have hIJ₁ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
Tactic: rw [ncard_eq_toFinset_card _ hIfin, ncard_eq_toFinset_card _ hJfin] at hIJ
Cleared hypotheses: hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
⊢ ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)
have aug : ∃ e ∈ hJfin.toFinset (s := J), e ∉ hIfin.toFinset (s := I) ∧ Indep (insert e (hIfin.toFinset (s := I)))
Tactic: have aug := indep_aug (hI _ (by simp)) (hJ _ (by simp)) hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
aug : ∃ e ∈ hJfin.toFinset (s := J), e ∉ hIfin.toFinset (s := I) ∧ Indep (insert e (hIfin.toFinset (s := I)))
⊢ ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)
have aug₁ : ∃ e ∈ J, e ∉ I ∧ Indep (insert e (hIfin.toFinset (s := I)))
Tactic: simp only [Finite.mem_toFinset] at aug
Cleared hypotheses: aug
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
aug : ∃ e ∈ J, e ∉ I ∧ Indep (insert e (hIfin.toFinset (s := I)))
⊢ ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)
have obtain : ∀ (e : α) (heJ : e ∈ J) (heI : e ∉ I) (hi : Indep (insert e (hIfin.toFinset (s := I)))),
  ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)
Tactic: obtain ⟨e, heJ, heI, hi⟩ := aug
Cleared hypotheses: aug
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
have obtain : ∀ (M : Matroid α) (h : ∀ (I : Set α), M.Indep I ↔ Indep I), ∃ (M_1 : Matroid α), M.E = M_1.E ∧ M_1.Indep = Indep
Tactic: obtain ⟨M, rfl, h⟩ := hM
Cleared hypotheses: E, hM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
⊢ Indep ∅
have obtain : ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I), M.Indep ∅
Tactic: obtain ⟨M, -, rfl⟩ := hex
Cleared hypotheses: Indep, hM, hex
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
⊢ ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
have obtain : ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I) ⦃I J : Set α⦄,
  M.Indep J → I ⊆ J → M.Indep I
Tactic: obtain ⟨M, -, rfl⟩ := hex
Cleared hypotheses: Indep, hM, hex
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
⊢ ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
have obtain : ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I) ⦃I B : Set α⦄,
  M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)
Tactic: obtain ⟨M, -, rfl⟩ := hex
Cleared hypotheses: Indep, hM, hex
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X
have obtain : ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I),
  ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
Tactic: obtain ⟨M, rfl, rfl⟩ := hex
Cleared hypotheses: E, Indep, hM, hex
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
⊢ ∀ (I : Set α), Indep I → I ⊆ E
have obtain : ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I) (I : Set α),
  M.Indep I → I ⊆ M.E
Tactic: obtain ⟨M, rfl, rfl⟩ := hex
Cleared hypotheses: E, Indep, hM, hex
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ ∃ (B : Set α), IsBase B
have obtain : ∀ (B : Set α) (h : IsBase B ∧ B.Finite), ∃ (B : Set α), IsBase B
Tactic: obtain ⟨B, h⟩ := exists_finite_base
Cleared hypotheses: exists_finite_base
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X
have obtain : ∀ (B : Set α) (hB : IsBase B) (hfin : B.Finite),
  ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X
Tactic: obtain ⟨B, hB, hfin⟩ := exists_finite_base
Cleared hypotheses: exists_finite_base
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X
have refine : ∀ X ⊆ E,
  ∀ (Y : Set α),
    (∃ (B : Set α), IsBase B ∧ Y ⊆ B) → ∀ (B' : Set α) (hB' : IsBase B') (hYB' : Y ⊆ B'), Y.encard ≤ (↑B.ncard : ℕ∞)
Tactic: refine fun X _ ↦ Matroid.existsMaximalSubsetProperty_of_bdd
      ⟨B.ncard, fun Y ⟨B', hB', hYB'⟩ ↦ ?_⟩ X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
h : X ⊆ E
Y : Set α
h_1 : ∃ (B : Set α), IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
⊢ Y.encard ≤ (↑B.ncard : ℕ∞)
have rw : Y.encard ≤ B'.encard
Tactic: rw [hfin.cast_ncard_eq, isBase_exchange.encard_isBase_eq hB hB']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).RankFinite
have obtain : ∀ (B : Set α) (hB : IsBase B) (hfin : B.Finite),
  (Matroid.ofExistsFiniteIsBase E IsBase sorry isBase_exchange subset_ground).RankFinite
Tactic: obtain ⟨B, hB, hfin⟩ := exists_finite_base
Cleared hypotheses: exists_finite_base
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
have tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
Tactic: tfae_have 1 ↔ 2 := Iff.rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
have tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
Tactic: tfae_have 2 ↔ 3 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e),
    isCircuit_def, minimal_iff_forall_ssubset, ssubset_singleton_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
have tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
Tactic: tfae_have 2 ↔ 4 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B
have simp : ¬M.Indep {e} ∧ e ∈ M.E ↔ (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
Tactic: simp only [dep_iff, singleton_subset_iff, mem_diff, forall_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ ¬M.Indep {e} ∧ e ∈ M.E ↔ (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
have refine : ∀ (h : (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x) (hi : M.Indep {e}), False
Tactic: refine ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩,
      fun h ↦ ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
hi : M.Indep {e}
⊢ False
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (heB : {e} ⊆ B), False
Tactic: obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
have tfae_4_iff_5 : M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B
Tactic: tfae_have 4 ↔ 5 := by
    simp only [dep_iff, singleton_subset_iff, mem_diff, forall_and]
    refine ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩,
      fun h ↦ ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩
    obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset
    exact h.2 _ hB (by simpa using heB)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.Indep {e} ↔ M.IsLoop e
have rw : ¬M.Indep {e} ↔ M.Dep {e}
Tactic: rw [← singleton_dep, ← not_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : ¬M.Indep {e} ↔ M.Dep {e}
⊢ ¬M.Indep {e} ↔ M.IsLoop e
have rw₁ : ¬M.Indep {e} ↔ ¬M.Indep {e}
Tactic: rw [← singleton_dep, ← not_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
have simp_rw : (∀ (B : Set α), M.IsBase B → e ∈ M.E \ B) ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
Tactic: simp_rw [isLoop_iff_forall_mem_compl_isBase, mem_diff, and_iff_right he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
simp_rw : (∀ (B : Set α), M.IsBase B → e ∈ M.E \ B) ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
have simp_rw₁ : (∀ (B : Set α), M.IsBase B → e ∈ M.E ∧ e ∉ B) ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
Tactic: simp_rw [isLoop_iff_forall_mem_compl_isBase, mem_diff, and_iff_right he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
he : M.IsLoop e
hC : M.IsCircuit C
h : e ∈ C
⊢ C = {e}
have rw : C = C
Tactic: rw [he.isCircuit.eq_of_subset_isCircuit hC (singleton_subset_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis I X ↔ I = ∅
have refine : ∀ (h : M.IsBasis I X), I = ∅
Tactic: refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
⊢ I = ∅
have this : M.IsBasis I M.loops
Tactic: have := (closure_eq_loops_of_subset hX) ▸ h.isBasis_closure_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
⊢ M.IsLoop e
have rw : e ∈ M.loops
Tactic: rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
rw : e ∈ M.loops
⊢ M.IsLoop e
have rw₁ : e ∈ M.closure ∅
Tactic: rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
rw : e ∈ M.loops
rw₁ : e ∈ M.closure ∅
⊢ M.IsLoop e
have rw₂ : {e} ⊆ M.closure ∅
Tactic: rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
rw : e ∈ M.loops
rw₁ : e ∈ M.closure ∅
rw₂ : {e} ⊆ M.closure ∅
⊢ M.IsLoop e
have rw₃ : M.closure {e} ⊆ M.closure ∅
Tactic: rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
rw : e ∈ M.loops
rw₁ : e ∈ M.closure ∅
rw₂ : {e} ⊆ M.closure ∅
rw₃ : M.closure {e} ⊆ M.closure ∅
⊢ M.IsLoop e
have rw₄ : M.loops ⊆ M.closure ∅
Tactic: rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
rw : e ∈ M.loops
rw₁ : e ∈ M.closure ∅
rw₂ : {e} ⊆ M.closure ∅
rw₃ : M.closure {e} ⊆ M.closure ∅
rw₄ : M.loops ⊆ M.closure ∅
⊢ M.IsLoop e
have rw₅ : M.closure ∅ ⊆ M.closure ∅
Tactic: rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ M.closure {e} = M.loops
have rw : M.closure {e} = M.loops ∧ e ∈ M.E ↔ M.closure {e} = M.loops
Tactic: rw [isLoop_iff_closure_eq_loops_and_mem_ground, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : M.closure {e} = M.loops ∧ e ∈ M.E ↔ M.closure {e} = M.loops
⊢ M.IsLoop e ↔ M.closure {e} = M.loops
have rw₁ : M.closure {e} = M.loops ↔ M.closure {e} = M.loops
Tactic: rw [isLoop_iff_closure_eq_loops_and_mem_ground, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∪ M.loops) = M.closure X
have rw : M.closure (X ∪ M.closure ∅) = M.closure X
Tactic: rw [← closure_empty, closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X ∪ M.closure ∅) = M.closure X
⊢ M.closure (X ∪ M.loops) = M.closure X
have rw₁ : M.closure (X ∪ ∅) = M.closure X
Tactic: rw [← closure_empty, closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X ∪ M.closure ∅) = M.closure X
rw₁ : M.closure (X ∪ ∅) = M.closure X
⊢ M.closure (X ∪ M.loops) = M.closure X
have rw₂ : M.closure X = M.closure X
Tactic: rw [← closure_empty, closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X \ M.loops) = M.closure X
have rw : M.closure (X \ M.loops ∪ M.loops) = M.closure X
Tactic: rw [← M.closure_union_loops_eq (X \ M.loops), diff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X \ M.loops ∪ M.loops) = M.closure X
⊢ M.closure (X \ M.loops) = M.closure X
have rw₁ : M.closure (X ∪ M.loops) = M.closure X
Tactic: rw [← M.closure_union_loops_eq (X \ M.loops), diff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X \ M.loops ∪ M.loops) = M.closure X
rw₁ : M.closure (X ∪ M.loops) = M.closure X
⊢ M.closure (X \ M.loops) = M.closure X
have rw₂ : M.closure (X ∪ M.closure ∅) = M.closure X
Tactic: rw [← M.closure_union_loops_eq (X \ M.loops), diff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X \ M.loops ∪ M.loops) = M.closure X
rw₁ : M.closure (X ∪ M.loops) = M.closure X
rw₂ : M.closure (X ∪ M.closure ∅) = M.closure X
⊢ M.closure (X \ M.loops) = M.closure X
have rw₃ : M.closure (X ∪ ∅) = M.closure X
Tactic: rw [← M.closure_union_loops_eq (X \ M.loops), diff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X \ M.loops ∪ M.loops) = M.closure X
rw₁ : M.closure (X ∪ M.loops) = M.closure X
rw₂ : M.closure (X ∪ M.closure ∅) = M.closure X
rw₃ : M.closure (X ∪ ∅) = M.closure X
⊢ M.closure (X \ M.loops) = M.closure X
have rw₄ : M.closure X = M.closure X
Tactic: rw [← M.closure_union_loops_eq (X \ M.loops), diff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E
have rw : (M ↾ R).closure ∅ = M.loops ∩ R ∪ R \ M.E
Tactic: rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
rw : (M ↾ R).closure ∅ = M.loops ∩ R ∪ R \ M.E
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E
have rw₁ : (M ↾ R).closure ∅ = M.closure ∅ ∩ R ∪ R \ M.E
Tactic: rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]