awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Basic (goal)
Goal:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun (M : Matroid α) ↦ (M.E, {B : Set α | M.IsBase B})
hf : Function.Injective f
⊢ (f '' {M : Matroid α | M.E ⊆ E}).Finite
have refine : f '' {M : Matroid α | M.E ⊆ E} ⊆
  SProd.sprod (α := Set (Set α)) (β := Set (Set (Set α))) {b : Set α | b ⊆ E}
    {b : Set (Set α) | b ⊆ {b : Set α | b ⊆ E}}
Tactic: refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
have simp_rw : Minimal M.Dep C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
Tactic: simp_rw [isCircuit_def, minimal_subset_iff, eq_comm (a := C)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
simp_rw : Minimal M.Dep C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
have simp_rw₁ : (M.Dep C ∧ ∀ ⦃t : Set α⦄, M.Dep t → t ⊆ C → C = t) ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
Tactic: simp_rw [isCircuit_def, minimal_subset_iff, eq_comm (a := C)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ M.Indep X
have rw : ¬M.Dep X
Tactic: rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun (x : Set α) ↦ ¬M.Indep x) C
have simp_rw : ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t
Tactic: simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
have rw : M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)
Tactic: rw [IsCircuit, minimal_iff_forall_ssubset, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
have inr : ∀
  (this :
    ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
  (hCE : ¬C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
Tactic: wlog hCE : C ⊆ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
inr :
  ∀
    (this :
      ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E),
        M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
    (hCE : ¬C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
have wlog : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
Tactic: wlog hCE : C ⊆ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ M.IsCircuit (insert e I)
have rw : ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})
Tactic: rw [isCircuit_iff_dep_forall_diff_singleton_indep, hI.insert_dep_iff, and_iff_right ⟨he, heI⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ M.Indep (insert e I \ {f})
have inr : e ∈ M.E \ M.closure (I \ {f})
Tactic: rw [← insert_diff_singleton_comm (by rintro rfl; contradiction),
    (hI.diff _).insert_indep_iff_of_notMem (by simp [heI])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ M.IsCircuit (insert e I)
have refine : ∀ (heI : e ∈ I), False
Tactic: refine hI.insert_isCircuit_of_forall (fun heI ↦ ?_) he h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
⊢ False
have obtain : ∀ (f : α) (hf : f ∈ I) (hne : f ≠ e), False
Tactic: obtain ⟨f, hf, hne⟩ := hInt.exists_ne e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C
have nth_rw : M.IsBasis (C \ {e}) (insert e C)
Tactic: nth_rw 2 [← insert_eq_of_mem he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e C)
have rw : M.Dep C ∨ e ∈ C \ {e}
Tactic: rw [← insert_diff_singleton, (hC.diff_singleton_indep he).isBasis_insert_iff,
    insert_diff_singleton, insert_eq_of_mem he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}
have refine_1 : ∀ (h : M.IsBasis I C), ∃ e ∈ C, I = C \ {e}
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
refine_1 : ∀ (h : M.IsBasis I C), ∃ e ∈ C, I = C \ {e}
⊢ M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}
have refine_2 : (∃ e ∈ C, I = C \ {e}) → M.IsBasis I C
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ ∃ e ∈ C, I = C \ {e}
have refine_1 : ∀ (e : α) (he : e ∈ C ∧ e ∉ I), ∃ e ∈ C, I = C \ {e}
Tactic: obtain ⟨e, he⟩ := exists_of_ssubset
      (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I
have rw : (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
Tactic: rw [hC.isBasis_iff_eq_diff_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
have refine_1 : (∃ e ∈ C, I = C \ {e}) → ∀ (e : α) (he : e ∈ C) (hI : I = C \ {e}), C = insert e I
Tactic: refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
    fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
refine_1 : (∃ e ∈ C, I = C \ {e}) → ∀ (e : α) (he : e ∈ C) (hI : I = C \ {e}), C = insert e I
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
have refine_2 : (∃ e ∈ C \ I, C = insert e I) → ∀ (e : α) (he : e ∈ C \ I) (hC : C = insert e I), I = C \ {e}
Tactic: refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
    fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I
have refine_1 : C = insert e (C \ {e})
Tactic: rw [hI, insert_diff_singleton, insert_eq_of_mem he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
refine_1 : C = insert e (C \ {e})
⊢ C = insert e I
have refine_1₁ : C = insert e C
Tactic: rw [hI, insert_diff_singleton, insert_eq_of_mem he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
refine_1 : C = insert e (C \ {e})
refine_1₁ : C = insert e C
⊢ C = insert e I
have refine_1₂ : C = C
Tactic: rw [hI, insert_diff_singleton, insert_eq_of_mem he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC_1 : M.IsCircuit C
h : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}
have refine_2 : I = insert e I \ {e}
Tactic: rw [hC, insert_diff_self_of_notMem he.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC_1 : M.IsCircuit C
h : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
refine_2 : I = insert e I \ {e}
⊢ I = C \ {e}
have refine_2₁ : I = I
Tactic: rw [hC, insert_diff_self_of_notMem he.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hC : M.IsCircuit C
hCR : C ⊆ R
⊢ (M ↾ R).IsCircuit C
have simp_rw : ∀ (hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C),
  (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C
Tactic: simp_rw [isCircuit_iff, restrict_dep_iff, dep_iff, and_imp] at *
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R
have refine : (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R
Tactic: refine ⟨?_, fun h ↦ h.1.isCircuit_restrict_of_subset h.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R
have simp_rw : ¬M.Indep C →
  C ⊆ R →
    (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
      ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R
Tactic: simp_rw [isCircuit_iff, restrict_dep_iff, and_imp, dep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) =
    insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
have simp_rw : insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) = insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
Tactic: simp_rw [closure_subset_closure_iff_subset_closure
    (show {e} ⊆ M.E by simpa using mem_ground_of_mem_closure he), singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) = insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
have rw : Eq (α := Set α) (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
  (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
Tactic: rw [inter_eq_self_of_subset_right (sInter_subset_of_mem (by simpa))]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ M.fundCircuit e X = {e}
have suffices : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
Tactic: suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ M.fundCircuit e X = {e}
have suffices : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
Tactic: suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
have simp_rw : ∀ a ∈ X, (∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t) → a = e
Tactic: simp_rw [← M.closure_inter_ground {e}, singleton_inter_eq_empty.2 heX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ M.IsCircuit (M.fundCircuit e I)
have aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
Tactic: have aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I := sInter_subset_of_mem (by simpa)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (M.fundCircuit e I)
have rw : M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
Tactic: rw [fundCircuit_eq_sInter hecl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
have refine_1 : e ∉ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}
Tactic: refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
refine_1 : e ∉ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}
⊢ M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
have refine_2 : e ∈ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
Tactic: refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
refine_1 : e ∉ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}
refine_2 : e ∈ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
⊢ M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
have refine_3 : ∀ (f : α),
  Membership.mem (γ := Set α) (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) f →
    e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})
Tactic: refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
have refine_2 : Membership.mem (γ := Set α)
  (⋂ (J : Set α), ⋂ (_ : Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} J), M.closure J) e
Tactic: rw [hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (f : α),
    Membership.mem (γ := Set α) (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) f →
      e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})
have refine_3 : ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})
Tactic: simp only [mem_sInter, mem_setOf_eq, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})
have inl : ∀ (hecl : x ∈ M.closure I) (heI : x ∉ I), x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})
Tactic: obtain rfl | hne := eq_or_ne x e
Cleared hypotheses: e, hecl, heI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
inl : ∀ (hecl : x ∈ M.closure I) (heI : x ∉ I), x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})
have inr : ∀ (hne : x ≠ e), x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})
Tactic: obtain rfl | hne := eq_or_ne x e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})
have inr : (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})
Tactic: suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x}) by
    simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm,
      (hI.diff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})
have inr : ∀ (h : e ∉ M.closure (I \ {x})) (J : Set α) (hJ : J ⊆ I) (heJ : e ∈ M.closure J) (hxJ : x ∉ J), e ∈ M.closure (I \ {x})
Tactic: refine ⟨fun h hecl ↦ (h _ diff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
⊢ C = M.fundCircuit e I
have inl : ∀ (hCI : C ⊆ I), C = M.fundCircuit e I
Tactic: obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
inl : ∀ (hCI : C ⊆ I), C = M.fundCircuit e I
⊢ C = M.fundCircuit e I
have inr : ∀ (heC : e ∈ C) (hCeI : C \ {e} ⊆ I), C = M.fundCircuit e I
Tactic: obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ C = M.fundCircuit e I
have refine_1 : e ∈ M.closure I
Tactic: refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
refine_1 : e ∈ M.closure I
⊢ C = M.fundCircuit e I
have refine_2 : ∀ (heI : e ∈ I), False
Tactic: refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I
have refine_1 : M.Dep (insert e I) ∨ e ∈ I
Tactic: rw [hI.mem_closure_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
⊢ C = M.fundCircuit e I
have inr : M.fundCircuit e I ⊆ C
Tactic: suffices hss : M.fundCircuit e I ⊆ C by
    refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss
    · rw [hI.mem_closure_iff]
      exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))
    exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
⊢ M.fundCircuit e I ⊆ C
have heCcl : e ∈ M.closure (C \ {e})
Tactic: have heCcl := (hC.diff_singleton_isBasis heC).subset_closure heC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
⊢ M.fundCircuit e I ⊆ C
have heI : e ∈ M.closure I
Tactic: have heI : e ∈ M.closure I := M.closure_subset_closure hCeI heCcl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ M.fundCircuit e I ⊆ C
have inr : insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C
Tactic: rw [fundCircuit_eq_sInter heI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C
have inr : Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} (C \ {e})
Tactic: refine insert_subset heC <| (sInter_subset_of_mem (t := C \ {e}) ?_).trans diff_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I
have simp_rw : insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
Tactic: simp_rw [fundCircuit, M.restrict_closure_eq (R := R) (X := {e}) (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
have a : insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
a :
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
have a₁ : insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) ⊆
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
have a : ∀ (J : Set α) (hJI : J ⊆ I), M.closure {e} ⊆ M.closure J → M.closure {e} ∩ R ⊆ (M ↾ R).closure J
Tactic: gcongr 5 with J hJI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J
have a : M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E
Tactic: simp only [restrict_closure_eq']