awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
refine :
  𝒢.HasDetPlusMinusOne →
    ∀ {g : GL n R} (hg : g ∈ 𝒢.adjoinNegOne),
      Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
        Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)
⊢ 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne

Tactic:
refine ⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetPlusMinusOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : g ∈ 𝒢
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
HasDetPlusMinusOne.det_eq hg

Premises used: Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : g ∈ 𝒢
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
exact HasDetPlusMinusOne.det_eq hg

Premises used: Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
pos :
  ∀ (hn : Even (Fintype.card n)),
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
      Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)
neg :
  ∀ (hn : ¬Even (Fintype.card n)),
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
      Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
by_cases hn : Even (Fintype.card n)

Premises used: Fintype.card, Even
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : Even (Fintype.card n)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (-1 : Rˣ)

Tactic:
HasDetPlusMinusOne.det_eq hg

Premises used: Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h_1 : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : Even (Fintype.card n)
h :
  Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (1 : Rˣ)
h₁ :
  Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (-1 : Rˣ)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
convert! HasDetPlusMinusOne.det_eq hg using 1

Premises used: Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : Even (Fintype.card n)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (1 : Rˣ)

Tactic:
simp [Units.ext_iff, det_neg, hn]

Premises used: Units.ext_iff, Matrix.det_neg
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : Even (Fintype.card n)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (-1 : Rˣ)

Tactic:
simp [Units.ext_iff, det_neg, hn]

Premises used: Units.ext_iff, Matrix.det_neg
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (-1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (1 : Rˣ)

Tactic:
(HasDetPlusMinusOne.det_eq hg).symm

Premises used: Or.symm, Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h_1 : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
h :
  Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (-1 : Rˣ)
h₁ :
  Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (1 : Rˣ)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ∨
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ)

Tactic:
convert! (HasDetPlusMinusOne.det_eq hg).symm using 1

Premises used: Or.symm, Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (-1 : Rˣ)

Tactic:
simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

Premises used: Units.ext_iff, neg_eq_iff_eq_neg, Nat.not_even_iff_odd, Matrix.det_neg, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
h : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (-1 : Rˣ) ↔
    Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) (-g) : Rˣ) (1 : Rˣ)

Tactic:
simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

Premises used: Units.ext_iff, neg_eq_iff_eq_neg, Nat.not_even_iff_odd, Matrix.det_neg, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
⊢ 𝒢.adjoinNegOne.HasDetOne ↔ 𝒢.HasDetOne

Tactic:
⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩

Premises used: Subgroup.HasDetOne.det_eq, Subgroup.HasDetOne.mk, Iff.intro, Subgroup.le_adjoinNegOne
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
refine :
  𝒢.HasDetOne →
    ∀ {g : GL n R} (hg : g ∈ 𝒢.adjoinNegOne),
      Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)
⊢ 𝒢.adjoinNegOne.HasDetOne ↔ 𝒢.HasDetOne

Tactic:
refine ⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
h : 𝒢.HasDetOne
g : GL n R
hg : g ∈ 𝒢
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)

Tactic:
HasDetOne.det_eq hg

Premises used: Subgroup.HasDetOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
h : 𝒢.HasDetOne
g : GL n R
hg : g ∈ 𝒢
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)

Tactic:
exact HasDetOne.det_eq hg

Premises used: Subgroup.HasDetOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
h : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ Eq.{u_3 + 1} (α := Rˣ) ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g : Rˣ) (1 : Rˣ)

Tactic:
simpa [Units.ext_iff, det_neg, hn] using HasDetOne.det_eq hg

Premises used: Units.ext_iff, Subgroup.HasDetOne.det_eq, Matrix.det_neg
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R_1 : Type u_2
inst_2 : Ring R_1
R : Type u_3
inst_3 : CommRing R
𝒢 : Subgroup (GL n R)
inst_4 : 𝒢.HasDetPlusMinusOne
⊢ 𝒢.adjoinNegOne.HasDetPlusMinusOne

Tactic:
Subgroup.hasDetPlusMinusOne_adjoinNegOne_iff.2 ‹_›

Premises used: Iff.mpr, Subgroup.hasDetPlusMinusOne_adjoinNegOne_iff
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R_1 : Type u_2
inst_2 : Ring R_1
R : Type u_3
inst_3 : CommRing R
𝒢 : Subgroup (GL n R)
inst_4 : 𝒢.HasDetOne
inst_5 : Fact (Even (Fintype.card n))
⊢ 𝒢.adjoinNegOne.HasDetOne

Tactic:
(Subgroup.hasDetOne_adjoinNegOne_iff Fact.out).2 ‹_›

Premises used: Iff.mpr, Subgroup.hasDetOne_adjoinNegOne_iff, Fact.out
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst_3 : 𝒢.IsArithmetic
⊢ 𝒢.adjoinNegOne.IsArithmetic

Tactic:
⟨(𝒢.commensurable_adjoinNegOne_self).trans IsArithmetic.is_commensurable⟩

Premises used: Subgroup.IsArithmetic.mk, Subgroup.IsArithmetic.is_commensurable, Subgroup.commensurable_adjoinNegOne_self, Subgroup.Commensurable.trans
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)

Tactic:
.mul (.mul ?_ mdifferentiable_const) (mdifferentiable_denom_zpow g _)

Premises used: mdifferentiable_const, _private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash, MDifferentiable.mul, UpperHalfPlane.mdifferentiable_denom_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
refine : MDiff fun (x : ℍ) ↦ (σ g : (a : ℂ) → ℂ) (f (g • x))
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)

Tactic:
refine .mul (.mul ?_ mdifferentiable_const) (mdifferentiable_denom_zpow g _)
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ MDiff fun (x : ℍ) ↦ (σ g : (a : ℂ) → ℂ) (f (g • x))

Tactic:
simpa only [σ, hg, ↓reduceIte] using hf.comp (mdifferentiable_smul hg)

Premises used: MDifferentiable.comp, reduceIte, UpperHalfPlane.σ, UpperHalfPlane.mdifferentiable_smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k J f = fun (τ : ℍ) ↦
    (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))))

Tactic:
simp [slash_def, J_smul]

Premises used: UpperHalfPlane.J_smul, ModularForm.slash_def
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
simp :
  ∀ (hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}),
    DifferentiableOn ℂ (F := ℂ)
      (fun (x : ℂ) ↦
        (starRingEnd ℂ : (a : ℂ) → ℂ)
          (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
      {z : ℂ | 0 < z.im}
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k J f)

Tactic:
simp only [mdifferentiable_iff, slash_J, Function.comp_def] at hf ⊢

Premises used: _private.0.slash_J, Function.comp_def, UpperHalfPlane.mdifferentiable_iff
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
z : ℂ
h : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
⊢ Eq (α := ℂ)
    ((fun (x : ℂ) ↦
        ((starRingEnd ℂ : (a : ℂ) → ℂ)
            (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))) :
          ℂ))
      z)
    ((fun (x : ℂ) ↦ ((starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))) : ℂ))
      z)

Tactic:
simp [ofComplex_apply_of_im_pos h]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
⊢ Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}

Tactic:
have : {z | 0 < z.im}.EqOn (fun x ↦ conj (f <| ofComplex <| -conj ↑(ofComplex x)))
      (fun x ↦ conj (f <| ofComplex <| -conj x)) := fun z h ↦ by simp [ofComplex_apply_of_im_pos h]
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
this :
  Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    {z : ℂ | 0 < z.im}

Tactic:
.congr (fun z hz ↦ DifferentiableAt.differentiableWithinAt ?_) this

Premises used: DifferentiableOn.congr, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
this :
  Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}
refine :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z),
    DifferentiableAt ℂ (F := ℂ)
      (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)))) z
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    {z : ℂ | 0 < z.im}

Tactic:
refine .congr (fun z hz ↦ DifferentiableAt.differentiableWithinAt ?_) this
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
this :
  Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
⊢ 0 < Complex.im (-(starRingEnd ℂ : (a : ℂ) → ℂ) z)

Tactic:
simpa using hz
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
this :
  Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
⊢ 0 < Complex.im (-(starRingEnd ℂ : (a : ℂ) → ℂ) z)

Tactic:
have : 0 < (-conj z).im := by simpa using hz
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
this_1 :
  Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
this : 0 < Complex.im (-(starRingEnd ℂ : (a : ℂ) → ℂ) z)
⊢ DifferentiableAt ℂ (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) (-(starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)

Tactic:
have := hf.differentiableAt (isOpen_upperHalfPlaneSet.mem_nhds this)
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) {z : ℂ | 0 < z.im}
this_1 :
  Set.EqOn (β := ℂ)
    (fun (x : ℂ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑((↑ofComplex : ℂ → ℍ) x) : ℂ)))))
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x))))
    {z : ℂ | 0 < z.im}
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
this_2 : 0 < Complex.im (-(starRingEnd ℂ : (a : ℂ) → ℂ) z)
this :
  DifferentiableAt ℂ (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) (-(starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)))) z

Tactic:
simpa using (this.comp _ differentiable_neg.differentiableAt).star_star.neg

Premises used: Differentiable.differentiableAt, DifferentiableAt.neg, DifferentiableAt.star_star, differentiable_neg, DifferentiableAt.comp
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)

Tactic:
g.det_ne_zero.lt_or_gt.elim (fun hg ↦ ?_) (hf.slash_of_pos k)

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, _private.0.MDifferentiable.slash_of_pos, Or.elim, Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0

Tactic:
refine g.det_ne_zero.lt_or_gt.elim (fun hg ↦ ?_) (hf.slash_of_pos k)

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, _private.0.MDifferentiable.slash_of_pos, Or.elim, Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ g = J * (J * g)

Tactic:
simp [← mul_assoc, ← sq]

Premises used: mul_assoc, sq
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
rw :
  MDiff
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (J * g)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k J f))
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)

Tactic:
rw [show g = J * (J * g) by simp [← mul_assoc, ← sq], SlashAction.slash_mul]

Premises used: SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (J * g)) : ℝ)

Tactic:
simpa using hg
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ MDiff
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (J * g)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k J f))

Tactic:
exact (hf.slashJ k).slash_of_pos _ (by simpa using hg)

Premises used: _private.0.MDifferentiable.slashJ, _private.0.MDifferentiable.slash_of_pos
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
h : Eq (α := (a : ℍ) → ℂ) ((fun (f : ModularForm Γ k) ↦ f.toFun) f) ((fun (f : ModularForm Γ k) ↦ f.toFun) g)
mk :
  ∀ (toSlashInvariantForm : SlashInvariantForm Γ k) (holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ))
    (bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k)
    (h :
      Eq (α := (a : ℍ) → ℂ)
        ((fun (f : ModularForm Γ k) ↦ f.toFun)
          { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
        ((fun (f : ModularForm Γ k) ↦ f.toFun) g)),
    { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' :
        ModularForm Γ k } =
      g
⊢ f = g

Tactic:
cases f