awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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)
x : Fin 2 → ℝ
h :
  (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 0 x) : ℂ) * (↑z : ℂ) +
      (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 1 x) : ℂ) * 1 =
    (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
⊢ (f : (a : Fin 2 → ℝ) → ℂ) x = (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)

Tactic:
dsimp only [π₀, π₁, f, LinearMap.coe_proj, real_smul, LinearMap.coe_smulRight,
      LinearMap.add_apply]

Premises used: Complex.real_smul, LinearMap.add_apply, LinearMap.coe_proj, LinearMap.coe_smulRight
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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)
x : Fin 2 → ℝ
h h₁ :
  (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 0 x) : ℂ) * (↑z : ℂ) +
      (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 1 x) : ℂ) =
    (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
⊢ (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 0 x) : ℂ) * (↑z : ℂ) +
      (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 1 x) : ℂ) * 1 =
    (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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)
⊢ Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)

Tactic:
have f_def : ⇑f = fun p : Fin 2 → ℝ => (p 0 : ℂ) * ↑z + p 1 := by
    ext1
    dsimp only [π₀, π₁, f, LinearMap.coe_proj, real_smul, LinearMap.coe_smulRight,
      LinearMap.add_apply]
    rw [mul_one]
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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) : ℂ)
h :
  ∀ (x : Fin 2 → ℤ),
    Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
      (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
          (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) x :
        ℝ)
⊢ 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))

Tactic:
ext1
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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) : ℂ)
x : Fin 2 → ℤ
h :
  Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
        ((fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) ∘ fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) x :
      ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
        (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) x :
      ℝ)

Tactic:
rw [f_def]
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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) : ℂ)
x : Fin 2 → ℤ
h :
  Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(↑(x 1) : ℝ) : ℂ)) : ℝ)
h₁ h₂ :
  Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) ((↑(↑(x 0) : ℝ) : ℂ) * (↑z : ℂ) + (↑(↑(x 1) : ℝ) : ℂ)) : ℝ)

Tactic:
rw [ofReal_intCast, ofReal_intCast]

Premises used: Complex.ofReal_intCast
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : 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) : ℂ)
⊢ 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))

Tactic:
have :
    (fun p : Fin 2 → ℤ => normSq ((p 0 : ℂ) * ↑z + ↑(p 1))) =
      normSq ∘ f ∘ fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p := by
    ext1
    rw [f_def]
    dsimp only [Function.comp_def]
    rw [ofReal_intCast, ofReal_intCast]
-- 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))
rw :
  Tendsto (α := Fin 2 → ℤ) (β := ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
    cofinite atTop
⊢ Tendsto (β := ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ))) cofinite
    atTop

Tactic:
rw [this]
-- 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_2 :
  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 ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
this : ((↑z : ℂ).im⁻¹ • g) ∘ₗ f = LinearMap.id
⊢ f.ker = ⊥

Tactic:
LinearMap.ker_eq_bot_of_inverse this

Premises used: LinearMap.ker_eq_bot_of_inverse
-- 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_2 :
  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 ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
this : ((↑z : ℂ).im⁻¹ • g) ∘ₗ f = LinearMap.id
⊢ f.ker = ⊥

Tactic:
exact LinearMap.ker_eq_bot_of_inverse this

Premises used: LinearMap.ker_eq_bot_of_inverse
-- 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 ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
suffices : ((↑z : ℂ).im⁻¹ • g) ∘ₗ f = LinearMap.id
⊢ f.ker = ⊥

Tactic:
suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this
-- 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 ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
h :
  ∀ (x : Fin 2 → ℝ),
    Eq (α := Fin 2 → ℝ) ((((↑z : ℂ).im⁻¹ • g) ∘ₗ f : (a : Fin 2 → ℝ) → Fin 2 → ℝ) x : Fin 2 → ℝ)
      ((LinearMap.id : (a : Fin 2 → ℝ) → Fin 2 → ℝ) x : Fin 2 → ℝ)
⊢ ((↑z : ℂ).im⁻¹ • g) ∘ₗ f = LinearMap.id

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- 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 → ℝ
⊢ (↑z : ℂ).im ≠ 0

Tactic:
have hz : (z : ℂ).im ≠ 0 := z.2.ne'
-- 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 :
  HSMul.hSMul (β := Fin 2 → ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : Fin 2 → ℝ) =
    c
⊢ Eq (α := Fin 2 → ℝ) ((((↑z : ℂ).im⁻¹ • g) ∘ₗ f : (a : Fin 2 → ℝ) → Fin 2 → ℝ) c : Fin 2 → ℝ)
    ((LinearMap.id : (a : Fin 2 → ℝ) → Fin 2 → ℝ) c : Fin 2 → ℝ)

Tactic:
rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]

Premises used: LinearMap.smul_apply, LinearMap.id_apply, LinearMap.comp_apply
-- 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 :
  ∀ (i : Fin 2),
    HSMul.hSMul (β := Fin 2 → ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : Fin 2 → ℝ)
        i =
      c i
⊢ HSMul.hSMul (β := Fin 2 → ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : Fin 2 → ℝ) =
    c

Tactic:
ext i
-- 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
i : Fin 2
h :
  HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹
      ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℝ) =
    c ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹
      ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℝ) =
    c ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) i : ℝ) = c i

Tactic:
fin_cases i
-- 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 : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
⊢ HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹
      ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℝ) =
    c ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
change (z : ℂ).im⁻¹ * (f c).im = c 0

Premises used: UpperHalfPlane.coe, Complex.im, OfNat.ofNat, DFunLike.coe
-- 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 : ℂ).im⁻¹ * Complex.im ((fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) c) = c 0
h₁ : (↑z : ℂ).im⁻¹ * (((↑(c 0) : ℂ) * (↑z : ℂ)).im + (↑(c 1) : ℂ).im) = c 0
h₂ : (↑z : ℂ).im⁻¹ * (c 0 * (↑z : ℂ).im + (↑(c 1) : ℂ).im) = c 0
h₃ : (↑z : ℂ).im⁻¹ * (c 0 * (↑z : ℂ).im + 0) = c 0
h₄ : (↑z : ℂ).im⁻¹ * (c 0 * (↑z : ℂ).im) = c 0
h₅ : c 0 * ((↑z : ℂ).im⁻¹ * (↑z : ℂ).im) = c 0
h₆ : c 0 * 1 = c 0
h₇ h₈ : c 0 = c 0
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0

Tactic:
rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]

Premises used: Complex.add_im, mul_left_comm, Complex.im_ofReal_mul, Complex.ofReal_im, mul_one, add_zero, inv_mul_cancel₀
-- 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 : ℂ).im⁻¹ *
      (HMul.hMul (β := ℂ) (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : ℂ)).im =
    c 1
⊢ HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹
      ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℝ) =
    c ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
change (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1

Premises used: HMul.hMul, UpperHalfPlane.coe, Complex.im, starRingEnd, OfNat.ofNat, DFunLike.coe