awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
rw : (M ↾ R).closure ∅ = M.loops ∩ R ∪ R \ M.E
rw₁ : (M ↾ R).closure ∅ = M.closure ∅ ∩ R ∪ R \ M.E
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E
have rw₂ : M.closure (∅ ∩ R) ∩ R ∪ R \ M.E = M.closure ∅ ∩ R ∪ R \ M.E
Tactic: rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
rw : (M ↾ R).closure ∅ = M.loops ∩ R ∪ R \ M.E
rw₁ : (M ↾ R).closure ∅ = M.closure ∅ ∩ R ∪ R \ M.E
rw₂ : M.closure (∅ ∩ R) ∩ R ∪ R \ M.E = M.closure ∅ ∩ R ∪ R \ M.E
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E
have rw₃ : M.closure ∅ ∩ R ∪ R \ M.E = M.closure ∅ ∩ R ∪ R \ M.E
Tactic: rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).loops = M.loops ∩ R
have rw : M.loops ∩ R ∪ R \ M.E = M.loops ∩ R
Tactic: rw [restrict_loops_eq', diff_eq_empty.2 hR, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M.loops ∩ R ∪ R \ M.E = M.loops ∩ R
⊢ (M ↾ R).loops = M.loops ∩ R
have rw₁ : M.loops ∩ R ∪ ∅ = M.loops ∩ R
Tactic: rw [restrict_loops_eq', diff_eq_empty.2 hR, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M.loops ∩ R ∪ R \ M.E = M.loops ∩ R
rw₁ : M.loops ∩ R ∪ ∅ = M.loops ∩ R
⊢ (M ↾ R).loops = M.loops ∩ R
have rw₂ : M.loops ∩ R = M.loops ∩ R
Tactic: rw [restrict_loops_eq', diff_eq_empty.2 hR, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ (M ↾ R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)
have simp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
Tactic: simp only [isLoop_iff, restrict_closure_eq', empty_inter, mem_union, mem_inter_iff, mem_diff,
    ← closure_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₇ : e ∈ R → e ∉ M.E → e ∈ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₈ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₈ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mp₉ mp₁₀ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₁₁ : e ∈ M.closure ∅ → e ∈ R → e ∉ M.closure ∅ → e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₈ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mp₉ mp₁₀ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₁ : e ∈ M.closure ∅ → e ∈ R → e ∉ M.closure ∅ → e ∉ M.E
mp₁₂ mp₁₃ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mp₁₄ : e ∈ R → e ∉ M.E → e ∉ M.closure ∅ → e ∉ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₈ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mp₉ mp₁₀ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₁ : e ∈ M.closure ∅ → e ∈ R → e ∉ M.closure ∅ → e ∉ M.E
mp₁₂ mp₁₃ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₄ : e ∈ R → e ∉ M.E → e ∉ M.closure ∅ → e ∉ M.E
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₉ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.E → e ∉ M.closure ∅ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₈ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mp₉ mp₁₀ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₁ : e ∈ M.closure ∅ → e ∈ R → e ∉ M.closure ∅ → e ∉ M.E
mp₁₂ mp₁₃ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₄ : e ∈ R → e ∉ M.E → e ∉ M.closure ∅ → e ∉ M.E
mpr₉ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.E → e ∉ M.closure ∅ → False
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
have mpr₁₀ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.E → e ∉ R → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M N : Matroid α
e : α
hNM : N ≤r M
⊢ N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e
Tactic: obtain ⟨R, hR, rfl⟩ := hNM
Cleared hypotheses: N, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e
have simp : e ∈ R → e ∉ M.E → M.IsLoop e
Tactic: simp only [restrict_isLoop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e
have rw : f e ∈ (M.map f hf).loops ↔ M.IsLoop e
Tactic: rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
rw : f e ∈ (M.map f hf).loops ↔ M.IsLoop e
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e
have rw₁ : f e ∈ f '' M.loops ↔ M.IsLoop e
Tactic: rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
rw : f e ∈ (M.map f hf).loops ↔ M.IsLoop e
rw₁ : f e ∈ f '' M.loops ↔ M.IsLoop e
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e
have rw₂ : e ∈ M.loops ↔ M.IsLoop e
Tactic: rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
rw : f e ∈ (M.map f hf).loops ↔ M.IsLoop e
rw₁ : f e ∈ f '' M.loops ↔ M.IsLoop e
rw₂ : e ∈ M.loops ↔ M.IsLoop e
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e
have rw₃ : e ∈ M.loops ↔ e ∈ M.loops
Tactic: rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
⊢ (M.comap f).loops = f ⁻¹' M.loops
have rw : (M.comap f).closure ∅ = f ⁻¹' M.loops
Tactic: rw [loops, comap_closure_eq, image_empty, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
rw : (M.comap f).closure ∅ = f ⁻¹' M.loops
⊢ (M.comap f).loops = f ⁻¹' M.loops
have rw₁ : f ⁻¹' M.closure (f '' ∅) = f ⁻¹' M.loops
Tactic: rw [loops, comap_closure_eq, image_empty, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
rw : (M.comap f).closure ∅ = f ⁻¹' M.loops
rw₁ : f ⁻¹' M.closure (f '' ∅) = f ⁻¹' M.loops
⊢ (M.comap f).loops = f ⁻¹' M.loops
have rw₂ : f ⁻¹' M.closure ∅ = f ⁻¹' M.loops
Tactic: rw [loops, comap_closure_eq, image_empty, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
rw : (M.comap f).closure ∅ = f ⁻¹' M.loops
rw₁ : f ⁻¹' M.closure (f '' ∅) = f ⁻¹' M.loops
rw₂ : f ⁻¹' M.closure ∅ = f ⁻¹' M.loops
⊢ (M.comap f).loops = f ⁻¹' M.loops
have rw₃ : f ⁻¹' M.closure ∅ = f ⁻¹' M.closure ∅
Tactic: rw [loops, comap_closure_eq, image_empty, loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ M.loops = E ∧ M.E = E
have rw : (loopyOn E).closure ∅ = E ∧ (loopyOn E).E = E
Tactic: rw [h, loops]
-- 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
⊢ M = loopyOn E
have rw : M = loopyOn M.E
Tactic: rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']