awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
is_commensurable : (Γ ⊓ Γ').relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
⊢ (Γ ⊓ Γ').Commensurable (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
have is_commensurable₁ : relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) (Γ ⊓ Γ') ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
have is_commensurable : Γ.relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
Tactic: apply relIndex_inf_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
is_commensurable : Γ.relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
⊢ (Γ ⊓ Γ').relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
have is_commensurable₁ : Γ'.relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
Tactic: apply relIndex_inf_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
⊢ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) (Γ ⊓ Γ') ≠ 0
have is_commensurable : Γ.relIndex (Γ ⊓ Γ') ≠ 0
Tactic: apply relIndex_ne_zero_trans (K := Γ) IsArithmetic.is_commensurable.2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
⊢ Γ.relIndex (Γ ⊓ Γ') ≠ 0
have is_commensurable : Ne (α := ℕ) 1 0
Tactic: rw [relIndex_eq_one.mpr inf_le_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
⊢ DiscreteTopology.{u_1} ↥(MonoidHom.range (map (Int.castRingHom ℝ)))
have refine : Topology.IsEmbedding.{u_1, u_1} (X := SL n ℤ) (Y := SL n ℝ) (⇑(map (Int.castRingHom ℝ)) : (a : SL n ℤ) → SL n ℝ)
Tactic: refine (Topology.IsEmbedding.toHomeomorph ?_).discreteTopology
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst_2 : 𝒢.IsArithmetic
⊢ DiscreteTopology ↥𝒢
have rw : DiscreteTopology ↥(MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
Tactic: rw [is_commensurable.discreteTopology_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
ha : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} a
hb : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} b
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have inl : ∀ (ha : a ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
ha : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} a
hb : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} b
inl : ∀ (ha : a ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have inr : ∀ (ha : -a ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
hb : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} b
ha : a ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have inl : ∀ (hb : b ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
hb : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} b
ha : a ∈ 𝒢
inl : ∀ (hb : b ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have inl₁ : ∀ (hb : -b ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
hb : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} b
ha : -a ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have inr : ∀ (hb : b ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
hb : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} b
ha : -a ∈ 𝒢
inr : ∀ (hb : b ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have inr₁ : ∀ (hb : -b ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
ha : a ∈ 𝒢
hb : b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have this : a * b ∈ 𝒢
Tactic: have := mul_mem ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
ha : a ∈ 𝒢
hb : -b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have this : a * -b ∈ 𝒢
Tactic: have := mul_mem ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
ha : -a ∈ 𝒢
hb : b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have this : -a * b ∈ 𝒢
Tactic: have := mul_mem ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
a b : GL n R
ha : -a ∈ 𝒢
hb : -b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)
have this : -a * -b ∈ 𝒢
Tactic: have := mul_mem ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
x : GL n R
ha : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
have inl : ∀ (ha : x ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
Tactic: rcases ha with (ha | ha)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
x : GL n R
ha : Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x
inl : ∀ (ha : x ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
have inr : ∀ (ha : -x ∈ 𝒢), Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
Tactic: rcases ha with (ha | ha)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
x : GL n R
ha : x ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
have this : x⁻¹ ∈ 𝒢
Tactic: have := inv_mem ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
x : GL n R
ha : -x ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹
have this : (-x)⁻¹ ∈ 𝒢
Tactic: have := inv_mem ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
h𝒢 : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne = 2
have refine : ∀ b ∈ 𝒢.adjoinNegOne, b * -1 ∈ 𝒢 ∨ b ∈ 𝒢
Tactic: refine relIndex_eq_two_iff_exists_notMem_and.mpr ⟨_, 𝒢.negOne_mem_adjoinNegOne, h𝒢, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
have pos : ∀ (hG : -1 ∈ 𝒢), 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
Tactic: by_cases hG : -1 ∈ 𝒢
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_2
inst_2 : Ring R
𝒢 : Subgroup (GL n R)
pos : ∀ (hG : -1 ∈ 𝒢), 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
have neg : ∀ (hG : -1 ∉ 𝒢), 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
Tactic: by_cases hG : -1 ∈ 𝒢
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_3
inst_2 : CommRing R
𝒢 : Subgroup (GL n R)
⊢ 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne
have 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ˣ)
Tactic: refine ⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetPlusMinusOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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ˣ)
have 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ˣ)
Tactic: by_cases hn : Even (Fintype.card n)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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ˣ)
⊢ 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ˣ)
have 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ˣ)
Tactic: by_cases hn : Even (Fintype.card n)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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ˣ)
have 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ˣ)
Tactic: convert! HasDetPlusMinusOne.det_eq hg using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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ˣ)
⊢ 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ˣ)
have 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ˣ)
Tactic: convert! HasDetPlusMinusOne.det_eq hg using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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ˣ)
have 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ˣ)
Tactic: convert! (HasDetPlusMinusOne.det_eq hg).symm using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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ˣ)
⊢ 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ˣ)
have 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ˣ)
Tactic: convert! (HasDetPlusMinusOne.det_eq hg).symm using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups (goal)
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
have 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ˣ)
Tactic: refine ⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
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)
have refine : MDiff fun (x : ℍ) ↦ (σ g : (a : ℂ) → ℂ) (f (g • x))
Tactic: refine .mul (.mul ?_ mdifferentiable_const) (mdifferentiable_denom_zpow g _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k J f)
have 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}
Tactic: simp only [mdifferentiable_iff, slash_J, Function.comp_def] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
Goal:
f : ℍ → ℂ
k : ℤ
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}
have 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}
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
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}
have refine : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z),
  DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)))) z
Tactic: refine .congr (fun z hz ↦ DifferentiableAt.differentiableWithinAt ?_) this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
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
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)))) z
have this₁ : 0 < Complex.im (-(starRingEnd ℂ : (a : ℂ) → ℂ) z)
Tactic: have : 0 < (-conj z).im := by simpa using hz
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
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 ℂ (F := ℂ)
    (fun (x : ℂ) ↦ (starRingEnd ℂ : (a : ℂ) → ℂ) (f ((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)))) z
have this₁ : DifferentiableAt ℂ (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) x)) (-(starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
Tactic: have := hf.differentiableAt (isOpen_upperHalfPlaneSet.mem_nhds this)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
Goal:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
⊢ MDiff (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
have hg : (↑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)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
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 g f)
have 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))
Tactic: rw [show g = J * (J * g) by simp [← mul_assoc, ← sq], SlashAction.slash_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
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)
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h