awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ insert i t, k i) g
      (∏ i ∈ insert i t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#(insert i t)) : ℤ) 1))
      (∏ i ∈ insert i t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have insert : ∀ (hi : i ∉ ∅)
  (IH :
    @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
      HSMul.hSMul (β := ℍ → ℂ)
        (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
          (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
        (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))),
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ insert i ∅, k i) g
      (∏ i ∈ insert i ∅, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(card (α := ι) (insert i ∅)) : ℤ) 1))
      (∏ i ∈ insert i ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
Cleared hypotheses: t, hi, IH
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
insert :
  ∀ (hi : i ∉ ∅)
    (IH :
      @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
        HSMul.hSMul (β := ℍ → ℂ)
          (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
            (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
          (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))),
    @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ Insert.insert i ∅, k i) g
        (∏ i ∈ Insert.insert i ∅, f i) =
      HSMul.hSMul (β := ℍ → ℂ)
        (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
          (HSub.hSub (α := ℤ) (↑(card (α := ι) (Insert.insert i ∅)) : ℤ) 1))
        (∏ i ∈ Insert.insert i ∅,
          @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ Insert.insert i t, k i) g
      (∏ i ∈ Insert.insert i t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#(Insert.insert i t)) : ℤ) 1))
      (∏ i ∈ Insert.insert i t,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have insert₁ : ∀ (ht : t.Nonempty),
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ Insert.insert i t, k i) g
      (∏ i ∈ Insert.insert i t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#(Insert.insert i t)) : ℤ) 1))
      (∏ i ∈ Insert.insert i t,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
ht : t.Nonempty
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ insert i t, k i) g
      (∏ i ∈ insert i t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#(insert i t)) : ℤ) 1))
      (∏ i ∈ insert i t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have insert : (|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| *
      HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1)) •
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i) *
      ∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i)) =
  HPow.hPow (α := ℝ) (β := ℤ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| (↑(#t) : ℤ) •
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i) *
      ∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
      ← mul_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
ht : t.Nonempty
⊢ (|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| *
        HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
          (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1)) •
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i) *
        ∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i)) =
    HPow.hPow (α := ℝ) (β := ℤ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| (↑(#t) : ℤ) •
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i) *
        ∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have insert : |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| *
    HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
      (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1) =
  HPow.hPow (α := ℝ) (β := ℤ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| (↑(#t) : ℤ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
ht : t.Nonempty
⊢ |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| *
      HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1) =
    HPow.hPow (α := ℝ) (β := ℤ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| (↑(#t) : ℤ)
have insert : |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| *
    HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
      (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1) =
  HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
    (1 + HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1)
Tactic: nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
ht : t.Nonempty
⊢ |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| *
      HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1) =
    HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
      (1 + HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1)
have insert : Ne (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 0 ∨
  1 + HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1 ≠ 0 ∨ Eq (α := ℤ) 1 0 ∧ HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1 = 0
Tactic: rw [zpow_add', zpow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
      (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
ht : t.Nonempty
⊢ Ne (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 0 ∨
    1 + HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1 ≠ 0 ∨ Eq (α := ℤ) 1 0 ∧ HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1 = 0
have insert : Ne (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 0
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k i) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have empty : @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
  HSMul.hSMul (β := ℍ → ℂ)
    (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
      (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
    (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
    ext _
    simp [slash_apply]
  | insert i t hi IH =>
    rcases t.eq_empty_or_nonempty with rfl | ht
    · simp
    simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
      ← mul_smul]
    congr 1
    nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
    rw [zpow_add', zpow_one]
    left
    exact abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
empty :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
      (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k i) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
      HSMul.hSMul (β := ℍ → ℂ)
        (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
          (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
        (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))),
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ insert i t, k i) g
      (∏ i ∈ insert i t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#(insert i t)) : ℤ) 1))
      (∏ i ∈ insert i t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
    ext _
    simp [slash_apply]
  | insert i t hi IH =>
    rcases t.eq_empty_or_nonempty with rfl | ht
    · simp
    simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
      ← mul_smul]
    congr 1
    nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
    rw [zpow_add', zpow_one]
    left
    exact abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k i) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have empty : @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
  HSMul.hSMul (β := ℍ → ℂ)
    (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
      (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
    (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
    ext _
    simp [slash_apply]
  | insert i t hi IH =>
    rcases t.eq_empty_or_nonempty with rfl | ht
    · simp
    simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
      ← mul_smul]
    congr 1
    nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
    rw [zpow_add', zpow_one]
    left
    exact abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
empty :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
      (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k i) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ t, k i) g (∏ i ∈ t, f i) =
      HSMul.hSMul (β := ℍ → ℂ)
        (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
          (HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1))
        (∏ i ∈ t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))),
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ insert i t, k i) g
      (∏ i ∈ insert i t, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#(insert i t)) : ℤ) 1))
      (∏ i ∈ insert i t, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
    ext _
    simp [slash_apply]
  | insert i t hi IH =>
    rcases t.eq_empty_or_nonempty with rfl | ht
    · simp
    simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
      ← mul_smul]
    congr 1
    nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
    rw [zpow_add', zpow_one]
    left
    exact abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ k * (↑(#s) : ℤ) = ∑ i ∈ s, k
have rw : k * (↑(#s) : ℤ) = #s • k
Tactic: rw [Finset.sum_const, nsmul_eq_mul']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
rw : k * (↑(#s) : ℤ) = #s • k
⊢ k * (↑(#s) : ℤ) = ∑ i ∈ s, k
have rw₁ : k * (↑(#s) : ℤ) = k * (↑(#s) : ℤ)
Tactic: rw [Finset.sum_const, nsmul_eq_mul']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (hypothesis)
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k * (↑(#s) : ℤ)) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))
have this : k * (↑(#s) : ℤ) = ∑ i ∈ s, k
Tactic: have : k * (#s) = ∑ i ∈ s, k := by
    rw [Finset.sum_const, nsmul_eq_mul']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
this : k * (↑(#s) : ℤ) = ∑ i ∈ s, k
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k * (↑(#s) : ℤ)) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))
have rw : @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k) g (∏ i ∈ s, f i) =
  HSMul.hSMul (β := ℍ → ℂ)
    (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
      (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
    (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k * (↑(Fintype.card ι) : ℤ)) g
      (∏ i : ι, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| (Fintype.card ι - 1))
      (∏ i : ι, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))
have this : 0 < Fintype.card ι
Tactic: have : 0 < Fintype.card ι := Fintype.card_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashInvariantForms (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (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
Tactic: cases f
Cleared hypotheses: f, h