-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[nolint unusedHavesSuffices]
private lemma equivTree_left_inv (p) : equivTreeInvFun (equivTreeToFun p) = p

Proof state:
case pos
p : DyckWord
h : p = 0
⊢ DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p) = p

Tactic:
simp [h, equivTreeToFun, equivTreeInvFun]

Result:
no goals

Proof state:
case neg
p : DyckWord
h : ¬p = 0
⊢ DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p) = p

Tactic:
rw [equivTreeToFun]

Result:
case neg
p : DyckWord
h : ¬p = 0
⊢ DyckWord.equivTreeInvFun
      (if h : p = 0 then Tree.nil
      else
        let_fun this := ⋯;
        let_fun this := ⋯;
        node () (DyckWord.equivTreeToFun p.insidePart) (DyckWord.equivTreeToFun p.outsidePart)) =
    p

Proof state:
p : DyckWord
⊢ DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p) = p

Tactic:
by_cases h : p = 0

Result:
case pos
p : DyckWord
h : p = 0
⊢ DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p) = p

case neg
p : DyckWord
h : ¬p = 0
⊢ DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p) = p

Proof state:
case neg
p : DyckWord
h : ¬p = 0
this✝ : p.insidePart.semilength < p.semilength
this : p.outsidePart.semilength < p.semilength
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
exact nest_insidePart_add_outsidePart h

Result:
no goals

Proof state:
case neg
p : DyckWord
h : ¬p = 0
this✝ : p.insidePart.semilength < p.semilength
this : p.outsidePart.semilength < p.semilength
⊢ (DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.insidePart)).nest +
      DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.outsidePart) =
    p

Tactic:
rw [equivTree_left_inv p.insidePart, equivTree_left_inv p.outsidePart]

Result:
case neg
p : DyckWord
h : ¬p = 0
this✝ : p.insidePart.semilength < p.semilength
this : p.outsidePart.semilength < p.semilength
⊢ p.insidePart.nest + p.outsidePart = p

Proof state:
case neg
p : DyckWord
h : ¬p = 0
⊢ (DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.insidePart)).nest +
      DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.outsidePart) =
    p

Tactic:
have := semilength_insidePart_lt h

Result:
case neg
p : DyckWord
h : ¬p = 0
this : p.insidePart.semilength < p.semilength
⊢ (DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.insidePart)).nest +
      DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.outsidePart) =
    p

Proof state:
case neg
p : DyckWord
h : ¬p = 0
this : p.insidePart.semilength < p.semilength
⊢ (DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.insidePart)).nest +
      DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.outsidePart) =
    p

Tactic:
have := semilength_outsidePart_lt h

Result:
case neg
p : DyckWord
h : ¬p = 0
this✝ : p.insidePart.semilength < p.semilength
this : p.outsidePart.semilength < p.semilength
⊢ (DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.insidePart)).nest +
      DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.outsidePart) =
    p

Proof state:
case neg
p : DyckWord
h : ¬p = 0
⊢ DyckWord.equivTreeInvFun
      (if h : p = 0 then Tree.nil
      else
        let_fun this := ⋯;
        let_fun this := ⋯;
        node () (DyckWord.equivTreeToFun p.insidePart) (DyckWord.equivTreeToFun p.outsidePart)) =
    p

Tactic:
simp_rw [h, dite_false, equivTreeInvFun]

Result:
case neg
p : DyckWord
h : ¬p = 0
⊢ (DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.insidePart)).nest +
      DyckWord.equivTreeInvFun (DyckWord.equivTreeToFun p.outsidePart) =
    p