α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ (∀ (x : α), x • a = a) ↔ ∃ x, ∀ (y : ↑(orbit α a)), y = x
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ a ∈ fixedPoints α β ↔ Fintype.card ↑(orbit α a) = 1
rw [Fintype.card_eq_one_iff, mem_fixedPoints]
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ (∀ (x : α), x • a = a) → ∃ x, ∀ (y : ↑(orbit α a)), y = x

case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ (∃ x, ∀ (y : ↑(orbit α a)), y = x) → ∀ (x : α), x • a = a
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ (∀ (x : α), x • a = a) ↔ ∃ x, ∀ (y : ↑(orbit α a)), y = x
constructor
no goals
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ (∀ (x : α), x • a = a) → ∃ x, ∀ (y : ↑(orbit α a)), y = x
exact fun h => ⟨⟨a, mem_orbit_self _⟩, fun ⟨b, ⟨x, hx⟩⟩ => Subtype.eq <| by simp [h x, hx.symm]⟩
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
h : ∀ (x : α), x • a = a
x✝ : ↑(orbit α a)
b : β
x : α
hx : (fun x => x • a) x = b
⊢ ↑{ val := b, property := (_ : ∃ y, (fun x => x • a) y = b) } = ↑{ val := a, property := (_ : a ∈ orbit α a) }
simp [h x, hx.symm]
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
h : ∃ x, ∀ (y : ↑(orbit α a)), y = x
x : α
⊢ x • a = a
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
⊢ (∃ x, ∀ (y : ↑(orbit α a)), y = x) → ∀ (x : α), x • a = a
intro h x
case mpr.intro.mk
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
x : α
z : β
hz : z ∈ orbit α a
hz₁ : ∀ (y : ↑(orbit α a)), y = { val := z, property := hz }
⊢ x • a = a
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
h : ∃ x, ∀ (y : ↑(orbit α a)), y = x
x : α
⊢ x • a = a
rcases h with ⟨⟨z, hz⟩, hz₁⟩
no goals
case mpr.intro.mk
α : Type u
β : Type v
γ : Type w
inst✝² : Monoid α
inst✝¹ : MulAction α β
a : β
inst✝ : Fintype ↑(orbit α a)
x : α
z : β
hz : z ∈ orbit α a
hz₁ : ∀ (y : ↑(orbit α a)), y = { val := z, property := hz }
⊢ x • a = a
calc
  x • a = z := Subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
  _ = a := (Subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm