Theorem: FreeGroup.append_homotopic (GroupComp/WordProblem/FreeGroup.lean)

State before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
⊢ L₁ ∼ L₂ → L₁ ++ L₃ ∼ L₂ ++ L₃
Tactic:
intro eqn
State after:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ L₁ ++ L₃ ∼ L₂ ++ L₃

State before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ L₁ ++ L₃ ∼ L₂ ++ L₃
Tactic:
show mk (L₁ ++ L₃) = mk (L₂ ++ L₃)
State after:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk (L₁ ++ L₃) = mk (L₂ ++ L₃)

State before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk (L₁ ++ L₃) = mk (L₂ ++ L₃)
Tactic:
rw [← mul_mk, ← mul_mk]
State after:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk L₁ * mk L₃ = mk L₂ * mk L₃

State before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk L₁ * mk L₃ = mk L₂ * mk L₃
Tactic:
rw [eqn]
State after:
no goals