no goals
ι : Type ?u.20220
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
⊢ replicate 0 a = replicate 0 b ↔ 0 = 0 ∨ a = b
simp
no goals
ι : Type ?u.20220
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
n : ℕ
⊢ a = b ↔ n + 1 = 0 ∨ a = b
simp only [n.succ_ne_zero, false_or]