Theorem: Languages.concat_exp_comm (FOL/Parsing/Text.lean)

State before:
α : Type
L : Language α
n : ℕ
⊢ concat (exp L n) L = concat L (exp L n)
Tactic:
induction n
State after:
case zero
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)

case succ
α : Type
L : Language α
n✝ : ℕ
a✝ : concat (exp L n✝) L = concat L (exp L n✝)
⊢ concat (exp L (n✝ + 1)) L = concat L (exp L (n✝ + 1))

State before:
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)
Tactic:
case zero =>
  simp only [exp]
  simp only [concat]
  simp
State after:
no goals

State before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (exp L (k + 1)) L = concat L (exp L (k + 1))
Tactic:
case succ k ih =>
  simp only [exp]
  conv => left; simp only [ih]
  simp only [thm_3_c]
State after:
no goals

State before:
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)
Tactic:
simp only [exp]
State after:
α : Type
L : Language α
⊢ concat {[]} L = concat L {[]}

State before:
α : Type
L : Language α
⊢ concat {[]} L = concat L {[]}
Tactic:
simp only [concat]
State after:
α : Type
L : Language α
⊢ {x | ∃ s ∈ {[]}, ∃ t ∈ L, s ++ t = x} = {x | ∃ s ∈ L, ∃ t ∈ {[]}, s ++ t = x}

State before:
α : Type
L : Language α
⊢ {x | ∃ s ∈ {[]}, ∃ t ∈ L, s ++ t = x} = {x | ∃ s ∈ L, ∃ t ∈ {[]}, s ++ t = x}
Tactic:
simp
State after:
no goals

State before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (exp L (k + 1)) L = concat L (exp L (k + 1))
Tactic:
simp only [exp]
State after:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat (exp L k) L) L = concat L (concat (exp L k) L)

State before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat (exp L k) L) L = concat L (concat (exp L k) L)
Tactic:
conv => left; simp only [ih]
State after:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat L (exp L k)) L = concat L (concat (exp L k) L)

State before:
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat L (exp L k)) L = concat L (concat (exp L k) L)
Tactic:
simp only [thm_3_c]
State after:
no goals