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

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R✝
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
this : Fintype ι
i j : ι
ne : j ≠ i
⊢ (Pi.single j 1 * r' j) i = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd a b = a

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
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').1 = gcd 0 x

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R✝
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
this : Fintype ι
i : ι
⊢ r i = (∑ i, Pi.single i 1 * r' i) i

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝³ x✝² : R
x✝¹ : x✝³ ∈ span R S
x✝ : x✝² ∈ span R S
h₁ : x✝³ • m ∈ span R (S • T)
h₂ : x✝² • m ∈ span R (S • T)
⊢ (x✝³ + x✝²) • m ∈ span R (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✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').1 = gcd x y

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
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R✝
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
⊢ pi ((fun I i ↦ map (Pi.evalRingHom R i) I) I) = I

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝² x✝¹ : R
x✝ : x✝¹ ∈ span R S
h : x✝¹ • m ∈ span R (S • T)
⊢ (x✝² • x✝¹) • m ∈ span R (S • T)

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁷ : Semiring R✝
inst✝⁶ : Semiring S
inst✝⁵ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝⁴ : FunLike G S R✝
inst✝³ : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝² : (i : ι) → Semiring (R i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal I

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
⊢ comap f ⊥ ≤ I

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝¹ : R
x✝ : x✝¹ ∈ Ideal.span S
⊢ x✝¹ • 0 ∈ span R (S • T)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (↑f.symm) (map (↑f) I) = I

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (↑f) (comap (↑f.symm) I) = I

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
y : S
⊢ f.symm y ∈ I ↔ y ∈ map f I

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
x : R
⊢ f x ∈ map f I ↔ x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝³ x✝² : M
x✝¹ : x✝³ ∈ span R T
x✝ : x✝² ∈ span R T
h₁ : ∀ r ∈ Ideal.span S, r • x✝³ ∈ span R (S • T)
h₂ : ∀ r ∈ Ideal.span S, r • x✝² ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • (x✝³ + x✝²) ∈ span R (S • T)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I ↔ ∃ x ∈ I, e x = y

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
inst✝¹ : RingHomClass F R S
hf : Function.Surjective ⇑f
p : Ideal S
inst✝ : p.IsPrime
⊢ Submonoid.map f (comap f p).primeCompl = p.primeCompl

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
r' : R
m : M
hm : m ∈ span R T
mem : ∀ r ∈ Ideal.span S, r • m ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • r' • m ∈ span R (S • T)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
r : R
hr : r ∈ Ideal.span S
m : M
hm : m ∈ span R T
⊢ r • m ∈ span R (S • T)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
I✝ J : Ideal R
K✝ L : Ideal S
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass F R S
ι : Sort u_3
hf : Function.Bijective ⇑f
I : Ideal R
K x✝¹ x✝ : Ideal S
⊢ { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
      { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝ ↔
    x✝¹ ≤ x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
⊢ m ∈ S • T → m ∈ ↑(Ideal.span S • span R T)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ map f I = ⊤ ↔ I = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ (map f I).IsMaximal ↔ I.IsMaximal

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
K : Ideal S
⊢ (comap f K).IsMaximal ↔ K.IsMaximal

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
s : Set M
x : M
⊢ x ∈ I • span R s ↔ x ∈ span R (↑I • s)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
r : R
h : f r ∈ map f I
s : R
hsi : s ∈ ↑I
hfsr : f s = f r
⊢ f (r - s) = 0

Tactic:
by

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

Goal state before:
pp: case mpr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) → x ∈ I • span R (Set.range f)

Tactic:
rintro ⟨a, ha, rfl⟩
    exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
⊢ Order.coheight (comap f I) = Order.coheight I

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this : map f J = ⊤
⊢ J = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : P a b (r, s, t)
p' : P a b (r', s', t')
⊢ P a b (xgcdAux r s t r' s' t')

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
⊢ (comap f K).IsMaximal

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ P a b (a, 1, 0)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ P a b (b, 0, 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
by

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

Goal state before:
pp: S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
⊢ ⇑f '' ↑I * ⇑f '' ↑J ⊆ ↑(map f (I * J))

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
⊢ map f 1 = 1

Tactic:
simp only [one_eq_top, Ideal.map_top f]

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
⊢ map f 1 = 1

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
inst✝¹ : EuclideanDomain R✝
inst✝ : DecidableEq R✝
R : Type u_1
e : EuclideanDomain R
this : DecidableEq R
a b : R
h : a * b = 0
h0 : ¬a = 0 ∧ ¬b = 0
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K.radical = (comap f K).radical

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
hK : K.IsRadical
⊢ (Ideal.comap f K).IsRadical

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
a b : R
n : ℕ
hab : b ∣ a
⊢ (a / b) ^ n = a ^ n / b ^ n

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
hxy : gcd x y = 0
⊢ x ∣ lcm x y

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
⊢ comap f K ^ n ≤ comap f (K ^ n)

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
hxy : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
⊢ x * z * gcd x y = x * y

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
hxy : gcd x y = 0
⊢ y ∣ lcm x y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ q, q.IsPrime ∧ comap f q = p

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
hxy : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
⊢ gcd x y * (y * z) = x * y

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
⊢ r ∈ ker f ↔ f r = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* R
g : T →+* S
⊢ Ideal.comap g (ker f) = ker (f.comp g)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ 1 ∉ ker f

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝¹ : Semiring S
ι : Type u_3
R : ι → Type u_4
inst✝ : (i : ι) → Semiring (R i)
φ : (i : ι) → S →+* R i
⊢ ker (RingHom.pi φ) = ⨅ i, ker (φ i)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
⊢ ker ↑f = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
F' : Type u_3
inst✝¹ : EquivLike F' R S
inst✝ : RingEquivClass F' R S
f : F'
⊢ ker f = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ ker (e.toRingHom.comp f) = ker f

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ker f = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
s : Set ι
f : ι → M
x : M
⊢ x ∈ I • span R (f '' s) ↔ ∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun i c ↦ c • f ↑i) = x

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 z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
this : x * y ∣ z * gcd x y
⊢ x * y / gcd x y ∣ z

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ Ideal.span {r} • N = r • N

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective ⇑f
⊢ ker (f.comp g) = ker g

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'
⊢ x ∈ M'

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
x y : R
⊢ x - y ∈ ker f ↔ f x = f y

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : Module R M
r : R
⊢ r ∈ annihilator R M ↔ (LinearMap.lsmul R M) r = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
r : R
N : Submodule R M
f : M →ₗ[R] M'
⊢ map f (r • N) = r • map f N

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ 1 = ⊤

Tactic:
Submodule.one_eq_span,

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ R ∙ 1 = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ 1 = ⊤

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
m : M
⊢ f (x • m) = f 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : x ∈ Module.annihilator R M'
⊢ x ∈ Module.annihilator R M

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
⊢ I * ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
⊢ ⊥ * I = ⊥

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 z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ lcm 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
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : x ∈ Module.annihilator R M
⊢ x ∈ Module.annihilator R M'

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
R₀ : Type u_4
inst✝³ : CommSemiring R₀
inst✝² : Module R₀ M
inst✝¹ : Algebra R₀ R
inst✝ : IsScalarTower R₀ R M
⊢ Ideal.comap (algebraMap R₀ R) (annihilator R M) = annihilator R₀ M

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ ∀ (m : M), (r - s) • m = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ ∀ (a_1 : M), a • a_1 = 0 • a_1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M = ⊥ ↔ FaithfulSMul R M

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
h : annihilator R M = ⊤
m m' : M
⊢ m = m'

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
⊢ annihilator R (M × M') = annihilator R M ⊓ annihilator R M'

Tactic:
by

Goal state after: