Theorem: LO.Propositional.Classical.Derivation.length_cast (Logic/Propositional/Classical/Basic/Calculus.lean)

State before:
α : Type u_1
Δ Δ₁ Δ₂ Γ : Sequent α
d :  ⊢¹ Δ
e : Δ = Γ
⊢ length (Derivation.cast d e) = length d
Tactic:
rcases e with rfl
State after:
α : Type u_1
Δ Δ₁ Δ₂ : Sequent α
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d

State before:
α : Type u_1
Δ Δ₁ Δ₂ : Sequent α
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d
Tactic:
simp[Derivation.cast]
State after:
no goals