-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[nolint unusedHavesSuffices]
lemma semilength_eq_numNodes_equivTree (p) : p.semilength = (equivTree p).numNodes

Proof state:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.semilength = (DyckWord.equivTreeToFun p.insidePart).numNodes + (DyckWord.equivTreeToFun p.outsidePart).numNodes + 1

Tactic:
have := semilength_insidePart_lt h

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

Proof state:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.semilength = (equivTree p).numNodes

Tactic:
rw [equivTree, Equiv.coe_fn_mk, equivTreeToFun]

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

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

Tactic:
rfl

Result:
no goals

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

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
⊢ p.semilength = (DyckWord.equivTreeToFun p.insidePart).numNodes + (DyckWord.equivTreeToFun p.outsidePart).numNodes + 1

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

Tactic:
simp_rw [h, dite_false, numNodes]

Result:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.semilength = (DyckWord.equivTreeToFun p.insidePart).numNodes + (DyckWord.equivTreeToFun p.outsidePart).numNodes + 1

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

Tactic:
rw [← semilength_insidePart_add_semilength_outsidePart_add_one h,
  semilength_eq_numNodes_equivTree p.insidePart,
  semilength_eq_numNodes_equivTree p.outsidePart]

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

Proof state:
p : DyckWord
⊢ p.semilength = (equivTree p).numNodes

Tactic:
by_cases h : p = 0

Result:
case pos
p : DyckWord
h : p = 0
⊢ p.semilength = (equivTree p).numNodes

case neg
p : DyckWord
h : ¬p = 0
⊢ p.semilength = (equivTree p).numNodes

Proof state:
case pos
p : DyckWord
h : p = 0
⊢ p.semilength = (equivTree p).numNodes

Tactic:
simp [h, equivTree, equivTreeToFun]

Result:
no goals