awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
⊢ M = loopyOn E
have rw₁ : M.closure ∅ = M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
⊢ M = loopyOn E
have rw₂ : M.loops = M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
rw₂ : M.loops = M.E
⊢ M = loopyOn E
have rw₃ : E = M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
rw₂ : M.loops = M.E
rw₃ : E = M.E
⊢ M = loopyOn E
have rw₄ : E = E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M ↾ X = loopyOn X
have rw : (M ↾ X).loops = X ∧ (M ↾ X).E = X
Tactic: rw [eq_loopyOn_iff_loops, restrict_loops_eq', inter_eq_self_of_subset_right hX,
    union_eq_self_of_subset_right diff_subset, and_iff_left M.restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
rw : (M ↾ X).loops = X ∧ (M ↾ X).E = X
⊢ M ↾ X = loopyOn X
have rw₁ : M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
Tactic: rw [eq_loopyOn_iff_loops, restrict_loops_eq', inter_eq_self_of_subset_right hX,
    union_eq_self_of_subset_right diff_subset, and_iff_left M.restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
rw : (M ↾ X).loops = X ∧ (M ↾ X).E = X
rw₁ : M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
⊢ M ↾ X = loopyOn X
have rw₂ : X ∪ X \ M.E = X ∧ (M ↾ X).E = X
Tactic: rw [eq_loopyOn_iff_loops, restrict_loops_eq', inter_eq_self_of_subset_right hX,
    union_eq_self_of_subset_right diff_subset, and_iff_left M.restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
rw : (M ↾ X).loops = X ∧ (M ↾ X).E = X
rw₁ : M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
rw₂ : X ∪ X \ M.E = X ∧ (M ↾ X).E = X
⊢ M ↾ X = loopyOn X
have rw₃ : X = X ∧ (M ↾ X).E = X
Tactic: rw [eq_loopyOn_iff_loops, restrict_loops_eq', inter_eq_self_of_subset_right hX,
    union_eq_self_of_subset_right diff_subset, and_iff_left M.restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
rw : (M ↾ X).loops = X ∧ (M ↾ X).E = X
rw₁ : M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
rw₂ : X ∪ X \ M.E = X ∧ (M ↾ X).E = X
rw₃ : X = X ∧ (M ↾ X).E = X
⊢ M ↾ X = loopyOn X
have rw₄ : X = X
Tactic: rw [eq_loopyOn_iff_loops, restrict_loops_eq', inter_eq_self_of_subset_right hX,
    union_eq_self_of_subset_right diff_subset, and_iff_left M.restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h_1 : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
⊢ M = loopyOn E
have rw : M = loopyOn M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h_1 : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
⊢ M = loopyOn E
have rw₁ : M.closure ∅ = M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h_1 : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
⊢ M = loopyOn E
have rw₂ : M.loops = M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h_1 : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
rw₂ : M.loops = M.E
⊢ M = loopyOn E
have rw₃ : E = M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h_1 : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
rw₂ : M.loops = M.E
rw₃ : E = M.E
⊢ M = loopyOn E
have rw₄ : E = E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsNonloop e
⊢ M.IsLoop e
have rwa : ∀ (h : ¬(¬M.IsLoop e ∧ e ∈ M.E)), M.IsLoop e
Tactic: rwa [isNonloop_iff, and_iff_left he, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsNonloop e
rwa : ∀ (h : ¬(¬M.IsLoop e ∧ e ∈ M.E)), M.IsLoop e
⊢ M.IsLoop e
have rwa₁ : ∀ (h : ¬¬M.IsLoop e), M.IsLoop e
Tactic: rwa [isNonloop_iff, and_iff_left he, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsNonloop e
rwa : ∀ (h : ¬(¬M.IsLoop e ∧ e ∈ M.E)), M.IsLoop e
rwa₁ : ∀ (h : ¬¬M.IsLoop e), M.IsLoop e
⊢ M.IsLoop e
have rwa₂ : ∀ (h : M.IsLoop e), M.IsLoop e
Tactic: rwa [isNonloop_iff, and_iff_left he, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.IsLoop e
have rw : ¬¬M.IsLoop e ↔ M.IsLoop e
Tactic: rw [← not_isLoop_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : ¬¬M.IsLoop e ↔ M.IsLoop e
⊢ ¬M.IsNonloop e ↔ M.IsLoop e
have rw₁ : M.IsLoop e ↔ M.IsLoop e
Tactic: rw [← not_isLoop_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsNonloop e ↔ e ∈ M.E \ M.loops
have rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
Tactic: rw [isNonloop_iff, IsLoop, and_comm, mem_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
⊢ M.IsNonloop e ↔ e ∈ M.E \ M.loops
have rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
Tactic: rw [isNonloop_iff, IsLoop, and_comm, mem_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
⊢ M.IsNonloop e ↔ e ∈ M.E \ M.loops
have rw₂ : e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E \ M.loops
Tactic: rw [isNonloop_iff, IsLoop, and_comm, mem_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
rw₂ : e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E \ M.loops
⊢ M.IsNonloop e ↔ e ∈ M.E \ M.loops
have rw₃ : e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E ∧ e ∉ M.loops
Tactic: rw [isNonloop_iff, IsLoop, and_comm, mem_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops
have pos : ∀ (he : e ∈ M.E), ¬M.IsNonloop e ↔ M.closure {e} = M.loops
Tactic: by_cases he : e ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
pos : ∀ (he : e ∈ M.E), ¬M.IsNonloop e ↔ M.closure {e} = M.loops
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops
have neg : ∀ (he : e ∉ M.E), ¬M.IsNonloop e ↔ M.closure {e} = M.loops
Tactic: by_cases he : e ∈ M.E
-- 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.IsNonloop e
have rw : M.IsLoop e ∨ ¬M.IsLoop e
Tactic: rw [isNonloop_iff, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ M.IsNonloop e
have rw : M.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E
Tactic: rw [isNonloop_iff, ← singleton_dep, dep_iff, not_and, not_imp_not, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.IsNonloop e
have rw : ¬M.IsLoop e
Tactic: rw [← not_isLoop_iff (hI.subset_ground h)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
⊢ M.IsNonloop e
have rw : ¬M.IsCircuit {e}
Tactic: rw [← not_isLoop_iff (hK.subset_ground he), ← singleton_isCircuit]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
he' : M.IsCircuit {e}
⊢ False
have obtain : ∀ (f : α) (he : f ∈ K) (he' : M.IsCircuit {f}) (hfe : f ≠ f), False
Tactic: obtain ⟨f, ⟨rfl, -⟩, hfe⟩ := (he'.isCocircuit_inter_nontrivial hK ⟨e, by simp [he]⟩).exists_ne e
Cleared hypotheses: e, he, he'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
⊢ M.IsNonloop e
have refine : ∀ (hlp : M.IsLoop e), False
Tactic: refine isNonloop_of_not_isLoop (hC.subset_ground he) (fun hlp ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.IsLoop e
⊢ False
have h₁ : LT.lt (α := ℕ∞) 1 1
Tactic: rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h
Cleared hypotheses: h, he, hlp
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsNonloop e ↔ e ∉ M.loops
have rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∉ M.loops
Tactic: rw [isNonloop_iff, isLoop_iff, 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.IsLoop e ∧ e ∈ M.E ↔ e ∉ M.loops
⊢ M.IsNonloop e ↔ e ∉ M.loops
have rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∉ M.loops
Tactic: rw [isNonloop_iff, isLoop_iff, 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.IsLoop e ∧ e ∈ M.E ↔ e ∉ M.loops
rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∉ M.loops
⊢ M.IsNonloop e ↔ e ∉ M.loops
have rw₂ : e ∉ M.loops ↔ e ∉ M.loops
Tactic: rw [isNonloop_iff, isLoop_iff, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ f ∈ M.closure {e}
have rw : ∀ (hef : e ∈ M.closure (insert f ∅)), f ∈ M.closure (insert e ∅)
Tactic: rw [← union_empty {_}, singleton_union] at *
Cleared hypotheses: hef
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ M.IsNonloop f
have rw : f ∈ M.E ∧ ¬M.IsLoop f
Tactic: rw [isNonloop_iff, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ f ∈ M.E ∧ ¬M.IsLoop f
have by_contra! : ∀ (h : ∀ (_ : f ∈ M.E), M.IsLoop f), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), M.IsLoop f
⊢ False
have apply : M.IsLoop e
Tactic: apply he.not_isLoop
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), M.IsLoop f
⊢ M.IsLoop e
have h₁ : ∀ (_ : f ∈ M.E), f ∈ M.loops
Tactic: rw [isLoop_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
⊢ e ∈ M.loops
have h₁ : M.loops = M.closure {f}
Tactic: convert! hef using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
⊢ M.loops = M.closure {f}
have h₁ : ∀ (hf : f ∈ M.E), M.loops = M.closure {f}
Tactic: obtain (hf | hf) := em (f ∈ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
h₁ : ∀ (hf : f ∈ M.E), M.loops = M.closure {f}
⊢ M.loops = M.closure {f}
have h₂ : ∀ (hf : f ∉ M.E), M.loops = M.closure {f}
Tactic: obtain (hf | hf) := em (f ∈ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∈ M.E
⊢ M.loops = M.closure {f}
have h₁ : M.closure M.loops = M.closure {f}
Tactic: rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∈ M.E
h₁ : M.closure M.loops = M.closure {f}
⊢ M.loops = M.closure {f}
have h₂ : M.closure (insert f M.loops) = M.closure {f}
Tactic: rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∈ M.E
h₁ : M.closure M.loops = M.closure {f}
h₂ : M.closure (insert f M.loops) = M.closure {f}
⊢ M.loops = M.closure {f}
have h₃ : M.closure (insert f ∅) = M.closure {f}
Tactic: rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∈ M.E
h₁ : M.closure M.loops = M.closure {f}
h₂ : M.closure (insert f M.loops) = M.closure {f}
h₃ : M.closure (insert f ∅) = M.closure {f}
⊢ M.loops = M.closure {f}
have h₄ : M.closure {f} = M.closure {f}
Tactic: rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∉ M.E
⊢ M.loops = M.closure {f}
have h₁ : M.closure {f} = M.loops
Tactic: rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∉ M.E
h₁ : M.closure {f} = M.loops
⊢ M.loops = M.closure {f}
have h₂ : M.closure ({f} ∩ M.E) = M.loops
Tactic: rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∉ M.E
h₁ : M.closure {f} = M.loops
h₂ : M.closure ({f} ∩ M.E) = M.loops
⊢ M.loops = M.closure {f}
have h₃ : M.closure (M.E ∩ {f}) = M.loops
Tactic: rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∉ M.E
h₁ : M.closure {f} = M.loops
h₂ : M.closure ({f} ∩ M.E) = M.loops
h₃ : M.closure (M.E ∩ {f}) = M.loops
⊢ M.loops = M.closure {f}
have h₄ : M.closure ∅ = M.loops
Tactic: rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∉ M.E
h₁ : M.closure {f} = M.loops
h₂ : M.closure ({f} ∩ M.E) = M.loops
h₃ : M.closure (M.E ∩ {f}) = M.loops
h₄ : M.closure ∅ = M.loops
⊢ M.loops = M.closure {f}
have h₅ : M.closure ∅ = M.closure ∅
Tactic: rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ M.closure {e} = M.closure {f}
have rw : M.closure {e} = M.closure (M.closure {f})
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
⊢ M.closure {e} = M.closure {f}
have rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
⊢ M.closure {e} = M.closure {f}
have rw₂ : M.closure {e} = M.closure {e, f}
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
rw₂ : M.closure {e} = M.closure {e, f}
⊢ M.closure {e} = M.closure {f}
have rw₃ : M.closure (M.closure {e}) = M.closure {e, f}
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
rw₂ : M.closure {e} = M.closure {e, f}
rw₃ : M.closure (M.closure {e}) = M.closure {e, f}
⊢ M.closure {e} = M.closure {f}
have rw₄ : M.closure (insert f (M.closure {e})) = M.closure {e, f}
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
rw₂ : M.closure {e} = M.closure {e, f}
rw₃ : M.closure (M.closure {e}) = M.closure {e, f}
rw₄ : M.closure (insert f (M.closure {e})) = M.closure {e, f}
⊢ M.closure {e} = M.closure {f}
have rw₅ : M.closure {f, e} = M.closure {e, f}
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
rw₂ : M.closure {e} = M.closure {e, f}
rw₃ : M.closure (M.closure {e}) = M.closure {e, f}
rw₄ : M.closure (insert f (M.closure {e})) = M.closure {e, f}
rw₅ : M.closure {f, e} = M.closure {e, f}
⊢ M.closure {e} = M.closure {f}
have rw₆ : M.closure {e, f} = M.closure {e, f}
Tactic: rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}
have refine_1 : ∀ (h : M.closure {e} = M.closure {f}), M.IsCircuit {e, f}
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
refine_1 : ∀ (h : M.closure {e} = M.closure {f}), M.IsCircuit {e, f}
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}
have refine_2 : ∀ (h : M.IsCircuit {e, f}), M.closure {e} = M.closure {f}
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {f}
have rw : e ∈ M.closure {e}
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ M.IsCircuit {e, f}
have hf : M.IsNonloop f
Tactic: have hf := he.isNonloop_of_mem_closure (by rw [← h]; exact M.mem_closure_self e)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.IsCircuit {e, f}
have refine_1 : ¬M.Indep {e, f} ∧ ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})
Tactic: rw [isCircuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff,
      and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})
have refine_1 : ¬M.Indep {e, f}
Tactic: suffices ¬ M.Indep {e, f} by simpa [pair_diff_left hef, hf, pair_diff_right hef, he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ ¬M.Indep {e, f}
have refine_1 : e ∉ M.E \ M.closure {f}
Tactic: rw [Indep.insert_indep_iff_of_notMem (by simpa) (by simpa)]