awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
g : ℂ →ₗ[ℝ] Fin 2 → ℝ :=
  LinearMap.pi (φ := fun (a : Fin 2) ↦ ℝ)
    ![imLm,
      imLm ∘ₗ
        HSMul.hSMul (β := ℂ →ₗ[ℝ] ℂ) (↑z : ℂ)
          (↑(↑conjAe : ℂ →ₐ[ℝ] ℂ) :
            [inst : FunLike (ℂ →ₐ[ℝ] ℂ) ℂ ℂ] → [SemilinearMapClass (ℂ →ₐ[ℝ] ℂ) (RingHom.id ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
c : Fin 2 → ℝ
hz : (↑z : ℂ).im ≠ 0
h : ((↑z : ℂ) * (↑(c 1) : ℂ)).im = (↑z : ℂ).im * c 1
⊢ (↑z : ℂ).im⁻¹ *
      (HMul.hMul (β := ℂ) (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : ℂ)).im =
    c 1

Tactic:
rw [f_def, map_add, 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]

Premises used: Complex.add_im, inv_mul_eq_iff_eq_mul₀, map_add, mul_left_comm, zero_add, map_mul, Complex.mul_conj, mul_add, Complex.ofReal_im, Complex.conj_ofReal, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
g : ℂ →ₗ[ℝ] Fin 2 → ℝ :=
  LinearMap.pi (φ := fun (a : Fin 2) ↦ ℝ)
    ![imLm,
      imLm ∘ₗ
        HSMul.hSMul (β := ℂ →ₗ[ℝ] ℂ) (↑z : ℂ)
          (↑(↑conjAe : ℂ →ₐ[ℝ] ℂ) :
            [inst : FunLike (ℂ →ₐ[ℝ] ℂ) ℂ ℂ] → [SemilinearMapClass (ℂ →ₐ[ℝ] ℂ) (RingHom.id ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
c : Fin 2 → ℝ
hz : (↑z : ℂ).im ≠ 0
⊢ ((↑z : ℂ) * (↑(c 1) : ℂ)).im = (↑z : ℂ).im * c 1

Tactic:
simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]

Premises used: Complex.mul_im, zero_add, MulZeroClass.mul_zero, Complex.ofReal_re, Complex.ofReal_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
⊢ f.ker = ⊥

Tactic:
have hf : LinearMap.ker f = ⊥ := by
    let g : ℂ →ₗ[ℝ] Fin 2 → ℝ :=
      LinearMap.pi ![imLm, imLm.comp ((z : ℂ) • ((conjAe : ℂ →ₐ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ))]
    suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this
    apply LinearMap.ext
    intro c
    have hz : (z : ℂ).im ≠ 0 := z.2.ne'
    rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]
    ext i
    dsimp only [Pi.smul_apply, LinearMap.pi_apply, smul_eq_mul]
    fin_cases i
    · change (z : ℂ).im⁻¹ * (f c).im = c 0
      rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
    · change (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1
      rw [f_def, map_add, 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]
      simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
⊢ IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)

Tactic:
have hf' : IsClosedEmbedding f := f.isClosedEmbedding_of_injective hf
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
⊢ Tendsto (β := (i : Fin 2) → ℝ) (fun (k : (i : Fin 2) → ℤ) (i : Fin 2) ↦ (↑(k i) : ℝ))
    (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℤ) fun (x : Fin 2) ↦ cofinite)
    (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℝ) fun (x : Fin 2) ↦ cocompact ℝ)

Tactic:
Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite

Premises used: Int.tendsto_coe_cofinite, Filter.Tendsto.pi_map_coprodᵢ
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
h : Eq (α := Filter (Fin 2 → ℤ)) cofinite (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℤ) fun (x : Fin 2) ↦ cofinite)
h₁ :
  Eq (α := Filter (Fin 2 → ℝ)) (cocompact (Fin 2 → ℝ))
    (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℝ) fun (x : Fin 2) ↦ cocompact ℝ)
⊢ Tendsto (β := Fin 2 → ℝ) (fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))

Tactic:
convert! Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite

Premises used: Int.tendsto_coe_cofinite, Filter.Tendsto.pi_map_coprodᵢ
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
h h₁ : Eq (α := Filter (Fin 2 → ℤ)) cofinite cofinite
⊢ Eq (α := Filter (Fin 2 → ℤ)) cofinite (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℤ) fun (x : Fin 2) ↦ cofinite)

Tactic:
rw [coprodᵢ_cofinite]

Premises used: Filter.coprodᵢ_cofinite
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
h h₁ : Eq (α := Filter (Fin 2 → ℝ)) (cocompact (Fin 2 → ℝ)) (cocompact ((d : Fin 2) → ℝ))
⊢ Eq (α := Filter (Fin 2 → ℝ)) (cocompact (Fin 2 → ℝ))
    (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℝ) fun (x : Fin 2) ↦ cocompact ℝ)

Tactic:
rw [coprodᵢ_cocompact]

Premises used: Filter.coprodᵢ_cocompact
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
⊢ Tendsto (β := Fin 2 → ℝ) (fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))

Tactic:
have h₂ : Tendsto (fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p) cofinite (cocompact _) := by
    convert! Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
    · rw [coprodᵢ_cofinite]
    · rw [coprodᵢ_cocompact]
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
h₂ : Tendsto (β := Fin 2 → ℝ) (fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))
⊢ Tendsto (α := Fin 2 → ℤ) (β := ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
    cofinite atTop

Tactic:
tendsto_normSq_cocompact_atTop.comp (hf'.tendsto_cocompact.comp h₂)

Premises used: Complex.tendsto_normSq_cocompact_atTop, Topology.IsClosedEmbedding.tendsto_cocompact, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this_1 : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
f_def :
  Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)
this :
  Eq (α := (p : Fin 2 → ℤ) → ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)))
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
hf : f.ker = ⊥
hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
h₂ : Tendsto (β := Fin 2 → ℝ) (fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))
⊢ Tendsto (α := Fin 2 → ℤ) (β := ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
    cofinite atTop

Tactic:
exact tendsto_normSq_cocompact_atTop.comp (hf'.tendsto_cocompact.comp h₂)

Premises used: Complex.tendsto_normSq_cocompact_atTop, Topology.IsClosedEmbedding.tendsto_cocompact, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Modular
Goal:
p : Fin 2 → ℤ
g : Matrix (Fin 2) (Fin 2) ℝ
⊢ (lcRow0 p : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ) g = (↑(p 0) : ℝ) * g 0 0 + (↑(p 1) : ℝ) * g 0 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
ℝ : HPow.hPow (α := ℝ) (β := ℕ) (↑(cd 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (-(↑(cd 1) : ℝ)) 2 ≠ 0
⊢ (Fin 2 → ℝ) ≃ₗ[ℝ] Fin 2 → ℝ

Tactic:
refine
        LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)
          (GeneralLinearGroup.toLin (planeConformalMatrix (cd 0 : ℝ) (-(cd 1 : ℝ)) ?_))

Premises used: Int.cast, Matrix.GeneralLinearGroup.toLin, Real, LinearMap.GeneralLinearGroup.generalLinearEquiv, OfNat.ofNat, DFunLike.coe, Neg.neg, Matrix.planeConformalMatrix
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
norm_cast : ¬HPow.hPow (β := ℕ) (cd 0) 2 + HPow.hPow (β := ℕ) (-cd 1) 2 = 0
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(cd 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (-(↑(cd 1) : ℝ)) 2 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
rw : ¬HPow.hPow (β := ℕ) (cd 0) 2 + HPow.hPow (β := ℕ) (cd 1) 2 = 0
⊢ ¬HPow.hPow (β := ℕ) (cd 0) 2 + HPow.hPow (β := ℕ) (-cd 1) 2 = 0

Tactic:
rw [neg_sq]

Premises used: neg_sq
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬HPow.hPow (β := ℕ) (cd 0) 2 + HPow.hPow (β := ℕ) (cd 1) 2 = 0

Tactic:
hcd.sq_add_sq_ne_zero

Premises used: IsCoprime.sq_add_sq_ne_zero
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬HPow.hPow (β := ℕ) (cd 0) 2 + HPow.hPow (β := ℕ) (cd 1) 2 = 0

Tactic:
exact hcd.sq_add_sq_ne_zero

Premises used: IsCoprime.sq_add_sq_ne_zero
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
⊢ Continuous mB

Tactic:
continuous_matrix ?_

Premises used: continuous_matrix
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
refine : ∀ (i j : Fin 2), Continuous (Y := ℝ) fun (a : ℝ) ↦ mB a i j
⊢ Continuous mB

Tactic:
refine continuous_matrix ?_

Premises used: continuous_matrix
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
⊢ ∀ (i j : Fin 2), Continuous (Y := ℝ) fun (a : ℝ) ↦ mB a i j

Tactic:
simp only [mB, Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero,
      cons_val_one, and_self_iff]

Premises used: Fin.forall_fin_two, Matrix.cons_val_one, continuous_const, Matrix.cons_val_zero, continuous_id', Matrix.of_apply, and_self_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
⊢ Continuous mB

Tactic:
have hmB : Continuous mB := by
    refine continuous_matrix ?_
    simp only [mB, Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero,
      cons_val_one, and_self_iff]
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
⊢ Tendsto
    (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦
      (lcRow0 cd : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
        (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
          Matrix (Fin 2) (Fin 2) ℝ))
    cofinite (cocompact ℝ)

Tactic:
Filter.Tendsto.of_tendsto_comp ?_ (comap_cocompact_le hmB)

Premises used: Filter.comap_cocompact_le, Filter.Tendsto.of_tendsto_comp
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
refine :
  Tendsto (α := { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd })
    (mB ∘ fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦
      (lcRow0 cd : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
        (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
          Matrix (Fin 2) (Fin 2) ℝ))
    cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto
    (fun (g : { g : SL(2, ℤ) // (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 = cd }) ↦
      (lcRow0 cd : (a : Matrix (Fin 2) (Fin 2) ℝ) → ℝ)
        (↑((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (↑g : SL(2, ℤ))) :
          Matrix (Fin 2) (Fin 2) ℝ))
    cofinite (cocompact ℝ)

Tactic:
refine Filter.Tendsto.of_tendsto_comp ?_ (comap_cocompact_le hmB)

Premises used: Filter.comap_cocompact_le, Filter.Tendsto.of_tendsto_comp
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast
⊢ Tendsto (β := Matrix (Fin 2) (Fin 2) ℝ) (fun (m : Matrix (Fin 2) (Fin 2) ℤ) ↦ m.map Int.cast) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
      Tendsto.pi_map_coprodᵢ fun _ : Fin 2 =>
        Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite

Premises used: Filter.coprodᵢ_cocompact, Filter.coprodᵢ_cofinite, Int.tendsto_coe_cofinite, Filter.Tendsto.pi_map_coprodᵢ
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast
⊢ Tendsto (β := Matrix (Fin 2) (Fin 2) ℝ) (fun (m : Matrix (Fin 2) (Fin 2) ℤ) ↦ m.map Int.cast) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
have cocompact_ℝ_to_cofinite_ℤ_matrix :
    Tendsto (fun m : Matrix (Fin 2) (Fin 2) ℤ => Matrix.map m ((↑) : ℤ → ℝ)) cofinite
      (cocompact _) := by
    simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
      Tendsto.pi_map_coprodᵢ fun _ : Fin 2 =>
        Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (β := Matrix (Fin 2) (Fin 2) ℝ) (fun (m : Matrix (Fin 2) (Fin 2) ℤ) ↦ m.map Int.cast) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
have hf₁ : Tendsto f₁ cofinite (cocompact _) :=
    cocompact_ℝ_to_cofinite_ℤ_matrix.comp Subtype.coe_injective.tendsto_cofinite
-- Module: Mathlib.NumberTheory.Modular
Goal:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ :=
  fun (t : ℝ) ↦ (of : (a : Fin 2 → Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) ![![t, -(↑1 : ℝ)], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun (g : SL(2, ℤ)) ↦ (↑g : Matrix (Fin 2) (Fin 2) ℤ).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix :
  Tendsto (β := Matrix (Fin 2) (Fin 2) ℝ) (fun (m : Matrix (Fin 2) (Fin 2) ℤ) ↦ m.map Int.cast) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ IsClosedEmbedding (X := Matrix (Fin 2) (Fin 2) ℝ) (Y := Matrix (Fin 2) (Fin 2) ℝ)
    (⇑(lcRow0Extend hcd) : (a : Matrix (Fin 2) (Fin 2) ℝ) → Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
have hf₂ : IsClosedEmbedding (lcRow0Extend hcd) :=
    (lcRow0Extend hcd).toContinuousLinearEquiv.toHomeomorph.isClosedEmbedding