mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
⊢ span L ↑(Submodule.inclusionSpan L i.range ∘ₗ i.rangeRestrict).range = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
⊢ span L ↑(Submodule.inclusionSpan L j.range ∘ₗ j.rangeRestrict).range = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
x : M'
y : N'
⊢ ∀ x ∈ ↑i.range, ∀ y ∈ ↑j.range, ((restrictScalarsₗ K L N L K ∘ₗ ↑K p) x) y ∈ (Algebra.linearMap K L).range

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
x : M'
y : N'
⊢ i x ∈ ↑i.range

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
x : M'
y : N'
⊢ j y ∈ ↑j.range

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ (a * b' - 1) * (1 - (mk (I ^ (n + 1))) c) + (1 - (mk (I ^ (n + 1))) c) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
⊢ IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Ring R✝
I✝ J K : Ideal R✝
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ I ^ b • ⊤ ≤ comap (I ^ a • N).subtype (I ^ c • N)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ Function.Injective ⇑(powSMulQuotInclusion I M h N)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℤ
⊢ T R (m * n) = (T R m).comp (T R n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
⊢ factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤ = powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(I ^ a • ⊤) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ (powSMulQuotInclusion I M h N).range = map (I ^ c • N).mkQ (I ^ a • N)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
⊢ IsFiniteLength R N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
⊢ ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥(s.toFun 0)

Tactic:
change IsFiniteLength R s.head

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥(RelSeries.head s)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℤ
⊢ C R (m * n) = (C R m).comp (C R n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : (s.toFun i.castSucc, s.toFun i.succ) ∈ {(x, y) | JordanHolderLattice.IsMaximal x y} := s.step i
this✝ : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
this : ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] ↥(s.toFun i.succ ⊓ s.toFun i.castSucc)
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
inf_of_le_right cov.le

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : (s.toFun i.castSucc, s.toFun i.succ) ∈ {(x, y) | JordanHolderLattice.IsMaximal x y} := s.step i
this✝ : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
this : ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] ↥(s.toFun i.castSucc)
⊢ IsFiniteLength R ↥(s.toFun i.succ)
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
b : α
x✝ : 0 < ↑b
⊢ ↑x * 0 < ↑x * ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : ↑a < ↑b
⊢ ↑x * ↑a < ↑x * ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
b : α
x✝ : 0 < ↑b
⊢ 0 * ↑x < ↑b * ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : ↑a < ↑b
⊢ ↑a * ↑x < ↑b * ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x✝¹ : 0 ≤ 0
a b : WithZero α
x✝ : a ≤ b
⊢ 0 * a ≤ 0 * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
x✝² : 0 ≤ ↑x
x✝¹ : WithZero α
x✝ : 0 ≤ x✝¹
⊢ ↑x * 0 ≤ ↑x * x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
x✝ : 0 ≤ ↑x
a : α
h : ↑a ≤ 0
⊢ ↑x * ↑a ≤ ↑x * 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : ↑a ≤ ↑b
⊢ ↑x * ↑a ≤ ↑x * ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x✝¹ : 0 ≤ 0
a b : WithZero α
x✝ : a ≤ b
⊢ a * 0 ≤ b * 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
x✝² : 0 ≤ ↑x
x✝¹ : WithZero α
x✝ : 0 ≤ x✝¹
⊢ 0 * ↑x ≤ x✝¹ * ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
x✝ : 0 ≤ ↑x
a : α
h : ↑a ≤ 0
⊢ ↑a * ↑x ≤ 0 * ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : ↑a ≤ ↑b
⊢ ↑a * ↑x ≤ ↑b * ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ StrictMono ⇑withZeroUnitsEquiv

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s✝ : Set (Submodule R M)
hs : sSupIndep s✝ ∧ sSup s✝ = ⊤ ∧ ∀ m ∈ s✝, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
H : IsFiniteLength R N
hf : Function.Injective ⇑f
⊢ IsFiniteLength R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
H : IsFiniteLength R M
hf : Function.Surjective ⇑f
⊢ IsFiniteLength R N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
⊢ StrictMono ⇑embedding

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : f.ValueGroup₀
ha : 0 < a
b c : f.ValueGroup₀
hbc : b < c
⊢ a * b < a * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x✝ : f.ValueGroup₀
⊢ 0 ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : f.ValueGroup₀ˣ
⊢ 0 < embedding ↑a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Order.krullDim (Submodule R M) ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M = Order.height ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M = Order.coheight ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M = 0 ↔ Subsingleton M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ 0 < length R M ↔ Nontrivial M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝¹ : IsNoetherian R M
this✝ : IsArtinian R M
t : LTSeries (Submodule R M)
t' : RelSeries {(a, b) | a ⋖ b}
i : Fin (t.length + 1) ↪ Fin (t'.length + 1)
hi : t'.toFun ∘ ⇑i = t.toFun
ht₁ : t'.head = ⊥
ht₂ : t'.last = ⊤
this : Fin s.length ≃ Fin t'.length
⊢ t.length ≤ t'.length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝¹ : IsNoetherian R M
this✝ : IsArtinian R M
t : LTSeries (Submodule R M)
t' : RelSeries {(a, b) | a ⋖ b}
i : Fin (t.length + 1) ↪ Fin (t'.length + 1)
hi : t'.toFun ∘ ⇑i = t.toFun
ht₁ : t'.head = ⊥
ht₂ : t'.last = ⊤
this : Fin s.length ≃ Fin t'.length
h : t.length ≤ t'.length
⊢ t'.length = s.length

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsDomain R
inst✝ : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : (fun a ↦ n • a) a = (fun a ↦ n • a) b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
⊢ ↑s.length = length R M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
⊢ f (-1) ^ Nat.succ 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M = ⊤ ↔ InfiniteDimensionalOrder (Submodule R M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M ≠ ⊤ ↔ FiniteDimensionalOrder (Submodule R M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ f (-x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x y : R
⊢ f (x - y) = f (y - x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
⊢ length R M ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ FiniteDimensionalOrder (Submodule R M) ↔ IsFiniteLength R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
⊢ FiniteDimensionalOrder (Submodule R M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ ↑(length R ↥N) = ↑(Order.height N)

Tactic:
rw [Order.height_eq_krullDim_Iic, coe_length, Order.krullDim_eq_of_orderIso (Submodule.mapIic _)]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ length R ↥N = Order.height N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ length R (M ⧸ N) = Order.coheight N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ Module.length R M = Module.length R N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
this : RingHomSurjective (algebraMap S R)
⊢ ∀ (m : S) (x : M), (AddHom.id M).toFun (m • x) = (algebraMap S R) m • (AddHom.id M).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
⊢ length S M = length R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R ↥⊤ = length R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
N : Submodule R M
⊢ Order.height N < ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : N ≠ ⊤
⊢ Module.length R ↥N < Module.length R M

Tactic:
by

Goal state after: