mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
⊢ Associates.mk (if x✝ = 1 then 1 else Quotient.out x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
⊢ (if 1 = 1 then 1 else Quotient.out 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
⊢ NormalizationMonoid α

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I + J = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝ : CommMonoidWithZero α
normUnit : α → αˣ
normUnit_zero : normUnit 0 = 1
normUnit_one : normUnit 1 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units : ∀ (u : αˣ), normUnit ↑u = u⁻¹
a : α
u : αˣ
ha : a ≠ 0
⊢ normUnit (a * ↑u) = u⁻¹ * normUnit a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
⊢ normUnit ↑u = u⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
⊢ normalize ↑u = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ x = 0 → normalize x = 0

Tactic:
rintro rfl; exact normalize_zero

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ x = 0 → normalize x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ Ideal.span {a} ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : DivisionMonoid α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : IsUnit a
⊢ (↑a)⁻¹ ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : Group α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : ↑a ≠ 0
⊢ IsUnit a ↔ (↑a)⁻¹ ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ a ∈ nonunits ↥S ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ normalize (normalize x) = normalize x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I ⊔ J = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
u : αˣ
a✝ : Nontrivial α
⊢ a = 0 → normalize a = normalize (a * ↑u)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : ↑a ≠ 0
⊢ a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
⊢ Associated a b → normalize a = normalize b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
h : Associated a b
ha : normalize a = a
hb : normalize b = b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ IsCoprime I J

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
⊢ (s.gcd fun j ↦ f j / s.gcd f) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : IsLeftCancelMulZero α
x y : α
⊢ normalize x = normalize y ↔ x ∣ y ∧ y ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : Associates α
⊢ ∀ (a : α), Associates.out ⟦a⟧ = 0 ↔ ⟦a⟧ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ Associates.out 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), a ∣ Associates.out ⟦a_1⟧ ↔ Associates.mk a ≤ ⟦a_1⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), Associates.out ⟦a_1⟧ ∣ a ↔ ⟦a_1⟧ ≤ Associates.mk a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (GCDMonoid.gcd (s.gcd g) a) (f b) = GCDMonoid.gcd a (GCDMonoid.gcd (g b) (s.gcd g))

Tactic:
gcd_assoc,

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd a (GCDMonoid.gcd (g b) (s.gcd g))
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
a b : Associates α
x✝¹ x✝ : α
⊢ (⟦x✝¹⟧ * ⟦x✝⟧).out = Associates.out ⟦x✝¹⟧ * Associates.out ⟦x✝⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
⊢ GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ s.gcd f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ gcd a b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
ha : a ≠ 0
⊢ gcd a b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hb : b ≠ 0
⊢ gcd a b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd 1 a) 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd a 1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
⊢ a = 0 → gcd (a * b) (a * c) = normalize a * gcd b c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : gcd (a * b) (a * c) = normalize (a * gcd b c)
⊢ gcd (a * b) (a * c) = normalize a * gcd b c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp1 : (↑s).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ ∀ j ∈ s, IsCoprime (J a) (J j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
⊢ gcd (b * a) (c * a) = gcd b c * normalize a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ Associated (gcd (b * a) (c * a)) (gcd b c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ gcd a b = b ↔ b ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd (k * m) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd (m * k) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd m (k * n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd m (n * k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ m * gcd k n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s).Pairwise (IsCoprime on J)
⊢ ∏ i ∈ s, J i = ⨅ i ∈ s, J i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical = I ↔ I.IsRadical

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
n : α
a✝ : GCDMonoid α
H : 0 ∣ 0 * n
⊢ 0 = 0 * n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
⊢ Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
h : IsGCDMonoid α
k m n : α
H : k ∣ m * n
⊢ ∃ a₁ a₂, a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ (I ⊓ J).IsRadical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ⊥.IsRadical ↔ IsReduced R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
⊢ ⊥.IsRadical

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n : α
⊢ gcd k (m * n) ∣ gcd k m * gcd k n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ (s.inf f).radical = (f i).radical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd (d₁ ^ k) b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
x : R
hxm : x ∉ m
hrmx : r ∉ (m ⊔ span {x}).radical
⊢ x ∈ m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ d₁ ^ k ∣ a * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
⊢ m ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ (factors a).prod ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ c ∣ a * b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
⊢ {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ (i ::ₘ s).prod ~ᵤ i * a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
h : f = 0
⊢ IsUnit (f.prod * ↑u)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
⊢ {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ WfDvdMonoid α

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
hn0 : a ≠ 0
hnu : ¬IsUnit a
⊢ ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)
⊢ P a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ IsPrimal a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton α
a : α
⊢ Irreducible a ↔ Prime a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (factors a).prod ~ᵤ a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ factors 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
⊢ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
⊢ Prime x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ factors a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ (factors a).card = 1

Tactic:
by

Goal state after: