awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
rw : M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
⊢ M.closure K = K ∪ M.loops
have rw₁ : M.closure ∅ ∪ K = ∅ ∪ K ∪ M.loops
Tactic: rw [← empty_union K, closure_union_eq_of_subset_coloops _ hK, empty_union, union_comm,
    closure_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
rw : M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
rw₁ : M.closure ∅ ∪ K = ∅ ∪ K ∪ M.loops
⊢ M.closure K = K ∪ M.loops
have rw₂ : M.closure ∅ ∪ K = K ∪ M.loops
Tactic: rw [← empty_union K, closure_union_eq_of_subset_coloops _ hK, empty_union, union_comm,
    closure_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
rw : M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
rw₁ : M.closure ∅ ∪ K = ∅ ∪ K ∪ M.loops
rw₂ : M.closure ∅ ∪ K = K ∪ M.loops
⊢ M.closure K = K ∪ M.loops
have rw₃ : K ∪ M.closure ∅ = K ∪ M.loops
Tactic: rw [← empty_union K, closure_union_eq_of_subset_coloops _ hK, empty_union, union_comm,
    closure_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
rw : M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
rw₁ : M.closure ∅ ∪ K = ∅ ∪ K ∪ M.loops
rw₂ : M.closure ∅ ∪ K = K ∪ M.loops
rw₃ : K ∪ M.closure ∅ = K ∪ M.loops
⊢ M.closure K = K ∪ M.loops
have rw₄ : K ∪ M.loops = K ∪ M.loops
Tactic: rw [← empty_union K, closure_union_eq_of_subset_coloops _ hK, empty_union, union_comm,
    closure_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (X \ K) = M.closure X \ K
have nth_rw : M.closure (X \ K) = M.closure (X ∩ K ∪ X \ K) \ K
Tactic: nth_rw 2 [← inter_union_diff X K]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (X \ K) = M.closure (X ∩ K ∪ X \ K) \ K
have rw : ∀ ⦃a : α⦄, a ∈ K → ∀ ⦃b : α⦄, b ∈ M.closure (X \ K) → a ≠ b
Tactic: rw [union_comm, closure_union_eq_of_subset_coloops _ (inter_subset_right.trans hK),
    union_diff_distrib, diff_eq_empty.mpr inter_subset_right, union_empty, eq_comm,
    sdiff_eq_self_iff_disjoint, disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
heK : e ∈ K
heX : e ∈ M.closure (X \ K)
⊢ False
have heX₁ : e ∈ X \ K
Tactic: rw [IsColoop.mem_closure_iff_mem (hK heK)] at heX
Cleared hypotheses: heX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X K : Set α
hXK : Disjoint X K
hK : K ⊆ M.coloops
⊢ Disjoint (M.closure X) K
have rwa : M.closure X ∩ K = ∅
Tactic: rwa [disjoint_iff_inter_eq_empty, closure_inter_eq_of_subset_coloops X hK,
    ← disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X K : Set α
hXK : Disjoint X K
hK : K ⊆ M.coloops
rwa : M.closure X ∩ K = ∅
⊢ Disjoint (M.closure X) K
have rwa₁ : X ∩ K = ∅
Tactic: rwa [disjoint_iff_inter_eq_empty, closure_inter_eq_of_subset_coloops X hK,
    ← disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
⊢ M.Indep (insert e I)
have h : e ∉ I
Tactic: refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)
have rw : e ∉ M.closure I
Tactic: rw [← hI.notMem_closure_iff_of_notMem h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
⊢ M.Indep (I ∪ K) ↔ M.Indep I
have refine : ∀ (h : M.Indep I), M.Indep (I ∪ K)
Tactic: refine ⟨fun h ↦ h.subset subset_union_left, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
h : M.Indep I
⊢ M.Indep (I ∪ K)
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), M.Indep (I ∪ K)
Tactic: obtain ⟨B, hB, hIB⟩ := h.exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
⊢ M.Indep (I \ K) ↔ M.Indep I
have rw : M.Indep (I \ K ∪ K) ↔ M.Indep I
Tactic: rw [← union_indep_iff_indep_of_subset_coloops hK, diff_union_self,
    union_indep_iff_indep_of_subset_coloops hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
rw : M.Indep (I \ K ∪ K) ↔ M.Indep I
⊢ M.Indep (I \ K) ↔ M.Indep I
have rw₁ : M.Indep (I ∪ K) ↔ M.Indep I
Tactic: rw [← union_indep_iff_indep_of_subset_coloops hK, diff_union_self,
    union_indep_iff_indep_of_subset_coloops hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
rw : M.Indep (I \ K ∪ K) ↔ M.Indep I
rw₁ : M.Indep (I ∪ K) ↔ M.Indep I
⊢ M.Indep (I \ K) ↔ M.Indep I
have rw₂ : M.Indep I ↔ M.Indep I
Tactic: rw [← union_indep_iff_indep_of_subset_coloops hK, diff_union_self,
    union_indep_iff_indep_of_subset_coloops hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.Indep M.coloops
have rw : M.Indep ∅
Tactic: rw [← empty_union M.coloops, union_coloops_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
have inr : ∀
  (this :
    ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
      (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
  (heR : e ∉ R), (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
Tactic: wlog heR : e ∈ R
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
inr :
  ∀
    (this :
      ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
        (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
    (heR : e ∉ R), (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
have wlog : ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
  (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
Tactic: wlog heR : e ∈ R
Cleared hypotheses: R, hRE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
e_1 : α_1
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
have rw : (∀ ⦃C : Set α⦄, (M ↾ R).IsCircuit C → e ∉ C) ↔ (¬∃ C ⊆ insert e (R \ {e}), M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
Tactic: rw [isColoop_iff_forall_notMem_isCircuit heR, mem_closure_iff_exists_isCircuit (by simp)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
e_1 : α_1
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (∀ ⦃C : Set α⦄, (M ↾ R).IsCircuit C → e ∉ C) ↔ (¬∃ C ⊆ insert e (R \ {e}), M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
have simp : (∀ ⦃C : Set α⦄, M.IsCircuit C ∧ C ⊆ R → e ∉ C) ↔ (¬∃ C ⊆ insert e R, M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
Tactic: simp only [restrict_isCircuit_iff hRE, insert_diff_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
⊢ 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.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
have rw : M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
Tactic: rw [← diff_coloops_indep_iff, ← @diff_coloops_indep_iff _ M₂, ← hc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
have inl : ∀ (hdj : Disjoint I M₁.loops), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
Tactic: obtain hdj | hndj := em (Disjoint I (M₁.loops))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
inl : ∀ (hdj : Disjoint I M₁.loops), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
have inr : ∀ (hndj : ¬Disjoint I M₁.loops), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
Tactic: obtain hdj | hndj := em (Disjoint I (M₁.loops))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
have inl : Disjoint (I \ M₁.coloops) (M₁.loops ∪ M₁.coloops)
Tactic: rw [h _ (diff_subset.trans hI)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) (M₁.loops ∪ M₁.coloops)
have inl : Disjoint (I \ M₁.coloops) M₁.loops ∧ Disjoint (I \ M₁.coloops) M₁.coloops
Tactic: rw [disjoint_union_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
have inr : ∀ (e : α) (heI : e ∈ I) (hel : M₁.IsLoop e), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
Tactic: obtain ⟨e, heI, hel : M₁.IsLoop e⟩ := not_disjoint_iff_nonempty_inter.mp hndj
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
have inr : ¬M₂.Indep (I \ M₁.coloops)
Tactic: refine iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
⊢ ¬M₂.Indep (I \ M₁.coloops)
have hel₁ : M₂.IsLoop e
Tactic: rw [isLoop_iff, hl, ← isLoop_iff] at hel
Cleared hypotheses: hel
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₁.coloops)
have inr : ¬M₂.Indep (I \ M₂.coloops)
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M.Loopless
he : e ∈ M.E
⊢ M.IsNonloop e
have rw : e ∉ ∅
Tactic: rw [← not_isLoop_iff, isLoop_iff, loops_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.Loopless
hI : I.Subsingleton
hIE : I ⊆ M.E
⊢ M.Indep I
have inl : ∀ (hI : Set.Subsingleton.{u_1} (α := α) ∅) (hIE : ∅ ⊆ M.E), M.Indep ∅
Tactic: obtain rfl | ⟨x, rfl⟩ := hI.eq_empty_or_singleton
Cleared hypotheses: I, hI, hIE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.Loopless
hI : I.Subsingleton
hIE : I ⊆ M.E
inl : ∀ (hI : Set.Subsingleton.{u_1} (α := α) ∅) (hIE : ∅ ⊆ M.E), M.Indep ∅
⊢ M.Indep I
have inr : ∀ (x : α) (hI : Set.Subsingleton (α := α) {x}) (hIE : {x} ⊆ M.E), M.Indep {x}
Tactic: obtain rfl | ⟨x, rfl⟩ := hI.eq_empty_or_singleton
Cleared hypotheses: I, hI, hIE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
⊢ M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
have rw : (∀ e ∈ M.E, ¬M.IsLoop e) ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
Tactic: rw [loopless_iff_forall_not_isLoop]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
have suffices : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
Tactic: suffices (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton by
    rw [loopless_iff_forall_not_isLoop]
    contrapose!
    exact this
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
have refine : (∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton) →
  ∀ (C : Set α) (hC : M.IsCircuit C) (hCs : C.Subsingleton), ∃ x ∈ M.E, M.IsLoop x
Tactic: refine ⟨fun ⟨e, _, he⟩ ↦ ⟨{e}, he.isCircuit, by simp⟩, fun ⟨C, hC, hCs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
h : ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
C : Set α
hC : M.IsCircuit C
hCs : C.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x
have inl : ∀ (hC : M.IsCircuit ∅) (hCs : Set.Subsingleton.{u_1} (α := α) ∅), ∃ x ∈ M.E, M.IsLoop x
Tactic: obtain (rfl | ⟨e, rfl⟩) := hCs.eq_empty_or_singleton
Cleared hypotheses: C, hC, hCs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
h : ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
C : Set α
hC : M.IsCircuit C
hCs : C.Subsingleton
inl : ∀ (hC : M.IsCircuit ∅) (hCs : Set.Subsingleton.{u_1} (α := α) ∅), ∃ x ∈ M.E, M.IsLoop x
⊢ ∃ x ∈ M.E, M.IsLoop x
have inr : ∀ (e : α) (hC : M.IsCircuit {e}) (hCs : Set.Subsingleton (α := α) {e}), ∃ x ∈ M.E, M.IsLoop x
Tactic: obtain (rfl | ⟨e, rfl⟩) := hCs.eq_empty_or_singleton
Cleared hypotheses: C, hC, hCs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M N : Matroid α
inst : M.Loopless
hR : N ≤r M
⊢ N.Loopless
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).Loopless
Tactic: obtain ⟨R, hR, rfl⟩ := hR
Cleared hypotheses: N, hR
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Loopless
have rw : (M ↾ R).loops = ∅
Tactic: rw [loopless_iff, restrict_loops_eq hR, M.loops_eq_empty, empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
R : Set α
hR : R ⊆ M.E
rw : (M ↾ R).loops = ∅
⊢ (M ↾ R).Loopless
have rw₁ : M.loops ∩ R = ∅
Tactic: rw [loopless_iff, restrict_loops_eq hR, M.loops_eq_empty, empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
R : Set α
hR : R ⊆ M.E
rw : (M ↾ R).loops = ∅
rw₁ : M.loops ∩ R = ∅
⊢ (M ↾ R).Loopless
have rw₂ : ∅ ∩ R = ∅
Tactic: rw [loopless_iff, restrict_loops_eq hR, M.loops_eq_empty, empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
R : Set α
hR : R ⊆ M.E
rw : (M ↾ R).loops = ∅
rw₁ : M.loops ∩ R = ∅
rw₂ : ∅ ∩ R = ∅
⊢ (M ↾ R).Loopless
have rw₃ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [loopless_iff, restrict_loops_eq hR, M.loops_eq_empty, empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
⊢ M.removeLoops = M
have rw : M ↾ {e : α | M.IsNonloop e} = M
Tactic: rw [removeLoops, ← Loopless.ground_eq, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
rw : M ↾ {e : α | M.IsNonloop e} = M
⊢ M.removeLoops = M
have rw₁ : M ↾ M.E = M
Tactic: rw [removeLoops, ← Loopless.ground_eq, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
rw : M ↾ {e : α | M.IsNonloop e} = M
rw₁ : M ↾ M.E = M
⊢ M.removeLoops = M
have rw₂ : M = M
Tactic: rw [removeLoops, ← Loopless.ground_eq, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops = M ↔ M.Loopless
have refine : ∀ (h : M.removeLoops = M), M.Loopless
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ M.removeLoops_eq_self⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
h : M.removeLoops = M
⊢ M.Loopless
have rw : M.removeLoops.Loopless
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops ↾ M.E = M
have rw : (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E = M.E ∧
  ∀ ⦃I : Set α⦄, I ⊆ (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E → ((M ↾ {e : α | M.IsNonloop e} ↾ M.E).Indep I ↔ M.Indep I)
Tactic: rw [removeLoops, ext_iff_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E = M.E ∧
    ∀ ⦃I : Set α⦄, I ⊆ (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E → ((M ↾ {e : α | M.IsNonloop e} ↾ M.E).Indep I ↔ M.Indep I)
have simp : ∀ ⦃I : Set α⦄, I ⊆ M.E → ((M.Indep I ∧ I ⊆ {e : α | M.IsNonloop e}) ∧ I ⊆ M.E ↔ M.Indep I)
Tactic: simp only [restrict_ground_eq, restrict_indep_iff, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops.Indep = M.Indep
have h : ∀ (I : Set α), M.removeLoops.Indep I ↔ M.Indep I
Tactic: ext I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.removeLoops.Indep I ↔ M.Indep I
have h : M.Indep I → I ⊆ {e : α | M.IsNonloop e}
Tactic: rw [removeLoops_eq_restrict, restrict_indep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops.IsBasis' = M.IsBasis'
have h : ∀ (x x_1 : Set α), M.removeLoops.IsBasis' x x_1 ↔ M.IsBasis' x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops.IsBase = M.IsBase
have h : ∀ (B : Set α), M.removeLoops.IsBase B ↔ M.IsBase B
Tactic: ext B
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.removeLoops.IsBase B ↔ M.IsBase B
have h : Maximal M.removeLoops.Indep B ↔ M.IsBase B
Tactic: rw [isBase_iff_maximal_indep, removeLoops_indep_eq, isBase_iff_maximal_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : Maximal M.removeLoops.Indep B ↔ M.IsBase B
⊢ M.removeLoops.IsBase B ↔ M.IsBase B
have h₁ : Maximal M.Indep B ↔ M.IsBase B
Tactic: rw [isBase_iff_maximal_indep, removeLoops_indep_eq, isBase_iff_maximal_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : Maximal M.removeLoops.Indep B ↔ M.IsBase B
h₁ : Maximal M.Indep B ↔ M.IsBase B
⊢ M.removeLoops.IsBase B ↔ M.IsBase B
have h₂ : Maximal M.Indep B ↔ Maximal M.Indep B
Tactic: rw [isBase_iff_maximal_indep, removeLoops_indep_eq, isBase_iff_maximal_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops.IsNonloop = M.IsNonloop
have h : ∀ (e : α), M.removeLoops.IsNonloop e ↔ M.IsNonloop e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e
have h : (M ↾ {e : α | M.IsNonloop e}).IsNonloop e ↔ M.IsNonloop e
Tactic: rw [removeLoops_eq_restrict, restrict_isNonloop_iff, mem_setOf, and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : (M ↾ {e : α | M.IsNonloop e}).IsNonloop e ↔ M.IsNonloop e
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e
have h₁ : M.IsNonloop e ∧ Membership.mem (γ := Set α) {e : α | M.IsNonloop e} e ↔ M.IsNonloop e
Tactic: rw [removeLoops_eq_restrict, restrict_isNonloop_iff, mem_setOf, and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : (M ↾ {e : α | M.IsNonloop e}).IsNonloop e ↔ M.IsNonloop e
h₁ : M.IsNonloop e ∧ Membership.mem (γ := Set α) {e : α | M.IsNonloop e} e ↔ M.IsNonloop e
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e
have h₂ : M.IsNonloop e ∧ M.IsNonloop e ↔ M.IsNonloop e
Tactic: rw [removeLoops_eq_restrict, restrict_isNonloop_iff, mem_setOf, and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : (M ↾ {e : α | M.IsNonloop e}).IsNonloop e ↔ M.IsNonloop e
h₁ : M.IsNonloop e ∧ Membership.mem (γ := Set α) {e : α | M.IsNonloop e} e ↔ M.IsNonloop e
h₂ : M.IsNonloop e ∧ M.IsNonloop e ↔ M.IsNonloop e
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e
have h₃ : M.IsNonloop e ↔ M.IsNonloop e
Tactic: rw [removeLoops_eq_restrict, restrict_isNonloop_iff, mem_setOf, and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e : α | M.IsNonloop e}
⊢ M.removeLoops ↾ X = M ↾ X
have rwa : M ↾ {e : α | M.IsNonloop e} ↾ X = M ↾ X
Tactic: rwa [removeLoops_eq_restrict, restrict_restrict_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e : α | M.IsNonloop e}
rwa : M ↾ {e : α | M.IsNonloop e} ↾ X = M ↾ X
⊢ M.removeLoops ↾ X = M ↾ X
have rwa₁ : M ↾ X = M ↾ X
Tactic: rwa [removeLoops_eq_restrict, restrict_restrict_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ (M ↾ univ).removeLoops = M.removeLoops
have rw : M ↾ {e : α | (M ↾ univ).IsNonloop e} = M ↾ {e : α | M.IsNonloop e}
Tactic: rw [removeLoops_eq_restrict, restrict_restrict_eq _ (subset_univ _), removeLoops_eq_restrict]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M N : Matroid α
hNM : N ≤r M
inst : N.Loopless
⊢ N ≤r M.removeLoops
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hNM : M ↾ R ≤r M) [(M ↾ R).Loopless], M ↾ R ≤r M.removeLoops
Tactic: obtain ⟨R, hR, rfl⟩ := hNM.exists_eq_restrict
Cleared hypotheses: N, hNM, inst