awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
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 p
have B : ∀ (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))
Tactic: have B : ∀ s : Finset ℤ, M (s.sum fun n : ℤ => C (p n) * T n) := by
    apply Finset.induction
    · convert! h_C 0
      simp only [Finset.sum_empty, map_zero]
    · intro n s ns ih
      rw [Finset.sum_insert ns]
      exact h_add A ih
-- 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))
B :
  ∀ (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))
⊢ M p
have h : p =
  ∑ n ∈ p.support,
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n)
Tactic: convert! B p.support
-- 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))
B :
  ∀ (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))
⊢ p =
    ∑ n ∈ p.support,
      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 : ∀ (a : ℤ),
  Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ n ∈ p.support,
            HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹])
              (T n) :
          (a : ℤ) → R)
        a :
      R)
Tactic: ext 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))
B :
  ∀ (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))
a : ℤ
⊢ Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ n ∈ p.support,
            HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹])
              (T n) :
          (a : ℤ) → R)
        a :
      R)
have h : Eq (α := R) ((p : (a : ℤ) → R) a : R)
  ((∑ x ∈ p.support, AddMonoidAlgebra.single x ((p : (a : ℤ) → R) x) : (a : ℤ) → R) a : R)
Tactic: simp_rw [← single_eq_C_mul_T]
-- 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))
B :
  ∀ (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))
a : ℤ
⊢ Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ x ∈ p.support, AddMonoidAlgebra.single x ((p : (a : ℤ) → R) x) : (a : ℤ) → R) a : R)
have h : ∀ b ∈ p.support,
  b ≠ a → Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
Tactic: rw [Finset.sum_apply', Finset.sum_eq_single a, single_eq_same]
-- 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))
B :
  ∀ (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))
a : ℤ
h :
  ∀ b ∈ p.support,
    b ≠ a → Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
⊢ Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ x ∈ p.support, AddMonoidAlgebra.single x ((p : (a : ℤ) → R) x) : (a : ℤ) → R) a : R)
have h₁ : a ∉ p.support → Eq (α := R) (((AddMonoidAlgebra.single a ((p : (a : ℤ) → R) a) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
Tactic: rw [Finset.sum_apply', Finset.sum_eq_single a, single_eq_same]
-- 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))
B :
  ∀ (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))
a b : ℤ
h : b ∈ p.support
hb : b ≠ a
⊢ Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
have h : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [single_eq_of_ne' hb]
-- 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))
B :
  ∀ (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))
a : ℤ
ha : a ∉ p.support
⊢ Eq (α := R) (((AddMonoidAlgebra.single a ((p : (a : ℤ) → R) a) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
have h : Eq (α := R) ((p : (a : ℤ) → R) a : R) (0 : R)
Tactic: rw [single_eq_same, notMem_support_iff.mp ha]
-- 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))
B :
  ∀ (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))
a : ℤ
ha : a ∉ p.support
h : Eq (α := R) ((p : (a : ℤ) → R) a : R) (0 : R)
⊢ Eq (α := R) (((AddMonoidAlgebra.single a ((p : (a : ℤ) → R) a) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
have h₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [single_eq_same, notMem_support_iff.mp ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ motive p
have refine_1 : ∀ (a : R), motive ((C : (a : R) → R[T;T⁻¹]) a)
Tactic: refine p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
refine_1 : ∀ (a : R), motive ((C : (a : R) → R[T;T⁻¹]) a)
⊢ motive p
have refine_2 : ∀ (n : ℕ) (a : R),
  motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
    motive
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
        (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
Tactic: refine p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
refine_1 : ∀ (a : R), motive ((C : (a : R) → R[T;T⁻¹]) a)
refine_2 :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
⊢ motive p
have refine_3 : ∀ (n : ℕ) (a : R),
  motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
    motive
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
        (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
Tactic: refine p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
a : R
⊢ motive ((C : (a : R) → R[T;T⁻¹]) a)
have h : (C : (a : R) → R[T;T⁻¹]) a = HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)
Tactic: convert! C_mul_T 0 a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ T n * HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T m) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T m) * T n
have rw : Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)))
  (AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1))
Tactic: rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
p q : R[T;T⁻¹]
hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p
hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
⊢ r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
have add : r • p + r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
Tactic: rw [smul_add, mul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
p q : R[T;T⁻¹]
hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p
hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
add : r • p + r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
⊢ r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
have add₁ : r • p + r • q =
  HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
Tactic: rw [smul_add, mul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
p q : R[T;T⁻¹]
hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p
hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
add : r • p + r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
add₁ :
  r • p + r • q =
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
      HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
⊢ r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
have add₂ : HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p + r • q =
  HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
Tactic: rw [smul_add, mul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
p q : R[T;T⁻¹]
hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p
hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
add : r • p + r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
add₁ :
  r • p + r • q =
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
      HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
add₂ :
  HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p + r • q =
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
      HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
⊢ r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
have add₃ : HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q =
  HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
Tactic: rw [smul_add, mul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℤ
s : R
⊢ r • HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n) =
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))
have C_mul_T : Eq (α := R[T;T⁻¹]) (Finsupp.single 0 (r * s)) ((C : (a : R) → R[T;T⁻¹]) (r * s))
Tactic: rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      Finsupp.smul_single']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[T;T⁻¹]
⊢ r • f = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) f
have add : ∀ (p q : R[T;T⁻¹]) (hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p)
  (hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q),
  r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
Tactic: induction f using LaurentPolynomial.induction_on' with
  | add _ _ hp hq =>
    rw [smul_add, mul_add, hp, hq]
  | C_mul_T n s =>
    rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      Finsupp.smul_single']
    rfl
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[T;T⁻¹]
add :
  ∀ (p q : R[T;T⁻¹]) (hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p)
    (hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q),
    r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
⊢ r • f = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) f
have C_mul_T : ∀ (n : ℤ) (s : R),
  r • HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n) =
    HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))
Tactic: induction f using LaurentPolynomial.induction_on' with
  | add _ _ hp hq =>
    rw [smul_add, mul_add, hp, hq]
  | C_mul_T n s =>
    rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      Finsupp.smul_single']
    rfl
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
⊢ Eq (α := R[X])
    ((trunc : (a : R[T;T⁻¹]) → R[X])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n)) :
      R[X])
    (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0 : R[X])
have a : Eq (α := R[ℕ])
  ((toFinsuppIso R : (a : R[X]) → R[ℕ])
      ((trunc : (a : R[T;T⁻¹]) → R[X])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n))) :
    R[ℕ])
  ((toFinsuppIso R : (a : R[X]) → R[ℕ]) (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])
Tactic: apply (toFinsuppIso R).injective
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
⊢ Eq (α := R[ℕ])
    ((toFinsuppIso R : (a : R[X]) → R[ℕ])
        ((trunc : (a : R[T;T⁻¹]) → R[X])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n))) :
      R[ℕ])
    ((toFinsuppIso R : (a : R[X]) → R[ℕ]) (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])
have a : Eq (α := R[ℕ])
  (((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ (↑x : ℤ)) sorry : (ℤ →₀ R) →+ ℕ →₀ R) : (a : R[T;T⁻¹]) → R[ℕ])
      (AddMonoidAlgebra.single n r) :
    R[ℕ])
  (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])
Tactic: simp only [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply,
    RingHom.toAddMonoidHom_eq_coe, RingEquiv.toRingHom_eq_coe, Int.ofNat_eq_natCast,
    AddMonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.apply_symm_apply, toFinsuppIso_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
⊢ Eq (α := R[ℕ])
    (((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ (↑x : ℤ)) ⋯ : (ℤ →₀ R) →+ ℕ →₀ R) : (a : R[T;T⁻¹]) → R[ℕ])
        (AddMonoidAlgebra.single n r) :
      R[ℕ])
    (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])
have a : Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) sorry)
  (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0))
Tactic: erw [comapDomain.addMonoidHom_apply Int.ofNat_injective]