mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
h_eq : ↑hi.choose = ↑hj.choose
⊢ sli[↑hi.choose] = sli[↑hj.choose]

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
h_eq : ↑hi.choose = ↑hj.choose
⊢ sli[↑hi.choose] = sli[↑hj.choose]
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ (R ∙ 1).toSubMulAction ↔ ∃ r, r • 1 = x✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ (R ∙ 1).toSubMulAction ↔ ∃ r, r • 1 = x✝
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m✝ : M
hm✝ : m✝ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m✝ : M
hm✝ : m✝ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 • n✝ ∈ ⊥

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 • n✝ ∈ ⊥
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 ∈ ⊥

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 ∈ ⊥
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 ∈ ⨆ i, t✝ i • N

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 ∈ ⨆ i, t✝ i • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → x • s + y • s ∈ ⨆ i, t✝ i • N

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → x • s + y • s ∈ ⨆ i, t✝ i • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N

Tactic:
;

Goal state after:
case refine_1
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ 1 • m ∈ 1 • N

Tactic:
;

Goal state after:
case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ 1 • m ∈ 1 • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case inl
R : Type u
inst✝⁴ : Semiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : NoZeroDivisors A
N : Submodule R A
⊢ ⊥ * N = ⊥

pp: case inr
R : Type u
inst✝⁴ : Semiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : NoZeroDivisors A
M : Submodule R A
⊢ M * ⊥ = ⊥

Tactic:
;

Goal state after:
case inl
R : Type u
inst✝⁴ : Semiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : NoZeroDivisors A
N : Submodule R A
⊢ ⊥ * N = ⊥

case inr
R : Type u
inst✝⁴ : Semiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : NoZeroDivisors A
M : Submodule R A
⊢ M * ⊥ = ⊥
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
r : R
⊢ (algebraMap R A) r ∈ 1

Tactic:
simp [one_eq_range]

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 ∈ 1 ↔ ∃ y, (algebraMap R A) y = x

Tactic:
simp [one_eq_range]

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
S T : Set A
⊢ map₂ (LinearMap.mul R A) (span R S) (span R T) = span R (S * T)

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
⊢ map₂ (LinearMap.mul R A) (span R S) (span R T) = span R (S * T)
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 N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap (map₂ (LinearMap.mul R A) M N) = ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Tactic:
;

Goal state after:
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'
⊢ map f.toLinearMap (map₂ (LinearMap.mul R A) M N) = ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : IsScalarTower α A A
a : α
S T : Submodule R A
⊢ (a • S) • T = a • S • T

Tactic:
rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]

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
s t : Submodule R A
⊢ map₂ (LinearMap.mul R A) s t = span R (↑s * ↑t)

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s t : Submodule R A
⊢ map₂ (LinearMap.mul R A) s t = span R (↑s * ↑t)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
hx : x ≠ 0
a : S
ha : a ∈ p
⊢ x⁻¹ * (DistribSMul.toLinearMap R S x) a ∈ p

Tactic:
;

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
hx : x ≠ 0
a : S
ha : a ∈ p
⊢ x⁻¹ * (DistribSMul.toLinearMap R S x) a ∈ p
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
inst✝ : FaithfulSMul R A
r : Rˣ
⊢ R ∙ (algebraMap R A) ↑r = 1

Tactic:
;

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : Rˣ
⊢ R ∙ (algebraMap R A) ↑r = 1
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
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ x✝ ∈ Submonoid.map (algebraMap R A) (IsUnit.submonoid R)

Tactic:
;

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ x✝ ∈ Submonoid.map (algebraMap R A) (IsUnit.submonoid R)
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
inst✝ : FaithfulSMul R A
x✝ : Aˣ
⊢ x✝ ∈ (Units.map ↑(spanSingleton R)).ker ↔ x✝ ∈ (Units.map ↑(algebraMap R A)).range

Tactic:
;

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : Aˣ
⊢ x✝ ∈ (Units.map ↑(spanSingleton R)).ker ↔ x✝ ∈ (Units.map ↑(algebraMap R A)).range
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:
;

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 ↦ x • x_1) y' = y
⊢ (fun x_1 ↦ x • x_1) y' ∈ ↑I

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 ↦ x • x_1) y' = y
⊢ (fun x_1 ↦ x • x_1) y' ∈ ↑I
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.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
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ ∀ (r : R) ⦃m : M⦄, m ∈ ⇑(algebraMap S R) '' s • N → m ∈ s • restrictScalars S N → r • m ∈ s • restrictScalars S N

Tactic:
intro r

Goal state after:
case refine_1.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
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
⊢ ∀ ⦃m : M⦄, m ∈ ⇑(algebraMap S R) '' s • N → m ∈ s • restrictScalars S N → r • m ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : ι → Type u_7} [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)]
    [∀ (i : ι), IsNoetherian R (M i)], IsNoetherian R ((i : ι) → M i)

Tactic:
by
  apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)
  · infer_instance
  · exact fun ih ↦ isNoetherian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
α✝ β✝ : Type u_6
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R N
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
α✝ β✝ : Type u_6
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R N
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
α✝ β✝ : Type u_6
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R N
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ x, M✝ (e x))

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
α✝ β✝ : Type u_6
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R N
inst✝ : ∀ (i : β✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ x, M✝ (e x))
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥⊥

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥⊥
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S P
ι : Type u_6
inst✝² : Finite ι
α✝ : Type u_6
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S P
ι : Type u_6
inst✝² : Finite ι
α✝ : Type u_6
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S P
ι : Type u_6
inst✝² : Finite ι
α✝ : Type u_6
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(M✝ none ⊔ ⨆ b, M✝ (some b))

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S P
ι : Type u_6
inst✝² : Finite ι
α✝ : Type u_6
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(M✝ none ⊔ ⨆ b, M✝ (some b))
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
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ 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
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ K
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
F : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : FunLike F R S
inst✝¹ : RingHomClass F R S
f : F
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
le : comap f I ≤ P
r : R
hp : r ∈ ↑P.primeCompl
hI : f r ∈ ↑I
⊢ False

Tactic:
;

Goal state after:
R : Type u
F : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : FunLike F R S
inst✝¹ : RingHomClass F R S
f : F
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
le : comap f I ≤ P
r : R
hp : r ∈ ↑P.primeCompl
hI : f r ∈ ↑I
⊢ False
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
inst✝ : K.IsTwoSided
a✝ b : R
ha : a✝ ∈ comap f K
⊢ f a✝ * f b ∈ 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
inst✝ : K.IsTwoSided
a✝ b : R
ha : a✝ ∈ comap f K
⊢ f a✝ * f b ∈ K