[GOAL]
M : Type u
α : Type v
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
⊢ (fun m => m • a) 1 = a
[PROOFSTEP]
simp [MulAction.one_smul]
[GOAL]
M : Type u
α : Type v
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ (m * m') • a = a
[PROOFSTEP]
rw [← smul_smul, hb, ha]
[GOAL]
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1
[PROOFSTEP]
rw [Fintype.card_eq_one_iff, mem_fixedPoints]
[GOAL]
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ (∀ (m : M), m • a = a) ↔ ∃ x, ∀ (y : ↑(orbit M a)), y = x
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ (∀ (m : M), m • a = a) → ∃ x, ∀ (y : ↑(orbit M a)), y = x
[PROOFSTEP]
exact fun h => ⟨⟨a, mem_orbit_self _⟩, fun ⟨a, ⟨x, hx⟩⟩ => Subtype.eq <| by simp [h x, hx.symm]⟩
[GOAL]
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a✝ : α
inst✝ : Fintype ↑(orbit M a✝)
h : ∀ (m : M), m • a✝ = a✝
x✝ : ↑(orbit M a✝)
a : α
x : M
hx : (fun m => m • a✝) x = a
⊢ ↑{ val := a, property := (_ : ∃ y, (fun m => m • a✝) y = a) } = ↑{ val := a✝, property := (_ : a✝ ∈ orbit M a✝) }
[PROOFSTEP]
simp [h x, hx.symm]
[GOAL]
case mpr
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ (∃ x, ∀ (y : ↑(orbit M a)), y = x) → ∀ (m : M), m • a = a
[PROOFSTEP]
intro h x
[GOAL]
case mpr
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
h : ∃ x, ∀ (y : ↑(orbit M a)), y = x
x : M
⊢ x • a = a
[PROOFSTEP]
rcases h with ⟨⟨z, hz⟩, hz₁⟩
[GOAL]
case mpr.intro.mk
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
x : M
z : α
hz : z ∈ orbit M a
hz₁ : ∀ (y : ↑(orbit M a)), y = { val := z, property := hz }
⊢ x • a = a
[PROOFSTEP]
calc
  x • a = z := Subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
  _ = a := (Subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
src✝ : Submonoid G := Stabilizer.submonoid G a
m : G
ha : m • a = a
⊢ m⁻¹ • a = a
[PROOFSTEP]
rw [inv_smul_eq_iff, ha]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)
[PROOFSTEP]
rw [inv_smul_smul]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ∀ (x y : ↑(orbit G a)), ∃ g, g • x = y
[PROOFSTEP]
rintro ⟨_, g, rfl⟩ ⟨_, h, rfl⟩
[GOAL]
case mk.intro.mk.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g h : G
⊢ ∃ g_1,
    g_1 • { val := (fun m => m • a) g, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) g) } =
      { val := (fun m => m • a) h, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) h) }
[PROOFSTEP]
use h * g⁻¹
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g h : G
⊢ (h * g⁻¹) • { val := (fun m => m • a) g, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) g) } =
    { val := (fun m => m • a) h, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) h) }
[PROOFSTEP]
ext1
[GOAL]
case h.a
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g h : G
⊢ ↑((h * g⁻¹) • { val := (fun m => m • a) g, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) g) }) =
    ↑{ val := (fun m => m • a) h, property := (_ : ∃ y, (fun m => m • a) y = (fun m => m • a) h) }
[PROOFSTEP]
simp [mul_smul]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ a ∈ orbit G (g • a)
[PROOFSTEP]
simp only [orbit_smul, mem_orbit_self]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)
[PROOFSTEP]
simp only [orbit_smul, mem_orbit]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ a ∈ orbit G b → b ∈ orbit G a
[PROOFSTEP]
simp [orbit_eq_iff.symm, eq_comm]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ ∀ {z : α}, a ∈ orbit G b → b ∈ orbit G z → a ∈ orbit G z
[PROOFSTEP]
simp (config := { contextual := true }) [orbit_eq_iff.symm, eq_comm]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
letI := orbitRel G α
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
⊢ Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ f ⁻¹' (f '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
ext a
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) ↔ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' (f '' U) → a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
rintro ⟨b, hb, hab⟩
[GOAL]
case h.mp.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a b : α
hb : b ∈ U
hab : f b = f a
⊢ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
obtain ⟨g, rfl⟩ := Quotient.exact hab
[GOAL]
case h.mp.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
[PROOFSTEP]
rw [Set.mem_iUnion]
[GOAL]
case h.mp.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m => m • a) g ∈ U
hab : f ((fun m => m • a) g) = f a
⊢ ∃ i, a ∈ (fun x x_1 => x • x_1) i '' U
[PROOFSTEP]
exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
[GOAL]
case h.mpr
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U → a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : a ∈ ⋃ (g : G), (fun x x_1 => x • x_1) g '' U
⊢ a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
rw [Set.mem_iUnion] at hx 
[GOAL]
case h.mpr
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : ∃ i, a ∈ (fun x x_1 => x • x_1) i '' U
⊢ a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
obtain ⟨g, u, hu₁, hu₂⟩ := hx
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ a ∈ f ⁻¹' (f '' U)
[PROOFSTEP]
rw [Set.mem_preimage, Set.mem_image_iff_bex]
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ ∃ x x_1, f x = f a
[PROOFSTEP]
refine' ⟨g⁻¹ • a, _, by simp only [Quotient.eq']; use g⁻¹⟩
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ f (g⁻¹ • a) = f a
[PROOFSTEP]
simp only [Quotient.eq']
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ Setoid.r (g⁻¹ • a) a
[PROOFSTEP]
use g⁻¹
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ g⁻¹ • a ∈ U
[PROOFSTEP]
rw [← hu₂]
[GOAL]
case h.mpr.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ g⁻¹ • (fun x x_1 => x • x_1) g u ∈ U
[PROOFSTEP]
convert hu₁
[GOAL]
case h.e'_4
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x x_1 => x • x_1) g u = a
⊢ g⁻¹ • (fun x x_1 => x • x_1) g u = u
[PROOFSTEP]
simp only [inv_smul_smul]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
[PROOFSTEP]
letI := orbitRel G α
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
[PROOFSTEP]
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
[PROOFSTEP]
refine' ⟨fun h a a_in_U g g_in_V => h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, _⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, _⟩
[GOAL]
case refine'_1
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
a : α
a_in_U : a ∈ U
g : G
g_in_V : g • a ∈ V
⊢ (fun m => m • g • a) g⁻¹ = a
[PROOFSTEP]
simp
[GOAL]
case refine'_2
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ (∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V) → Disjoint (f '' U) (f '' V)
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
⊢ Disjoint (f '' U) (f '' V)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
case refine'_2
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
⊢ ∀ ⦃a : Quotient (orbitRel G α)⦄, a ∈ f '' U → ¬a ∈ f '' V
[PROOFSTEP]
rintro _ ⟨b, hb₁, hb₂⟩ ⟨c, hc₁, hc₂⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
a✝ : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a✝
c : α
hc₁ : c ∈ V
hc₂ : f c = a✝
⊢ False
[PROOFSTEP]
obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V
a✝ : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a✝
g : G
hc₁ : (fun m => m • b) g ∈ V
hc₂ : f ((fun m => m • b) g) = a✝
⊢ False
[PROOFSTEP]
exact h b hb₁ g hc₁
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
x : Quotient G α
⊢ a ∈ orbit x ↔ Quotient.mk'' a = x
[PROOFSTEP]
induction x using Quotient.inductionOn'
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' a = Quotient.mk'' a✝
[PROOFSTEP]
rw [Quotient.eq'']
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Setoid.r a a✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
⊢ orbit x = MulAction.orbit G (φ x)
[PROOFSTEP]
conv_lhs => rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
| orbit x
[PROOFSTEP]
rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
| orbit x
[PROOFSTEP]
rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : Function.RightInverse φ Quotient.mk'
| orbit x
[PROOFSTEP]
rw [← hφ x]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer G a)
[PROOFSTEP]
ext h
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer G a)
[PROOFSTEP]
rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul, mul_left_inv, one_smul, ←
  mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
[GOAL]
G : Type u
α : Type v
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : Setoid.Rel (orbitRel G α) a b
g : G := Classical.choose h
hg : g • b = a
⊢ stabilizer G a = Subgroup.map (MulEquiv.toMonoidHom (↑MulAut.conj g)) (stabilizer G b)
[PROOFSTEP]
rw [← hg, stabilizer_smul_eq_stabilizer_map_conj]
[GOAL]
G : Type u
α : Type v
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
⊢ stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer G a)
[PROOFSTEP]
ext h
[GOAL]
case h
G : Type u
α : Type v
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g +ᵥ a) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer G a)
[PROOFSTEP]
rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd, add_left_neg, zero_vadd, ←
  mem_stabilizer_iff, AddSubgroup.mem_map_equiv, AddAut.conj_symm_apply]
[GOAL]
G : Type u
α : Type v
inst✝¹ : AddGroup G
inst✝ : AddAction G α
a b : α
h : Setoid.Rel (orbitRel G α) a b
g : G := Classical.choose h
hg : g +ᵥ b = a
⊢ stabilizer G a = AddSubgroup.map (AddEquiv.toAddMonoidHom (↑AddAut.conj g)) (stabilizer G b)
[PROOFSTEP]
rw [← hg, stabilizer_vadd_eq_stabilizer_map_conj]
[GOAL]
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a = b
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a - b = 0
[PROOFSTEP]
refine' h _ _
[GOAL]
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ k • (a - b) = 0
[PROOFSTEP]
rw [smul_sub, h', sub_self]
