Theorem: rewrite_test (Katydid/Std/Tipe2.lean)

State before:
α✝ : Type u_1
a b c : α✝
⊢ a ≡ b → b ≡ c → a ≡ c
Tactic:
intro ab bc
State after:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c

State before:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Tactic:
constructor
State after:
case a
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a = c

State before:
case a
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a = c
Tactic:
cases ab with
| mk ab =>
  rw [ab]
  cases bc with
  | mk bc =>
    rw [bc]
State after:
no goals

State before:
case a.mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ a = c
Tactic:
rw [ab]
State after:
case a.mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b = c

State before:
case a.mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b = c
Tactic:
cases bc with
| mk bc =>
  rw [bc]
State after:
no goals

State before:
case a.mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ b = c
Tactic:
rw [bc]
State after:
no goals