Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case h1
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t2'.unit = List.length (left ++ right)

pp: case h2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t1.unit = List.length (left ++ right)

pp: case h_coef2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.coef ≠ 0

pp: case h_lt
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.unit < t1.unit

Tactic:
<;>

Goal state after:
case h1
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t2'.unit = List.length (left ++ right)

case h2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ List.length t1.unit = List.length (left ++ right)

case h_coef2
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.coef ≠ 0

case h_lt
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := ⋯
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.unit < t1.unit