mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.single r ⟨n, hn⟩) = r • n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1

Tactic:
intro j

Goal state after:
case insert.mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
⊢ j ∈ insert i is → update g i x j ∈ f j
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : P
⊢ x₁ ⊗ₜ[R] x₂ = x₁ ⊗ₜ[R] x₂

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : ¬P
⊢ 0 ⊗ₜ[R] x₂ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
h✝ : ¬P
⊢ x₁ ⊗ₜ[R] 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case empty
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
α : Type u_22
m : α → M
n : N
⊢ (∑ a ∈ ∅, m a) ⊗ₜ[R] n = ∑ a ∈ ∅, m a ⊗ₜ[R] n

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case empty
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
α : Type u_22
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ ∅, n a = ∑ a ∈ ∅, m ⊗ₜ[R] n a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ Finset.univ → g i ∈ f i), ∏ i, g i = a) ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i, g i = a

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ map LinearMap.id LinearMap.id = LinearMap.id

Tactic:
ext
  simp only [mk_apply, id_coe, compr₂ₛₗ_apply, _root_.id, map_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : Module R P
inst✝² : Module R Q
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
m : M₂
n : N₂
⊢ (map ↑f ↑g ∘ₛₗ map ↑f.symm ↑g.symm) (m ⊗ₜ[R₂] n) = LinearMap.id (m ⊗ₜ[R₂] n)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : AddMonoidWithOne R
⊢ (Nat.castAddMonoidHom R) 1 = ((multiplesHom R) 1) 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : Module R P
inst✝² : Module R Q
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
m : M
n : N
⊢ (map ↑f.symm ↑g.symm ∘ₛₗ map ↑f ↑g) (m ⊗ₜ[R] n) = LinearMap.id (m ⊗ₜ[R] n)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
a : α
⊢ a + a = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
a b : α
⊢ a + b = a ↔ b ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
a b : α
⊢ a + b = b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
a b c : α
⊢ a + b ≤ c ↔ a ≤ c ∧ b ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: m n : ℕ+
⊢ IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
h : IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Tactic:
exact h.1.mul_left (ih h.2)

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
x✝ : I
⊢ x✝ ∈ ∅ → IsCoprime (s x✝) x

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case empty
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑∅).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ ∅, s i ∣ z
⊢ ∏ x ∈ ∅, s x ∣ z

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
i : I
hir : i ∈ r
⊢ a ∈ ↑(insert a r)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i = toInt val j ↔ val i = val j

Tactic:
simp [toInt_le_toInt, le_antisymm_iff]

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map f.toLinearMap 1 ↔ x✝ ∈ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
X✝ : A
⊢ op X✝ ∈ map (↑(opLinearEquiv R)) 1 ↔ op X✝ ∈ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 1 ↔ x✝ ∈ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
⊢ span R (↑M * {1}) = M

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
x✝ : A'
⊢ x✝ ∈ (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ ↔
    x✝ ∈ (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
x✝ : I
⊢ x✝ ∈ ∅ → IsRelPrime (s x✝) x

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
T : Type u_1
U : Type u_2
inst✝¹ : Semiring T
inst✝ : Semiring U
f : R →+* S
g : T →+* U
fst✝ : R
snd✝ : T
⊢ (fst✝, snd✝) ∈ RingHom.ker (f.prodMap g) ↔ (fst✝, snd✝) ∈ (RingHom.ker f).prod (RingHom.ker g)

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
⊢ ∀ (x : R × S), x ∈ ⊤.prod ⊤ ↔ x ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (RingHom.fst R S) (I.prod J) = I

Tactic:
ext x
  rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
x✝ : Ideal R × Ideal S
I : Ideal R
J : Ideal S
⊢ (fun I ↦ (map (RingHom.fst R S) I, map (RingHom.snd R S) I)) ((fun I ↦ I.1.prod I.2) (I, J)) = (I, J)

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
⊢ span (∅ ×ˢ ∅) = (span ∅).prod (span ∅)

Tactic:
simp

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

Goal state before:
pp: case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) * (1, 0) ∈ I.prod J

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
r : S
x : M
r_in : r ∈ s
x_in : x ∈ restrictScalars S N
⊢ r • x ∈ restrictScalars S (⇑(algebraMap S R) '' s • N)

Tactic:
rw [restrictScalars_mem, ← algebraMap_smul R r]

Goal state after:
case refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
r : S
x : M
r_in : r ∈ s
x_in : x ∈ restrictScalars S N
⊢ (algebraMap S R) r • x ∈ ⇑(algebraMap S R) '' s • N
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ {generator (Ideal.map (RingHom.fst R S) I)}.Nonempty

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ {generator (Ideal.map (RingHom.snd R S) I)}.Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Orzech

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
⊢ Submodule.map f ⊥ ≤ Submodule.map i ⊥

Tactic:
simp

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
inst✝ : RingHomClass F R S
I : Ideal S
c x : R
hx : f x ∈ I
⊢ f c * f x ∈ I

Tactic:
exact mul_mem_left I _ hx

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ ∃ P x x_1, ∃ (_ : Free R P) (_ : Module.Finite R P), ∃ f, Surjective ⇑f

Tactic:
rcases Module.Finite.exists_fin' R M with ⟨m, f', hf'⟩

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
⊢ ∃ P x x_1, ∃ (_ : Free R P) (_ : Module.Finite R P), ∃ f, Surjective ⇑f
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)

Tactic:
· subst hz
    rw [div_zero, div_zero, mul_zero]

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)
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
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ I • comap f p ≤ comap f (I • p)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
hr : r ∈ I i
⊢ (Pi.evalRingHom R i) (Pi.single i r) = r

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = 0 ∧ b = 0 → gcd a b = 0

Tactic:
rintro ⟨rfl, rfl⟩
    exact gcd_zero_right _

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 : ι
⊢ (Pi.evalRingHom R i) (r' i) = (Pi.single i 1 * r' i) i

Tactic:
simp

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
h :
  { 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:
have := map_mono (f := f) h

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
hf : Function.Bijective ⇑f
I : Ideal R
K x✝¹ x✝ : Ideal S
h :
  { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
    { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝
this :
  map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹) ≤
    map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝)
⊢ x✝¹ ≤ x✝
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_1.refine_2
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
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ 0 • f i = 0

Tactic:
simp

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
      rw [lcm, hxy, div_zero]
      exact dvd_zero _

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
      rw [lcm, hxy, div_zero]
      exact dvd_zero _

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

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
q : Ideal S
hq : q.IsPrime
inst✝ : (comap f q).IsPrime
⊢ comap f (map f (comap f q)) = comap f q

Tactic:
simp

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
x✝ : R
⊢ x✝ ∈ ker ↑f ↔ x✝ ∈ ⊥

Tactic:
simp

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'
x✝ : R
⊢ x✝ ∈ ker f ↔ x✝ ∈ ⊥

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ (n✝ + 1) ≤ J ^ (n✝ + 1)

Tactic:
| succ _ hn =>

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

Tactic:
simp

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

Tactic:
simp

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

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

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

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

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

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

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

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp

Goal state after: