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:
cases ab with
| mk ab =>
  rw [ab]
  cases bc with
  | mk bc =>
    rw [bc]
    constructor
    rfl
State after:
no goals

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

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

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

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

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