awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
hz₁ : IsUnit z
⊢ IsUnit x

Tactic:
simp_rw [mul_zero, zero_add, add_zero] at hx hy hz

Premises used: zero_add, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
hz₁ : IsUnit z
hx₁ : IsUnit x
⊢ IsUnit y

Tactic:
simp_rw [mul_zero, zero_add, add_zero] at hx hy hz

Premises used: zero_add, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hz : IsUnit z
hx : IsUnit x
hy : IsUnit y
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial

Tactic:
⟨k, m, n, hkm, hmn, hx.unit, hy.unit, hz.unit, rfl⟩

Premises used: Polynomial.IsUnitTrinomial, Exists.intro, IsUnit.unit, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp :
  card (α := ℕ) {k, m, n} = 3 ∧
    ∀ (k_1 : ℕ),
      Membership.mem (γ := Finset ℕ) {k, m, n} k_1 →
        IsUnit
          ((HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
                  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
                HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).coeff
            k_1)
hz : IsUnit z
hx : IsUnit x
hy : IsUnit y
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) x : ℤ[X]) (HPow.hPow (α := ℤ[X]) X k) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) y : ℤ[X]) (HPow.hPow (α := ℤ[X]) X m) +
      HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) z : ℤ[X]) (HPow.hPow (α := ℤ[X]) X n)).IsUnitTrinomial

Tactic:
exact ⟨k, m, n, hkm, hmn, hx.unit, hy.unit, hz.unit, rfl⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
rw : p.IsUnitTrinomial ↔ Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3

Tactic:
rw [natDegree_mul_mirror, natTrailingDegree_mul_mirror, ← mul_add,
    Nat.mul_div_right _ zero_lt_two, coeff_mul_mirror]

Premises used: Polynomial.natDegree_mul_mirror, Polynomial.natTrailingDegree_mul_mirror, mul_add, zero_lt_two, Polynomial.coeff_mul_mirror, Nat.mul_div_right
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3

Tactic:
⟨?_, fun hp => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
refine_1 : p.IsUnitTrinomial → Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
refine_2 : ∀ (hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3), p.IsUnitTrinomial
⊢ p.IsUnitTrinomial ↔ Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3

Tactic:
refine ⟨?_, fun hp => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
refine_1 : HPow.hPow (β := ℕ) (↑u : ℤ) 2 + (HPow.hPow (β := ℕ) (↑v : ℤ) 2 + HPow.hPow (β := ℕ) (↑w : ℤ) 2) = 3
⊢ Eq (α := ℤ) (sum (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3

Tactic:
rw [sum_def, trinomial_support hkm hmn u.ne_zero v.ne_zero w.ne_zero,
      sum_insert (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
      sum_insert (mt mem_singleton.mp hmn.ne), sum_singleton, trinomial_leading_coeff' hkm hmn,
      trinomial_middle_coeff hkm hmn, trinomial_trailing_coeff' hkm hmn]

Premises used: Finset.mem_singleton, Polynomial.trinomial_trailing_coeff', Polynomial.trinomial_leading_coeff', mt, Units.ne_zero, Finset.mem_insert, not_or_intro, Finset.sum_singleton, Polynomial.trinomial_middle_coeff, Polynomial.sum_def, Iff.mp, LT.lt.trans, Polynomial.trinomial_support, Finset.sum_insert, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
refine_1 : 1 + HAdd.hAdd (α := ℤ) 1 1 = 3
⊢ HPow.hPow (β := ℕ) (↑u : ℤ) 2 + (HPow.hPow (β := ℕ) (↑v : ℤ) 2 + HPow.hPow (β := ℕ) (↑w : ℤ) 2) = 3

Tactic:
simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq, Units.val_one]

Premises used: Int.units_sq, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ 1 + HAdd.hAdd (α := ℤ) 1 1 = 3

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
⊢ ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1

Tactic:
have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk =>
      Int.sq_eq_one_of_sq_le_three
        ((single_le_sum (fun k _ => sq_nonneg (p.coeff k)) hk).trans hp.le) (mem_support_iff.mp hk)
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
⊢ p.IsUnitTrinomial

Tactic:
isUnitTrinomial_iff.mpr ⟨?_, fun k hk => .of_pow_eq_one (key k hk) two_ne_zero⟩

Premises used: Iff.mpr, Polynomial.isUnitTrinomial_iff, two_ne_zero, And.intro, IsUnit.of_pow_eq_one
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
refine_2 : #p.support = 3
⊢ p.IsUnitTrinomial

Tactic:
refine isUnitTrinomial_iff.mpr ⟨?_, fun k hk => .of_pow_eq_one (key k hk) two_ne_zero⟩

Premises used: Iff.mpr, Polynomial.isUnitTrinomial_iff, two_ne_zero, And.intro, IsUnit.of_pow_eq_one
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
⊢ Eq (α := ℤ) (↑(#p.support) : ℤ) 3

Tactic:
rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_cast] at hp

Premises used: Polynomial.sum_def, Nat.smul_one_eq_cast, Finset.sum_congr, rfl, Finset.sum_const
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (p.sum fun (x : ℕ) (x_1 : ℤ) ↦ HPow.hPow (β := ℕ) x_1 2) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
hp₁ : Eq (α := ℤ) (↑(#p.support) : ℤ) 3
⊢ ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1

Tactic:
rw [sum_def, sum_congr rfl key, sum_const, Nat.smul_one_eq_cast] at hp

Premises used: Polynomial.sum_def, Nat.smul_one_eq_cast, Finset.sum_congr, rfl, Finset.sum_const
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (↑(#p.support) : ℤ) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
⊢ #p.support = 3

Tactic:
Nat.cast_injective hp

Premises used: Nat.cast_injective
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : Eq (α := ℤ) (↑(#p.support) : ℤ) 3
key : ∀ k ∈ p.support, HPow.hPow (β := ℕ) (p.coeff k) 2 = 1
⊢ #p.support = 3

Tactic:
exact Nat.cast_injective hp

Premises used: Nat.cast_injective
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
rw : (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔ q.IsUnitTrinomial
rw₁ :
  (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔
    (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
rw₂ rw₃ :
  (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3 ↔
    (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial

Tactic:
rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]

Premises used: Polynomial.isUnitTrinomial_iff'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
rwa : n - m < n - k
rwa₁ rwa₂ rwa₃ rwa₄ : k < m
⊢ n - m + k < n

Tactic:
rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]

Premises used: lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le, LT.lt.le
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
⊢ n - m + k < n

Tactic:
have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
    {
      toFinsupp :=
        Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
          (HMul.hMul (α := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
              (trinomial k (n - m + k) n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ))).toFinsupp }
⊢ HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
    { toFinsupp := Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }

Tactic:
rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero]

Premises used: Units.ne_zero, Polynomial.trinomial_mirror
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
simp_rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + k) ((↑u : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (k + (n - m + k)) ((↑u : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (k + n) ((↑u : ℤ) * (↑u : ℤ))) +
            (HAdd.hAdd (α := ℕ →₀ ℤ)
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + k) ((↑v : ℤ) * (↑w : ℤ))))
                (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + (n - m + k)) ((↑v : ℤ) * (↑v : ℤ)))) +
              Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ)
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + k) ((↑w : ℤ) * (↑w : ℤ))))
              (Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
                (AddMonoidAlgebra.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)))) +
            Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
              (AddMonoidAlgebra.single (n + n) ((↑w : ℤ) * (↑u : ℤ)))) }
⊢ HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (m + n)) +
        HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) (HPow.hPow (α := ℤ[X]) X (n - m + k + n))) =
    {
      toFinsupp :=
        Finsupp.filter (fun (x : ℕ) ↦ x ∈ Set.Ioo (k + n) (n + n))
          (HMul.hMul (α := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
              (trinomial k (n - m + k) n (↑w : ℤ) (↑v : ℤ) (↑u : ℤ))).toFinsupp }

Tactic:
simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial,
    toFinsupp_add, toFinsupp_monomial, AddMonoidAlgebra, Finsupp.filter_add]

Premises used: add_mul, Polynomial.toFinsupp_monomial, Polynomial.C_mul_X_pow_eq_monomial, Finsupp.filter_add, Polynomial.trinomial_def, Polynomial.toFinsupp_add, mul_add, AddMonoidAlgebra, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
simp :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) (Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))
          (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) }
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + 0 + (HAdd.hAdd (α := ℕ →₀ ℤ) 0 0 + Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ))) +
          (HAdd.hAdd (α := ℕ →₀ ℤ) 0 (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) + 0) }

Tactic:
simp only [add_zero, zero_add]

Premises used: zero_add, add_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) { toFinsupp := Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ)) }
      { toFinsupp := Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ)) }
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    {
      toFinsupp :=
        HAdd.hAdd (α := ℕ →₀ ℤ) (Finsupp.single (m + n) ((↑v : ℤ) * (↑u : ℤ)))
          (Finsupp.single (n + (n - m + k)) ((↑w : ℤ) * (↑v : ℤ))) }

Tactic:
rw [ofFinsupp_add]

Premises used: Polynomial.ofFinsupp_add
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
rw :
  HAdd.hAdd (α := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X])) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
rw₁ :
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑w : ℤ)) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
rw₂ :
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
rw₃ rw₄ :
  HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (m + n) : (a : ℤ) → ℤ[X]) (↑u : ℤ) : ℤ[X]) +
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑v : ℤ) : ℤ[X])
        ((monomial (n - m + k + n) : (a : ℤ) → ℤ[X]) (↑w : ℤ) : ℤ[X]) =
    HAdd.hAdd (α := ℤ[X]) (β := ℤ[X]) ((monomial (m + n) : (a : ℤ) → ℤ[X]) ((↑v : ℤ) * (↑u : ℤ)) : ℤ[X])
      ((monomial (n + (n - m + k)) : (a : ℤ) → ℤ[X]) ((↑w : ℤ) * (↑v : ℤ)) : ℤ[X])

Tactic:
rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]

Premises used: Units.val, HSub.hSub, Polynomial.C_mul_monomial, add_comm, HAdd.hAdd, mul_comm
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
fun h => h.2.ne rfl

Premises used: And.right, Not, rfl, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => h.2.ne rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + (n - m + k) < n + n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
h : k + n < n + (n - m + k)
⊢ n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)

Tactic:
refine ⟨?_, by gcongr⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
h : n + k < n + (n - m + k)
h₁ : k < n - m + k
h₂ : 0 < n - m
h₃ h₄ h₅ h₆ : m < n
⊢ k + n < n + (n - m + k)

Tactic:
rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]

Premises used: tsub_pos_iff_lt, add_comm, lt_add_iff_pos_left, add_lt_add_iff_left
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
fun h => h.1.ne (add_comm k n)

Premises used: add_comm, And.left, Not, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => h.1.ne (add_comm k n)
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
h : k + n < m + n
h₁ : m + n < n + n
⊢ m + n ∈ Set.Ioo (k + n) (n + n)

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ k + n < m + n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ m + n < n + n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
h : n + k ∉ Set.Ioo (n + k) (n + n)
⊢ m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

Tactic:
rw [← add_assoc, add_tsub_cancel_of_le hmn.le, add_comm]

Premises used: add_assoc, LT.lt.le, add_comm, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (n + k) (n + n)

Tactic:
fun h => h.1.ne rfl

Premises used: And.left, Not, rfl, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (n + k) (n + n)

Tactic:
exact fun h => h.1.ne rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
fun h => h.1.ne rfl

Premises used: And.left, Not, rfl, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
exact fun h => h.1.ne rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

Tactic:
fun h => asymm ((add_lt_add_iff_left k).mp h.1) key

Premises used: asymm, And.left, Iff.mp, Not, add_lt_add_iff_left