-- Mathlib/NumberTheory/Modular.lean
theorem tendsto_normSq_coprime_pair :
    Filter.Tendsto (fun p : Fin 2 → ℤ => normSq ((p 0 : ℂ) * z + p 1)) cofinite atTop

Proof state:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
⊢ ((↑z).im⁻¹ • g) ∘ₗ f = LinearMap.id

Tactic:
apply LinearMap.ext

Result:
case h
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
⊢ ∀ (x : Fin 2 → ℝ), (((↑z).im⁻¹ • g) ∘ₗ f) x = LinearMap.id x

Proof state:
case h
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = (⇑normSq ∘ (fun p => ↑(p 0) * ↑z + ↑(p 1)) ∘ fun p => Int.cast ∘ p) x✝

Tactic:
dsimp only [Function.comp_def]

Result:
case h
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = normSq (↑↑(x✝ 0) * ↑z + ↑↑(x✝ 1))

Proof state:
case h
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ • g (f c) = c

Tactic:
ext i

Result:
case h.h
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
i : Fin 2
⊢ ((↑z).im⁻¹ • g (f c)) i = c i

Proof state:
case h.h.«1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * (starRingEnd ℂ) (f c)).im = c 1

Tactic:
rw [f_def, RingHom.map_add, RingHom.map_mul, mul_add, mul_left_comm, mul_conj, conj_ofReal,
  conj_ofReal, ← ofReal_mul, add_im, ofReal_im, zero_add, inv_mul_eq_iff_eq_mul₀ hz]

Result:
case h.h.«1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z * ↑(c 1)).im = (↑z).im * c 1

Proof state:
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
⊢ ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)

Tactic:
ext1

Result:
case h
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
x✝ : Fin 2 → ℝ
⊢ f x✝ = ↑(x✝ 0) * ↑z + ↑(x✝ 1)

Proof state:
case h
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = normSq (↑↑(x✝ 0) * ↑z + ↑↑(x✝ 1))

Tactic:
rw [ofReal_intCast, ofReal_intCast]

Result:
no goals

Proof state:
case h
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
⊢ (((↑z).im⁻¹ • g) ∘ₗ f) c = LinearMap.id c

Tactic:
have hz : (z : ℂ).im ≠ 0 := z.2.ne'

Result:
case h
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (((↑z).im⁻¹ • g) ∘ₗ f) c = LinearMap.id c

Proof state:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
⊢ LinearMap.ker f = ⊥

Tactic:
let g : ℂ →ₗ[ℝ] Fin 2 → ℝ :=
  LinearMap.pi ![imLm, imLm.comp ((z : ℂ) • ((conjAe : ℂ →ₐ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ))]

Result:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)
this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
⊢ LinearMap.ker f = ⊥

Proof state:
case h
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
x✝ : Fin 2 → ℝ
⊢ ↑(Function.eval 0 x✝) * ↑z + ↑(Function.eval 1 x✝) * 1 = ↑(x✝ 0) * ↑z + ↑(x✝ 1)

Tactic:
rw [mul_one]

Result:
no goals