awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
⊢ dickson 2 0 1 = HPow.hPow (α := R[X]) (β := ℕ) X 1

Tactic:
simp only [dickson_one, pow_one]

Premises used: pow_one, Polynomial.dickson_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
simp : HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)
⊢ dickson 2 0 (n + 2) = HPow.hPow (α := R[X]) X (n + 2)

Tactic:
simp only [dickson_add_two, C_0, zero_mul, sub_zero]

Premises used: sub_zero, Polynomial.C_0, MulZeroClass.zero_mul, Polynomial.dickson_add_two
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 2)
rw₁ : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
rw₂ : HPow.hPow (α := R[X]) X (n + 1) * X = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
rw₃ rw₄ : HPow.hPow (α := R[X]) X (n + 1) * X = HPow.hPow (α := R[X]) X (n + 1) * X
⊢ HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)

Tactic:
rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]

Premises used: pow_add, HAdd.hAdd, pow_one, mul_comm, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
simp : eval (x + y) (HSub.hSub (α := R[X]) 3 (↑1 : R[X])) = HAdd.hAdd (α := R) 1 1
⊢ eval (x + y) (dickson 1 1 0) = HPow.hPow (β := ℕ) x 0 + HPow.hPow (β := ℕ) y 0

Tactic:
simp only [pow_zero, dickson_zero]

Premises used: pow_zero, Polynomial.dickson_zero
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (HSub.hSub (α := R[X]) 3 (↑1 : R[X])) = HAdd.hAdd (α := R) 1 1

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 1) = HPow.hPow (β := ℕ) x 1 + HPow.hPow (β := ℕ) y 1

Tactic:
simp only [eval_X, dickson_one, pow_one]

Premises used: Polynomial.eval_X, pow_one, Polynomial.dickson_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
simp : (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
⊢ eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,
      C_1, eval_one]

Premises used: Polynomial.C_1, Polynomial.eval_X, Polynomial.eval_mul, Polynomial.dickson_add_two, Polynomial.eval_one, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
simp : x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n)
| (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n)

Tactic:
simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]

Premises used: add_mul, mul_assoc, mul_comm, mul_add, pow_succ', one_mul
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
conv_lhs : x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]

Premises used: add_mul, mul_assoc, mul_comm, mul_add, pow_succ', one_mul
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
rw :
  HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
      ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    1
rw₁ :
  Eq (α := R[X])
    ((C : (a : R) → R[X])
        (HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
      R[X])
    (1 : R[X])
rw₂ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1

Tactic:
rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]

Premises used: Polynomial.C_1, two_mul, Polynomial.C_add, invOf_two_add_invOf_two
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
rw : HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) 2 = 1

Tactic:
rw [mul_comm, two_mul_C_half_eq_one]

Premises used: _private.0.Polynomial.two_mul_C_half_eq_one, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
⊢ HSub.hSub (α := R[X]) 3 (↑1 : R[X]) = Chebyshev.C R (↑0 : ℤ)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
rw : Eq (α := R[X]) X (Chebyshev.C R (↑1 : ℤ))
rw₁ : Eq (α := R[X]) X (Chebyshev.C R 1)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) X X
⊢ Eq (α := R[X]) (dickson 1 1 1) (Chebyshev.C R (↑1 : ℤ))

Tactic:
rw [dickson_one, Nat.cast_one, Chebyshev.C_one]

Premises used: Polynomial.Chebyshev.C_one, Polynomial.dickson_one, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw :
  HMul.hMul (α := R[X]) X (Chebyshev.C R (↑(n + 1) : ℤ)) - HMul.hMul (α := R[X]) 1 (Chebyshev.C R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) X (Chebyshev.C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - Chebyshev.C R (↑n : ℤ)
⊢ Eq (α := R[X]) (dickson 1 1 (n + 2)) (Chebyshev.C R (↑(n + 2) : ℤ))

Tactic:
rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.C_add_two,
      dickson_one_one_eq_chebyshev_C (n + 1), dickson_one_one_eq_chebyshev_C n]

Premises used: Polynomial.C_1, Polynomial.dickson_add_two, Nat.cast_add, HAdd.hAdd, Polynomial.Chebyshev.C_add_two, OfNat.ofNat, Nat.cast_two
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ HMul.hMul (α := R[X]) X (Chebyshev.C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
      HMul.hMul (α := R[X]) 1 (Chebyshev.C R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) X (Chebyshev.C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - Chebyshev.C R (↑n : ℤ)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℕ
⊢ dickson 1 1 n =
    2 *
      comp (Chebyshev.T R (↑n : ℤ))
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
(dickson_one_one_eq_chebyshev_C R n).trans (Chebyshev.C_eq_two_mul_T_comp_half_mul_X R n)

Premises used: Polynomial.dickson_one_one_eq_chebyshev_C, Nat.cast, Polynomial.Chebyshev.C_eq_two_mul_T_comp_half_mul_X, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℕ
⊢ Chebyshev.T R (↑n : ℤ) =
    (C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
      comp (dickson 1 1 n) (HMul.hMul (α := R[X]) 2 X)

Tactic:
dickson_one_one_eq_chebyshev_C R n ▸ Chebyshev.T_eq_half_mul_C_comp_two_mul_X R n

Premises used: Polynomial.dickson_one_one_eq_chebyshev_C, Eq.rec, Nat.cast, Polynomial.Chebyshev.T_eq_half_mul_C_comp_two_mul_X, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
⊢ HSub.hSub (α := R[X]) 3 (↑2 : R[X]) = Chebyshev.S R (↑0 : ℤ)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
rw : Eq (α := R[X]) X (Chebyshev.S R (↑1 : ℤ))
rw₁ : Eq (α := R[X]) X (Chebyshev.S R 1)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) X X
⊢ Eq (α := R[X]) (dickson 2 1 1) (Chebyshev.S R (↑1 : ℤ))

Tactic:
rw [dickson_one, Nat.cast_one, Chebyshev.S_one]

Premises used: Polynomial.dickson_one, Nat.cast_one, Polynomial.Chebyshev.S_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw :
  HMul.hMul (α := R[X]) X (Chebyshev.S R (↑(n + 1) : ℤ)) - HMul.hMul (α := R[X]) 1 (Chebyshev.S R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) X (Chebyshev.S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - Chebyshev.S R (↑n : ℤ)
⊢ Eq (α := R[X]) (dickson 2 1 (n + 2)) (Chebyshev.S R (↑(n + 2) : ℤ))

Tactic:
rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.S_add_two,
      dickson_two_one_eq_chebyshev_S (n + 1), dickson_two_one_eq_chebyshev_S n]

Premises used: Polynomial.C_1, Polynomial.dickson_add_two, Nat.cast_add, HAdd.hAdd, Polynomial.Chebyshev.S_add_two, OfNat.ofNat, Nat.cast_two
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ HMul.hMul (α := R[X]) X (Chebyshev.S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
      HMul.hMul (α := R[X]) 1 (Chebyshev.S R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) X (Chebyshev.S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - Chebyshev.S R (↑n : ℤ)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℕ
⊢ dickson 2 1 n =
    comp (Chebyshev.U R (↑n : ℤ))
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
(dickson_two_one_eq_chebyshev_S R n).trans (Chebyshev.S_eq_U_comp_half_mul_X R n)

Premises used: Polynomial.dickson_two_one_eq_chebyshev_S, Polynomial.Chebyshev.S_eq_U_comp_half_mul_X, Nat.cast, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Chebyshev.U R (↑n : ℤ) = comp (dickson 2 1 n) (HMul.hMul (α := R[X]) 2 X)

Tactic:
dickson_two_one_eq_chebyshev_S R n ▸ (Chebyshev.S_comp_two_mul_X R n).symm

Premises used: Polynomial.dickson_two_one_eq_chebyshev_S, Polynomial.Chebyshev.S_comp_two_mul_X, Eq.rec, Nat.cast, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
⊢ Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)

Tactic:
simp only [eq_intCast, Int.cast_one]

Premises used: eq_intCast, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
⊢ Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)

Tactic:
have h : (1 : R) = Int.castRingHom R 1 := by simp only [eq_intCast, Int.cast_one]
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
rw :
  Eq (α := R[X]) (dickson 1 ((Int.castRingHom R : (a : ℤ) → R) 1) (m * n) : R[X])
    (comp (dickson 1 ((Int.castRingHom R : (a : ℤ) → R) 1) m) (dickson 1 ((Int.castRingHom R : (a : ℤ) → R) 1) n) :
      R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
simp :
  Eq.{u_1 + 1} (α := R[X]) (map (R := ℤ) (Int.castRingHom R) (dickson 1 1 (m * n)))
    (map (R := ℤ) (Int.castRingHom R) (comp (dickson 1 1 m) (dickson 1 1 n)))
⊢ Eq (α := R[X]) (dickson 1 ((Int.castRingHom R : (a : ℤ) → R) 1) (m * n) : R[X])
    (comp (dickson 1 ((Int.castRingHom R : (a : ℤ) → R) 1) m) (dickson 1 ((Int.castRingHom R : (a : ℤ) → R) 1) n) :
      R[X])

Tactic:
simp only [← map_dickson (Int.castRingHom R), ← map_comp]

Premises used: Polynomial.map_dickson, Int.castRingHom, Polynomial.map_comp
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
e_a : Eq (α := ℤ[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))
⊢ Eq.{u_1 + 1} (α := R[X]) (map (R := ℤ) (Int.castRingHom R) (dickson 1 1 (m * n)))
    (map (R := ℤ) (Int.castRingHom R) (comp (dickson 1 1 m) (dickson 1 1 n)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
e_a : map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))
⊢ Eq (α := ℤ[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))

Tactic:
apply map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, Polynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
e_a :
  ((HAdd.hAdd (α := ℚ[X]) (Chebyshev.T ℚ (↑m : ℤ)) (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ))).comp
      (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X) =
    ((HAdd.hAdd (α := ℚ[X]) (Chebyshev.T ℚ (↑m : ℤ)) (Chebyshev.T ℚ (↑m : ℤ))).comp
          (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
            X)).comp
      ((HAdd.hAdd (α := ℚ[X]) (Chebyshev.T ℚ (↑n : ℤ)) (Chebyshev.T ℚ (↑n : ℤ))).comp
        (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
⊢ map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))

Tactic:
simp only [map_dickson, map_comp, eq_intCast, Int.cast_one, dickson_one_one_eq_chebyshev_T,
    Nat.cast_mul, Chebyshev.T_mul, two_mul, ← add_comp]

Premises used: Polynomial.map_dickson, Polynomial.Chebyshev.T_mul, two_mul, eq_intCast, Polynomial.add_comp, Nat.cast_mul, Polynomial.dickson_one_one_eq_chebyshev_T, Polynomial.map_comp, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
e_a :
  ((HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ))).comp
      (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X) =
    (((HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp
              (HMul.hMul (α := ℚ[X])
                ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)).comp
          (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))).comp
      (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)
⊢ ((HAdd.hAdd (α := ℚ[X]) (Chebyshev.T ℚ (↑m : ℤ)) (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ))).comp
      (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X) =
    ((HAdd.hAdd (α := ℚ[X]) (Chebyshev.T ℚ (↑m : ℤ)) (Chebyshev.T ℚ (↑m : ℤ))).comp
          (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
            X)).comp
      ((HAdd.hAdd (α := ℚ[X]) (Chebyshev.T ℚ (↑n : ℤ)) (Chebyshev.T ℚ (↑n : ℤ))).comp
        (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))

Tactic:
simp only [← two_mul, ← comp_assoc]

Premises used: Polynomial.comp_assoc, two_mul
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
e_a :
  (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ)) =
    ((HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp
          (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
            X)).comp
      (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))
⊢ ((HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ))).comp
      (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X) =
    (((HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp
              (HMul.hMul (α := ℚ[X])
                ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)).comp
          (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))).comp
      (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
apply eval₂_congr rfl rfl

Premises used: Polynomial.eval₂_congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
e_a :
  (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ)) =
    (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp
      ((HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
            X).comp
        (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ))))
⊢ (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ)) =
    ((HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp
          (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
            X)).comp
      (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))

Tactic:
rw [comp_assoc]

Premises used: Polynomial.comp_assoc
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
apply :
  Chebyshev.T ℚ (↑n : ℤ) =
    (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X).comp
      (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))
⊢ (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp (Chebyshev.T ℚ (↑n : ℤ)) =
    (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑m : ℤ))).comp
      ((HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
            X).comp
        (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ))))

Tactic:
apply eval₂_congr rfl _ rfl

Premises used: Polynomial.eval₂_congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
rw :
  Chebyshev.T ℚ (↑n : ℤ) =
    comp ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
        (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ))) *
      comp X (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))
rw₁ :
  Chebyshev.T ℚ (↑n : ℤ) =
    (C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
      comp X (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))
rw₂ :
  Chebyshev.T ℚ (↑n : ℤ) =
    (C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
      HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ))
rw₃ :
  Chebyshev.T ℚ (↑n : ℤ) =
    HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) 2 *
      Chebyshev.T ℚ (↑n : ℤ)
rw₄ : Chebyshev.T ℚ (↑n : ℤ) = HMul.hMul (α := ℚ[X]) 1 (Chebyshev.T ℚ (↑n : ℤ))
rw₅ rw₆ : Eq (α := ℚ[X]) (Chebyshev.T ℚ (↑n : ℤ)) (Chebyshev.T ℚ (↑n : ℤ))
⊢ Chebyshev.T ℚ (↑n : ℤ) =
    (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X).comp
      (HMul.hMul (α := ℚ[X]) 2 (Chebyshev.T ℚ (↑n : ℤ)))

Tactic:
rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]

Premises used: Polynomial.X_comp, _private.0.Polynomial.C_half_mul_two_eq_one, mul_assoc, Polynomial.C_comp, Polynomial.mul_comp, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
rw : Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 n) (dickson 1 1 m))
rw₁ : Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (n * m)) (comp (dickson 1 1 n) (dickson 1 1 m))
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) (comp (dickson 1 1 n) (dickson 1 1 m)) (comp (dickson 1 1 n) (dickson 1 1 m))
⊢ Eq.{u_1 + 1} (α := R[X]) (comp (dickson 1 1 m) (dickson 1 1 n)) (comp (dickson 1 1 n) (dickson 1 1 m))

Tactic:
rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]

Premises used: Polynomial.dickson_one_one_mul, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
rw : CharP (ZMod p) p
⊢ CharP K p

Tactic:
rw [← f.charP_iff_charP]

Premises used: RingHom.charP_iff_charP
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP (ZMod p) p

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP K p

Tactic:
have : CharP K p := by
      rw [← f.charP_iff_charP]
      infer_instance
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this : CharP K p
⊢ Infinite K

Tactic:
haveI : Infinite K :=
      Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
        (IsFractionRing.injective _ _)
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this_1 : CharP K p
this : Infinite K
⊢ ∃ (K : Type) (x : Field K) (_ : CharP K p), Infinite K

Tactic:
⟨K, ?_, ?_, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this_1 : CharP K p
this : Infinite K
refine_1 : Field K
refine_2 : CharP K p
refine_3 : Infinite K
⊢ ∃ (K : Type) (x : Field K) (_ : CharP K p), Infinite K

Tactic:
refine ⟨K, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this_1 : CharP K p
this : Infinite K
⊢ Field K

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this_1 : CharP K p
this : Infinite K
⊢ CharP K p

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this_1 : CharP K p
this : Infinite K
⊢ Infinite K

Tactic:
infer_instance