G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
⊢ ∃! x, ↑x.fst * ↑x.snd = g
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
⊢ IsComplement' H (MulAction.stabilizer G a)
refine' isComplement_iff_existsUnique.mpr fun g => _
case intro
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
⊢ ∃! x, ↑x.fst * ↑x.snd = g
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
⊢ ∃! x, ↑x.fst * ↑x.snd = g
obtain ⟨h, hh⟩ := h2 g
case intro
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∃! x, ↑x.fst * ↑x.snd = g
case intro
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
⊢ ∃! x, ↑x.fst * ↑x.snd = g
have hh' : (↑h * g) • a = a := by rwa [mul_smul]
case intro
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∀ (y : ↑↑H × ↑↑(MulAction.stabilizer G a)),
    (fun x => ↑x.fst * ↑x.snd = g) y → y = (h⁻¹, { val := ↑h * g, property := hh' })
case intro
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∃! x, ↑x.fst * ↑x.snd = g
refine' ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left ↑h g, _⟩
case intro.mk.mk
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
⊢ (h', { val := g, property := hg }) =
    (h⁻¹,
      { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
        property := hh' })
case intro
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∀ (y : ↑↑H × ↑↑(MulAction.stabilizer G a)),
    (fun x => ↑x.fst * ↑x.snd = g) y → y = (h⁻¹, { val := ↑h * g, property := hh' })
rintro ⟨h', g, hg : g • a = a⟩ rfl
case intro.mk.mk
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
h1 : h * h' = 1
⊢ (h', { val := g, property := hg }) =
    (h⁻¹,
      { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
        property := hh' })
case intro.mk.mk
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
⊢ (h', { val := g, property := hg }) =
    (h⁻¹,
      { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
        property := hh' })
specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])
case intro.mk.mk
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
h1 : h * h' = 1
⊢ ↑(h', { val := g, property := hg }).snd =
    ↑(h⁻¹,
          { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
            property := hh' }).snd
case intro.mk.mk
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
h1 : h * h' = 1
⊢ (h', { val := g, property := hg }) =
    (h⁻¹,
      { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
        property := hh' })
refine' Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext _)
no goals
case intro.mk.mk
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
h1 : h * h' = 1
⊢ ↑(h', { val := g, property := hg }).snd =
    ↑(h⁻¹,
          { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
            property := hh' }).snd
rwa [Subtype.ext_iff, coe_one, coe_mul, ← self_eq_mul_left, mul_assoc (↑h) (↑h') g] at h1
no goals
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
⊢ (↑h * g) • a = a
rwa [mul_smul]
no goals
G : Type u_2
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_1
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
⊢ (h * h') • a = a
rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]