case h
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ 1 = ↑(Int.castRingHom R) 1

R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
have h : (1 : R) = Int.castRingHom R 1
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
case h
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ 1 = ↑(Int.castRingHom R) 1

R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
simp only [eq_intCast, Int.cast_one]
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 (↑(Int.castRingHom R) 1) (m * n) =
    comp (dickson 1 (↑(Int.castRingHom R) 1) m) (dickson 1 (↑(Int.castRingHom R) 1) n)
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
rw [h]
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ map (Int.castRingHom R) (dickson 1 1 (m * n)) = map (Int.castRingHom R) (comp (dickson 1 1 m) (dickson 1 1 n))
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 (↑(Int.castRingHom R) 1) (m * n) =
    comp (dickson 1 (↑(Int.castRingHom R) 1) m) (dickson 1 (↑(Int.castRingHom R) 1) n)
simp only [← map_dickson (Int.castRingHom R), ← map_comp]
case e_a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ map (Int.castRingHom R) (dickson 1 1 (m * n)) = map (Int.castRingHom R) (comp (dickson 1 1 m) (dickson 1 1 n))
congr 1
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))
case e_a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
apply map_injective (Int.castRingHom ℚ) Int.cast_injective
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (comp (Chebyshev.T ℚ m + Chebyshev.T ℚ m) (Chebyshev.T ℚ n)) (↑C ⅟2 * X) =
    comp (comp (Chebyshev.T ℚ m + Chebyshev.T ℚ m) (↑C ⅟2 * X)) (comp (Chebyshev.T ℚ n + Chebyshev.T ℚ n) (↑C ⅟2 * X))
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))
simp only [map_dickson, map_comp, eq_intCast, Int.cast_one, dickson_one_one_eq_chebyshev_T,
  Chebyshev.T_mul, two_mul, ← add_comp]
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n)) (↑C ⅟2 * X) =
    comp (comp (comp (2 * Chebyshev.T ℚ m) (↑C ⅟2 * X)) (2 * Chebyshev.T ℚ n)) (↑C ⅟2 * X)
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (comp (Chebyshev.T ℚ m + Chebyshev.T ℚ m) (Chebyshev.T ℚ n)) (↑C ⅟2 * X) =
    comp (comp (Chebyshev.T ℚ m + Chebyshev.T ℚ m) (↑C ⅟2 * X)) (comp (Chebyshev.T ℚ n + Chebyshev.T ℚ n) (↑C ⅟2 * X))
simp only [← two_mul, ← comp_assoc]
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n) = comp (comp (2 * Chebyshev.T ℚ m) (↑C ⅟2 * X)) (2 * Chebyshev.T ℚ n)
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n)) (↑C ⅟2 * X) =
    comp (comp (comp (2 * Chebyshev.T ℚ m) (↑C ⅟2 * X)) (2 * Chebyshev.T ℚ n)) (↑C ⅟2 * X)
apply eval₂_congr rfl rfl
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n) = comp (2 * Chebyshev.T ℚ m) (comp (↑C ⅟2 * X) (2 * Chebyshev.T ℚ n))
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n) = comp (comp (2 * Chebyshev.T ℚ m) (↑C ⅟2 * X)) (2 * Chebyshev.T ℚ n)
rw [comp_assoc]
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ Chebyshev.T ℚ n = comp (↑C ⅟2 * X) (2 * Chebyshev.T ℚ n)
case e_a.a
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n) = comp (2 * Chebyshev.T ℚ m) (comp (↑C ⅟2 * X) (2 * Chebyshev.T ℚ n))
apply eval₂_congr rfl _ rfl
no goals
R : Type u_1
S : Type ?u.228109
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ Chebyshev.T ℚ n = comp (↑C ⅟2 * X) (2 * Chebyshev.T ℚ n)
rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]