awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
hp : IsUnitTrinomial 0
⊢ False

Tactic:
simpa using hp.card_support_eq_three

Premises used: Polynomial.IsUnitTrinomial.card_support_eq_three
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
k : ℕ
hk : k ∈ p.support
obtain :
  ∀ (k_1 m n : ℕ) (hkm : k_1 < m) (hmn : m < n) (u v w : ℤˣ)
    (hk : k ∈ support (trinomial k_1 m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))),
    IsUnit (coeff (trinomial k_1 m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k)
⊢ IsUnit (p.coeff k)

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k_1 ∈ support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
⊢ Membership.mem (γ := Finset ℕ) {k, m, n} k_1

Tactic:
have := support_trinomial' k m n (u : ℤ) v w hk
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k_1 ∈ support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
this : Membership.mem (γ := Finset ℕ) {k, m, n} k_1
⊢ k_1 = k ∨ k_1 = m ∨ k_1 = n

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at this

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k_1 ∈ support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
this : k_1 = k ∨ k_1 = m ∨ k_1 = n
inl :
  ∀ (hkm : k_1 < m) (hk : k_1 ∈ support (trinomial k_1 m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))),
    IsUnit (coeff (trinomial k_1 m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
inr :
  ∀ (hkm : k < k_1) (hmn : k_1 < n) (hk : k_1 ∈ support (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))),
    IsUnit (coeff (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
inr₁ :
  ∀ (hmn : m < k_1) (hk : k_1 ∈ support (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))),
    IsUnit (coeff (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)

Tactic:
rcases this with (rfl | rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
rw rw₁ : (↑u : ℤ) = (↑u : ℤ)
⊢ (↑u : ℤ) = coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k

Tactic:
rw [trinomial_trailing_coeff' hkm hmn]

Premises used: Polynomial.trinomial_trailing_coeff'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k)

Tactic:
refine ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k n : ℕ
u v w : ℤˣ
hkm : k < k_1
hmn : k_1 < n
hk : k_1 ∈ support (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
rw rw₁ : (↑v : ℤ) = (↑v : ℤ)
⊢ (↑v : ℤ) = coeff (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1

Tactic:
rw [trinomial_middle_coeff hkm hmn]

Premises used: Polynomial.trinomial_middle_coeff
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k n : ℕ
u v w : ℤˣ
hkm : k < k_1
hmn : k_1 < n
hk : k_1 ∈ support (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
⊢ IsUnit (coeff (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)

Tactic:
refine ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k_1
hk : k_1 ∈ support (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
rw rw₁ : (↑w : ℤ) = (↑w : ℤ)
⊢ (↑w : ℤ) = coeff (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1

Tactic:
rw [trinomial_leading_coeff' hkm hmn]

Premises used: Polynomial.trinomial_leading_coeff'
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k_1 k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k_1
hk : k_1 ∈ support (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
⊢ IsUnit (coeff (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)

Tactic:
refine ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ IsUnit p.leadingCoeff

Tactic:
hp.coeff_isUnit (natDegree_mem_support_of_nonzero hp.ne_zero)

Premises used: Polynomial.IsUnitTrinomial.coeff_isUnit, Polynomial.leadingCoeff, Polynomial.natDegree_mem_support_of_nonzero, Polynomial.IsUnitTrinomial.ne_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ IsUnit p.trailingCoeff

Tactic:
hp.coeff_isUnit (natTrailingDegree_mem_support_of_nonzero hp.ne_zero)

Premises used: Polynomial.IsUnitTrinomial.coeff_isUnit, Polynomial.trailingCoeff, Polynomial.natTrailingDegree_mem_support_of_nonzero, Polynomial.IsUnitTrinomial.ne_zero
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)

Tactic:
⟨fun hp => ⟨hp.card_support_eq_three, fun k => hp.coeff_isUnit⟩, fun hp => ?_⟩

Premises used: Polynomial.IsUnitTrinomial.coeff_isUnit, Polynomial.IsUnitTrinomial.card_support_eq_three, And.intro, Iff.intro
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
refine : ∀ (hp : #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)), p.IsUnitTrinomial
⊢ p.IsUnitTrinomial ↔ #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)

Tactic:
refine ⟨fun hp => ⟨hp.card_support_eq_three, fun k => hp.coeff_isUnit⟩, fun hp => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
obtain :
  ∀ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (x y z : ℤ) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0)
    (hp :
      #(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)).support =
          3 ∧
        ∀
          k_1 ∈
            (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)).support,
          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)),
    (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
⊢ p.IsUnitTrinomial

Tactic:
obtain ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩ := card_support_eq_three.mp hp.1

Premises used: Polynomial.card_support_eq_three, And.left, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp :
  #(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)).support =
      3 ∧
    ∀
      k_1 ∈
        (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)).support,
      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)
⊢ 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)

Tactic:
rw [support_trinomial hkm hmn hx hy hz] at hp

Premises used: Polynomial.support_trinomial
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
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)
⊢ 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)

Tactic:
replace hx := hp.2 k (mem_insert_self k {m, n})
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hy : y ≠ 0
hz : z ≠ 0
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
    ((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)
⊢ 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
      m)

Tactic:
replace hy := hp.2 m (mem_insert_of_mem (mem_insert_self m {n}))
-- Module: Mathlib.Algebra.Polynomial.UnitTrinomial
Goal:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hz : z ≠ 0
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
    ((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)
hy :
  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
      m)
⊢ 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
      n)

Tactic:
replace hz := hp.2 n (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n)))
-- 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
    ((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)
hy :
  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
      m)
hz :
  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
      n)
⊢ IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)

Tactic:
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.coeff_add, Polynomial.coeff_X_pow_self, mul_one
-- 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
    ((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)
hy :
  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
      m)
hz :
  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
      n)
hx₁ : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
⊢ IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)

Tactic:
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.coeff_add, Polynomial.coeff_X_pow_self, mul_one
-- 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
    ((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)
hy :
  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
      m)
hz :
  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
      n)
hx₁ : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy₁ : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
⊢ IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)

Tactic:
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.coeff_add, Polynomial.coeff_X_pow_self, mul_one
-- 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 * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnit (x + y * 0 + z * 0)

Tactic:
rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx

Premises used: LT.lt.trans, if_neg, LT.lt.ne
-- 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 * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
hx₁ : IsUnit (x + y * 0 + z * 0)
⊢ IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)

Tactic:
rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx

Premises used: LT.lt.trans, if_neg, LT.lt.ne
-- 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 * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
hx₁ : IsUnit (x + y * 0 + z * 0)
hy₁ : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
⊢ IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)

Tactic:
rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx

Premises used: LT.lt.trans, if_neg, LT.lt.ne
-- 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 * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnit (x * 0 + y + z * 0)

Tactic:
rw [if_neg hkm.ne', if_neg hmn.ne] at hy

Premises used: LT.lt.ne', if_neg, LT.lt.ne
-- 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 * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
hy₁ : IsUnit (x * 0 + y + z * 0)
⊢ IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)

Tactic:
rw [if_neg hkm.ne', if_neg hmn.ne] at hy

Premises used: LT.lt.ne', if_neg, LT.lt.ne
-- 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 * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ IsUnit (x * 0 + y * 0 + z)

Tactic:
rw [if_neg (hkm.trans hmn).ne', if_neg hmn.ne'] at hz

Premises used: LT.lt.ne', LT.lt.trans, if_neg
-- 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)
⊢ IsUnit z

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

Premises used: zero_add, MulZeroClass.mul_zero, add_zero