awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ 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
have 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
Tactic: simp [pointwise_smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S
have rw : a⁻¹⁻¹ • x ∈ S ↔ a • x ∈ S
Tactic: rw [mem_pointwise_smul_iff_inv_smul_mem, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S
have rw₁ : a • x ∈ S ↔ a • x ∈ S
Tactic: rw [mem_pointwise_smul_iff_inv_smul_mem, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T
have rw : a⁻¹ • a • S ≤ a⁻¹ • T ↔ S ≤ a⁻¹ • T
Tactic: rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T
have rw₁ : S ≤ a⁻¹ • T ↔ S ≤ a⁻¹ • T
Tactic: rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T
have rw : a⁻¹ • S ≤ a⁻¹ • a • T ↔ a⁻¹ • S ≤ T
Tactic: rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T
have rw₁ : a⁻¹ • S ≤ T ↔ a⁻¹ • S ≤ T
Tactic: rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ (g • I).IsPrime
have 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)
Tactic: rw [I.pointwise_smul_eq_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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)
have refine : ∀ (σ : M) (hσ : Membership.mem (γ := Subgroup M) (inertia M P) σ) (x : R), x ∈ σ • P ↔ x ∈ P
Tactic: refine fun σ hσ ↦ SetLike.ext fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ x ∈ σ • P ↔ x ∈ P
have rw : σ⁻¹ • 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ x ∈ σ • P ↔ x ∈ P
have rw₁ : σ⁻¹ • x ∈ P ↔ x + (σ⁻¹ • x - 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ x ∈ σ • P ↔ x ∈ P
have rw₂ : σ⁻¹ • 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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))
have 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)
Tactic: refine (Subgroup.normal_subgroupOf_iff (inertia_le_stabilizer P)).mpr fun g s hg hs x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ Membership.mem (γ := AddSubgroup R) (Submodule.toAddSubgroup P) ((s * g * s⁻¹) • x - x)
have rw : g • s⁻¹ • x - s⁻¹ • x ∈ P
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ 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
have 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
Tactic: rw [← (stabilizerEquiv I e he).apply_symm_apply n, stabilizerEquiv_apply_smul,
    (stabilizerEquiv I e he).apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ 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
have 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
Tactic: rw [← (stabilizerEquiv I e he).apply_symm_apply n, stabilizerEquiv_apply_smul,
    (stabilizerEquiv I e he).apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
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
⊢ 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
have 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
Tactic: rw [← (stabilizerEquiv I e he).apply_symm_apply n, stabilizerEquiv_apply_smul,
    (stabilizerEquiv I e he).apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
Goal:
M : Type u_1
inst : Group M
N : Type u_3
inst_1 : Group N
R : Type u_4
inst_2 : Ring R
inst_3 : MulSemiringAction M R
inst_4 : 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
n : ↥(inertia N I)
x : R
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x =
    n • x
have rw : HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
    (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I))
        ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
          (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n)) :
      ↥(inertia M I))
    x =
  HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(inertia N I))
    ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
        (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n) :
      ↥(inertia N I))
    x
Tactic: rw [← (inertiaEquiv I e he).apply_symm_apply n, inertiaEquiv_apply_smul,
    (inertiaEquiv I e he).apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
Goal:
M : Type u_1
inst : Group M
N : Type u_3
inst_1 : Group N
R : Type u_4
inst_2 : Ring R
inst_3 : MulSemiringAction M R
inst_4 : 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
n : ↥(inertia N I)
x : R
rw :
  HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I))
          ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
            (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n)) :
        ↥(inertia M I))
      x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(inertia N I))
      ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
          (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n) :
        ↥(inertia N I))
      x
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x =
    n • x
have rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
    (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I))
        ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
          (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n)) :
      ↥(inertia M I))
    x =
  HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
    (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x
Tactic: rw [← (inertiaEquiv I e he).apply_symm_apply n, inertiaEquiv_apply_smul,
    (inertiaEquiv I e he).apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
Goal:
M : Type u_1
inst : Group M
N : Type u_3
inst_1 : Group N
R : Type u_4
inst_2 : Ring R
inst_3 : MulSemiringAction M R
inst_4 : 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
n : ↥(inertia N I)
x : R
rw :
  HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I))
          ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
            (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n)) :
        ↥(inertia M I))
      x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(inertia N I))
      ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
          (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n) :
        ↥(inertia N I))
      x
rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I))
          ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I))
            (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n)) :
        ↥(inertia M I))
      x =
    HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
      (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x =
    n • x
have rw₂ : HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
    (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x =
  HSMul.hSMul.{u_1, u_4, u_4} (α := ↥(inertia M I))
    (((I.inertiaEquiv e he).symm : (a : ↥(inertia N I)) → ↥(inertia M I)) n : ↥(inertia M I)) x
Tactic: rw [← (inertiaEquiv I e he).apply_symm_apply n, inertiaEquiv_apply_smul,
    (inertiaEquiv I e he).apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (hypothesis)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : HPow.hPow (β := ℕ) r 0 ∈ I
⊢ r ∈ I
have H₁ : 1 ∈ I
Tactic: rw [pow_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (hypothesis)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : ∀ (H : r ^ n ∈ I), r ∈ I
H : r ^ (n + 1) ∈ I
⊢ r ∈ I
have H₁ : r ^ n * r ∈ I
Tactic: rw [pow_succ] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
H : r ^ n ∈ I
⊢ r ∈ I
have zero : ∀ (H : HPow.hPow (β := ℕ) r 0 ∈ I), r ∈ I
Tactic: induction n with
  | zero =>
    rw [pow_zero] at H
    exact hI.one_notMem.elim H
  | succ n ih =>
    rw [pow_succ] at H
    exact Or.casesOn (hI.mem_or_mem H) ih id
Cleared hypotheses: n, H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
H : r ^ n ∈ I
zero : ∀ (H : HPow.hPow (β := ℕ) r 0 ∈ I), r ∈ I
⊢ r ∈ I
have succ : ∀ (n : ℕ) (ih : ∀ (H : r ^ n ∈ I), r ∈ I) (H : r ^ (n + 1) ∈ I), r ∈ I
Tactic: induction n with
  | zero =>
    rw [pow_zero] at H
    exact hI.one_notMem.elim H
  | succ n ih =>
    rw [pow_succ] at H
    exact Or.casesOn (hI.mem_or_mem H) ih id
Cleared hypotheses: n, H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ ¬I.IsPrime ↔ I = ⊤ ∨ ∃ (x : α) (_ : x ∉ I) (y : α) (_ : y ∉ I), x * y ∈ I
have simp_rw : (I = ⊤ ∨ ∃ (x : α) (x_1 : α) (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔
  I = ⊤ ∨ ∃ (x : α) (_ : x ∉ I) (y : α) (_ : y ∉ I), x * y ∈ I
Tactic: simp_rw [Ideal.isPrime_iff, not_and_or, Ne, Classical.not_not, not_forall, not_or]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
h : Eq.{u + 1} (α := Ideal α) ⊥ ⊤
⊢ Eq.{u + 1} (α := α) 1 0
have rwa : ∀ (h : Membership.mem (γ := Ideal α) ⊥ 1), Eq.{u + 1} (α := α) 1 0
Tactic: rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
h : Eq.{u + 1} (α := Ideal α) ⊥ ⊤
rwa : ∀ (h : Membership.mem (γ := Ideal α) ⊥ 1), Eq.{u + 1} (α := α) 1 0
⊢ Eq.{u + 1} (α := α) 1 0
have rwa₁ : ∀ (h : Eq.{u + 1} (α := α) 1 0), Eq.{u + 1} (α := α) 1 0
Tactic: rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
inst_2 : I.IsPrime
x y : α
hx : y ∉ I
⊢ x * y ∈ I ↔ x ∈ I
have rw : x ∈ I ∨ y ∈ I ↔ x ∈ I
Tactic: rw [Ideal.IsPrime.mul_mem_iff_mem_or_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prime (goal)
Goal:
α : Type u
inst : Semiring α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
⊢ Eq.{u + 1} (α := Submonoid α) (primeCompl ⊥) (nonZeroDivisors α)
have h : ∀ (x : α),
  Membership.mem (γ := Submonoid α) (primeCompl ⊥) x ↔
    Membership.mem (γ := Submonoid α) (nonZeroDivisors α : Submonoid α) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
⊢ I = prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)
have h : ∀ (x : R × S),
  x ∈ I ↔
    Membership.mem (γ := Ideal (R × S))
      (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) x
Tactic: apply Ideal.ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔
    Membership.mem (γ := Ideal (R × S))
      (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (r, s)
have h : (r, s) ∈ I ↔
  (∃ x ∈ I, (RingHom.fst R S : (a : R × S) → R) x = (r, s).1) ∧
    ∃ x ∈ I, (RingHom.snd R S : (a : R × S) → S) x = (r, s).2
Tactic: rw [mem_prod, mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective,
    mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔
    (∃ x ∈ I, (RingHom.fst R S : (a : R × S) → R) x = (r, s).1) ∧
      ∃ x ∈ I, (RingHom.snd R S : (a : R × S) → S) x = (r, s).2
have h : ((∃ x ∈ I, (RingHom.fst R S : (a : R × S) → R) x = (r, s).1) ∧
    ∃ x ∈ I, (RingHom.snd R S : (a : R × S) → S) x = (r, s).2) →
  (r, s) ∈ I
Tactic: refine ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ map (F := R × S →+* R) (RingHom.fst R S) (I.prod J) = I
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (I.prod J)) x ↔ x ∈ I
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ Membership.mem (γ := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (I.prod J)) x ↔ x ∈ I
have h : (∃ x_1 ∈ I.prod J, (RingHom.fst R S : (a : R × S) → R) x_1 = x) ↔ x ∈ I
Tactic: rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ map (F := R × S →+* S) (RingHom.snd R S) (I.prod J) = J
have h : ∀ (x : S), Membership.mem (γ := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (I.prod J)) x ↔ x ∈ J
Tactic: ext x