awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
inst_3 : SMul α β
inst_4 : IsScalarTower G α β
a : α
b : β
h : Injective.{u_2 + 1, u_3 + 1} (β := β) fun (x : α) ↦ x • b
⊢ Eq (α := Subgroup G) (stabilizer G (a • b)) (stabilizer G a)
have refine : ∀ (a_1 : G) (ha : Membership.mem (γ := Subgroup G) (stabilizer G (a • b)) a_1),
  Membership.mem (γ := Subgroup G) (stabilizer G a) a_1
Tactic: refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
β : Type u_3
inst : Group G
inst_1 : MulAction G β
α : Type u_4
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : SMulCommClass G α β
a : α
b : β
⊢ Eq (α := Subgroup G) (stabilizer G (a⁻¹ • a • b)) (stabilizer G b)
have rw : Eq (α := Subgroup G) (stabilizer G b) (stabilizer G b)
Tactic: rw [inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.DomAct.Basic (goal)
Goal:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst : SMul M α
inst_1 : FaithfulSMul M α
inst_2 : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₁ : M) a =
    HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a
have rcases : ∀ (x y : β) (hne : x ≠ y),
  HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₁ : M) a =
    HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a
Tactic: rcases exists_pair_ne β with ⟨x, y, hne⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.DomAct.Basic (goal)
Goal:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst : SMul M α
inst_1 : FaithfulSMul M α
inst_2 : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : x ≠ y
⊢ HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₁ : M) a =
    HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a
have contrapose! : ∀
  (hne :
    HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₁ : M) a ≠
      HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a),
  x = y
Tactic: contrapose! hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.DomAct.Basic (goal)
Goal:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst : SMul M α
inst_1 : FaithfulSMul M α
inst_2 : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne :
  HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₁ : M) a ≠
    HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a
⊢ x = y
have haveI : ∀ (this : DecidableEq α), x = y
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.DomAct.Basic (hypothesis)
Goal:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst : SMul M α
inst_1 : FaithfulSMul M α
inst_2 : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne :
  HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₁ : M) a ≠
    HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a
this : DecidableEq α
⊢ x = y
have h₁ : (c₁ • update (β := fun (a : α) ↦ β) (const α x) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a) y)
    a =
  (c₂ • update (β := fun (a : α) ↦ β) (const α x) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c₂ : M) a) y)
    a
Tactic: replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
⊢ fixedBy α g⁻¹ = fixedBy α g
have h : ∀ (x : α), x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : α
⊢ x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g
have h : g⁻¹ • x = x ↔ x ∈ fixedBy α g
Tactic: rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : α
h : g⁻¹ • x = x ↔ x ∈ fixedBy α g
⊢ x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g
have h₁ : g⁻¹ • x = x ↔ g • x = x
Tactic: rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : α
h : g⁻¹ • x = x ↔ x ∈ fixedBy α g
h₁ : g⁻¹ • x = x ↔ g • x = x
⊢ x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g
have h₂ : x = g • x ↔ g • x = x
Tactic: rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : α
h : g⁻¹ • x = x ↔ x ∈ fixedBy α g
h₁ : g⁻¹ • x = x ↔ g • x = x
h₂ : x = g • x ↔ g • x = x
⊢ x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g
have h₃ : g • x = x ↔ g • x = x
Tactic: rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
⊢ g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
have rw : g • a = a ↔ a ∈ fixedBy α g
Tactic: rw [mem_fixedBy, smul_left_cancel_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
have rw : g⁻¹ • a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹
Tactic: rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
rw : g⁻¹ • a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
have rw₁ : a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹
Tactic: rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
rw : g⁻¹ • a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹
rw₁ : a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
have rw₂ : a ∈ fixedBy α g ↔ a ∈ fixedBy α g
Tactic: rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ a ∈ fixedBy α (g ^ j)
have rw : 1 ∣ j
Tactic: rw [mem_fixedBy, zpow_smul_eq_iff_minimalPeriod_dvd, minimalPeriod_eq_one_iff_fixedBy.mpr h,
    Int.natCast_one]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m₁ m₂ : M
a : α
⊢ a ∈ fixedBy α m₁ ∩ fixedBy α m₂ → a ∈ fixedBy α (m₁ * m₂)
have this : ∀ (h₁ : a ∈ fixedBy α m₁) (h₂ : a ∈ fixedBy α m₂), a ∈ fixedBy α (m₁ * m₂)
Tactic: ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ a ∈ fixedBy α (m₁ * m₂)
have rw : (m₁ * m₂) • a = a
Tactic: rw [mem_fixedBy, mul_smul, h₂, h₁]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
rw : (m₁ * m₂) • a = a
⊢ a ∈ fixedBy α (m₁ * m₂)
have rw₁ : m₁ • m₂ • a = a
Tactic: rw [mem_fixedBy, mul_smul, h₂, h₁]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
rw : (m₁ * m₂) • a = a
rw₁ : m₁ • m₂ • a = a
⊢ a ∈ fixedBy α (m₁ * m₂)
have rw₂ : m₁ • a = a
Tactic: rw [mem_fixedBy, mul_smul, h₂, h₁]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
rw : (m₁ * m₂) • a = a
rw₁ : m₁ • m₂ • a = a
rw₂ : m₁ • a = a
⊢ a ∈ fixedBy α (m₁ * m₂)
have rw₃ : a = a
Tactic: rw [mem_fixedBy, mul_smul, h₂, h₁]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
⊢ h • fixedBy α g = fixedBy α (h * g * h⁻¹)
have h₁ : ∀ (a : α), a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
a : α
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
have h₁ : h⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
Tactic: simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
a : α
h₁ : h⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
have h₂ : g • h⁻¹ • a = h⁻¹ • a ↔ (h * g * h⁻¹) • a = a
Tactic: simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
a : α
h₁ : h⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
h₂ : g • h⁻¹ • a = h⁻¹ • a ↔ (h * g * h⁻¹) • a = a
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
have h₃ : g • h⁻¹ • a = h⁻¹ • a ↔ h • g • h⁻¹ • a = a
Tactic: simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
have simp_rw : g • s = s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
Tactic: simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
simp_rw : g • s = s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
have simp_rw₁ : s = g⁻¹ • s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
Tactic: simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
simp_rw : g • s = s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
simp_rw₁ : s = g⁻¹ • s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
have simp_rw₂ : (∀ (x : α), x ∈ s ↔ x ∈ g⁻¹ • s) ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
Tactic: simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
simp_rw : g • s = s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
simp_rw₁ : s = g⁻¹ • s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
simp_rw₂ : (∀ (x : α), x ∈ s ↔ x ∈ g⁻¹ • s) ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
have simp_rw₃ : (∀ (x : α), x ∈ s ↔ g • x ∈ s) ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
Tactic: simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s
have rw : Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s
Tactic: rw [← fixedBy_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s
have h : ∀ (x : α), x ∈ g⁻¹ • s ↔ x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ x ∈ g⁻¹ • s ↔ x ∈ s
have h : g • x ∈ s ↔ x ∈ s
Tactic: rw [Set.mem_inv_smul_set_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s
have xs : ∀ (gxs : g • x ∈ s), x ∈ s
Tactic: refine ⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
gxs : g • x ∈ s
⊢ x ∈ s
have xs : ∀ (s_ss_fixedBy : s ⊆ fixedBy α g⁻¹) (x : α) (gxs : g • x ∈ s), x ∈ s
Tactic: rw [← fixedBy_inv] at s_ss_fixedBy
Cleared hypotheses: s_ss_fixedBy, x, gxs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
⊢ x ∈ s
have xs : ∀ (gxs : g⁻¹ • g • x ∈ s), x ∈ s
Tactic: rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs
Cleared hypotheses: gxs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
xs : ∀ (gxs : g⁻¹ • g • x ∈ s), x ∈ s
⊢ x ∈ s
have xs₁ : ∀ (gxs : x ∈ s), x ∈ s
Tactic: rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs
Cleared hypotheses: gxs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s
have rw : Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s
Tactic: rw [← fixedBy_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s
have h : ∀ (a : α), a ∈ g⁻¹ • s ↔ a ∈ s
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ a ∈ g⁻¹ • s ↔ a ∈ s
have h : g • a ∈ s ↔ a ∈ s
Tactic: rw [Set.mem_inv_smul_set_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ g • a ∈ s ↔ a ∈ s
have pos : a ∈ fixedBy α g → (g • a ∈ s ↔ a ∈ s)
Tactic: by_cases a ∈ fixedBy α g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
pos : a ∈ fixedBy α g → (g • a ∈ s ↔ a ∈ s)
⊢ g • a ∈ s ↔ a ∈ s
have neg : a ∉ fixedBy α g → (g • a ∈ s ↔ a ∈ s)
Tactic: by_cases a ∈ fixedBy α g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_fixed : a ∈ fixedBy α g
⊢ g • a ∈ s ↔ a ∈ s
have rw : a ∈ s ↔ a ∈ s
Tactic: rw [a_fixed]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
⊢ g • a ∈ s ↔ a ∈ s
have mp : g • a ∈ s → a ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
mp : g • a ∈ s → a ∈ s
⊢ g • a ∈ s ↔ a ∈ s
have mpr : a ∈ s → g • a ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : g • a ∈ s
⊢ a ∈ s
have mp : a ∈ (fixedBy α g)ᶜ
Tactic: apply s_subset
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : a ∈ s
⊢ g • a ∈ s
have mpr : g • a ∈ (fixedBy α g)ᶜ
Tactic: apply s_subset
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : a ∈ s
⊢ g • a ∈ (fixedBy α g)ᶜ
have mpr : g • a ∉ fixedBy α g
Tactic: rwa [Set.mem_compl_iff, smul_mem_fixedBy_iff_mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) h) (fixedBy α g)
have h₁ : ∀ (x : α), x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₃ : (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₃ : (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₄ : (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₃ : (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₄ : (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₅ : h⁻¹ • g • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₃ : (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₄ : (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₅ : h⁻¹ • g • x = h⁻¹ • x ↔ x ∈ fixedBy α g
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₆ : g • x = x ↔ x ∈ fixedBy α g
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₃ : (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₄ : (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₅ : h⁻¹ • g • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₆ : g • x = x ↔ x ∈ fixedBy α g
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
have h₇ : g • x = x ↔ g • x = x
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) h) (fixedBy α g)ᶜ
have rw : h • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
Tactic: rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
rw : h • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) h) (fixedBy α g)ᶜ
have rw₁ : (h • fixedBy α g)ᶜ = (fixedBy α g)ᶜ
Tactic: rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
rw : h • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
rw₁ : (h • fixedBy α g)ᶜ = (fixedBy α g)ᶜ
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) h) (fixedBy α g)ᶜ
have rw₂ : (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
Tactic: rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : FaithfulSMul M α
m : M
⊢ fixedBy α m = Set.univ ↔ m = 1
have rw : (∀ (x : α), x ∈ fixedBy α m) ↔
  Eq.{u_1 + 1} (α := α → α) (fun (x2 : α) ↦ m • x2) fun (x2 : α) ↦ HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x2
Tactic: rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.FixedPoints (goal)
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔
    Eq.{u_1 + 1} (α := α → α) (fun (x2 : α) ↦ m • x2) fun (x2 : α) ↦ HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x2
have simp_rw : (∀ (x : α), x ∈ fixedBy α m) ↔ ∀ (x : α), m • x = HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x
Tactic: simp_rw [funext_iff, one_smul, mem_fixedBy]