case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ M p
refine' p.induction_on (fun a => _) (fun {p q} => h_add p q) _ _ <;>
    try exact fun n f _ => h_C_mul_T _ f
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ ↑C a = ↑C a * T 0
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
convert h_C_mul_T 0 a
no goals
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ ↑C a = ↑C a * T 0
exact (mul_one _).symm
no goals
case refine'_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
exact fun n f _ => h_C_mul_T _ f