awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
pos :
  ∀ (a0 : a = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
have neg : ∀ (a0 : ¬a = 0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
Tactic: by_cases a0 : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : a = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0
have rw : ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
Tactic: rw [a0, C_0, zero_mul, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : a = 0
rw : ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0
have rw₁ : (0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
Tactic: rw [a0, C_0, zero_mul, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : a = 0
rw : ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
rw₁ : (0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0
have rw₂ : natDegree.{u} (R := R) 0 = 0
Tactic: rw [a0, C_0, zero_mul, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : a = 0
rw : ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
rw₁ : (0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
rw₂ : natDegree.{u} (R := R) 0 = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [a0, C_0, zero_mul, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
have neg : M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Inductions (goal)
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
⊢ M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
have neg : M ((monomial (n + 1) : (a : R) → R[X]) a)
Tactic: rw [C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
t : R
n : ℤ
⊢ (((C : (a : R) → R[T;T⁻¹]) t : R[T;T⁻¹]) : (a : ℤ) → R) n = if n = 0 then t else 0
have rw : (if 0 = n then t else 0) = if n = 0 then t else 0
Tactic: rw [← single_eq_C, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℤ
⊢ T (m - n) = HMul.hMul (α := R[T;T⁻¹]) (T m) (T (-n))
have rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (m - n)) (T (m + -n))
Tactic: rw [← T_add, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (m - n)) (T (m + -n))
⊢ T (m - n) = HMul.hMul (α := R[T;T⁻¹]) (T m) (T (-n))
have rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (m + -n)) (T (m + -n))
Tactic: rw [← T_add, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m : ℤ
n : ℕ
⊢ HPow.hPow (α := R[T;T⁻¹]) (T m) n = T ((↑n : ℤ) * m)
have rw : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = T ((↑n : ℤ) * m)
Tactic: rw [T, T, single_pow, one_pow, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m : ℤ
n : ℕ
rw : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = T ((↑n : ℤ) * m)
⊢ HPow.hPow (α := R[T;T⁻¹]) (T m) n = T ((↑n : ℤ) * m)
have rw₁ : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = AddMonoidAlgebra.single ((↑n : ℤ) * m) 1
Tactic: rw [T, T, single_pow, one_pow, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m : ℤ
n : ℕ
rw : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = T ((↑n : ℤ) * m)
rw₁ : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = AddMonoidAlgebra.single ((↑n : ℤ) * m) 1
⊢ HPow.hPow (α := R[T;T⁻¹]) (T m) n = T ((↑n : ℤ) * m)
have rw₂ : Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) (HPow.hPow (α := R) 1 n)) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
Tactic: rw [T, T, single_pow, one_pow, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m : ℤ
n : ℕ
rw : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = T ((↑n : ℤ) * m)
rw₁ : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = AddMonoidAlgebra.single ((↑n : ℤ) * m) 1
rw₂ :
  Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) (HPow.hPow (α := R) 1 n))
    (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
⊢ HPow.hPow (α := R[T;T⁻¹]) (T m) n = T ((↑n : ℤ) * m)
have rw₃ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) 1) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
Tactic: rw [T, T, single_pow, one_pow, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
m : ℤ
n : ℕ
rw : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = T ((↑n : ℤ) * m)
rw₁ : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = AddMonoidAlgebra.single ((↑n : ℤ) * m) 1
rw₂ :
  Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) (HPow.hPow (α := R) 1 n))
    (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
rw₃ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) 1) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
⊢ HPow.hPow (α := R[T;T⁻¹]) (T m) n = T ((↑n : ℤ) * m)
have rw₄ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
Tactic: rw [T, T, single_pow, one_pow, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((Polynomial.C : (a : R) → R[X]) r) : R[T;T⁻¹])
    ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
have h : (C : (a : R) → R[T;T⁻¹]) r =
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑0 : ℤ))
Tactic: convert! Polynomial.toLaurent_C_mul_T 0 r
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) X : R[T;T⁻¹]) (T 1 : R[T;T⁻¹])
have this : Eq.{u_1 + 1} (α := R[X]) X ((monomial 1 : (a : R) → R[X]) 1)
Tactic: have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
⊢ HMul.hMul (α := R[T;T⁻¹]) (T (-n)) (T n) = 1
have rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (-n + n)) 1
Tactic: rw [← T_add, neg_add_cancel, T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (-n + n)) 1
⊢ HMul.hMul (α := R[T;T⁻¹]) (T (-n)) (T n) = 1
have rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1
Tactic: rw [← T_add, neg_add_cancel, T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (-n + n)) 1
rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1
⊢ HMul.hMul (α := R[T;T⁻¹]) (T (-n)) (T n) = 1
have rw₂ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) 1 1
Tactic: rw [← T_add, neg_add_cancel, T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
⊢ HMul.hMul (α := R[T;T⁻¹]) (T n) (T (-n)) = 1
have rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (n + -n)) 1
Tactic: rw [← T_add, add_neg_cancel, T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (n + -n)) 1
⊢ HMul.hMul (α := R[T;T⁻¹]) (T n) (T (-n)) = 1
have rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1
Tactic: rw [← T_add, add_neg_cancel, T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (n + -n)) 1
rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1
⊢ HMul.hMul (α := R[T;T⁻¹]) (T n) (T (-n)) = 1
have rw₂ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) 1 1
Tactic: rw [← T_add, add_neg_cancel, T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
n : ℤ
a : R
⊢ M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
have refine_1 : M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0))
Tactic: refine Int.induction_on n ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
n : ℤ
a : R
refine_1 : M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0))
⊢ M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
have refine_2 : ∀ (i : ℕ),
  M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑i : ℤ))) →
    M
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
        (T (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)))
Tactic: refine Int.induction_on n ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
n : ℤ
a : R
refine_1 : M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0))
refine_2 :
  ∀ (i : ℕ),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑i : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)))
⊢ M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
have refine_3 : ∀ (i : ℕ),
  M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑i : ℤ)))) →
    M
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
        (T (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)))
Tactic: refine Int.induction_on n ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
⊢ M p
have have : ∀ (A : ∀ {n : ℤ} {a : R}, M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))),
  M p
Tactic: have A : ∀ {n : ℤ} {a : R}, M (C a * T n) := by
    intro n a
    refine Int.induction_on n ?_ ?_ ?_
    · simpa only [T_zero, mul_one] using h_C a
    · exact fun m => h_C_mul_T m a
    · exact fun m => h_C_mul_T_Z m a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
A : ∀ {n : ℤ} {a : R}, M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (s : Finset ℤ),
    M
      (∑ n ∈ s,
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
have empty : M (∑ n ∈ ∅, HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
Tactic: apply Finset.induction
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
A : ∀ {n : ℤ} {a : R}, M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
empty :
  M
    (∑ n ∈ ∅,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
⊢ ∀ (s : Finset ℤ),
    M
      (∑ n ∈ s,
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
have insert : ∀ (a : ℤ) (s : Finset ℤ),
  a ∉ s →
    M
        (∑ n ∈ s,
          HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n)) →
      M
        (∑ n ∈ insert a s,
          HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
Tactic: apply Finset.induction
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
A : ∀ {n : ℤ} {a : R}, M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ M
    (∑ n ∈ ∅,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
have h : Eq.{u_1 + 1} (α := R[T;T⁻¹])
  (∑ n ∈ ∅, HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
  ((C : (a : R) → R[T;T⁻¹]) 0)
Tactic: convert! h_C 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
A : ∀ {n : ℤ} {a : R}, M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
n : ℤ
s : Finset ℤ
ns : n ∉ s
ih :
  M
    (∑ n ∈ s,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
⊢ M
    (∑ n ∈ insert n s,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
have insert : M
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n) +
    ∑ x ∈ s,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) x) : R[T;T⁻¹]) (T x))
Tactic: rw [Finset.sum_insert ns]