awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.closure (J ∩ R) ∩ R ∪ R \ M.E
have a : M.closure {e} ⊆ M.closure (J ∩ R)
Tactic: refine (inter_subset_inter_left _ ?_).trans subset_union_left
-- 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} ⊆ M.closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})
have a : ∀ (J : Set α) (hJI : J ⊆ I), M.closure {e} ∩ R ⊆ (M ↾ R).closure J → M.closure {e} ⊆ M.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} ∩ R ⊆ (M ↾ R).closure J
⊢ M.closure {e} ⊆ M.closure J
have a : {e} ⊆ M.closure J
Tactic: refine closure_subset_closure_of_subset_closure ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
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} ∩ R ⊆ (M ↾ R).closure J
⊢ {e} ⊆ M.closure J
have heJ₁ : M.closure {e} ∩ R ⊆ M.closure J ∩ R
Tactic: rw [restrict_closure_eq _ (hJI.trans hIR) hR] at heJ
Cleared hypotheses: heJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
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} ∩ R ⊆ M.closure J ∩ R
⊢ {e} ⊆ M.closure J
have heJ₁ : M.closure {e} ∩ R ⊆ M.closure J
Tactic: simp only [subset_inter_iff, inter_subset_right, and_true] at heJ
Cleared hypotheses: heJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
⊢ M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
have refine : ∀ (h : M.closure A ⊆ B ∪ univ \ M.E), M.closure A ⊆ B
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ M.closure A ⊆ B
have refine : (B ∪ univ \ M.E) ∩ M.E ⊆ B
Tactic: refine (subset_inter h (M.closure_subset_ground A)).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I
have aux : ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
Tactic: have aux (A B) : M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B := by
    refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
    refine (subset_inter h (M.closure_subset_ground A)).trans ?_
    simp [union_inter_distrib_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
⊢ ∃ C ⊆ X, M.IsCircuit C
have obtain : ∀ (I : Set α) (hI : M.IsBasis I X), ∃ C ⊆ X, M.IsCircuit C
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
⊢ ∃ C ⊆ X, M.IsCircuit C
have obtain : ∀ (e : α) (heX : e ∈ X) (heI : e ∉ I), ∃ C ⊆ X, M.IsCircuit C
Tactic: obtain ⟨e, heX, heI⟩ := exists_of_ssubset
    (hI.subset.ssubset_of_ne (by rintro rfl; exact hI.indep.not_dep hX))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E
have simp_rw : ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E
Tactic: simp_rw [indep_iff_not_dep, dep_iff_superset_isCircuit']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C
have rw : (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E ↔ ∀ C ⊆ I, ¬M.IsCircuit C
Tactic: rw [indep_iff_forall_subset_not_isCircuit', and_iff_left hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
rw : (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E ↔ ∀ C ⊆ I, ¬M.IsCircuit C
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C
have rw₁ : (∀ C ⊆ I, ¬M.IsCircuit C) ↔ ∀ C ⊆ I, ¬M.IsCircuit C
Tactic: rw [indep_iff_forall_subset_not_isCircuit', and_iff_left hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.closure (C \ {e}) = M.closure C
have rw : M.closure C = M.closure C
Tactic: rw [(hC.diff_singleton_isBasis he).closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∉ C
⊢ M.closure (C \ {e}) = M.closure C
have rw : M.closure C = M.closure C
Tactic: rw [diff_singleton_eq_self he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure (C \ {e})
have rw : C ⊆ M.closure C
Tactic: rw [hC.closure_diff_singleton_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
⊢ M₁ = M₂
have h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
Tactic: have h' {C} : M₁.IsCircuit C ↔ M₂.IsCircuit C :=
    (em (C ⊆ M₁.E)).elim (h (C := C)) (fun hC ↦ iff_of_false (mt IsCircuit.subset_ground hC)
      (mt IsCircuit.subset_ground fun hss ↦ hC (hss.trans_eq hE.symm)))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
⊢ M₁ = M₂
have refine : ∀ (I : Set α) (hI : I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
Tactic: refine ext_indep hE fun I hI ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
have simp_rw : (∀ C ⊆ I, ¬M₁.IsCircuit C) ↔ M₂.Indep I
Tactic: simp_rw [indep_iff_forall_subset_not_isCircuit hI, h',
    indep_iff_forall_subset_not_isCircuit (hI.trans_eq hE)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
simp_rw : (∀ C ⊆ I, ¬M₁.IsCircuit C) ↔ M₂.Indep I
⊢ M₁.Indep I ↔ M₂.Indep I
have simp_rw₁ : (∀ C ⊆ I, ¬M₂.IsCircuit C) ↔ M₂.Indep I
Tactic: simp_rw [indep_iff_forall_subset_not_isCircuit hI, h',
    indep_iff_forall_subset_not_isCircuit (hI.trans_eq hE)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
⊢ M₁ = M₂
have refine_1 : ∀ (C : Set α) (hCE : C ⊆ M₁.E) (hC : M₁.IsCircuit C), M₂.IsCircuit C
Tactic: refine ext_isCircuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
refine_1 : ∀ (C : Set α) (hCE : C ⊆ M₁.E) (hC : M₁.IsCircuit C), M₂.IsCircuit C
⊢ M₁ = M₂
have refine_2 : ∀ (C : Set α) (hCE : C ⊆ M₁.E) (hC : M₂.IsCircuit C), M₁.IsCircuit C
Tactic: refine ext_isCircuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
⊢ M₂.IsCircuit C
have refine_1 : ∀ (C' : Set α) (hC'C : C' ⊆ C) (hC' : M₂.IsCircuit C'), M₂.IsCircuit C
Tactic: obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
⊢ M₁.IsCircuit C
have refine_2 : ∀ (C' : Set α) (hC'C : C' ⊆ C) (hC' : M₁.IsCircuit C'), M₁.IsCircuit C
Tactic: obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff hCE).1 (h₂ C hC)).exists_isCircuit_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
have inl : ∀ (hι : IsEmpty ι), ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
inl : ∀ (hι : IsEmpty ι), ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
have inr : ∀ (hι : Nonempty ι), ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
have hcl₁ : ∃ C ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
Tactic: rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl
Cleared hypotheses: hcl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : ∃ C ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
have obtain : ∀ (C' : Set α) (hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})) (hC' : M.IsCircuit C') (hzC' : z ∈ C'),
  ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
Tactic: obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
Cleared hypotheses: hcl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
have refine : C' ⊆ J ∪ ⋃ (i : ι), I i
Tactic: refine ⟨C', ?_, hC', hzC'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ (i : ι), I i
have rwa : ∀ (hC'ss : C' ⊆ insert z (J \ {z} ∪ ⋃ (i : ι), I i)) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
Tactic: rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
Cleared hypotheses: hC'ss, hC', hzC'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
rwa :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z} ∪ ⋃ (i : ι), I i)) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
⊢ C' ⊆ J ∪ ⋃ (i : ι), I i
have rwa₁ : ∀ (hC'ss : C' ⊆ insert z (J \ {z}) ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
Tactic: rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
Cleared hypotheses: hC'ss, hC', hzC'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
rwa :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z} ∪ ⋃ (i : ι), I i)) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
rwa₁ :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z}) ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
⊢ C' ⊆ J ∪ ⋃ (i : ι), I i
have rwa₂ : ∀ (hC'ss : C' ⊆ insert z J ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
Tactic: rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
Cleared hypotheses: hC'ss, hC', hzC'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
rwa :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z} ∪ ⋃ (i : ι), I i)) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
rwa₁ :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z}) ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
rwa₂ : ∀ (hC'ss : C' ⊆ insert z J ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
⊢ C' ⊆ J ∪ ⋃ (i : ι), I i
have rwa₃ : ∀ (hC'ss : C' ⊆ J ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
Tactic: rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
Cleared hypotheses: hC'ss, hC', hzC'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
have inr : z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
Tactic: suffices hcl : z ∈ M.closure ((⋃ i, I i) ∪ (J \ {z})) by
    rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl
    obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
    refine ⟨C', ?_, hC', hzC'⟩
    rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
⊢ z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
have hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
Tactic: have hC' (i) : M.closure (I i) = M.closure (insert (x i) (I i)) := by
    simpa [diff_singleton_eq_self (hxI _)] using (hC i).closure_diff_singleton_eq (x i)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
have inr : z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ (i : ι), I i)
Tactic: rw [closure_union_congr_left <| closure_iUnion_congr _ _ hC',
    iUnion_insert_eq_range_union_iUnion, union_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ (i : ι), I i)
have inr : (J ∪ range x) \ {z} ⊆ range x ∪ J \ {z}
Tactic: refine mem_of_mem_of_subset (hJx.mem_closure_diff_singleton_of_mem (.inl hzJ))
    (M.closure_subset_closure (subset_trans ?_ subset_union_left))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ (J ∪ range x) \ {z} ⊆ range x ∪ J \ {z}
have inr : range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}
Tactic: rw [union_diff_distrib, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_5 : ∀ (hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'),
  ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
Tactic: have hwin := IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i}))
    (J := C₀ \ range x) (z := z) (by simp) (fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
refine_5 :
  ∀ (hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_1 : ∀ (i : ι), M.IsCircuit (insert (x i) ((fun (i : ι) ↦ C i \ {x i}) i))
Tactic: have hwin := IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i}))
    (J := C₀ \ range x) (z := z) (by simp) (fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
refine_5 :
  ∀ (hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : ι), M.IsCircuit (insert (x i) ((fun (i : ι) ↦ C i \ {x i}) i))
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_2 : M.IsCircuit (C₀ \ range x ∪ range x)
Tactic: have hwin := IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i}))
    (J := C₀ \ range x) (z := z) (by simp) (fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
refine_5 :
  ∀ (hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : ι), M.IsCircuit (insert (x i) ((fun (i : ι) ↦ C i \ {x i}) i))
refine_2 : M.IsCircuit (C₀ \ range x ∪ range x)
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_3 : z ∉ range x
Tactic: have hwin := IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i}))
    (J := C₀ \ range x) (z := z) (by simp) (fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
refine_5 :
  ∀ (hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : ι), M.IsCircuit (insert (x i) ((fun (i : ι) ↦ C i \ {x i}) i))
refine_2 : M.IsCircuit (C₀ \ range x ∪ range x)
refine_3 : z ∉ range x
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_4 : ∀ (i : ι), z ∉ (fun (i : ι) ↦ C i \ {x i}) i
Tactic: have hwin := IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i}))
    (J := C₀ \ range x) (z := z) (by simp) (fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
have refine_5 : ∀ (C' : Set α) (hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i) (hC' : M.IsCircuit C')
  (hzC' : z ∈ C'), ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
Tactic: obtain ⟨C', hC'ss, hC', hzC'⟩ := hwin
Cleared hypotheses: hwin