mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
]

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : x * y = p * z
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : x * y = p * z
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd ∈ s
⊢ hd * L.prod = hd * L.prod

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u v : Mˣ
⊢ x * (↑u * ↑v) = x * (↑u * ↑v)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x * f ↑u = f x * f ↑u

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a = b

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a = b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Tactic:
]

Goal state after:
N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b

Tactic:
]

Goal state after:
N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case e'_3
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a * a ^ n = a * a ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case e'_4
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ b * b ^ n = b * b ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ -L.prod = -L.prod

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c = a * c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
a : M
u : Mˣ
⊢ a = 0 ↔ a = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_1.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ y * z ~ᵤ y

Tactic:
]

Goal state after:
case mp.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ y * z ~ᵤ y
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd ∈ s
⊢ hd * -L.prod = hd * -L.prod

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsRight M₀ = nonZeroDivisorsRight M₀

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ M₀⁰ = M₀⁰

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (x : M₀), r * x = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsRight M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsRight M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ L.prod = L.prod

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₁ ^ k₁

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₁ ^ k₁
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r x : M₀
hr : r ∈ M₀⁰
⊢ x = 0 ↔ x = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀ ∧ b ∈ nonZeroDivisorsRight M₀

Tactic:
]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀ ∧ b ∈ nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x✝¹ x✝ : M
⊢ x✝¹ = x✝ ↔ x✝¹ = x✝

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ~ᵤ q ↔ p ~ᵤ q

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Associates M
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk a = Associates.mk a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ IsUnit a ↔ IsUnit a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a' b' c' : Associates M
a b c : M
⊢ ⟦a * (b * c)⟧ = ⟦a * (b * c)⟧

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a' b' : Associates M
a b : M
⊢ ⟦b * a⟧ = ⟦b * a⟧

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : Associates M
⊢ a = 1 ↔ a = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ a ~ᵤ 1 ↔ a ~ᵤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ b = a * ⟨c, ⋯⟩

Tactic:
simp_rw [Subtype.ext_iff, Submonoid.coe_mul, hc]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0

Tactic:
]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0

Tactic:
]

Goal state after:
case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
]

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp.mk.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0

Tactic:
]

Goal state after:
case mp.mk.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})

Tactic:
]

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ b ≠ 0

Tactic:
]

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ b ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk 0 = Associates.mk 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' ⇑f ⁻¹' {0}) ≤ map f s

Tactic:
]

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' ⇑f ⁻¹' {0}) ≤ map f s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ ⇑f '' ⇑f ⁻¹' {0} ⊆ ↑(map f s)

Tactic:
]

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ ⇑f '' ⇑f ⁻¹' {0} ⊆ ↑(map f s)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : M) (b : Associates M),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : M) (b : Associates M),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ ⇑f ⁻¹' {0} ⊆ ↑s

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ ⇑f ⁻¹' {0} ⊆ ↑s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = ↑k * g

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a✝ : Associates M
a : M
ha : Quot.mk (⇑(Associated.setoid M)) a ≠ 0
a₁✝ : Associates M
b : M
a₂✝ : Associates M
c : M
h :
  (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) b) =
    (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) c)
u : Mˣ
hu : (fun x1 x2 ↦ x1 * x2) a b * ↑u = (fun x1 x2 ↦ x1 * x2) a c
⊢ a * b * ↑u = a * c

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a✝ : Associates M
a : M
ha : Quot.mk (⇑(Associated.setoid M)) a ≠ 0
a₁✝ : Associates M
b : M
a₂✝ : Associates M
c : M
h :
  (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) b) =
    (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) c)
u : Mˣ
hu : (fun x1 x2 ↦ x1 * x2) a b * ↑u = (fun x1 x2 ↦ x1 * x2) a c
⊢ a * b * ↑u = a * c
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective ⇑f ↔ Surjective ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c : Associates M
ha : a ≠ 0
d : Associates M
hd : a * c = a * b * d
⊢ a * c = a * b * d

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c : Associates M
ha : a ≠ 0
d : Associates M
hd : a * c = a * b * d
⊢ a * c = a * b * d
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
⊢ p = ⊥ ↔ p = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ q * ↑u = q * ↑u

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = r

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * b * ↑a = p

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * b * ↑a = p
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
]

Goal state after:
case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i