awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst_2 : 𝒢.IsArithmetic
⊢ FiniteIndex (G := SL(2, ℤ)) (comap (mapGL ℝ) 𝒢)

Tactic:
⟨𝒢.index_comap (mapGL (R := ℤ) ℝ) ▸ IsArithmetic.is_commensurable.1⟩

Premises used: Real, Subgroup.IsArithmetic.is_commensurable, Eq.rec, And.left, Subgroup.index_comap, Subgroup.FiniteIndex.mk, Matrix.SpecialLinearGroup.mapGL, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
rw : ∀ {g : GL (Fin 2) ℝ}, g ∈ Γ → Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1
⊢ Γ.HasDetPlusMinusOne

Tactic:
rw [hasDetPlusMinusOne_iff_abs_det]

Premises used: Subgroup.hasDetPlusMinusOne_iff_abs_det
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
obtain :
  ∀ (n : ℕ) (hn : 0 < n),
    n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ →
      ∀ (hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ),
        Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1
⊢ Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1

Tactic:
obtain ⟨n, hn, _, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero
    Subgroup.IsArithmetic.is_commensurable.2 hg

Premises used: Subgroup.IsArithmetic.is_commensurable, Subgroup.exists_pow_mem_of_relIndex_ne_zero, And.right
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
this : |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
⊢ Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1

Tactic:
simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]

Premises used: abs_pow_eq_one, Nat.ne_zero_of_lt, abs_pow
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
suffices : |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
⊢ Eq (α := ℝ) |(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| 1

Tactic:
suffices |(g.det ^ n).val| = 1 by simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
obtain :
  ∀ (t : SL(2, ℤ)) (ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n),
    |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1
⊢ |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1

Tactic:
obtain ⟨t, ht⟩ := hgn.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n
⊢ Eq (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (g ^ n) : ℝˣ)
    ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t) : ℝˣ)

Tactic:
have := congr_arg Matrix.GeneralLinearGroup.det ht.symm
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n
this :
  Eq (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (g ^ n) : ℝˣ)
    ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t) : ℝˣ)
⊢ HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n = 1

Tactic:
rw [Matrix.SpecialLinearGroup.det_mapGL, map_pow] at this

Premises used: map_pow, Matrix.SpecialLinearGroup.det_mapGL
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n_1 : Type u_1
inst : Fintype n_1
inst_1 : DecidableEq n_1
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left : n ≤ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) Γ
hgn : g ^ n ∈ MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ) ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) t = g ^ n
this : HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n = 1
⊢ |(↑(HPow.hPow (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g : ℝˣ) n) : ℝ)| = 1

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst_2 : 𝒢.IsArithmetic
⊢ 𝒢.IsFiniteRelIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
⟨IsArithmetic.is_commensurable.1⟩

Premises used: Subgroup.IsArithmetic.is_commensurable, And.left, Subgroup.IsFiniteRelIndex.mk
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
is_commensurable : (Γ ⊓ Γ').Commensurable (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (Γ ⊓ Γ').IsArithmetic

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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
is_commensurable₁ : relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) (Γ ⊓ Γ') ≠ 0
⊢ (Γ ⊓ Γ').Commensurable (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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
is_commensurable₁ : Γ'.relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0
⊢ (Γ ⊓ Γ').relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ≠ 0

Tactic:
apply relIndex_inf_ne_zero

Premises used: Subgroup.relIndex_inf_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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

Tactic:
IsArithmetic.is_commensurable.1

Premises used: Subgroup.IsArithmetic.is_commensurable, And.left
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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

Tactic:
exact IsArithmetic.is_commensurable.1

Premises used: Subgroup.IsArithmetic.is_commensurable, And.left
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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

Tactic:
IsArithmetic.is_commensurable.1

Premises used: Subgroup.IsArithmetic.is_commensurable, And.left
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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

Tactic:
exact IsArithmetic.is_commensurable.1

Premises used: Subgroup.IsArithmetic.is_commensurable, And.left
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
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 (Γ ⊓ Γ') ≠ 0
⊢ relIndex (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) (Γ ⊓ Γ') ≠ 0

Tactic:
apply relIndex_ne_zero_trans (K := Γ) IsArithmetic.is_commensurable.2

Premises used: Subgroup.IsArithmetic.is_commensurable, And.right, Subgroup.relIndex_ne_zero_trans
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
is_commensurable : Ne (α := ℕ) 1 0
⊢ Γ.relIndex (Γ ⊓ Γ') ≠ 0

Tactic:
rw [relIndex_eq_one.mpr inf_le_left]

Premises used: Iff.mpr, Subgroup.relIndex_eq_one, inf_le_left
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.IsArithmetic
inst_3 : Γ'.IsArithmetic
⊢ Ne (α := ℕ) 1 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
⊢ DiscreteTopology.{u_1} ↥(MonoidHom.range (G := SL n ℤ) (mapGL ℝ))

Tactic:
(isEmbedding_mapGL Real.isClosedEmbedding_intCast.1).toHomeomorph.discreteTopology

Premises used: Set.Mem, setOf, Topology.IsClosedEmbedding.toIsEmbedding, Homeomorph.discreteTopology, Real.isClosedEmbedding_intCast, Set.range, Topology.IsEmbedding.toHomeomorph, Matrix.SpecialLinearGroup.isEmbedding_mapGL
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
⊢ DiscreteTopology.{u_1} ↥(MonoidHom.range (map (Int.castRingHom ℝ)))

Tactic:
(Topology.IsEmbedding.toHomeomorph ?_).discreteTopology

Premises used: Set.Mem, setOf, Homeomorph.discreteTopology, Set.range, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
refine :
  Topology.IsEmbedding.{u_1, u_1} (X := SL n ℤ) (Y := SL n ℝ) (⇑(map (Int.castRingHom ℝ)) : (a : SL n ℤ) → SL n ℝ)
⊢ DiscreteTopology.{u_1} ↥(MonoidHom.range (map (Int.castRingHom ℝ)))

Tactic:
refine (Topology.IsEmbedding.toHomeomorph ?_).discreteTopology

Premises used: Homeomorph.discreteTopology, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
⊢ Topology.IsEmbedding.{u_1, u_1} (X := SL n ℤ) (Y := SL n ℝ) (⇑(map (Int.castRingHom ℝ)) : (a : SL n ℤ) → SL n ℝ)

Tactic:
Real.isClosedEmbedding_intCast.specialLinearGroup_map.1

Premises used: Topology.IsClosedEmbedding.specialLinearGroup_map, Topology.IsClosedEmbedding.toIsEmbedding
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
⊢ Topology.IsEmbedding.{u_1, u_1} (X := SL n ℤ) (Y := SL n ℝ) (⇑(map (Int.castRingHom ℝ)) : (a : SL n ℤ) → SL n ℝ)

Tactic:
exact Real.isClosedEmbedding_intCast.specialLinearGroup_map.1

Premises used: Topology.IsClosedEmbedding.specialLinearGroup_map, Topology.IsClosedEmbedding.toIsEmbedding
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
⊢ Topology.IsClosedEmbedding.{u_1, u_1} (X := SL n ℤ) (Y := GL n ℝ) (⇑(mapGL ℝ) : (a : SL n ℤ) → GL n ℝ)

Tactic:
isClosedEmbedding_mapGL Real.isClosedEmbedding_intCast

Premises used: Real.isClosedEmbedding_intCast, Matrix.SpecialLinearGroup.isClosedEmbedding_mapGL
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst_2 : 𝒢.IsArithmetic
rw : DiscreteTopology ↥(MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ DiscreteTopology ↥𝒢

Tactic:
rw [is_commensurable.discreteTopology_iff]

Premises used: Subgroup.IsArithmetic.is_commensurable, Subgroup.Commensurable.discreteTopology_iff
-- Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst_2 : 𝒢.IsArithmetic
⊢ DiscreteTopology ↥(MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
infer_instance
-- 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 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)
inr : ∀ (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)

Tactic:
rcases ha with ha | ha
-- 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 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)
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)

Tactic:
rcases hb with hb | hb
-- 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 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)
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)

Tactic:
rcases hb with hb | hb
-- 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 n R)
a b : GL n R
ha : a ∈ 𝒢
hb : b ∈ 𝒢
⊢ a * b ∈ 𝒢

Tactic:
have := mul_mem ha hb
-- 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 n R)
a b : GL n R
ha : a ∈ 𝒢
hb : b ∈ 𝒢
this : a * b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)

Tactic:
aesop
-- 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 n R)
a b : GL n R
ha : a ∈ 𝒢
hb : -b ∈ 𝒢
⊢ a * -b ∈ 𝒢

Tactic:
have := mul_mem ha hb
-- 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 n R)
a b : GL n R
ha : a ∈ 𝒢
hb : -b ∈ 𝒢
this : a * -b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)

Tactic:
aesop
-- 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 n R)
a b : GL n R
ha : -a ∈ 𝒢
hb : b ∈ 𝒢
⊢ -a * b ∈ 𝒢

Tactic:
have := mul_mem ha hb
-- 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 n R)
a b : GL n R
ha : -a ∈ 𝒢
hb : b ∈ 𝒢
this : -a * b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)

Tactic:
aesop
-- 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 n R)
a b : GL n R
ha : -a ∈ 𝒢
hb : -b ∈ 𝒢
⊢ -a * -b ∈ 𝒢

Tactic:
have := mul_mem ha hb
-- 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 n R)
a b : GL n R
ha : -a ∈ 𝒢
hb : -b ∈ 𝒢
this : -a * -b ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} (a * b)

Tactic:
aesop
-- 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 n R)
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} 1

Tactic:
simp
-- 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 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⁻¹
inr : ∀ (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⁻¹

Tactic:
rcases ha with (ha | ha)
-- 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 n R)
x : GL n R
ha : x ∈ 𝒢
⊢ x⁻¹ ∈ 𝒢

Tactic:
have := inv_mem ha
-- 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 n R)
x : GL n R
ha : x ∈ 𝒢
this : x⁻¹ ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹

Tactic:
aesop
-- 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 n R)
x : GL n R
ha : -x ∈ 𝒢
⊢ (-x)⁻¹ ∈ 𝒢

Tactic:
have := inv_mem ha
-- 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 n R)
x : GL n R
ha : -x ∈ 𝒢
this : (-x)⁻¹ ∈ 𝒢
⊢ Membership.mem (γ := Set (GL n R)) {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢} x⁻¹

Tactic:
aesop
-- 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 n R)
g : GL n R
⊢ g ∈ 𝒢.adjoinNegOne ↔ g ∈ 𝒢 ∨ -g ∈ 𝒢

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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 n R)
⊢ 𝒢 ≤ 𝒢.adjoinNegOne

Tactic:
fun _ hg ↦ .inl hg

Premises used: Set.Mem, setOf, Or.inl
-- 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 n R)
⊢ -1 ∈ 𝒢.adjoinNegOne

Tactic:
simp
-- 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 n R)
hG : -1 ∈ 𝒢
g : GL n R
hg : g ∈ 𝒢.adjoinNegOne
h : -g ∈ 𝒢
⊢ g ∈ 𝒢

Tactic:
simpa using mul_mem hG h

Premises used: MulMemClass.mul_mem
-- 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 n R)
h𝒢 : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne = 2

Tactic:
relIndex_eq_two_iff_exists_notMem_and.mpr ⟨_, 𝒢.negOne_mem_adjoinNegOne, h𝒢, ?_⟩

Premises used: Iff.mpr, Subgroup.negOne_mem_adjoinNegOne, Subgroup.relIndex_eq_two_iff_exists_notMem_and, And.intro, Exists.intro
-- 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 n R)
h𝒢 : -1 ∉ 𝒢
refine : ∀ b ∈ 𝒢.adjoinNegOne, b * -1 ∈ 𝒢 ∨ b ∈ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne = 2

Tactic:
refine relIndex_eq_two_iff_exists_notMem_and.mpr ⟨_, 𝒢.negOne_mem_adjoinNegOne, h𝒢, ?_⟩

Premises used: Iff.mpr, Subgroup.negOne_mem_adjoinNegOne, Subgroup.relIndex_eq_two_iff_exists_notMem_and, And.intro, Exists.intro
-- 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 n R)
h𝒢 : -1 ∉ 𝒢
⊢ ∀ b ∈ 𝒢.adjoinNegOne, b * -1 ∈ 𝒢 ∨ b ∈ 𝒢

Tactic:
simp [mem_adjoinNegOne_iff, or_comm]

Premises used: Subgroup.mem_adjoinNegOne_iff, or_comm
-- 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 n R)
pos : ∀ (hG : -1 ∈ 𝒢), 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
neg : ∀ (hG : -1 ∉ 𝒢), 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
by_cases hG : -1 ∈ 𝒢
-- 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 n R)
hG : -1 ∈ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
simp [adjoinNegOne_eq_self_iff.mpr hG]

Premises used: Iff.mpr, Subgroup.adjoinNegOne_eq_self_iff
-- 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 n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
simp [𝒢.relindex_adjoinNegOne_eq_two hG]

Premises used: Subgroup.relindex_adjoinNegOne_eq_two
-- 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 n R)
⊢ 𝒢.IsFiniteRelIndex 𝒢.adjoinNegOne

Tactic:
⟨𝒢.relIndex_adjoinNegOne_ne_zero⟩

Premises used: Subgroup.relIndex_adjoinNegOne_ne_zero, Subgroup.IsFiniteRelIndex.mk
-- 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 n R)
⊢ 𝒢.adjoinNegOne.relIndex 𝒢 ≠ 0

Tactic:
simp [Subgroup.relIndex_eq_one.mpr 𝒢.le_adjoinNegOne]

Premises used: Iff.mpr, Subgroup.relIndex_eq_one, Subgroup.le_adjoinNegOne
-- 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
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : T2Space R
𝒢 : Subgroup (GL n R)
inst_6 : DiscreteTopology ↥𝒢
rwa rwa₁ rwa₂ rwa₃ : DiscreteTopology ↥𝒢
⊢ DiscreteTopology ↥𝒢.adjoinNegOne

Tactic:
rwa [𝒢.commensurable_adjoinNegOne_self.discreteTopology_iff]

Premises used: Subgroup.commensurable_adjoinNegOne_self, Subgroup.Commensurable.discreteTopology_iff
-- 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)
⊢ 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne

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

Premises used: Subgroup.HasDetPlusMinusOne.det_eq, Iff.intro, Subgroup.le_adjoinNegOne, Subgroup.HasDetPlusMinusOne.mk