[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Commensurable H H
[PROOFSTEP]
simp [Commensurable]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : { x // x ∈ K }
⊢ Setoid.r a b ↔ Setoid.r (↑(Subgroup.equivSMul g K).toEquiv a) (↑(Subgroup.equivSMul g K).toEquiv b)
[PROOFSTEP]
dsimp
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : { x // x ∈ K }
⊢ Setoid.r a b ↔ Setoid.r (↑(Subgroup.equivSMul g K) a) (↑(Subgroup.equivSMul g K) b)
[PROOFSTEP]
rw [← Quotient.eq'', ← Quotient.eq'', QuotientGroup.eq', QuotientGroup.eq', Subgroup.mem_subgroupOf,
  Subgroup.mem_subgroupOf, ← MulEquiv.map_inv, ← MulEquiv.map_mul, Subgroup.equivSMul_apply_coe]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : { x // x ∈ K }
⊢ ↑(a⁻¹ * b) ∈ H ↔ g • ↑(a⁻¹ * b) ∈ g • H
[PROOFSTEP]
exact Subgroup.smul_mem_pointwise_smul_iff.symm
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : ConjAct G
⊢ Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)
[PROOFSTEP]
rw [commensurable_conj, inv_smul_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | Commensurable (g • H) H}
hb : b✝ ∈ {g | Commensurable (g • H) H}
⊢ a✝ * b✝ ∈ {g | Commensurable (g • H) H}
[PROOFSTEP]
rw [Set.mem_setOf_eq, mul_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | Commensurable (g • H) H}
hb : b✝ ∈ {g | Commensurable (g • H) H}
⊢ Commensurable (a✝ • b✝ • H) H
[PROOFSTEP]
exact trans ((commensurable_conj _).mp hb) ha
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 ∈
    { carrier := {g | Commensurable (g • H) H},
        mul_mem' :=
          (_ :
            ∀ {a b : ConjAct G},
              a ∈ {g | Commensurable (g • H) H} →
                b ∈ {g | Commensurable (g • H) H} → a * b ∈ {g | Commensurable (g • H) H}) }.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, one_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝¹ : ConjAct G
x✝ :
  x✝¹ ∈
    {
          toSubsemigroup :=
            { carrier := {g | Commensurable (g • H) H},
              mul_mem' :=
                (_ :
                  ∀ {a b : ConjAct G},
                    a ∈ {g | Commensurable (g • H) H} →
                      b ∈ {g | Commensurable (g • H) H} → a * b ∈ {g | Commensurable (g • H) H}) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := {g | Commensurable (g • H) H},
                    mul_mem' :=
                      (_ :
                        ∀ {a b : ConjAct G},
                          a ∈ {g | Commensurable (g • H) H} →
                            b ∈ {g | Commensurable (g • H) H} →
                              a * b ∈ {g | Commensurable (g • H) H}) }.carrier) }.toSubsemigroup.carrier
⊢ x✝¹⁻¹ ∈
    {
          toSubsemigroup :=
            { carrier := {g | Commensurable (g • H) H},
              mul_mem' :=
                (_ :
                  ∀ {a b : ConjAct G},
                    a ∈ {g | Commensurable (g • H) H} →
                      b ∈ {g | Commensurable (g • H) H} → a * b ∈ {g | Commensurable (g • H) H}) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := {g | Commensurable (g • H) H},
                    mul_mem' :=
                      (_ :
                        ∀ {a b : ConjAct G},
                          a ∈ {g | Commensurable (g • H) H} →
                            b ∈ {g | Commensurable (g • H) H} →
                              a * b ∈ {g | Commensurable (g • H) H}) }.carrier) }.toSubsemigroup.carrier
[PROOFSTEP]
rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]
