awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
τ : ℍ
⊢ f
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) /
        g
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) *
      (denom
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
            (↑τ : ℂ) ^
          k2 /
        denom
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
            (↑τ : ℂ) ^
          k1) =
    f
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) *
        (denom
              ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
              (↑τ : ℂ) ^
            k1)⁻¹ /
      (g
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) *
        (denom
              ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
              (↑τ : ℂ) ^
            k2)⁻¹)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
empty :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 =
    HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1
⊢ @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:
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]

Premises used: CharP.cast_eq_zero, Finset.prod_empty, Int.reduceNeg, zpow_one, Finset.card_empty, zpow_neg, Finset.sum_empty, zero_sub, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
empty :
  ∀ (x : ℍ),
    @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 x =
      HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1 x
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 =
    HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1

Tactic:
ext _
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
x : ℍ
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 x =
    HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1 x

Tactic:
simp [slash_apply]

Premises used: ModularForm.slash_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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))
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))
⊢ @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

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
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:
simp
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
⊢ ∑ i ∈ insert i t, k i = k i + ∑ i ∈ t, k i

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
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))
⊢ @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:
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]

Premises used: Nat.cast_succ, ModularForm.mul_slash, Finset.prod_insert, Finset.card_insert_of_notMem, mul_smul_comm, add_sub_cancel_right, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
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) : ℤ)
⊢ (|(↑((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:
congr 1
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
⊢ (↑(#t) : ℤ) = 1 + HSub.hSub (α := ℤ) (↑(#t) : ℤ) 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
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)
⊢ |(↑((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:
nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
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
⊢ |(↑((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:
rw [zpow_add', zpow_one]

Premises used: zpow_one, zpow_add'
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
insert : Ne (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 0
⊢ 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:
left
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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

Tactic:
abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.det_ne_zero, abs_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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

Tactic:
exact abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.det_ne_zero, abs_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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))
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.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))
⊢ @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))

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)

Premises used: CharP.cast_eq_zero, Iff.mpr, Nat.cast_succ, ModularForm.mul_slash, Finset.prod_empty, Int.reduceNeg, Matrix.GeneralLinearGroup.det_ne_zero, zpow_one, zpow_add', Insert.insert, abs_ne_zero, Finset.card_empty, zpow_neg, mul_smul_comm, Finset.sum_empty, add_sub_cancel_right, SemigroupAction.mul_smul, rfl, zero_sub, ModularForm.slash_apply, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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))
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.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))
⊢ @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))

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)

Premises used: CharP.cast_eq_zero, Iff.mpr, Nat.cast_succ, ModularForm.mul_slash, Finset.prod_empty, Int.reduceNeg, Matrix.GeneralLinearGroup.det_ne_zero, zpow_one, zpow_add', Insert.insert, abs_ne_zero, Finset.card_empty, zpow_neg, mul_smul_comm, Finset.sum_empty, add_sub_cancel_right, SemigroupAction.mul_smul, rfl, zero_sub, ModularForm.slash_apply, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
rw : k * (↑(#s) : ℤ) = #s • k
rw₁ rw₂ : k * (↑(#s) : ℤ) = k * (↑(#s) : ℤ)
⊢ k * (↑(#s) : ℤ) = ∑ i ∈ s, k

Tactic:
rw [Finset.sum_const, nsmul_eq_mul']

Premises used: nsmul_eq_mul', Finset.sum_const