α : Type u_1
as bs : List α
⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
rewrite.lean:18:22-18:31: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (List.reverse ?as).reverse
in the target expression
  as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)

α : Type u_1
as bs : List α
⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)
x y z : Nat
h₁ : x = y
h₂ : y = z
⊢ x = z
rewrite.lean:37:11-37:22: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern in the current goal

x y z : Nat
h₁ : 0 + x = y
h₂ : 0 + y = z
⊢ x = z
m n k : Nat
h✝ : n = m
h : k = m
⊢ k = n
rewrite.lean:55:69-56:10: error: unsolved goals
α : Type
p : Prop
a b c : α
h : p → a = b
⊢ b = c

α : Type
p : Prop
a b c : α
h : p → a = b
⊢ p
f : Nat → Nat
w : ∀ (n : Nat), f n = 0
⊢ [f 1, 0, f 1, f 2] = [0, 0, 0, 0]
f : Nat → Nat
w : ∀ (n : Nat), f n = 0
⊢ [0, f 2, 0, f 2] = [0, 0, 0, 0]
f : Nat → Nat
w : ∀ (n : Nat), f n = 0
⊢ [0, f 2, 0, f 2] = [0, 0, 0, 0]
f : Nat → Nat
w : ∀ (n : Nat), f n = 0
⊢ [f 1, 0, f 1, 0] = [0, 0, 0, 0]
f : Nat → Nat
w : ∀ (n : Nat), f n = 0
⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0]
f : Nat → Nat
w : ∀ (n : Nat), f n = 0
⊢ [f 1, 0, f 1, f 2] = [0, 0, 0, 0]