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

Goal state before:
pp: case inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a

pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a

Tactic:
·

Goal state after:
case inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr
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 : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod

Tactic:
HP

Goal state after:
case cons.inr
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 : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C (-L.prod)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
·

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl.inl
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
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inl.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inr.inl
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
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inr.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
·

Goal state after:
case cons.inl.inl
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
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
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 * tl.prod = hd * L.prod

Tactic:
HP

Goal state after:
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
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inr.inl
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
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inr.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
·

Goal state after:
case cons.inl.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
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
ha : x ~ᵤ y
⊢ f x ~ᵤ f y

Tactic:
obtain ⟨u, ha⟩ := ha
  exact ⟨Units.map f u, by rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]⟩

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
⊢ -tl.prod = -L.prod

Tactic:
HP

Goal state after:
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
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case pos
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c

pp: case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c

Tactic:
·

Goal state after:
case pos
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr.inl
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
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inr.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
·

Goal state after:
case cons.inr.inl
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
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Module: Mathlib.Algebra.GroupWithZero.Associated

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

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)

Tactic:
·

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
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

pp: case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
·

Goal state after:
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
Module: Mathlib.Algebra.GroupWithZero.Associated

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

Tactic:
·

Goal state after:
case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)
Module: Mathlib.Algebra.GroupWithZero.Associated

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

pp: case refine_2.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Tactic:
·

Goal state after:
case refine_2.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_2.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Tactic:
·

Goal state after:
case refine_2.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x → IsUnit y ∨ x ~ᵤ y

pp: case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x

Tactic:
·

Goal state after:
case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x → IsUnit y ∨ x ~ᵤ y
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case inl
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Subsingleton M₀
⊢ Submonoid.map f S ≤ M₀'⁰

pp: case inr
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Nontrivial M₀
⊢ Submonoid.map f S ≤ M₀'⁰

Tactic:
·

Goal state after:
case inl
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Subsingleton M₀
⊢ Submonoid.map f S ≤ M₀'⁰
Module: Mathlib.Algebra.GroupWithZero.Associated

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

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 ∨ x ~ᵤ y

Tactic:
·

Goal state after:
case mp.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit y
⊢ IsUnit y ∨ x ~ᵤ y
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 ∨ x ~ᵤ 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 ∨ x ~ᵤ y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x

Tactic:
·

Goal state after:
case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

pp: case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
·

Goal state after:
case mpr.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
·

Goal state after:
case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case inr
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Nontrivial M₀
⊢ Submonoid.map f S ≤ M₀'⁰

Tactic:
·

Goal state after:
case inr
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
h✝ : Nontrivial M₀
⊢ Submonoid.map f S ≤ M₀'⁰
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
·

Goal state after:
case cons.inr.inr
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, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
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
⊢ x * (a * b) = 0

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

Tactic:
·

Goal state after:
case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x * (a * b) = 0
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
⊢ x * (a * b) = 0

Tactic:
·

Goal state after:
case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 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
⊢ comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})

pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (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
⊢ comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) → ∃ c, b = a * c

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b

Tactic:
·

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) → ∃ c, b = a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b

Tactic:
·

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ x, x * a = 0 ∧ x ≠ 0

pp: case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * a = 0 ∧ x ≠ 0) → ∃ x, x * Associates.mk a = 0 ∧ x ≠ 0

Tactic:
·

Goal state after:
case mp
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ x, 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
⊢ x * a = 0

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
⊢ x ≠ 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
⊢ x * a = 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
⊢ 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
⊢ x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) →
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
intro h b c dvd

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂) →
    ∀ (a_2 a_3 : M), a ∣ a_2 * a_3 → ∃ x x_1, x ∣ a_2 ∧ x_1 ∣ a_3 ∧ Associates.mk a = Associates.mk (x * x_1)

Tactic:
intro h b c dvd

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)