awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
inst_1 : SMul α G
inst_2 : SMulCommClass α G G
inst_3 : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
rw :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    ug • a • g
rw₁ :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) (a • g))
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
rw₂ :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    HMul.hMul (β := G) (a • HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
⊢ a • ug • g = ug • a • g
have rw₃ : a •
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
  a •
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
⊢ fixedPoints (ConjAct G) G = (↑(center G) : Set G)
have h : ∀ (x : G), x ∈ fixedPoints (ConjAct G) G ↔ x ∈ (↑(center G) : Set G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ g ∈ orbit (ConjAct G) h ↔ IsConj g h
have rw : (∃ (x : ConjAct G), x • h = g) ↔ ∃ (c : G), c * h * c⁻¹ = g
Tactic: rw [isConj_comm, isConj_iff, mem_orbit_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ (orbitRel (ConjAct G) G : G → G → Prop) g h = IsConj g h
have rw : (g ∈ orbit (ConjAct G) h) = IsConj g h
Tactic: rw [orbitRel_apply, mem_orbit_conjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
rw : (g ∈ orbit (ConjAct G) h) = IsConj g h
⊢ (orbitRel (ConjAct G) G : G → G → Prop) g h = IsConj g h
have rw₁ : IsConj g h = IsConj g h
Tactic: rw [orbitRel_apply, mem_orbit_conjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g : G
⊢ orbit (ConjAct G) g = ConjClasses.carrier (ConjClasses.mk g)
have h : ∀ (h : G), h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)
Tactic: ext h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)
have h₁ : h ∈ orbit (ConjAct G) g ↔ Eq (α := ConjClasses G) (ConjClasses.mk h) (ConjClasses.mk g)
Tactic: rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
h₁ : h ∈ orbit (ConjAct G) g ↔ Eq (α := ConjClasses G) (ConjClasses.mk h) (ConjClasses.mk g)
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)
have h₂ : h ∈ orbit (ConjAct G) g ↔ IsConj h g
Tactic: rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
h₁ : h ∈ orbit (ConjAct G) g ↔ Eq (α := ConjClasses G) (ConjClasses.mk h) (ConjClasses.mk g)
h₂ : h ∈ orbit (ConjAct G) g ↔ IsConj h g
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ ConjClasses.carrier (ConjClasses.mk g)
have h₃ : IsConj h g ↔ IsConj h g
Tactic: rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g : G
⊢ Eq (α := Subgroup G) (centralizer {g}) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g))
have h : ∀ (k : G),
  Membership.mem (γ := Subgroup G) (centralizer {g}) k ↔
    Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
Tactic: ext k
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g k : G
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) k ↔
    Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
have h : g * k = k * g ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
Tactic: simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g k : G
⊢ g * k = k * g ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
have h : k * g = g * k ↔ Membership.mem (γ := Subgroup G) (comap (MulEquiv.toMonoidHom toConjAct) (stabilizer (ConjAct G) g)) k
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
⊢ (↑((MulEquiv.symm ((MulAut.conjNormal : (a : G) → MulAut ↥H) g) : (a : ↥H) → ↥H) h) : G) = g⁻¹ * (↑h : G) * g
have change : HMul.hMul (β := G)
    (HMul.hMul (α := G)
      ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) : G)
      (↑h : G))
    (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹⁻¹ : G) =
  g⁻¹ * (↑h : G) * g
Tactic: change _ * _⁻¹⁻¹ = _
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
h : ↥H
⊢ HMul.hMul (β := G)
      (HMul.hMul (α := G)
        ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) :
          G)
        (↑h : G))
      (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹⁻¹ : G) =
    g⁻¹ * (↑h : G) * g
have rw : HMul.hMul (β := G)
    (HMul.hMul (α := G)
      ((ofConjAct : (a : ConjAct G) → G) (((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g)⁻¹ : ConjAct G) : G)
      (↑h : G))
    ((MulEquiv.toMonoidHom toConjAct : (a : G) → ConjAct G) g : ConjAct G) =
  g⁻¹ * (↑h : G) * g
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
a : G
ha : a ∈ map H.subtype K
b : G
⊢ b * a * b⁻¹ ∈ map H.subtype K
have obtain : ∀ (a : ↥H) (ha : a ∈ (↑K : Set ↥H)), HMul.hMul (β := G) b ((H.subtype : (a : ↥H) → G) a : G) * b⁻¹ ∈ map H.subtype K
Tactic: obtain ⟨a, ha, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (hypothesis)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
⊢ (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
have this : (↑u : ConjAct Mˣ) • x = x
Tactic: have : (u : ConjAct Mˣ) • x = x := u.2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : (↑u : ConjAct Mˣ) • x = x
⊢ (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
have rwa : ∀
  (this :
    HMul.hMul (β := Mˣ) (HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x)
        (((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ))⁻¹ : Mˣ) =
      x),
  (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
Tactic: rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : (↑u : ConjAct Mˣ) • x = x
rwa :
  ∀
    (this :
      HMul.hMul (β := Mˣ) (HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x)
          (((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ))⁻¹ : Mˣ) =
        x),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
⊢ (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
have rwa₁ : ∀
  (this :
    HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x =
      HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)),
  (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
Tactic: rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : (↑u : ConjAct Mˣ) • x = x
rwa :
  ∀
    (this :
      HMul.hMul (β := Mˣ) (HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x)
          (((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ))⁻¹ : Mˣ) =
        x),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x =
        HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
⊢ (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
have rwa₂ : ∀
  (this :
    (↑(HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x) : M) =
      (↑(HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)) : M)),
  (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
Tactic: rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : (↑u : ConjAct Mˣ) • x = x
rwa :
  ∀
    (this :
      HMul.hMul (β := Mˣ) (HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x)
          (((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ))⁻¹ : Mˣ) =
        x),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x =
        HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
rwa₂ :
  ∀
    (this :
      (↑(HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x) : M) =
        (↑(HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)) : M)),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
⊢ (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
have rwa₃ : ∀
  (this :
    (↑(HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)) : M) =
      (↑(HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x) : M)),
  (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
Tactic: rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {(↑x : M)}))ˣ
⊢ HSMul.hSMul (α := ConjAct Mˣ)
      ((ConjAct.toConjAct : (a : Mˣ) → ConjAct Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
              (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
            u) :
        ConjAct Mˣ)
      x =
    x
have simp : HMul.hMul (α := Mˣ)
    ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
          (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
        u :
      Mˣ)
    x =
  HMul.hMul (β := Mˣ) x
    ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
          (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
        u :
      Mˣ)
Tactic: simp only [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : α
m : M
h : a₂ ∈ orbit M a₁
⊢ m • a₂ ∈ orbit M a₁
have obtain : ∀ (x : M) (h : x • a₁ ∈ orbit M a₁), m • x • a₁ ∈ orbit M a₁
Tactic: obtain ⟨x, rfl⟩ := mem_orbit_iff.mp h
Cleared hypotheses: a₂, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u_1
γ : Type u_2
α : Type u_3
inst : SMul γ α
inst_1 : Monoid M
inst_2 : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ (m * m') • a = a
have rw : m • m' • a = a
Tactic: rw [← smul_smul, hb, ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u_1
γ : Type u_2
α : Type u_3
inst : SMul γ α
inst_1 : Monoid M
inst_2 : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
rw : m • m' • a = a
rw₁ : m • a = a
⊢ (m * m') • a = a
have rw₂ : a = a
Tactic: rw [← smul_smul, hb, ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
⊢ x • (a * b) = a * b
have rw : x • a * x • b = a * b
Tactic: rw [smul_mul', ha, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
rw : x • a * x • b = a * b
⊢ x • (a * b) = a * b
have rw₁ : a * x • b = a * b
Tactic: rw [smul_mul', ha, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
rw : x • a * x • b = a * b
rw₁ : a * x • b = a * b
⊢ x • (a * b) = a * b
have rw₂ : a * b = a * b
Tactic: rw [smul_mul', ha, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction M α
x : α
ha : x ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (submonoid M α))
x_1 : M
⊢ x_1 • x⁻¹ = x⁻¹
have rw : (x_1 • x)⁻¹ = x⁻¹
Tactic: rw [smul_inv', ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction M α
x : α
ha : x ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (submonoid M α))
x_1 : M
rw : (x_1 • x)⁻¹ = x⁻¹
⊢ x_1 • x⁻¹ = x⁻¹
have rw₁ : x⁻¹ = x⁻¹
Tactic: rw [smul_inv', ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)
have rw : orbit G a = orbit G a
Tactic: rw [inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a₁ a₂ : α
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁
have simp_rw : orbit G a₁ = orbit G a₂ ↔ orbit G a₂ = orbit G a₁
Tactic: simp_rw [← orbit_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : α
a b : (↑(orbit G x) : Type u_2)
⊢ a ∈ orbit.{u_1, u_2} (↥H) b ↔ (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
have refine_1 : ∀ (h : a ∈ orbit.{u_1, u_2} (↥H) b), (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : α
a b : (↑(orbit G x) : Type u_2)
refine_1 : ∀ (h : a ∈ orbit.{u_1, u_2} (↥H) b), (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
⊢ a ∈ orbit.{u_1, u_2} (↥H) b ↔ (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
have refine_2 : ∀ (h : (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)), a ∈ orbit.{u_1, u_2} (↥H) b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : α
a b : (↑(orbit G x) : Type u_2)
h : a ∈ orbit.{u_1, u_2} (↥H) b
⊢ (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
have refine_1 : ∀ (g : ↥H), (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
Tactic: rcases h with ⟨g, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : α
a b : (↑(orbit G x) : Type u_2)
h : (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
⊢ a ∈ orbit.{u_1, u_2} (↥H) b
have refine_2 : ∀ (g : ↥H) (h : (fun (m : ↥H) ↦ m • (↑b : α)) g = (↑a : α)), a ∈ orbit.{u_1, u_2} (↥H) b
Tactic: rcases h with ⟨g, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : α
a b : (↑(orbit G x) : Type u_2)
g : ↥H
h : g • (↑b : α) = (↑a : α)
⊢ a ∈ orbit.{u_1, u_2} (↥H) b
have h₁ : (↑g : G) • b = a
Tactic: rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : α
a b : (↑(orbit G x) : Type u_2)
g : ↥H
h : (↑g : G) • b = a
⊢ a ∈ orbit.{u_1, u_2} (↥H) b
have refine_2 : (↑g : G) • b ∈ orbit.{u_1, u_2} (↥H) b
Tactic: subst h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ f ⁻¹' f '' U = ⋃ (g : G), (fun (x : α) ↦ g • x) '' U
have h : ∀ (a : α), a ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
have h : a ∈ f ⁻¹' f '' U → Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
h : a ∈ f ⁻¹' f '' U → Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
⊢ a ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
have h₁ : Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a → a ∈ f ⁻¹' f '' U
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a b : α
hb : b ∈ U
hab : f b = f a
⊢ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
have h : ∀ (g : G) (hb : (fun (m : G) ↦ m • a) g ∈ U) (hab : f ((fun (m : G) ↦ m • a) g) = f a),
  Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
Tactic: obtain ⟨g, rfl⟩ := Quotient.exact hab
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun (m : G) ↦ m • a) g ∈ U
hab : f ((fun (m : G) ↦ m • a) g) = f a
⊢ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
have h : ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a
Tactic: rw [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
⊢ a ∈ f ⁻¹' f '' U
have hx₁ : ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a
Tactic: rw [Set.mem_iUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
hx : ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a
⊢ a ∈ f ⁻¹' f '' U
have h : ∀ (g : G) (u : α) (hu₁ : u ∈ U) (hu₂ : (fun (x : α) ↦ g • x) u = a), a ∈ f ⁻¹' f '' U
Tactic: obtain ⟨g, u, hu₁, hu₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun (x : α) ↦ g • x) u = a
⊢ ∃ x ∈ U, f x = f a
have h : g⁻¹ • a ∈ U
Tactic: refine ⟨g⁻¹ • a, ?_, by simp +instances [f, orbitRel, Quotient.eq']⟩