awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₇ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₁₁ : G.Adj v₁ v₂ → v₂ = x → ¬(x = v₁ ∨ x = v₂) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
mp₁₁ mp₁₂ mp₁₃ : G.Adj v₁ v₂ → v₂ = x → ¬(x = v₁ ∨ x = v₂) → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mpr₅ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
mp₁₁ mp₁₂ mp₁₃ : G.Adj v₁ v₂ → v₂ = x → ¬(x = v₁ ∨ x = v₂) → False
mpr₅ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mpr₆ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
mp₁₁ mp₁₂ mp₁₃ : G.Adj v₁ v₂ → v₂ = x → ¬(x = v₁ ∨ x = v₂) → False
mpr₅ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₆ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mpr₇ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₈ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mpr₉ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₁₀ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₁₄ : G.Adj v₁ v₂ → v₁ = x → ¬x = v₁ → ¬x = v₂ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
mp₁₁ mp₁₂ mp₁₃ : G.Adj v₁ v₂ → v₂ = x → ¬(x = v₁ ∨ x = v₂) → False
mpr₅ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₆ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mpr₇ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₈ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mpr₉ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₁₀ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mp₁₄ mp₁₅ mp₁₆ : G.Adj v₁ v₂ → v₁ = x → ¬x = v₁ → ¬x = v₂ → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₁₇ : G.Adj v₁ v₂ → v₂ = x → ¬x = v₁ → ¬x = v₂ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x : V
⊢ (fromEdgeSet (G.incidenceSet x)).edgeSet = G.incidenceSet x
have rw : G.incidenceSet x ⊆ Sym2.diagSetᶜ
Tactic: rw [edgeSet_fromEdgeSet, sdiff_eq_left, ← Set.subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x : V
⊢ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x
have simp_rw : (G.deleteEdges (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
Tactic: simp_rw [deleteIncidenceSet, deleteEdges, edgeSet_sdiff, edgeSet_fromEdgeSet_incidenceSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x : V
simp_rw : (G.deleteEdges (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
⊢ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x
have simp_rw₁ : (G \ fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
Tactic: simp_rw [deleteIncidenceSet, deleteEdges, edgeSet_sdiff, edgeSet_fromEdgeSet_incidenceSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x : V
simp_rw : (G.deleteEdges (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
simp_rw₁ : (G \ fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
⊢ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x
have simp_rw₂ : G.edgeSet \ (fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
Tactic: simp_rw [deleteIncidenceSet, deleteEdges, edgeSet_sdiff, edgeSet_fromEdgeSet_incidenceSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
⊢ x_1 ∈ (G.deleteIncidenceSet x).support → x_1 ∈ G.support \ {x}
have simp_rw : (∃ (w : V), G.Adj x_1 w ∧ x_1 ≠ x ∧ w ≠ x) → x_1 ∈ G.support \ {x}
Tactic: simp_rw [mem_support, deleteIncidenceSet_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
⊢ (∃ (w : V), G.Adj x_1 w ∧ x_1 ≠ x ∧ w ≠ x) → x_1 ∈ G.support \ {x}
have tauto : ∀ (w : V), G.Adj x_1 w → x_1 ≠ x → w ≠ x → x_1 ∈ G.support \ {x}
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
⊢ induce s (G.deleteIncidenceSet x) = induce s G
have Adj : ∀ (v₁ v₂ : (↑s : Type u_1)), (induce s (G.deleteIncidenceSet x)).Adj v₁ v₂ ↔ (induce s G).Adj v₁ v₂
Tactic: ext v₁ v₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : (↑s : Type u_1)
⊢ (induce s (G.deleteIncidenceSet x)).Adj v₁ v₂ ↔ (induce s G).Adj v₁ v₂
have Adj : G.Adj (↑v₁ : V) (↑v₂ : V) → (↑v₁ : V) ≠ x ∧ (↑v₂ : V) ≠ x
Tactic: simp_rw [comap_adj, Function.Embedding.coe_subtype, deleteIncidenceSet_adj, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (edgeFinset (induce {x}ᶜ G)) = #(G.deleteIncidenceSet x).edgeFinset
have h_notMem : x ∉ {x}ᶜ
Tactic: have h_notMem : x ∉ ({x}ᶜ : Set V) := Set.notMem_compl_iff.mpr (Set.mem_singleton x)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (edgeFinset (induce {x}ᶜ G)) = #(G.deleteIncidenceSet x).edgeFinset
have simp_rw : Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (Set.toFinset (edgeSet (induce {x}ᶜ (G.deleteIncidenceSet x)))) =
  #(G.deleteIncidenceSet x).edgeSet.toFinset
Tactic: simp_rw [edgeFinset, Set.toFinset_card,
    ← G.induce_deleteIncidenceSet_of_notMem h_notMem, ← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (Set.toFinset (edgeSet (induce {x}ᶜ (G.deleteIncidenceSet x)))) =
    #(G.deleteIncidenceSet x).edgeSet.toFinset
have h : (G.deleteIncidenceSet x).support ⊆ {x}ᶜ
Tactic: apply card_edgeFinset_induce_of_support_subset
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ (G.deleteIncidenceSet x).support ⊆ {x}ᶜ
have trans : (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
Tactic: trans G.support \ {x}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
trans : (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
⊢ (G.deleteIncidenceSet x).support ⊆ {x}ᶜ
have trans₁ : G.support \ {x} ⊆ {x}ᶜ
Tactic: trans G.support \ {x}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ G.support \ {x} ⊆ {x}ᶜ
have rw : G.support \ {x} ⊆ Set.univ \ {x}
Tactic: rw [Set.compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset x
have a : (↑(G.deleteIncidenceSet x).edgeFinset : Set (Sym2 V)) = (↑(G.edgeFinset \ G.incidenceFinset x) : Set (Sym2 V))
Tactic: apply Finset.coe_injective
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ (↑(G.deleteIncidenceSet x).edgeFinset : Set (Sym2 V)) = (↑(G.edgeFinset \ G.incidenceFinset x) : Set (Sym2 V))
have a : (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - G.degree x
have simp_rw : #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - #(G.incidenceFinset x)
Tactic: simp_rw [← card_incidenceFinset_eq_degree, ← card_sdiff_of_subset (G.incidenceFinset_subset x),
    edgeFinset_deleteIncidenceSet_eq_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
simp_rw : #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - #(G.incidenceFinset x)
⊢ #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - G.degree x
have simp_rw₁ : #(G.deleteIncidenceSet x).edgeFinset = #(G.edgeFinset \ G.incidenceFinset x)
Tactic: simp_rw [← card_incidenceFinset_eq_degree, ← card_sdiff_of_subset (G.incidenceFinset_subset x),
    edgeFinset_deleteIncidenceSet_eq_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ (G.deleteIncidenceSet x).edgeFinset = {x_1 ∈ G.edgeFinset | x ∉ x_1}
have rw : {x_1 ∈ G.edgeFinset | x_1 ∉ G.incidenceFinset x} = {x_1 ∈ G.edgeFinset | x ∉ x_1}
Tactic: rw [edgeFinset_deleteIncidenceSet_eq_sdiff, sdiff_eq_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ {x_1 ∈ G.edgeFinset | x_1 ∉ G.incidenceFinset x} = {x_1 ∈ G.edgeFinset | x ∉ x_1}
have H : ∀ x_1 ∈ G.edgeFinset, x_1 ∉ G.incidenceFinset x ↔ x ∉ x_1
Tactic: apply filter_congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
x_1 : Sym2 V
h : x_1 ∈ G.edgeFinset
⊢ x_1 ∉ G.incidenceFinset x ↔ x ∉ x_1
have H : x_1 ∈ G.edgeSet ∨ x ∉ x_1
Tactic: rw [incidenceFinset, Set.mem_toFinset, incidenceSet,
    Set.mem_setOf_eq, not_and, Classical.imp_iff_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
x_1 : Sym2 V
h : x_1 ∈ G.edgeFinset
⊢ x_1 ∈ G.edgeSet ∨ x ∉ x_1
have H : x_1 ∈ G.edgeSet
Tactic: left
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
x_1 : Sym2 V
h : x_1 ∈ G.edgeFinset
⊢ x_1 ∈ G.edgeSet
have H : ∀ (h : x_1 ∈ G.edgeSet), x_1 ∈ G.edgeSet
Tactic: rwa [mem_edgeFinset] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : x ∈ G.support
⊢ Fintype.card.{u_1} (↑(G.deleteIncidenceSet x).support : Type u_1) ≤ Fintype.card.{u_1} (↑G.support : Type u_1) - 1
have hx₁ : Set.toFinset {x} ⊆ G.support.toFinset
Tactic: rw [← Set.singleton_subset_iff, ← Set.toFinset_subset_toFinset] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
⊢ Fintype.card.{u_1} (↑(G.deleteIncidenceSet x).support : Type u_1) ≤ Fintype.card.{u_1} (↑G.support : Type u_1) - 1
have simp_rw : #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support \ {x}).toFinset
Tactic: simp_rw [← Set.card_singleton x, ← Set.toFinset_card, ← card_sdiff_of_subset hx,
    ← Set.toFinset_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
⊢ #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support \ {x}).toFinset
have a : (G.deleteIncidenceSet x).support.toFinset ⊆ (G.support \ {x}).toFinset
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
⊢ (G.deleteIncidenceSet x).support.toFinset ⊆ (G.support \ {x}).toFinset
have a : (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
Tactic: rw [Set.toFinset_subset_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
have refine_1 : ∀ (h : G.DeleteFar p r) (H : SimpleGraph V) (x : DecidableRel H.Adj) (hHG : H ≤ G) (hH : p H),
  r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
Tactic: refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩