awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₂ :
  reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₃ : reflect n (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₄ :
  reflect n
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₅ :
  (reflect n
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₆ :
  (reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)) +
          reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₇ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) k : ℕ)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
      reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
    HPow.hPow (α := R[X]) X k =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ ¬IsUnit p
have obtain : ∀ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ), ¬IsUnit (M := ℤ[X]) (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
Tactic: obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ #p.support = 3
have obtain : ∀ (k m n : ℕ) (hkm : k < m) (hmn : m < n) (u v w : ℤˣ), #(support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))) = 3
Tactic: obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
k : ℕ
hk : k ∈ p.support
⊢ IsUnit (p.coeff k)
have 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)
Tactic: obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
Cleared hypotheses: p, hp, hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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 : ℤ))
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
have this : Membership.mem (γ := Finset ℕ) {k, m, n} k_1
Tactic: have := support_trinomial' k m n (u : ℤ) v w hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
have this₁ : k_1 = k ∨ k_1 = m ∨ k_1 = n
Tactic: rw [mem_insert, mem_insert, mem_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
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
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
have 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)
Tactic: rcases this with (rfl | rfl | rfl)
Cleared hypotheses: k, hkm, hk, this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
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)
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
have 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)
Tactic: rcases this with (rfl | rfl | rfl)
Cleared hypotheses: m, hkm, hmn, hk, this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
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)
⊢ IsUnit (coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1)
have 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)
Tactic: rcases this with (rfl | rfl | rfl)
Cleared hypotheses: n, hmn, hk, this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ support (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ))
⊢ (↑u : ℤ) = coeff (trinomial k m n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k
have rw : (↑u : ℤ) = (↑u : ℤ)
Tactic: rw [trinomial_trailing_coeff' hkm hmn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
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 : ℤ))
⊢ (↑v : ℤ) = coeff (trinomial k k_1 n (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1
have rw : (↑v : ℤ) = (↑v : ℤ)
Tactic: rw [trinomial_middle_coeff hkm hmn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
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 : ℤ))
⊢ (↑w : ℤ) = coeff (trinomial k m k_1 (↑u : ℤ) (↑v : ℤ) (↑w : ℤ)) k_1
have rw : (↑w : ℤ) = (↑w : ℤ)
Tactic: rw [trinomial_leading_coeff' hkm hmn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
have refine : ∀ (hp : #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)), p.IsUnitTrinomial
Tactic: refine ⟨fun hp => ⟨hp.card_support_eq_three, fun k => hp.coeff_isUnit⟩, fun hp => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
p : ℤ[X]
hp : #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
⊢ p.IsUnitTrinomial
have 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
Tactic: obtain ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩ := card_support_eq_three.mp hp.1
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have 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)
Tactic: rw [support_trinomial hkm hmn hx hy hz] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have 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)
Tactic: replace hx := hp.2 k (mem_insert_self k {m, n})
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have 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)
Tactic: replace hy := hp.2 m (mem_insert_of_mem (mem_insert_self m {n}))
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have 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)
Tactic: replace hz := hp.2 n (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n)))
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have hx₁ : 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
Cleared hypotheses: hx, hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have hy₁ : 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
Cleared hypotheses: hx, hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have hz₁ : 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
Cleared hypotheses: hx, hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (hypothesis)
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)
⊢ (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
have hx₁ : IsUnit (x + y * 0 + z * 0)
Tactic: rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx
Cleared hypotheses: hx, hy, hz