mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
⊢ annihilator R (ι →₀ M) = annihilator R M

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
⊢ I ^ n ≤ J ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
i : R
hi : i ∈ I
j : R
hj : j ∈ J
⊢ i * j * b ∈ I * J

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : J.IsTwoSided
a✝ b : R
ha : a✝ ∈ I * J
x y : R
hx : x * b ∈ I * J
hy : y * b ∈ I * J
⊢ (x + y) * b ∈ I * J

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ (I ^ Nat.zero).IsTwoSided

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ (I ^ x✝¹.succ).IsTwoSided

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ annihilator R (Π₀ (i : ι), M i) = ⨅ i, annihilator R (M i)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
⊢ I ^ (n + 1) = I * I ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S T : Set R
inst✝ : (span S).IsTwoSided
⊢ ∀ (x : R), x ∈ S * T ↔ x ∈ S * T

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
r s : R
inst✝ : (span {r}).IsTwoSided
⊢ span {r} * span {s} = span {r * s}

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * c ∣ a * b

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
n : ℕ
⊢ span {s} ^ n = span {s ^ n}

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
I J : Ideal R
inst✝² : IsDomain R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} ≤ J * span {x} ↔ I ≤ J

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
I J : Ideal R
inst✝² : IsDomain R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} = J * span {x} ↔ I = J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ annihilator R ((i : ι) → M i) = ⨅ i, annihilator R (M i)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
I J : Ideal R
inst✝ : I.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊓ J ≠ ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² : R
x✝¹ : x✝² ∈ ⊤
x✝ : M
⊢ x✝ ∈ ⊥ → x✝² • x✝ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.annihilator = ⊤ ↔ N = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + y * z) / y = x / y + z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + z * y) / y = x / y + z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort w
f : ι → Submodule R M
r : R
H : r ∈ ⨅ i, (f i).annihilator
n : M
hn : n ∈ ⨆ i, f i
m₁ m₂ : M
h₁ : r • m₁ = 0
h₂ : r • m₂ = 0
⊢ r • (m₁ + m₂) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - y * z) / y = x / y - z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - z * y) / y = x / y - z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z + y) / z = x + y / z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x - y) / z = x - y / z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z - y) / z = x - y / z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
⊢ x / (y * z) = x / y / z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
⊢ x / y / z = x / (y * z)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y + z / t = (t * x + y * z) / (t * y)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y - z / t = (t * x - y * z) / (t * y)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y = z ↔ x = y * z

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x = y / z ↔ z * x = y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y = z / t ↔ t * x = y * z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a : S
⊢ e.symm (e a / e 0) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
⊢ b * e.symm (e a / e b) + e.symm (e a % e b) = a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ e b ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ EuclideanDomain.r (e (e.symm (e a % e b))) (e b)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ ¬EuclideanDomain.r (e (a * b)) (e a)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ K = ⊤
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).lcm = fold GCDMonoid.lcm (GCDMonoid.lcm 1 1) (s₁ + s₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ lcm 0 ∣ a ↔ ∀ (b : α), b ∈ 0 → b ∣ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.lcm ∣ a ↔ ∀ (b : α), b ∈ s → b ∣ a) → ((a_1 ::ₘ s).lcm ∣ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ∣ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (lcm 0) = lcm 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.lcm = s.lcm
⊢ normalize (a ::ₘ s).lcm = (a ::ₘ s).lcm

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
s : Multiset α
⊢ s.lcm = 0 ↔ 0 ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).lcm = lcm 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
by

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

Goal state before:
pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
intro a x _ hx
      rw [smul_comm, hx, smul_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ r ∈ (span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M
r : R
⊢ r ∈ (R ∙ g).annihilator ↔ r • g = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).annihilator = ⨅ g, (toSpanSingleton R M ↑g).ker

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M
⊢ (R ∙ g).annihilator = (toSpanSingleton R M g).ker

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I * annihilator I = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : K ⊔ J = ⊤
⊢ I * K ⊔ J = I ⊔ J

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ I ⊔ ⨅ i ∈ ∅, J i = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).gcd = fold GCDMonoid.gcd (GCDMonoid.gcd 0 0) (s₁ + s₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ a ∣ gcd 0 ↔ ∀ (b : α), b ∈ 0 → a ∣ b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (a ∣ s.gcd ↔ ∀ (b : α), b ∈ s → a ∣ b) → (a ∣ (a_1 ::ₘ s).gcd ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ∣ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (gcd 0) = gcd 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.gcd = s.gcd
⊢ normalize (a ::ₘ s).gcd = (a ::ₘ s).gcd

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
⊢ map f I = ⊥ ↔ I ≤ RingHom.ker f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
⊢ (map f I).IsPrime

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
hf : Function.Injective ⇑f
⊢ map f I = ⊥ ↔ I = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (r • I) = f r • map f I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd ≠ 0 ↔ ∃ x, x ∈ s ∧ x ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ ⨅ i_1 ∈ insert i t, J i_1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ I ⊔ ⨅ i ∈ s, J i = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ ∀ I ∈ A, y ∈ map f I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).gcd = gcd 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this : ∀ I ∈ A, f x' ∈ map f I
⊢ x - x' ∈ J

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ (⨅ i ∈ s, J i) ⊔ I = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).gcd = GCDMonoid.gcd a s.gcd

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ n = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map (fun x ↦ s.gcd * x) t
⊢ t.gcd = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f (c - a * b) = 0
⊢ a * b ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
⊢ (map f I).IsPrime

Tactic:
by

Goal state after: