awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) 2 = 1
have rw₁ : Eq.{u_1 + 1} (α := R[X]) 1 1
Tactic: rw [mul_comm, two_mul_C_half_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (dickson 1 1 1) (Chebyshev.C R (↑1 : ℤ))
have rw : Eq (α := R[X]) X (Chebyshev.C R (↑1 : ℤ))
Tactic: rw [dickson_one, Nat.cast_one, Chebyshev.C_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
rw : Eq (α := R[X]) X (Chebyshev.C R (↑1 : ℤ))
⊢ Eq (α := R[X]) (dickson 1 1 1) (Chebyshev.C R (↑1 : ℤ))
have rw₁ : Eq (α := R[X]) X (Chebyshev.C R 1)
Tactic: rw [dickson_one, Nat.cast_one, Chebyshev.C_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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)
⊢ Eq (α := R[X]) (dickson 1 1 1) (Chebyshev.C R (↑1 : ℤ))
have rw₂ : Eq.{u_1 + 1} (α := R[X]) X X
Tactic: rw [dickson_one, Nat.cast_one, Chebyshev.C_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Eq (α := R[X]) (dickson 1 1 (n + 2)) (Chebyshev.C R (↑(n + 2) : ℤ))
have 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 : ℤ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (dickson 2 1 1) (Chebyshev.S R (↑1 : ℤ))
have rw : Eq (α := R[X]) X (Chebyshev.S R (↑1 : ℤ))
Tactic: rw [dickson_one, Nat.cast_one, Chebyshev.S_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
rw : Eq (α := R[X]) X (Chebyshev.S R (↑1 : ℤ))
⊢ Eq (α := R[X]) (dickson 2 1 1) (Chebyshev.S R (↑1 : ℤ))
have rw₁ : Eq (α := R[X]) X (Chebyshev.S R 1)
Tactic: rw [dickson_one, Nat.cast_one, Chebyshev.S_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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)
⊢ Eq (α := R[X]) (dickson 2 1 1) (Chebyshev.S R (↑1 : ℤ))
have rw₂ : Eq.{u_1 + 1} (α := R[X]) X X
Tactic: rw [dickson_one, Nat.cast_one, Chebyshev.S_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Eq (α := R[X]) (dickson 2 1 (n + 2)) (Chebyshev.S R (↑(n + 2) : ℤ))
have 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 : ℤ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))
have h : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))
have 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])
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ 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])
have 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)))
Tactic: simp only [← map_dickson (Int.castRingHom R), ← map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ 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)))
have e_a : Eq (α := ℤ[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ Eq (α := ℤ[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 m) (dickson 1 1 n))
have e_a : map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))
Tactic: apply map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ ((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))
have 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)
Tactic: simp only [← two_mul, ← comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ ((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)
have 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 : ℤ)))
Tactic: apply eval₂_congr rfl rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ (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 : ℤ)))
have 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 : ℤ))))
Tactic: rw [comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ (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 : ℤ))))
have 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 : ℤ)))
Tactic: apply eval₂_congr rfl _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
h : Eq (α := R) (1 : R) ((Int.castRingHom R : (a : ℤ) → R) 1 : R)
⊢ 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 : ℤ)))
have 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 : ℤ)))
Tactic: rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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 : ℤ)))
⊢ 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 : ℤ)))
have rw₁ : Chebyshev.T ℚ (↑n : ℤ) =
  (C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
    comp X (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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 : ℤ)))
⊢ 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 : ℤ)))
have rw₂ : Chebyshev.T ℚ (↑n : ℤ) =
  (C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
    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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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 : ℤ))
⊢ 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 : ℤ)))
have rw₃ : Chebyshev.T ℚ (↑n : ℤ) =
  HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) 2 *
    Chebyshev.T ℚ (↑n : ℤ)
Tactic: rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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 : ℤ)
⊢ 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 : ℤ)))
have rw₄ : Chebyshev.T ℚ (↑n : ℤ) = HMul.hMul (α := ℚ[X]) 1 (Chebyshev.T ℚ (↑n : ℤ))
Tactic: rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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 : ℤ))
⊢ 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 : ℤ)))
have rw₅ : Eq (α := ℚ[X]) (Chebyshev.T ℚ (↑n : ℤ)) (Chebyshev.T ℚ (↑n : ℤ))
Tactic: rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) (comp (dickson 1 1 m) (dickson 1 1 n)) (comp (dickson 1 1 n) (dickson 1 1 m))
have rw : Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (m * n)) (comp (dickson 1 1 n) (dickson 1 1 m))
Tactic: rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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))
⊢ Eq.{u_1 + 1} (α := R[X]) (comp (dickson 1 1 m) (dickson 1 1 n)) (comp (dickson 1 1 n) (dickson 1 1 m))
have rw₁ : Eq.{u_1 + 1} (α := R[X]) (dickson 1 1 (n * m)) (comp (dickson 1 1 n) (dickson 1 1 m))
Tactic: rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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))
⊢ Eq.{u_1 + 1} (α := R[X]) (comp (dickson 1 1 m) (dickson 1 1 n)) (comp (dickson 1 1 n) (dickson 1 1 m))
have 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))
Tactic: rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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
have rw : CharP (ZMod p) p
Tactic: rw [← f.charP_iff_charP]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (hypothesis)
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
⊢ ∃ (K : Type) (x : Field K) (_ : CharP K p), Infinite K
have this : CharP K p
Tactic: have : CharP K p := by
      rw [← f.charP_iff_charP]
      infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (hypothesis)
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
⊢ ∃ (K : Type) (x : Field K) (_ : CharP K p), Infinite K
have this₁ : Infinite K
Tactic: haveI : Infinite K :=
      Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
        (IsFractionRing.injective _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
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
have refine_1 : Field K
Tactic: refine ⟨K, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ dickson 1 1 p = HPow.hPow (α := (ZMod p)[X]) X p
have obtain : ∀ (K : Type) (w : Field K), CharP K p → ∀ (H : Infinite K), dickson 1 1 p = HPow.hPow (α := (ZMod p)[X]) X p
Tactic: obtain ⟨K, _, _, H⟩ : ∃ (K : Type) (_ : Field K), ∃ _ : CharP K p, Infinite K := by
    let K := FractionRing (Polynomial (ZMod p))
    let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
    have : CharP K p := by
      rw [← f.charP_iff_charP]
      infer_instance
    haveI : Infinite K :=
      Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
        (IsFractionRing.injective _ _)
    refine ⟨K, ?_, ?_, ?_⟩ <;> infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
⊢ dickson 1 1 p = HPow.hPow (α := (ZMod p)[X]) X p
have a : Eq (α := K[X]) (map (ZMod.castHom sorry K) (dickson 1 1 p)) (map (ZMod.castHom sorry K) (HPow.hPow (α := (ZMod p)[X]) X p))
Tactic: apply map_injective (ZMod.castHom (dvd_refl p) K) (RingHom.injective _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
⊢ Eq (α := K[X]) (map (ZMod.castHom ⋯ K) (dickson 1 1 p)) (map (ZMod.castHom ⋯ K) (HPow.hPow (α := (ZMod p)[X]) X p))
have a : dickson 1 ((ZMod.castHom sorry K : (a : ZMod p) → K) 1) p = HPow.hPow (α := K[X]) X p
Tactic: rw [map_dickson, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
⊢ dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p = HPow.hPow (α := K[X]) X p
have a : Set.Infinite (α := K)
  {x : K | eval x (dickson 1 ((ZMod.castHom sorry K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
Tactic: apply eq_of_infinite_eval_eq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
⊢ Set.Infinite (α := K)
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
have a : Subset (α := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
  {x : K | eval x (dickson 1 ((ZMod.castHom sorry K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
Tactic: apply @Set.Infinite.mono _ { x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0 }
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
a :
  Subset (α := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
⊢ Set.Infinite (α := K)
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
have a₁ : Set.Infinite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
Tactic: apply @Set.Infinite.mono _ { x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0 }