awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P_1 : Ideal B
Q : Ideal C
p_1 : Ideal A
inst_10 : Q.LiesOver p_1
inst_11 : P_1.LiesOver p_1
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
hIP : p ≤ comap (F := R →+* A) (algebraMap R A) P
hIP₁ hIP₂ : LE.le (α := Ideal R) (under R P) (under R P)
⊢ map (F := R →+* A) (algebraMap R A) p ≤ P

Tactic:
rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]

Premises used: Ideal.map_le_iff_le_comap, Ideal.LiesOver.over
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommSemiring A
p : Ideal A
B : Type u_3
inst_2 : Semiring B
inst_3 : Algebra A B
Q : (↑(p.primesOver B) : Type u_3)
⊢ (↑Q : Ideal B).IsPrime

Tactic:
Q.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommSemiring A
p : Ideal A
B : Type u_3
inst_2 : Semiring B
inst_3 : Algebra A B
Q : (↑(p.primesOver B) : Type u_3)
⊢ (↑Q : Ideal B).LiesOver p

Tactic:
Q.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : Nontrivial S
inst_5 : Module.IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P
⊢ P.LiesOver p

Tactic:
have : P.LiesOver p := hP.2
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : Nontrivial S
inst_5 : Module.IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P
this : P.LiesOver p
⊢ P ≠ ⊥

Tactic:
ne_bot_of_liesOver_of_ne_bot hp P

Premises used: Ideal.ne_bot_of_liesOver_of_ne_bot
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : Nontrivial S
inst_5 : Module.IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P
this : P.LiesOver p
⊢ P ≠ ⊥

Tactic:
exact ne_bot_of_liesOver_of_ne_bot hp P

Premises used: Ideal.ne_bot_of_liesOver_of_ne_bot
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Monoid M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : CommRing R
inst_4 : MulSemiringAction M R
a : M
simp : HSMul.hSMul (β := Ideal R) a ⊤ = ⊤
⊢ HSMul.hSMul (β := Ideal R) a 1 = 1

Tactic:
simp only [Ideal.one_eq_top]

Premises used: Ideal.one_eq_top
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Monoid M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : CommRing R
inst_4 : MulSemiringAction M R
a : M
⊢ HSMul.hSMul (β := Ideal R) a ⊤ = ⊤

Tactic:
Ideal.map_top _

Premises used: Ideal.map_top
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Monoid M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : CommRing R
inst_4 : MulSemiringAction M R
a : M
⊢ HSMul.hSMul (β := Ideal R) a ⊤ = ⊤

Tactic:
exact Ideal.map_top _

Premises used: Ideal.map_top
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
⊢ a • S = map (F := R →+* R) (MulSemiringAction.toRingHom M R a) S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
r : R
S : Ideal R
⊢ r ∈ S → m • r ∈ m • S

Tactic:
fun h => subset_span <| Set.smul_mem_smul_set h

Premises used: Ideal.subset_span, Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
⊢ CovariantClass M (Ideal R) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => map_mono⟩

Premises used: CovariantClass.mk, Ideal.map_mono
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
⊢ HSMul.hSMul (β := Ideal R) a ⊥ = ⊥

Tactic:
map_bot

Premises used: Ideal.map_bot
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Ideal R
⊢ a • (S ⊔ T) = a • S ⊔ a • T

Tactic:
map_sup _ _ _

Premises used: Set.Mem, setOf, Ideal.map_sup
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
s : Set R
⊢ HSMul.hSMul (β := Ideal R) a (span s) = span (a • s)

Tactic:
Ideal.map_span _ _

Premises used: Ideal.map_span
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
inst_3 : MulSemiringAction.{u_1, u_2} Mᵐᵒᵖ R
inst_4 : IsCentralScalar M R
⊢ IsCentralScalar.{u_1, u_2} M (Ideal R)

Tactic:
⟨fun _ S => (congr_arg fun f => S.map f) <| RingHom.ext <| op_smul_eq_smul _⟩

Premises used: Ideal.map, RingHom.ext, congr_arg, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
h : ∀ (x : R), x ∈ (a • S).toAddSubmonoid ↔ x ∈ a • S.toAddSubmonoid
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
x : R
⊢ Function.Surjective (α := R) (β := R) (⇑(MulSemiringAction.toRingHom M R a) : (a : R) → R)

Tactic:
ha
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
x : R
⊢ Function.Surjective (α := R) (β := R) (⇑(MulSemiringAction.toRingHom M R a) : (a : R) → R)

Tactic:
exact ha
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
x : R
⊢ x ∈ (a • S).toAddSubmonoid ↔ x ∈ a • S.toAddSubmonoid

Tactic:
exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

Premises used: Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Monoid M
R : Type u_3
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
h :
  ∀ (x : R),
    Membership.mem (γ := AddSubgroup R) (Submodule.toAddSubgroup (a • S)) x ↔
      x ∈ HSMul.hSMul (β := AddSubgroup R) a (Submodule.toAddSubgroup S)
⊢ Submodule.toAddSubgroup (a • S) = HSMul.hSMul (β := AddSubgroup R) a (Submodule.toAddSubgroup S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Monoid M
R : Type u_3
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
x : R
⊢ Function.Surjective (α := R) (β := R) (⇑(MulSemiringAction.toRingHom M R a) : (a : R) → R)

Tactic:
ha
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Monoid M
R : Type u_3
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
x : R
⊢ Function.Surjective (α := R) (β := R) (⇑(MulSemiringAction.toRingHom M R a) : (a : R) → R)

Tactic:
exact ha
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Monoid M
R : Type u_3
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
x : R
⊢ Membership.mem (γ := AddSubgroup R) (Submodule.toAddSubgroup (a • S)) x ↔
    x ∈ HSMul.hSMul (β := AddSubgroup R) a (Submodule.toAddSubgroup S)

Tactic:
exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

Premises used: Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
h :
  ∀ (x : R),
    x ∈ a • S ↔
      Membership.mem (γ := Ideal R)
        (comap (F := R ≃+* R)
          (RingEquiv.symm
            (((MulSemiringAction.toRingAut M R : MonoidHom.{u_1, u_2} M (RingAut R)) : (a : M) → RingAut R) a))
          S)
        x
⊢ a • S =
    comap (F := R ≃+* R)
      (RingEquiv.symm
        (((MulSemiringAction.toRingAut M R : MonoidHom.{u_1, u_2} M (RingAut R)) : (a : M) → RingAut R) a))
      S

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
x : R
h :
  Membership.mem (γ := Ideal R) (map (F := R →+* R) (MulSemiringAction.toRingHom M R a) S) x ↔
    Membership.mem (γ := Ideal R) (map (F := R ≃+* R) (MulSemiringAction.toRingEquiv M R a) S) x
⊢ x ∈ a • S ↔
    Membership.mem (γ := Ideal R)
      (comap (F := R ≃+* R)
        (RingEquiv.symm
          (((MulSemiringAction.toRingAut M R : MonoidHom.{u_1, u_2} M (RingAut R)) : (a : M) → RingAut R) a))
        S)
      x

Tactic:
simp [pointwise_smul_def]

Premises used: Ideal.pointwise_smul_def
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
x : R
⊢ Membership.mem (γ := Ideal R) (map (F := R →+* R) (MulSemiringAction.toRingHom M R a) S) x ↔
    Membership.mem (γ := Ideal R) (map (F := R ≃+* R) (MulSemiringAction.toRingEquiv M R a) S) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : a • x ∈ a • S
⊢ x ∈ S

Tactic:
simpa using smul_mem_pointwise_smul a⁻¹ _ _ h

Premises used: Inv.inv, Ideal.smul_mem_pointwise_smul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : x ∈ a • S
⊢ a⁻¹ • x ∈ S

Tactic:
simpa using smul_mem_pointwise_smul a⁻¹ _ _ h

Premises used: Inv.inv, Ideal.smul_mem_pointwise_smul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : a⁻¹ • x ∈ S
⊢ x ∈ a • S

Tactic:
simpa using smul_mem_pointwise_smul a _ _ h

Premises used: Ideal.smul_mem_pointwise_smul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
x : R
rw : a⁻¹⁻¹ • x ∈ S ↔ a • x ∈ S
rw₁ rw₂ : a • x ∈ S ↔ a • x ∈ S
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
rw [mem_pointwise_smul_iff_inv_smul_mem, inv_inv]

Premises used: Ideal.mem_pointwise_smul_iff_inv_smul_mem, inv_inv
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Ideal R
h : a • S ≤ a • T
⊢ S ≤ T

Tactic:
simpa using smul_mono_right a⁻¹ h

Premises used: smul_mono_right, Inv.inv
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Ideal R
rw : a⁻¹ • a • S ≤ a⁻¹ • T ↔ S ≤ a⁻¹ • T
rw₁ rw₂ : S ≤ a⁻¹ • T ↔ S ≤ a⁻¹ • T
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]

Premises used: inv_smul_smul, Ideal.pointwise_smul_le_pointwise_smul_iff
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Ideal R
rw : a⁻¹ • S ≤ a⁻¹ • a • T ↔ a⁻¹ • S ≤ T
rw₁ rw₂ : a⁻¹ • S ≤ T ↔ a⁻¹ • S ≤ T
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]

Premises used: inv_smul_smul, Ideal.pointwise_smul_le_pointwise_smul_iff
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
I : Ideal R
H : I.IsPrime
g : M
rw :
  IsPrime
    (Ideal.comap (F := R ≃+* R)
      (RingEquiv.symm
        (((MulSemiringAction.toRingAut M R : MonoidHom.{u_1, u_2} M (RingAut R)) : (a : M) → RingAut R) g))
      I)
⊢ (g • I).IsPrime

Tactic:
rw [I.pointwise_smul_eq_comap]

Premises used: Ideal.pointwise_smul_eq_comap
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
I : Ideal R
H : I.IsPrime
g : M
⊢ IsPrime
    (Ideal.comap (F := R ≃+* R)
      (RingEquiv.symm
        (((MulSemiringAction.toRingAut M R : MonoidHom.{u_1, u_2} M (RingAut R)) : (a : M) → RingAut R) g))
      I)

Tactic:
apply H.comap

Premises used: Ideal.IsPrime.comap
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
I : Ideal R
g : M
⊢ (g • I).IsPrime ↔ I.IsPrime

Tactic:
⟨fun H ↦ inv_smul_smul g I ▸ H.smul g⁻¹, fun H ↦ H.smul g⟩

Premises used: Eq.rec, inv_smul_smul, Inv.inv, Ideal.IsPrime.smul, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Group M
R : Type u_3
inst_1 : Ring R
P : Ideal R
inst_2 : MulSemiringAction M R
⊢ LE.le (α := Subgroup M) (inertia M P) (MulAction.stabilizer M P)

Tactic:
fun σ hσ ↦ SetLike.ext fun x ↦ ?_

Premises used: Set.Mem, setOf, SetLike.ext
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Group M
R : Type u_3
inst_1 : Ring R
P : Ideal R
inst_2 : MulSemiringAction M R
refine : ∀ (σ : M) (hσ : Membership.mem (γ := Subgroup M) (inertia M P) σ) (x : R), x ∈ σ • P ↔ x ∈ P
⊢ LE.le (α := Subgroup M) (inertia M P) (MulAction.stabilizer M P)

Tactic:
refine fun σ hσ ↦ SetLike.ext fun x ↦ ?_

Premises used: SetLike.ext
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
inst : Group M
R : Type u_3
inst_1 : Ring R
P : Ideal R
inst_2 : MulSemiringAction M R
σ : M
hσ : Membership.mem (γ := Subgroup M) (inertia M P) σ
x : R
rw : σ⁻¹ • x ∈ P ↔ x ∈ P
rw₁ : σ⁻¹ • x ∈ P ↔ x + (σ⁻¹ • x - x) ∈ P
rw₂ rw₃ : σ⁻¹ • x ∈ P ↔ σ⁻¹ • x ∈ P
⊢ x ∈ σ • P ↔ x ∈ P

Tactic:
rw [Ideal.mem_pointwise_smul_iff_inv_smul_mem,
    ← P.add_mem_iff_left (a := x) ((inv_mem hσ) x), add_sub_cancel]

Premises used: Ideal.mem_pointwise_smul_iff_inv_smul_mem, InvMemClass.inv_mem, add_sub_cancel, Ideal.add_mem_iff_left
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Group M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : Ring R
P : Ideal R
inst_4 : MulSemiringAction M R
⊢ Subgroup.Normal (G := ↥(MulAction.stabilizer M P)) (Subgroup.subgroupOf (inertia M P) (MulAction.stabilizer M P))

Tactic:
(Subgroup.normal_subgroupOf_iff (inertia_le_stabilizer P)).mpr fun g s hg hs x ↦ ?_

Premises used: Iff.mpr, Subgroup.normal_subgroupOf_iff, Ideal.inertia_le_stabilizer
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Group M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : Ring R
P : Ideal R
inst_4 : MulSemiringAction M R
refine :
  ∀ (g s : M) (hg : Membership.mem (γ := Subgroup M) (inertia M P) g)
    (hs : Membership.mem (γ := Subgroup M) (MulAction.stabilizer M P) s) (x : R),
    Membership.mem (γ := AddSubgroup R) (Submodule.toAddSubgroup P) ((s * g * s⁻¹) • x - x)
⊢ Subgroup.Normal (G := ↥(MulAction.stabilizer M P)) (Subgroup.subgroupOf (inertia M P) (MulAction.stabilizer M P))

Tactic:
refine (Subgroup.normal_subgroupOf_iff (inertia_le_stabilizer P)).mpr fun g s hg hs x ↦ ?_

Premises used: Iff.mpr, Subgroup.normal_subgroupOf_iff, Ideal.inertia_le_stabilizer
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Group M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : Ring R
P : Ideal R
inst_4 : MulSemiringAction M R
g s : M
hg : Membership.mem (γ := Subgroup M) (inertia M P) g
hs : Membership.mem (γ := Subgroup M) (MulAction.stabilizer M P) s
x : R
rw : g • s⁻¹ • x - s⁻¹ • x ∈ P
⊢ Membership.mem (γ := AddSubgroup R) (Submodule.toAddSubgroup P) ((s * g * s⁻¹) • x - x)

Tactic:
rw [Submodule.mem_toAddSubgroup, ← Ideal.smul_mem_pointwise_smul_iff (a := s⁻¹), smul_sub,
    smul_smul, ← mul_assoc, inv_mul_cancel_left, mul_smul, Subgroup.inv_mem _ hs]

Premises used: inv_mul_cancel_left, mul_assoc, smul_smul, Submodule.mem_toAddSubgroup, smul_sub, Subgroup.inv_mem, Ideal.smul_mem_pointwise_smul_iff, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Group M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : Ring R
P : Ideal R
inst_4 : MulSemiringAction M R
g s : M
hg : Membership.mem (γ := Subgroup M) (inertia M P) g
hs : Membership.mem (γ := Subgroup M) (MulAction.stabilizer M P) s
x : R
⊢ g • s⁻¹ • x - s⁻¹ • x ∈ P

Tactic:
hg (s⁻¹ • x)

Premises used: Set.Mem, Inv.inv, HSMul.hSMul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Group M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : Ring R
P : Ideal R
inst_4 : MulSemiringAction M R
g s : M
hg : Membership.mem (γ := Subgroup M) (inertia M P) g
hs : Membership.mem (γ := Subgroup M) (MulAction.stabilizer M P) s
x : R
⊢ g • s⁻¹ • x - s⁻¹ • x ∈ P

Tactic:
exact hg (s⁻¹ • x)

Premises used: Inv.inv, HSMul.hSMul
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
N : Type u_3
inst_3 : Group N
inst_4 : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), HSMul.hSMul.{u_3, u_2, u_2} (α := N) ((e : (a : M) → N) m : N) x = m • x
x : M
⊢ Membership.mem (γ := Subgroup M) (MulAction.stabilizer M I) x ↔
    Membership.mem (α := N) (γ := Subgroup N) (MulAction.stabilizer N I) (((↑e : M ≃ N) : (a : M) → N) x : N)

Tactic:
simp [Ideal.ext_iff, Ideal.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, he]

Premises used: Ideal.mem_pointwise_smul_iff_inv_smul_mem, map_inv, Ideal.ext_iff
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
N : Type u_3
inst_3 : Group N
inst_4 : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), HSMul.hSMul.{u_3, u_2, u_2} (α := N) ((e : (a : M) → N) m : N) x = m • x
x x_1 : ↥(MulAction.stabilizer M I)
⊢ Equiv.toFun
      ((↑e : M ≃ N).subtypeEquiv (p := Membership.mem (γ := Subgroup M) (MulAction.stabilizer M I)) (q :=
        Membership.mem (γ := Subgroup N) (MulAction.stabilizer N I)) ⋯)
      (x * x_1) =
    HMul.hMul (α := ↥(MulAction.stabilizer N I))
      (Equiv.toFun
        ((↑e : M ≃ N).subtypeEquiv (p := Membership.mem (γ := Subgroup M) (MulAction.stabilizer M I)) (q :=
          Membership.mem (γ := Subgroup N) (MulAction.stabilizer N I)) ⋯)
        x)
      (Equiv.toFun
        ((↑e : M ≃ N).subtypeEquiv (p := Membership.mem (γ := Subgroup M) (MulAction.stabilizer M I)) (q :=
          Membership.mem (γ := Subgroup N) (MulAction.stabilizer N I)) ⋯)
        x_1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
N : Type u_3
inst_3 : Group N
inst_4 : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), HSMul.hSMul.{u_3, u_2, u_2} (α := N) ((e : (a : M) → N) m : N) x = m • x
m : ↥(MulAction.stabilizer M I)
x : R
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := ↥(MulAction.stabilizer N I))
      ((I.stabilizerEquiv e he : (a : ↥(MulAction.stabilizer M I)) → ↥(MulAction.stabilizer N I)) m :
        ↥(MulAction.stabilizer N I))
      x =
    m • x

Tactic:
simp [stabilizerEquiv, MulAction.subgroup_smul_def, ← he m x]

Premises used: MulAction.subgroup_smul_def, Subtype.val, Ideal.stabilizerEquiv
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
N : Type u_3
inst_3 : Group N
inst_4 : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), HSMul.hSMul.{u_3, u_2, u_2} (α := N) ((e : (a : M) → N) m : N) x = m • x
n : ↥(MulAction.stabilizer N I)
x : R
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(MulAction.stabilizer M I))
      (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I))
          ((I.stabilizerEquiv e he : (a : ↥(MulAction.stabilizer M I)) → ↥(MulAction.stabilizer N I))
            (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n)) :
        ↥(MulAction.stabilizer M I))
      x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := ↥(MulAction.stabilizer N I))
      ((I.stabilizerEquiv e he : (a : ↥(MulAction.stabilizer M I)) → ↥(MulAction.stabilizer N I))
          (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n) :
        ↥(MulAction.stabilizer N I))
      x
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(MulAction.stabilizer M I))
      (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I))
          ((I.stabilizerEquiv e he : (a : ↥(MulAction.stabilizer M I)) → ↥(MulAction.stabilizer N I))
            (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n)) :
        ↥(MulAction.stabilizer M I))
      x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(MulAction.stabilizer M I))
      (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n :
        ↥(MulAction.stabilizer M I))
      x
rw₂ rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(MulAction.stabilizer M I))
      (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n :
        ↥(MulAction.stabilizer M I))
      x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(MulAction.stabilizer M I))
      (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n :
        ↥(MulAction.stabilizer M I))
      x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(MulAction.stabilizer M I))
      (((I.stabilizerEquiv e he).symm : (a : ↥(MulAction.stabilizer N I)) → ↥(MulAction.stabilizer M I)) n :
        ↥(MulAction.stabilizer M I))
      x =
    n • x

Tactic:
rw [← (stabilizerEquiv I e he).apply_symm_apply n, stabilizerEquiv_apply_smul,
    (stabilizerEquiv I e he).apply_symm_apply]

Premises used: Ideal.stabilizerEquiv, Ideal.stabilizerEquiv_apply_smul, MulEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.Ideal.Pointwise
Goal:
M : Type u_1
R_1 : Type u_2
inst : Group M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
N : Type u_3
inst_3 : Group N
inst_4 : MulSemiringAction N R_1
R : Type u_4
inst_5 : Ring R
inst_6 : MulSemiringAction M R
inst_7 : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), HSMul.hSMul.{u_3, u_4, u_4} (α := N) ((e : (a : M) → N) m : N) x = m • x
x : M
⊢ Membership.mem (γ := Subgroup M) (inertia M I) x ↔
    Membership.mem (α := N) (γ := Subgroup N) (inertia N I) (((↑e : M ≃ N) : (a : M) → N) x : N)

Tactic:
simp [he]