case mp
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ → a ∈ M₁⁰ ∧ b ∈ M₁⁰

case mpr
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰ → a * b ∈ M₁⁰
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ ↔ a ∈ M₁⁰ ∧ b ∈ M₁⁰
constructor
case mp
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰
case mp
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ → a ∈ M₁⁰ ∧ b ∈ M₁⁰
intro h
case mp.left.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * a = 0
⊢ x * (a * b) = 0

case mp.right.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * b = 0
⊢ x * (a * b) = 0
case mp
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰
constructor <;> intro x h' <;> apply h
no goals
case mp.left.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * a = 0
⊢ x * (a * b) = 0
rw [← mul_assoc, h', zero_mul]
no goals
case mp.right.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * b = 0
⊢ x * (a * b) = 0
rw [mul_comm a b, ← mul_assoc, h', zero_mul]
case mpr.intro
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x = 0
case mpr
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰ → a * b ∈ M₁⁰
rintro ⟨ha, hb⟩ x hx
case mpr.intro.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a = 0
case mpr.intro
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x = 0
apply ha
case mpr.intro.a.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a * b = 0
case mpr.intro.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a = 0
apply hb
no goals
case mpr.intro.a.a
M : Type ?u.20654
M' : Type ?u.20657
M₁ : Type u_1
R : Type ?u.20663
R' : Type ?u.20666
F : Type ?u.20669
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a * b = 0
rw [mul_assoc, hx]