awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : SlashInvariantForm Γ k
toFun : ℍ → ℂ
slash_action_eq' :
  ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun = toFun
h : { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k }.toFun = g.toFun
⊢ { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k } = g
have mk : ∀ (toFun_1 : ℍ → ℂ)
  (slash_action_eq'_1 :
    ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun_1 = toFun_1)
  (h :
    { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k }.toFun =
      { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 : SlashInvariantForm Γ k }.toFun),
  { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k } =
    { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (hypothesis)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ (f : (a : ℍ) → ℂ) (γ • z) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
have this : (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)
Tactic: have : f (γ • z) = f z * denom γ z ^ k := by
    simpa [slash_def, σ, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ (denom_ne_zero _ _)),
      Subgroup.HasDetOne.det_eq hγ] using congr_fun (slash_action_eqn f γ hγ) z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)
⊢ (f : (a : ℍ) → ℂ) (γ • z) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
have rw : HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k) =
  HMul.hMul (β := ℂ)
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
    ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: rw [this, denom, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)
rw :
  HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ (f : (a : ℍ) → ℂ) (γ • z) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
have rw₁ : HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k) =
  HMul.hMul (β := ℂ)
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
    ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: rw [this, denom, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)
rw :
  HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ (f : (a : ℍ) → ℂ) (γ • z) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
have rw₂ : HMul.hMul (β := ℂ)
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
    ((f : (a : ℍ) → ℂ) z : ℂ) =
  HMul.hMul (β := ℂ)
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
    ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: rw [this, denom, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f g : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
have rw : HAdd.hAdd (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ))
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
  HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
Tactic: rw [SlashAction.add_slash, slash_action_eqn f γ hγ, slash_action_eqn g γ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f g : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  HAdd.hAdd (α := ℍ → ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ))
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
have rw₁ : HAdd.hAdd (α := ℍ → ℂ) (⇑f : (a : ℍ) → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
  HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
Tactic: rw [SlashAction.add_slash, slash_action_eqn f γ hγ, slash_action_eqn g γ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f g : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  HAdd.hAdd (α := ℍ → ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ))
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
rw₁ :
  HAdd.hAdd (α := ℍ → ℂ) (⇑f : (a : ℍ) → ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
have rw₂ : HAdd.hAdd (α := ℍ → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) =
  HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
Tactic: rw [SlashAction.add_slash, slash_action_eqn f γ hγ, slash_action_eqn g γ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetOne
α : Type u_2
inst_2 : SMul α ℂ
inst_3 : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw : @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
    (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) c 1) (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) c 1) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℂ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw : @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
    (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw₁ : @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
    (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
rw₁ :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw₂ : HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
rw₁ :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₂ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw₃ : HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
rw₁ :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₂ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₃ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw₄ : HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
rw₁ :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₂ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₃ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) (⇑f : (a : ℍ) → ℂ)
rw₄ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw₅ : HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
  HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
rw₁ :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₂ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₃ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) (⇑f : (a : ℍ) → ℂ)
rw₄ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
rw₅ :
  HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)
have rw₆ : HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ) =
  HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (-(⇑f : (a : ℍ) → ℂ)))
    (-(⇑f : (a : ℍ) → ℂ))
have rw : Eq (α := ℍ → ℂ) (-@SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (⇑f : (a : ℍ) → ℂ))
  (-(⇑f : (a : ℍ) → ℂ))
Tactic: rw [SlashAction.neg_slash, slash_action_eqn f γ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  Eq (α := ℍ → ℂ) (-@SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (⇑f : (a : ℍ) → ℂ))
    (-(⇑f : (a : ℍ) → ℂ))
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (-(⇑f : (a : ℍ) → ℂ)))
    (-(⇑f : (a : ℍ) → ℂ))
have rw₁ : Eq (α := ℍ → ℂ) (-(⇑f : (a : ℍ) → ℂ)) (-(⇑f : (a : ℍ) → ℂ))
Tactic: rw [SlashAction.neg_slash, slash_action_eqn f γ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
⊢ @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g (Function.const ℍ x) =
    Function.const ℍ x
have h : ∀ (x_1 : ℍ),
  @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g (Function.const ℍ x)
      x_1 =
    Function.const ℍ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (hypothesis)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj :
  j ∈
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k j
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))
have hj₁ : g * j * g⁻¹ ∈ Γ
Tactic: rw [map_inv, Γ.mem_inv_pointwise_smul_iff, toConjAct_smul] at hj
Cleared hypotheses: hj