case Qf
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (↑toLaurent f * T (-↑n))
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
⊢ Q f
induction' f using LaurentPolynomial.induction_on_mul_T with f n
case Qf.zero
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
⊢ Q (↑toLaurent f * T (-↑Nat.zero))

case Qf.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)))
case Qf
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (↑toLaurent f * T (-↑n))
induction' n with n hn
no goals
case Qf.zero
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
⊢ Q (↑toLaurent f * T (-↑Nat.zero))
simpa only [Nat.zero_eq, Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
case Qf.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)) * T 1)
case Qf.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)))
convert QT _ _
no goals
case Qf.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)) * T 1)
simpa using hn