awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₁ : (↑z : ℂ).im⁻¹ * (((↑(c 0) : ℂ) * (↑z : ℂ)).im + (↑(c 1) : ℂ).im) = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₂ : (↑z : ℂ).im⁻¹ * (c 0 * (↑z : ℂ).im + (↑(c 1) : ℂ).im) = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₃ : (↑z : ℂ).im⁻¹ * (c 0 * (↑z : ℂ).im + 0) = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₄ : (↑z : ℂ).im⁻¹ * (c 0 * (↑z : ℂ).im) = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₅ : c 0 * ((↑z : ℂ).im⁻¹ * (↑z : ℂ).im) = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₆ : c 0 * 1 = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h₇ : c 0 = c 0
Tactic: rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz,
        mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
⊢ 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, ⋯⟩)
have h : (↑z : ℂ).im⁻¹ * (HMul.hMul (β := ℂ) (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : ℂ)).im =
  c 1
Tactic: change (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 : ℂ).im⁻¹ *
      (HMul.hMul (β := ℂ) (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : ℂ)).im =
    c 1
have h : ((↑z : ℂ) * (↑(c 1) : ℂ)).im = (↑z : ℂ).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]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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))
⊢ Tendsto (α := Fin 2 → ℤ) (β := ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
    cofinite atTop
have hf : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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 = ⊥
⊢ Tendsto (α := Fin 2 → ℤ) (β := ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
    cofinite atTop
have hf' : IsClosedEmbedding (X := Fin 2 → ℝ) (Y := ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ)
Tactic: have hf' : IsClosedEmbedding f := f.isClosedEmbedding_of_injective hf
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℝ))
have h : Eq (α := Filter (Fin 2 → ℤ)) cofinite (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℤ) fun (x : Fin 2) ↦ cofinite)
Tactic: convert! Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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)
⊢ Tendsto (β := Fin 2 → ℝ) (fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))
have h₁ : Eq (α := Filter (Fin 2 → ℝ)) (cocompact (Fin 2 → ℝ))
  (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℝ) fun (x : Fin 2) ↦ cocompact ℝ)
Tactic: convert! Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℝ) → ℂ)
⊢ Eq (α := Filter (Fin 2 → ℤ)) cofinite (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℤ) fun (x : Fin 2) ↦ cofinite)
have h : Eq (α := Filter (Fin 2 → ℤ)) cofinite cofinite
Tactic: rw [coprodᵢ_cofinite]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℝ) → ℂ)
⊢ Eq (α := Filter (Fin 2 → ℝ)) (cocompact (Fin 2 → ℝ))
    (Filter.coprodᵢ (α := fun (i : Fin 2) ↦ ℝ) fun (x : Fin 2) ↦ cocompact ℝ)
have h : Eq (α := Filter (Fin 2 → ℝ)) (cocompact (Fin 2 → ℝ)) (cocompact ((d : Fin 2) → ℝ))
Tactic: rw [coprodᵢ_cocompact]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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 → ℤ) (β := ℝ)
    (Function.comp (β := ℂ) (⇑normSq : (a : ℂ) → ℝ)
      (Function.comp (β := Fin 2 → ℝ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℤ) ↦ Int.cast ∘ p))
    cofinite atTop
have h₂ : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ (Fin 2 → ℝ) ≃ₗ[ℝ] Fin 2 → ℝ
have ℝ : HPow.hPow (α := ℝ) (β := ℕ) (↑(cd 0) : ℝ) 2 + HPow.hPow (α := ℝ) (β := ℕ) (-(↑(cd 1) : ℝ)) 2 ≠ 0
Tactic: refine
        LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)
          (GeneralLinearGroup.toLin (planeConformalMatrix (cd 0 : ℝ) (-(cd 1 : ℝ)) ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have norm_cast : ¬HPow.hPow (β := ℕ) (cd 0) 2 + HPow.hPow (β := ℕ) (-cd 1) 2 = 0
Tactic: norm_cast