awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ Membership.mem (γ := Set (Fin 2 → R)) ((fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1) '' Set.univ) cd
have refine : (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
    (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) =
  cd
Tactic: refine ⟨⟨A, det_A_1⟩, Set.mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) =
    cd
have h : ∀ (x : Fin 2),
  (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) x =
    cd x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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) : ℂ)
have h : ∀ (x : Fin 2 → ℝ), (f : (a : Fin 2 → ℝ) → ℂ) x = (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℝ
⊢ (f : (a : Fin 2 → ℝ) → ℂ) x = (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
have h : (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 0 x) : ℂ) * (↑z : ℂ) +
    (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 1 x) : ℂ) * 1 =
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
Tactic: dsimp only [π₀, π₁, f, LinearMap.coe_proj, real_smul, LinearMap.coe_smulRight,
      LinearMap.add_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℝ
⊢ (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 0 x) : ℂ) * (↑z : ℂ) +
      (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 1 x) : ℂ) * 1 =
    (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
have h : (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 0 x) : ℂ) * (↑z : ℂ) +
    (↑(Function.eval (β := fun (a : Fin 2) ↦ ℝ) 1 x) : ℂ) =
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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)
⊢ Tendsto (β := ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ))) cofinite
    atTop
have f_def : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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))
have 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 :
      ℝ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℤ
⊢ 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 :
      ℝ)
have 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 :
    ℝ)
Tactic: rw [f_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 → ℤ
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) ((↑(↑(x 0) : ℝ) : ℂ) * (↑z : ℂ) + (↑(↑(x 1) : ℝ) : ℂ)) : ℝ)
have h : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
  ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(↑(x 1) : ℝ) : ℂ)) : ℝ)
Tactic: rw [ofReal_intCast, ofReal_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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) : ℝ) : ℂ)) : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) ((↑(↑(x 0) : ℝ) : ℂ) * (↑z : ℂ) + (↑(↑(x 1) : ℝ) : ℂ)) : ℝ)
have h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
  ((normSq : (a : ℂ) → ℝ) ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) : ℝ)
Tactic: rw [ofReal_intCast, ofReal_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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) : ℂ)
⊢ Tendsto (β := ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ))) cofinite
    atTop
have 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))
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]
-- 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))
⊢ Tendsto (β := ℝ) (fun (p : Fin 2 → ℤ) ↦ (normSq : (a : ℂ) → ℝ) ((↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ))) cofinite
    atTop
have 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
Tactic: rw [this]
-- 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 ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
⊢ f.ker = ⊥
have suffices : ((↑z : ℂ).im⁻¹ • g) ∘ₗ f = LinearMap.id
Tactic: suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this
-- 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 ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
⊢ ((↑z : ℂ).im⁻¹ • g) ∘ₗ f = LinearMap.id
have 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 → ℝ)
Tactic: apply LinearMap.ext
-- 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))
g : ℂ →ₗ[ℝ] Fin 2 → ℝ :=
  LinearMap.pi (φ := fun (a : Fin 2) ↦ ℝ)
    ![imLm,
      imLm ∘ₗ
        HSMul.hSMul (β := ℂ →ₗ[ℝ] ℂ) (↑z : ℂ)
          (↑(↑conjAe : ℂ →ₐ[ℝ] ℂ) :
            [inst : FunLike (ℂ →ₐ[ℝ] ℂ) ℂ ℂ] → [SemilinearMapClass (ℂ →ₐ[ℝ] ℂ) (RingHom.id ℝ) ℂ ℂ] → ℂ →ₗ[ℝ] ℂ)]
c : Fin 2 → ℝ
⊢ 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 → ℝ)
have hz : (↑z : ℂ).im ≠ 0
Tactic: have hz : (z : ℂ).im ≠ 0 := z.2.ne'
-- 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
⊢ 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 → ℝ)
have h : HSMul.hSMul (β := Fin 2 → ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : Fin 2 → ℝ) = c
Tactic: rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]
-- 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
⊢ HSMul.hSMul (β := Fin 2 → ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : Fin 2 → ℝ) =
    c
have h : ∀ (i : Fin 2),
  HSMul.hSMul (β := Fin 2 → ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) : Fin 2 → ℝ)
      i =
    c i
Tactic: ext i
-- 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
i : Fin 2
⊢ HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) i : ℝ) = c i
have h : HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹
    ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℝ) =
  c ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
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, ⋯⟩)
⊢ HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹ ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) i : ℝ) = c i
have h₁ : HMul.hMul (β := ℝ) (↑z : ℂ).im⁻¹
    ((g : (a : ℂ) → Fin 2 → ℝ) ((f : (a : Fin 2 → ℝ) → ℂ) c : ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℝ) =
  c ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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) (⟨0, ⋯⟩ : Fin 2)) : ℝ) =
    c ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
have h : (↑z : ℂ).im⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
Tactic: change (z : ℂ).im⁻¹ * (f c).im = c 0
-- 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⁻¹ * Complex.im ((f : (a : Fin 2 → ℝ) → ℂ) c) = c 0
have h : (↑z : ℂ).im⁻¹ * Complex.im ((fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)) 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]