awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 y : ↥(inertia M I)),
    Equiv.toFun
        ((↑e : M ≃ N).subtypeEquiv (p := Membership.mem (γ := Subgroup M) (inertia M I)) (q :=
          Membership.mem (γ := Subgroup N) (inertia N I)) ⋯)
        (x * y) =
      HMul.hMul (α := ↥(inertia N I))
        (Equiv.toFun
          ((↑e : M ≃ N).subtypeEquiv (p := Membership.mem (γ := Subgroup M) (inertia M I)) (q :=
            Membership.mem (γ := Subgroup N) (inertia N I)) ⋯)
          x)
        (Equiv.toFun
          ((↑e : M ≃ N).subtypeEquiv (p := Membership.mem (γ := Subgroup M) (inertia M I)) (q :=
            Membership.mem (γ := Subgroup N) (inertia N I)) ⋯)
          y)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Pointwise
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
m : ↥(inertia M I)
x : R
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := ↥(inertia N I))
      ((I.inertiaEquiv e he : (a : ↥(inertia M I)) → ↥(inertia N I)) m : ↥(inertia N I)) x =
    m • x

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

Premises used: MulAction.subgroup_smul_def, Subtype.val, Ideal.inertiaEquiv
-- Module: Mathlib.RingTheory.Ideal.Pointwise
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
rw₂ 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
⊢ 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

Tactic:
rw [← (inertiaEquiv I e he).apply_symm_apply n, inertiaEquiv_apply_smul,
    (inertiaEquiv I e he).apply_symm_apply]

Premises used: Ideal.inertiaEquiv_apply_smul, Ideal.inertiaEquiv, MulEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Ideal.IsPrime.mk, Ideal.IsPrime.mem_or_mem', Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
⊢ I ≠ ⊤

Tactic:
hI.1

Premises used: Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsPrime
x : α
hx : IsUnit x
⊢ x ∉ I

Tactic:
fun h ↦ ‹I.IsPrime›.ne_top (eq_top_of_isUnit_mem _ h hx)

Premises used: Ideal.eq_top_of_isUnit_mem, Ideal.IsPrime.ne_top, Not
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
⊢ 1 ∉ I

Tactic:
notMem_of_isUnit _ isUnit_one

Premises used: Ideal.notMem_of_isUnit, isUnit_one
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
⊢ 1 ∉ I

Tactic:
hI.one_notMem

Premises used: Ideal.IsPrime.one_notMem
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
x y : α
⊢ x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
hI.2

Premises used: Ideal.IsPrime.mem_or_mem'
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
x y : α
⊢ x ∉ I → y ∉ I → x * y ∉ I

Tactic:
fun hx hy h ↦
  hy ((hI.mem_or_mem h).resolve_left hx)

Premises used: Or.resolve_left, Ideal.IsPrime.mem_or_mem, Not
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
x y : α
h : x * y = 0
⊢ x ∈ I ∨ y ∈ I

Tactic:
hI.mem_or_mem (h.symm ▸ I.zero_mem)

Premises used: Eq.rec, Ideal.IsPrime.mem_or_mem, Ideal.zero_mem, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : HPow.hPow (β := ℕ) r 0 ∈ I
⊢ 1 ∈ I

Tactic:
rw [pow_zero] at H

Premises used: pow_zero
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : 1 ∈ I
⊢ r ∈ I

Tactic:
hI.one_notMem.elim H

Premises used: Ideal.IsPrime.one_notMem, Not.elim
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : 1 ∈ I
⊢ r ∈ I

Tactic:
exact hI.one_notMem.elim H

Premises used: Ideal.IsPrime.one_notMem, Not.elim
-- Module: Mathlib.RingTheory.Ideal.Prime
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 ^ n * r ∈ I

Tactic:
rw [pow_succ] at H

Premises used: pow_succ
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : ∀ (H : r ^ n ∈ I), r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I

Tactic:
Or.casesOn (hI.mem_or_mem H) ih id

Premises used: Or.casesOn, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : ∀ (H : r ^ n ∈ I), r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I

Tactic:
exact Or.casesOn (hI.mem_or_mem H) ih id
-- Module: Mathlib.RingTheory.Ideal.Prime
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
succ : ∀ (n : ℕ) (ih : ∀ (H : r ^ n ∈ I), r ∈ I) (H : r ^ (n + 1) ∈ I), r ∈ 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

Premises used: pow_succ, pow_zero
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
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
⊢ ¬I.IsPrime ↔ 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]

Premises used: Classical.not_not, Ne, not_or, not_and_or, Ideal.isPrime_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ (x : α) (x_1 : α) (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔
    I = ⊤ ∨ ∃ (x : α) (_ : x ∉ I) (y : α) (_ : y ∉ I), x * y ∈ I

Tactic:
or_congr Iff.rfl
      ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ =>
        ⟨x, y, hxy, hx, hy⟩⟩

Premises used: or_congr, HMul.hMul, Iff.rfl, Membership.mem, Exists, _private.0.Ideal.not_isPrime_iff.match_6, And, And.intro, Iff.intro, Exists.intro, Not, _private.0.Ideal.not_isPrime_iff.match_5
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ (x : α) (x_1 : α) (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔
    I = ⊤ ∨ ∃ (x : α) (_ : x ∉ I) (y : α) (_ : y ∉ I), x * y ∈ I

Tactic:
exact
    or_congr Iff.rfl
      ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ =>
        ⟨x, y, hxy, hx, hy⟩⟩

Premises used: or_congr, Iff.rfl, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Prime
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : Eq.{u + 1} (α := α) 1 0), Eq.{u + 1} (α := α) 1 0
⊢ Eq.{u + 1} (α := α) 1 0

Tactic:
rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h

Premises used: Submodule.mem_bot, Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
x y : α
h : Membership.mem (γ := Ideal α) ⊥ (x * y)
⊢ x * y = 0

Tactic:
simpa only [Submodule.mem_bot] using h

Premises used: Submodule.mem_bot
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
⊢ IsPrime.{u} (α := α) ⊥

Tactic:
isPrime_bot

Premises used: Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
hI : I.IsPrime
x y : α
h : x ∈ I
⊢ x * y ∈ I

Tactic:
I.mul_mem_right y h

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
hI : I.IsPrime
x y : α
h : y ∈ I
⊢ x * y ∈ I

Tactic:
I.mul_mem_left x h

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
hI : I.IsPrime
x y : α
h : x ∈ I
⊢ x * y ∈ I

Tactic:
exacts [I.mul_mem_right y h, I.mul_mem_left x h]

Premises used: Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
hn : 0 < n
⊢ r ^ n ∈ I ↔ r ∈ I

Tactic:
⟨hI.mem_of_pow_mem n, fun hr => I.pow_mem_of_mem hr n hn⟩

Premises used: Ideal.IsPrime.mem_of_pow_mem, Ideal.pow_mem_of_mem, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
inst_2 : I.IsPrime
x y : α
hx : x ∉ I
⊢ x * y ∈ I ↔ y ∈ I

Tactic:
grind [Ideal.IsPrime.mul_mem_iff_mem_or_mem]

Premises used: Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
inst_2 : I.IsPrime
x y : α
hx : y ∉ I
rw : x ∈ I ∨ y ∈ I ↔ x ∈ I
hI : I.IsPrime
⊢ x * y ∈ I ↔ x ∈ I

Tactic:
rw [Ideal.IsPrime.mul_mem_iff_mem_or_mem]

Premises used: Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
inst_2 : I.IsPrime
x y : α
hx : y ∉ I
⊢ x ∈ I ∨ y ∈ I ↔ x ∈ I

Tactic:
aesop
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
inst_2 : I.IsPrime
x y : α
hx : y ∉ I
⊢ I.IsPrime

Tactic:
aesop
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
P : Ideal α
inst_1 : P.IsPrime
x : α
⊢ x ∈ P.primeCompl ↔ x ∉ P

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
h :
  ∀ (x : α),
    Membership.mem (γ := Submonoid α) (primeCompl ⊥) x ↔
      Membership.mem (γ := Submonoid α) (nonZeroDivisors α : Submonoid α) x
⊢ Eq.{u + 1} (α := Submonoid α) (primeCompl ⊥) (nonZeroDivisors α)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
α : Type u
inst : Semiring α
inst_1 : Nontrivial α
inst_2 : NoZeroDivisors α
x : α
⊢ Membership.mem (γ := Submonoid α) (primeCompl ⊥) x ↔
    Membership.mem (γ := Submonoid α) (nonZeroDivisors α : Submonoid α) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
A : Type u_1
inst : Ring A
hbp : Ideal.IsPrime.{u_1} (α := A) ⊥
⊢ IsDomain A

Tactic:
@NoZeroDivisors.to_isDomain A _ ⟨1, 0, fun h => hbp.one_notMem h⟩ ⟨fun h => hbp.2 h⟩

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.RingTheory.Ideal.Prime
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h : I.IsPrime
⊢ I = ⊥

Tactic:
or_iff_not_imp_right.mp I.eq_bot_or_top h.1

Premises used: Classical.or_iff_not_imp_right, Ideal.eq_bot_or_top, Iff.mp, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ (↑(I.prod J) : Set (R × S)) = (↑I : Set R) ×ˢ (↑J : Set S)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Set.preimage, rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R × S
⊢ x ∈ I.prod J ↔ x.1 ∈ I ∧ x.2 ∈ J

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
⊢ ∀ (x : R × S), Membership.mem (γ := Ideal (R × S)) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Ideal (R × S)) ⊤ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
⊢ Eq (α := Ideal (R × S)) (prod ⊥ ⊥) ⊥

Tactic:
SetLike.coe_injective <| Set.singleton_prod_singleton

Premises used: SetLike.coe_injective, Set.singleton_prod_singleton
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I₁ I₂ : Ideal R
J₁ J₂ : Ideal S
hI : I₁ ≤ I₂
hJ : J₁ ≤ J₂
⊢ I₁.prod J₁ ≤ I₂.prod J₂

Tactic:
Set.prod_mono hI hJ

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Set.Subset, Set.preimage, Set.prod_mono
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I₁ I₂ : Ideal R
J : Ideal S
hI : I₁ ≤ I₂
⊢ I₁.prod J ≤ I₂.prod J

Tactic:
Set.prod_mono_left hI

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Set.Subset, Set.prod_mono_left, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J₁ J₂ : Ideal S
hJ : J₁ ≤ J₂
⊢ I.prod J₁ ≤ I.prod J₂

Tactic:
Set.prod_mono_right hJ

Premises used: Set.prod_mono_right, Set.Mem, setOf, Set.prod, Set.inter, Set.Subset, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
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
⊢ I = prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)

Tactic:
apply Ideal.ext

Premises used: Ideal.ext
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
r : R
s : S
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
⊢ (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)

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]

Premises used: Prod.fst_surjective, RingHom.snd, Ideal.mem_map_iff_of_surjective, RingHom.fst, Prod.snd_surjective, Ideal.mem_prod
-- Module: Mathlib.RingTheory.Ideal.Prod
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

Tactic:
⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, ?_⟩

Premises used: Prod.mk, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
r : R
s : S
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
⊢ (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:
refine ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ Membership.mem (α := R × S) I
    (((RingHom.fst R S : (a : R × S) → R) (r, s'), (RingHom.snd R S : (a : R × S) → S) (r', s)) : R × S)

Tactic:
simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)

Premises used: Ideal.add_mem, Prod.mk, Ideal.mul_mem_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (I.prod J)) x ↔ x ∈ I
⊢ map (F := R × S →+* R) (RingHom.fst R S) (I.prod J) = I

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R
h : (∃ x_1 ∈ I.prod J, (RingHom.fst R S : (a : R × S) → R) x_1 = x) ↔ x ∈ I
⊢ Membership.mem (γ := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (I.prod J)) x ↔ x ∈ I

Tactic:
rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]

Premises used: Prod.fst_surjective, Ideal.mem_map_iff_of_surjective, RingHom.fst
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ Membership.mem (α := R) I ((RingHom.fst R S : (a : R × S) → R) x : R)

Tactic:
h.1

Premises used: Set.Mem, setOf, Set.preimage, And.left
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ Membership.mem (α := R) I ((RingHom.fst R S : (a : R × S) → R) x : R)

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S : (a : R × S) → R) x_1 = x) ↔ x ∈ I

Tactic:
exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
h : ∀ (x : S), Membership.mem (γ := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (I.prod J)) x ↔ x ∈ J
⊢ map (F := R × S →+* S) (RingHom.snd R S) (I.prod J) = J

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : S
h : (∃ x_1 ∈ I.prod J, (RingHom.snd R S : (a : R × S) → S) x_1 = x) ↔ x ∈ J
⊢ Membership.mem (γ := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (I.prod J)) x ↔ x ∈ J

Tactic:
rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]

Premises used: RingHom.snd, Ideal.mem_map_iff_of_surjective, Prod.snd_surjective
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ Membership.mem (α := S) J ((RingHom.snd R S : (a : R × S) → S) x : S)

Tactic:
h.2

Premises used: Set.Mem, setOf, And.right, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ Membership.mem (α := S) J ((RingHom.snd R S : (a : R × S) → S) x : S)

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S : (a : R × S) → S) x_1 = x) ↔ x ∈ J

Tactic:
exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
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 × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J) = J.prod I

Tactic:
Trans.trans (ideal_prod_eq _) ?_

Premises used: Trans.trans, Ideal.ideal_prod_eq
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
refine :
  prod
      (map (R := S × R) (F := S × R →+* S) (RingHom.fst S R)
        (map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J)))
      (map (R := S × R) (F := S × R →+* R) (RingHom.snd S R)
        (map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J))) =
    J.prod I
⊢ map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J) = J.prod I

Tactic:
refine Trans.trans (ideal_prod_eq _) ?_

Premises used: Trans.trans, Ideal.ideal_prod_eq
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ prod
      (map (R := S × R) (F := S × R →+* S) (RingHom.fst S R)
        (map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J)))
      (map (R := S × R) (F := S × R →+* R) (RingHom.snd S R)
        (map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J))) =
    J.prod I

Tactic:
simp [map_map]

Premises used: Ideal.map_map
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J_1 : Ideal S
x : Prod.{u, v} (Ideal R) (Ideal S)
I : Ideal R
J : Ideal S
⊢ (fun (I : Ideal (R × S)) ↦
        ((map (F := R × S →+* R) (RingHom.fst R S) I, map (F := R × S →+* S) (RingHom.snd R S) I) :
          Prod.{u, v} (Ideal R) (Ideal S)))
      ((fun (I : Prod.{u, v} (Ideal R) (Ideal S)) ↦ I.1.prod I.2) (I, J)) =
    (I, J)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J_1 : Ideal S
I J : Ideal (R × S)
⊢ LE.le.{u} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* R) (RingHom.fst R S) J) ∧
      LE.le.{v} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I)
        (map (F := R × S →+* S) (RingHom.snd R S) J) ↔
    I ≤ J

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩

Premises used: And.intro, Iff.intro, Ideal.map_mono
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J_1 : Ideal S
I J : Ideal (R × S)
refine :
  ∀
    (h :
      LE.le.{u} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I)
          (map (F := R × S →+* R) (RingHom.fst R S) J) ∧
        LE.le.{v} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I)
          (map (F := R × S →+* S) (RingHom.snd R S) J)),
    I ≤ J
⊢ LE.le.{u} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* R) (RingHom.fst R S) J) ∧
      LE.le.{v} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I)
        (map (F := R × S →+* S) (RingHom.snd R S) J) ↔
    I ≤ J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩