awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : α
h : ∃ (i : Ω), x ∈ i.orbit
⊢ Membership.mem (γ := Set α) Set.univ x ↔ Membership.mem (γ := Set α) (⋃ (x : Ω), x.orbit) x

Tactic:
simp only [Set.mem_univ, Set.mem_iUnion, true_iff]

Premises used: Set.mem_iUnion, true_iff, Set.mem_univ
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : α
⊢ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : α
⊢ ∃ (i : Ω), x ∈ i.orbit

Tactic:
exact ⟨Quotient.mk'' x, by simp⟩
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
m : G
ha : m • a = a
rw : a = m • a
rw₁ rw₂ : a = a
⊢ m⁻¹ • a = a

Tactic:
rw [inv_smul_eq_iff, ha]

Premises used: inv_smul_eq_iff
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) g ↔ g • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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 : β
simp_rw : ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b
⊢ LE.le (α := Subgroup G) (stabilizer G a) (stabilizer G (a • b))

Tactic:
simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]

Premises used: smul_assoc, SetLike.le_def, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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_1 : α
b : β
a : G
h : a • a_1 = a_1
rw rw₁ : a_1 • b = a_1 • b
⊢ (a • a_1) • b = a_1 • b

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
α : Type u_2
β : Type u_3
G' : Type u_4
inst : Group G'
inst_1 : SMul α β
inst_2 : MulAction G' β
inst_3 : SMulCommClass G' α β
a : α
b : β
simp_rw : ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b
⊢ LE.le (α := Subgroup G') (stabilizer G' b) (stabilizer G' (a • b))

Tactic:
simp_rw [SetLike.le_def, mem_stabilizer_iff, smul_comm]

Premises used: SetLike.le_def, MulAction.mem_stabilizer_iff, SMulCommClass.smul_comm
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
α : Type u_2
β : Type u_3
G' : Type u_4
inst : Group G'
inst_1 : SMul α β
inst_2 : MulAction G' β
inst_3 : SMulCommClass G' α β
a_1 : α
b : β
a : G'
h : a • b = b
rw rw₁ : a_1 • b = a_1 • b
⊢ a_1 • a • b = a_1 • b

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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)

Tactic:
(le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_

Premises used: LE.le.antisymm', MulAction.le_stabilizer_smul_left
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
refine :
  ∀ (a_1 : G) (ha : Membership.mem (γ := Subgroup G) (stabilizer G (a • b)) a_1),
    Membership.mem (γ := Subgroup G) (stabilizer G a) a_1
⊢ Eq (α := Subgroup G) (stabilizer G (a • b)) (stabilizer G a)

Tactic:
refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_

Premises used: LE.le.antisymm', MulAction.le_stabilizer_smul_left
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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_1 : α
b : β
h : Injective.{u_2 + 1, u_3 + 1} (β := β) fun (x : α) ↦ x • b
a : G
ha : Membership.mem (γ := Subgroup G) (stabilizer G (a_1 • b)) a
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a_1) a

Tactic:
simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha

Premises used: smul_assoc, Function.Injective.eq_iff, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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 : β
rw rw₁ : Eq (α := Subgroup G) (stabilizer G b) (stabilizer G b)
⊢ Eq (α := Subgroup G) (stabilizer G (a⁻¹ • a • b)) (stabilizer G b)

Tactic:
rw [inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Group α
inst_3 : IsScalarTower G α α
a b : α
⊢ Eq (α := Subgroup G) (stabilizer G (a * b)) (stabilizer G a)

Tactic:
stabilizer_smul_eq_left a _ <| mul_left_injective _

Premises used: MulAction.stabilizer_smul_eq_left, mul_left_injective
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Group α
inst_3 : SMulCommClass G α α
a b : α
⊢ Eq (α := Subgroup G) (stabilizer G (a * b)) (stabilizer G b)

Tactic:
stabilizer_smul_eq_right a _

Premises used: MulAction.stabilizer_smul_eq_right
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
Goal:
M : Type u_1
α : Type u_2
N : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMulCommClass M N α
inst_3 : SMul N β
M' : Type u_5
inst_4 : SMul M' α
inst_5 : SMulCommClass M' N α
inst_6 : SMulCommClass M M' α
⊢ SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (MulActionHom.{u_3, u_3, u_2, u_4} (M := N) id α β)

Tactic:
DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Premises used: Function.Injective.smulCommClass, DFunLike.coe_injective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
Goal:
M : Type u_1
α : Type u_2
N : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMulCommClass M N α
inst_3 : SMul N β
c : Mᵈᵐᵃ
f : MulActionHom.{u_3, u_3, u_2, u_4} (M := N) id α β
a : α
⊢ Eq.{u_4 + 1} (α := β) ((c • f : (a : α) → β) a : β)
    ((f : (a : α) → β) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) a) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
Goal:
M : Type u_1
α : Type u_2
N : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMulCommClass M N α
inst_3 : SMul N β
c : M
f : MulActionHom.{u_3, u_3, u_2, u_4} (M := N) id α β
a : α
⊢ Eq.{u_4 + 1} (α := β) ((HSMul.hSMul (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) f : (a : α) → β) a : β)
    ((f : (a : α) → β) (c • a) : β)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : Monoid N
inst_3 : AddMonoid B
inst_4 : DistribMulAction N A
inst_5 : SMulCommClass M N A
inst_6 : DistribMulAction N B
M' : Type u_5
inst_7 : DistribSMul M' A
inst_8 : SMulCommClass M' N A
inst_9 : SMulCommClass M M' A
⊢ SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+[N] B)

Tactic:
DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Premises used: Function.Injective.smulCommClass, DFunLike.coe_injective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : Monoid N
inst_3 : AddMonoid B
inst_4 : DistribMulAction N A
inst_5 : SMulCommClass M N A
inst_6 : DistribMulAction N B
c : Mᵈᵐᵃ
f : A →+[N] B
a : A
⊢ Eq.{u_4 + 1} (α := B) ((c • f : (a : A) → B) a : B)
    ((f : (a : A) → B) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) a) : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : Monoid N
inst_3 : AddMonoid B
inst_4 : DistribMulAction N A
inst_5 : SMulCommClass M N A
inst_6 : DistribMulAction N B
c : M
f : A →+[N] B
a : A
⊢ Eq.{u_4 + 1} (α := B) ((HSMul.hSMul (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) f : (a : A) → B) a : B)
    ((f : (a : A) → B) (c • a) : B)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : One M
⊢ Eq.{u_1 + 1} (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) 1 : Mᵈᵐᵃ) (1 : Mᵈᵐᵃ)

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : One M
⊢ Eq.{u_1 + 1} (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) 1 : M) (1 : M)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : Mul M
a b : M
⊢ (mk : (a : M) → Mᵈᵐᵃ) (a * b) =
    HMul.hMul (α := Mᵈᵐᵃ) (β := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) b : Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) a : Mᵈᵐᵃ)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : Mul M
a b : Mᵈᵐᵃ
⊢ (Equiv.symm mk : (a : Mᵈᵐᵃ) → M) (a * b) =
    HMul.hMul (α := M) (β := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) b : M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) a : M)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : Inv M
a : M
⊢ Eq (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) a⁻¹ : Mᵈᵐᵃ) (((mk : (a : M) → Mᵈᵐᵃ) a)⁻¹ : Mᵈᵐᵃ)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : Inv M
a : Mᵈᵐᵃ
⊢ Eq (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) a⁻¹ : M) (((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) a)⁻¹ : M)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : Monoid M
a : M
n : ℕ
⊢ (mk : (a : M) → Mᵈᵐᵃ) (a ^ n) = HPow.hPow (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) a : Mᵈᵐᵃ) n

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : Monoid M
a : Mᵈᵐᵃ
n : ℕ
⊢ (Equiv.symm mk : (a : Mᵈᵐᵃ) → M) (a ^ n) = HPow.hPow (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) a : M) n

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : DivInvMonoid M
a : M
n : ℤ
⊢ (mk : (a : M) → Mᵈᵐᵃ) (a ^ n) = HPow.hPow (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) a : Mᵈᵐᵃ) n

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
inst : DivInvMonoid M
a : Mᵈᵐᵃ
n : ℤ
⊢ (Equiv.symm mk : (a : Mᵈᵐᵃ) → M) (a ^ n) = HPow.hPow (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) a : M) n

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_1
β : Type u_2
α : Type u_3
inst : SMul M α
c : Mᵈᵐᵃ
f : α → β
a : α
⊢ (c • f) a = f (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
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 : α
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
⊢ 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⟩

Premises used: exists_pair_ne
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
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
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
⊢ 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:
contrapose! hne
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
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
haveI : ∀ (this : DecidableEq α), x = y
⊢ x = y

Tactic:
haveI := Classical.decEq α
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
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 α
⊢ (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
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
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ᵈᵐᵃ
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 α
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
⊢ x = y

Tactic:
simpa [smul_apply, hne] using h

Premises used: DomMulAct.smul_apply
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M_1 : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
M : Type u_5
M' : Type u_6
A : Type u_7
B : Type u_8
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
inst_3 : MulOneClass B
inst_4 : Monoid M'
inst_5 : MulDistribMulAction M' A
inst_6 : SMulCommClass M M' A
⊢ SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →* B)

Tactic:
DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Premises used: Function.Injective.smulCommClass, DFunLike.coe_injective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_5
A : Type u_7
B : Type u_8
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
inst_3 : MulOneClass B
c : Mᵈᵐᵃ
f : A →* B
a : A
⊢ Eq.{u_8 + 1} (α := B) ((c • f : (a : A) → B) a : B)
    ((f : (a : A) → B) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) a) : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M : Type u_5
A : Type u_7
B : Type u_8
inst : Monoid M
inst_1 : Monoid A
inst_2 : MulDistribMulAction M A
inst_3 : MulOneClass B
c : M
f : A →* B
a : A
⊢ Eq.{u_8 + 1} (α := B) ((HSMul.hSMul (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) f : (a : A) → B) a : B)
    ((f : (a : A) → B) (c • a) : B)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M_1 : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
A : Type u_5
B : Type u_6
M : Type u_7
M' : Type u_8
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
inst_3 : DistribSMul M' A
inst_4 : SMulCommClass M M' A
⊢ SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+ B)

Tactic:
DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Premises used: Function.Injective.smulCommClass, DFunLike.coe_injective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
M_1 : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
A : Type u_5
B : Type u_6
M : Type u_7
M' : Type u_8
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
inst_3 : DistribSMul M' B
⊢ SMulCommClass Mᵈᵐᵃ M' (A →+ B)

Tactic:
DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Premises used: Function.Injective.smulCommClass, DFunLike.coe_injective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
A : Type u_5
B : Type u_6
M : Type u_7
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
c : Mᵈᵐᵃ
f : A →+ B
a : A
⊢ Eq.{u_6 + 1} (α := B) ((c • f : (a : A) → B) a : B)
    ((f : (a : A) → B) (HSMul.hSMul (α := M) ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) c : M) a) : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
A : Type u_5
B : Type u_6
M : Type u_7
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
c : M
f : A →+ B
a : A
⊢ Eq.{u_6 + 1} (α := B) ((HSMul.hSMul (α := Mᵈᵐᵃ) ((mk : (a : M) → Mᵈᵐᵃ) c : Mᵈᵐᵃ) f : (a : A) → B) a : B)
    ((f : (a : A) → B) (c • a) : B)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic
Goal:
A : Type u_5
B : Type u_6
M : Type u_7
inst : AddMonoid A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
c : Mᵈᵐᵃ
f : A →+ B
⊢ (⇑(c • f) : (a : A) → B) = HSMul.hSMul (β := (a : A) → B) c (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Embedding
Goal:
G : Type u_1
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : MulAction G β
g : G
f : α ↪ β
⊢ g • f = f.trans (Equiv.toEmbedding (MulAction.toPerm g))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Embedding
Goal:
G : Type u_1
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : MulAction G β
g : G
f : α ↪ β
a : α
⊢ (g • f : (a : α) → β) a = HSMul.hSMul (β := β) g ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Embedding
Goal:
G : Type u_1
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : MulAction G β
g : G
f : α ↪ β
⊢ (⇑(g • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) g (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Embedding
Goal:
G : Type u_1
G' : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : SMul G G'
inst_3 : MulAction G β
inst_4 : MulAction G' β
inst_5 : IsScalarTower G G' β
⊢ IsScalarTower G G' (α ↪ β)

Tactic:
⟨fun x y z => Function.Embedding.ext fun i => smul_assoc x y (z i)⟩

Premises used: smul_assoc, Function.Embedding.ext, IsScalarTower.mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.Embedding
Goal:
G : Type u_1
G' : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : MulAction G β
inst_3 : MulAction G' β
inst_4 : SMulCommClass G G' β
⊢ SMulCommClass G G' (α ↪ β)

Tactic:
⟨fun x y z => Function.Embedding.ext fun i => smul_comm x y (z i)⟩

Premises used: Function.Embedding.ext, SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.Embedding
Goal:
G : Type u_1
G' : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : MulAction G β
inst_2 : MulAction.{u_1, u_4} Gᵐᵒᵖ β
inst_3 : IsCentralScalar G β
⊢ IsCentralScalar G (α ↪ β)

Tactic:
⟨fun _ _ => Function.Embedding.ext fun _ => op_smul_eq_smul _ _⟩

Premises used: IsCentralScalar.mk, Function.Embedding.ext, DFunLike.coe, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
h : ∀ (x : α), x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g
⊢ fixedBy α g⁻¹ = fixedBy α g

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
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
h₃ h₄ : g • x = x ↔ g • x = x
⊢ x ∈ fixedBy α g⁻¹ ↔ x ∈ fixedBy α g

Tactic:
rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]

Premises used: inv_smul_eq_iff, eq_comm, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
rw : g • a = a ↔ a ∈ fixedBy α g
⊢ g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
rw [mem_fixedBy, smul_left_cancel_iff]

Premises used: smul_left_cancel_iff, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
⊢ g • a = a ↔ a ∈ fixedBy α g

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
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⁻¹
rw₂ rw₃ : a ∈ fixedBy α g ↔ a ∈ fixedBy α g
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]

Premises used: MulAction.fixedBy_inv, MulAction.smul_mem_fixedBy_iff_mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
g : G
⊢ Function.minimalPeriod (fun (x : α) ↦ g • x) a = 1 ↔ a ∈ fixedBy α g

Tactic:
Function.minimalPeriod_eq_one_iff_isFixedPt

Premises used: Function.minimalPeriod_eq_one_iff_isFixedPt, Set.Mem, setOf, MulAction.fixedBy, Function.IsFixedPt
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
rw : 1 ∣ j
⊢ a ∈ fixedBy α (g ^ j)

Tactic:
rw [mem_fixedBy, zpow_smul_eq_iff_minimalPeriod_dvd, minimalPeriod_eq_one_iff_fixedBy.mpr h,
    Int.natCast_one]

Premises used: Iff.mpr, MulAction.minimalPeriod_eq_one_iff_fixedBy, MulAction.zpow_smul_eq_iff_minimalPeriod_dvd, Int.natCast_one, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ 1 ∣ j

Tactic:
one_dvd j

Premises used: one_dvd
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ 1 ∣ j

Tactic:
exact one_dvd j

Premises used: one_dvd
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
h : ∀ (j : ℤ), a ∈ fixedBy α (g ^ j)
⊢ a ∈ fixedBy α g

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
j : ℤ
⊢ fixedBy α g ⊆ fixedBy α (g ^ j)

Tactic:
fun _ h ↦ mem_fixedBy_zpow h j

Premises used: Set.Subset, MulAction.mem_fixedBy_zpow
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
⊢ fixedBy.{u_3, u_1} (M := M) α 1 = Set.univ

Tactic:
Set.eq_univ_iff_forall.mpr <| one_smul M

Premises used: Iff.mpr, Set.eq_univ_iff_forall, one_smul
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m₁ m₂ : M
a : α
this : ∀ (h₁ : a ∈ fixedBy α m₁) (h₂ : a ∈ fixedBy α m₂), a ∈ fixedBy α (m₁ * m₂)
⊢ a ∈ fixedBy α m₁ ∩ fixedBy α m₂ → a ∈ fixedBy α (m₁ * m₂)

Tactic:
⟨h₁, h₂⟩
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
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
rw₃ rw₄ : a = a
⊢ a ∈ fixedBy α (m₁ * m₂)

Tactic:
rw [mem_fixedBy, mul_smul, h₂, h₁]

Premises used: SemigroupAction.mul_smul, MulAction.mem_fixedBy