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

Goal state before:
pp: case zero
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 ∈ s • N

Tactic:
;

Goal state after:
case zero
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 ∈ s • N
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
hK : K.IsPrime
x y : R
⊢ f x * f y ∈ K → f x ∈ K ∨ f y ∈ K

Tactic:
;

Goal state after:
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
hK : K.IsPrime
x y : R
⊢ f x * f y ∈ K → f x ∈ K ∨ f y ∈ K
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ x✝ • n + y✝ • n ∈ s • N

Tactic:
;

Goal state after:
case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ x✝ • n + y✝ • n ∈ s • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
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
s : Set R
x : R
hx : x ∈ s
⊢ f x ∈ ↑(map f (span s))

Tactic:
;

Goal state after:
case refine_1
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
s : Set R
x : R
hx : x ∈ s
⊢ f x ∈ ↑(map f (span s))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ (a✝¹ • c i • i) • n ∈ s • N

Tactic:
← mul_smul,

Goal state after:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ ((a✝¹ * c i) • i) • n ∈ s • N
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)

Tactic:
· simp only [b0, zero_mul]

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
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
⊢ 0 ∈ span R (S • T)

Tactic:
;

Goal state after:
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
⊢ 0 ∈ span R (S • T)
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 : ι
⊢ (Pi.evalRingHom R i) (r' i) = (Pi.single i 1 * r' i) i

Tactic:
;

Goal state after:
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 : ι
⊢ (Pi.evalRingHom R i) (r' i) = (Pi.single i 1 * r' i) i
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✝³ • m + x✝² • m ∈ span R (S • T)

Tactic:
;

Goal state after:
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✝³ • m + x✝² • m ∈ span R (S • T)
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:
;

Goal state after:
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)
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
⊢ 0 ∈ span R (S • T)

Tactic:
;

Goal state after:
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
⊢ 0 ∈ span R (S • T)
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✝³ + r • x✝² ∈ span R (S • T)

Tactic:
;

Goal state after:
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✝³ + r • x✝² ∈ span R (S • T)
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:
;

Goal state after:
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)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
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

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:
;

Goal state after:
case mp
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

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)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
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
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ f r * f s ∈ map f I * map f J

Tactic:
;

Goal state after:
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
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ f r * f s ∈ map f I * map f J
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
r : R
hri : r ∈ ↑I
s : R
hsj : s ∈ ↑J
⊢ f (r * s) ∈ ↑(map f (I * J))

Tactic:
;

Goal state after:
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
r : R
hri : r ∈ ↑I
s : R
hsj : s ∈ ↑J
⊢ f (r * s) ∈ ↑(map f (I * J))
Module: Mathlib.RingTheory.Ideal.Maps

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

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
x✝ : R
⊢ x✝ ∈ ker ↑f ↔ x✝ ∈ ⊥
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'
x✝ : R
⊢ x✝ ∈ ker f ↔ x✝ ∈ ⊥

Tactic:
;

Goal state after:
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'
x✝ : R
⊢ x✝ ∈ ker f ↔ x✝ ∈ ⊥
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:
ker_eq,

Goal state after:
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 ↔ ⇑f ⁻¹' {0} = ↑⊥
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), x • m = 0

Tactic:
;

Goal state after:
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), x • m = 0
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 : ∀ (m : M), x • m = 0
m : M'
⊢ x • m = 0

Tactic:
;

Goal state after:
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 : ∀ (m : M), x • m = 0
m : M'
⊢ x • m = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤

Tactic:
;

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤
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 ι
r : R
⊢ r ∈ annihilator R (ι →₀ M) ↔ r ∈ annihilator R M

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ r ∈ annihilator R (ι →₀ M) ↔ r ∈ annihilator R M
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
⊢ r • m = 0

Tactic:
;

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
⊢ r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
i : ι
⊢ (r • m) i = 0 i

Tactic:
;

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
i : ι
⊢ (r • m) i = 0 i
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)
r : R
⊢ r ∈ annihilator R (Π₀ (i : ι), M i) ↔ r ∈ ⨅ i, annihilator R (M i)

Tactic:
;

Goal state after:
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)
r : R
⊢ r ∈ annihilator R (Π₀ (i : ι), M i) ↔ r ∈ ⨅ i, annihilator R (M i)
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:
;

Goal state after:
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
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 * b + y * b ∈ I * J

Tactic:
;

Goal state after:
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 * b + y * b ∈ I * J
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * (x * y / gcd x y) = x * y
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 : ℕ
⊢ ⊤.IsTwoSided

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ ⊤.IsTwoSided
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
⊢ r • m = 0

Tactic:
;

Goal state after:
case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
⊢ r • m = 0
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
⊢ IsTwoSided (I ^ x✝¹ * I)

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ IsTwoSided (I ^ x✝¹ * I)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
i : ι
⊢ (r • m) i = 0 i

Tactic:
;

Goal state after:
case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
i : ι
⊢ (r • m) i = 0 i
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)
r : R
⊢ r ∈ annihilator R ((i : ι) → M i) ↔ r ∈ ⨅ i, annihilator R (M i)

Tactic:
;

Goal state after:
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)
r : R
⊢ r ∈ annihilator R ((i : ι) → M i) ↔ r ∈ ⨅ i, annihilator R (M i)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y

Tactic:
;

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c

Tactic:
;

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
ih : span {s} ^ 0 = span {s ^ 0}
⊢ span {s} ^ (0 + 1) = span {s ^ (0 + 1)}

pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
n : ℕ
ih : span {s} ^ n = span {s ^ n}
ne : n ≠ 0
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}

Tactic:
;

Goal state after:
case succ.inl
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
ih : span {s} ^ 0 = span {s ^ 0}
⊢ span {s} ^ (0 + 1) = span {s ^ (0 + 1)}

case succ.inr
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
n : ℕ
ih : span {s} ^ n = span {s ^ n}
ne : n ≠ 0
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
⊢ r • m = 0

Tactic:
;

Goal state after:
case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
⊢ r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
;

Goal state after:
case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)

case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
i : ι
⊢ (r • m) i = 0 i

Tactic:
;

Goal state after:
case mpr
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)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
i : ι
⊢ (r • m) i = 0 i
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
;

Goal state after:
case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
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
⊢ (∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0