mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : span ℕ ↑S = P
⊢ AddSubmonoid.closure ↑S = P.toAddSubmonoid

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : AddSubmonoid.closure ↑S = P.toAddSubmonoid
⊢ span ℕ ↑S = P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: G : Type u_3
inst✝ : AddCommGroup G
P : Submodule ℤ G
x✝ : P.FG
S : Finset G
hS : span ℤ ↑S = P
⊢ AddSubgroup.closure ↑S = P.toAddSubgroup

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: G : Type u_3
inst✝ : AddCommGroup G
P : Submodule ℤ G
x✝ : P.toAddSubgroup.FG
S : Finset G
hS : AddSubgroup.closure ↑S = P.toAddSubgroup
⊢ span ℤ ↑S = P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N

Tactic:
rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

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
⊢ N.FG ↔ ∃ n s, span R (range s) = N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
this : Fintype ↑(range g)
⊢ span A ↑(range g).toFinset = N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG ↔ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).FG ↔ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).Finite ↔ Module.Finite A B

Tactic:
by

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

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
⊢ IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFounded fun x1 x2 ↦ x1 > x2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ span R ↑{x} = R ∙ x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFoundedGT { N // N.FG }

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : (f ^ m) x ∈ ↑(LinearMap.ker (f ^ n))
⊢ x ∈ LinearMap.ker (f ^ (n + m))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul S M
r : M → M → Prop
hr : ∀ (s : S) {m m' : M}, r m m' → r (s • m) (s • m')
s : S
x✝¹ x✝ : M
h : (addConGen r).toSetoid x✝¹ x✝
⊢ ∀ (x y : M),
    (DistribSMul.toAddMonoidHom M s) (x + y) = (DistribSMul.toAddMonoidHom M s) x + (DistribSMul.toAddMonoidHom M s) y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : (Setoid.ker ⇑f) x✝¹ x✝
⊢ (Setoid.ker ⇑f) (r • x✝¹) (r • x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module S M
inst✝ : Module S N
f : M →ₗ[S] N
hf : Function.Surjective ⇑f
s : S
⊢ ∀ (x : ModuleCon.Quotient M (ker f.toDistribMulActionHom)),
    (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun (s • x) =
      (RingHom.id S) s • (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulStrictMono α β
ha : 0 < a
hb : b < 0
⊢ a • b < 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ 0 < a • b ↔ 0 < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ IsCofinal ∅ ↔ IsEmpty α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : Nonempty α
s : Set α
hs : IsCofinal s
⊢ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : α
⊢ IsCofinal {x} ↔ IsTop x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : OrderTop α
⊢ IsCofinal {⊤}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
⊢ IsCofinal t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
⊢ IsCofinal (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
⊢ IsCofinal (range Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set α
hs : IsCofinal (⇑e '' s)
⊢ IsCofinal s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsCofinal s ↔ ⋃ i ∈ s, Iic i = univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ⋃ i ∈ s, Iio i = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ a • b < 0 ↔ b < 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R ↑∅ = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ span R ↑hs.toFinset = span R s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : 0 < a • b
ha : 0 ≤ a
⊢ a • 0 < a • b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : a • b < 0
ha : 0 ≤ a
⊢ a • b < a • 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLE α β
h : 0 ≤ a • b
ha : 0 < a
⊢ a • 0 ≤ a • b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLE α β
h : a • b ≤ 0
ha : 0 < a
⊢ a • b ≤ a • 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ IsCofinal s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
ha : a < 0
hb : 0 < b
⊢ a • b < 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ 0 < a • b ↔ 0 < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
⊢ a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : a ≤ 0
hb : 0 ≤ b
⊢ a • b ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
⊢ 0 • b < a • b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬BddAbove s
⊢ IsCofinal s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Finset ι
N : ι → Submodule R M
h : ∀ i ∈ s, (N i).FG
⊢ (⨆ i ∈ s, N i).FG

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
⊢ (iSup N).FG

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
⊢ a • b < 0 • b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ ¬IsCofinal s ↔ BddAbove s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLE α β
h : 0 ≤ a • b
hb : 0 < b
⊢ 0 • b ≤ a • b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLE α β
h : a • b ≤ 0
hb : 0 < b
⊢ a • b ≤ 0 • b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ P ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
⊢ 0 ≤ ?m.53

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
⊢ IsCofinal {a | ∀ (b : α), r b a → b < a}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
⊢ x✝² • x✝¹ ≤ x✝² • x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ f a ⩿ f b ↔ a ⩿ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccLimit (f a) ↔ IsSuccLimit a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : β
ha : 0 ≤ x✝²
x✝¹ x✝ : α
hb : x✝¹ ≤ x✝
⊢ x✝¹ • x✝² ≤ x✝ • x✝²

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
M : Type u_2
inst✝² : Semiring R✝
inst✝¹ : AddCommMonoid M
inst✝ : Module R✝ M
P Q R : { P // P.FG }
hPR : P ≤ R
hQR : Q ≤ R
⊢ ⟨↑P ⊔ ↑Q, ⋯⟩ ≤ R

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), (p i).FG
⊢ (pi univ p).FG

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{u}
⊢ c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ #↑s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
N : Submodule R M
hs : N.FG
t : Set M
ht : t.Finite
span_t : span R t = N
⊢ span S (⇑f '' t) = Submodule.map f N

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ ∃ s, IsCofinal s ∧ #↑s = cof α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
x✝ : IsEmpty α
⊢ cof α = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α = 0 ↔ IsEmpty α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 0 ↔ Nonempty α

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ f.range.FG

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α = 1 ↔ ∃ x, IsTop x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁✝ b₂✝ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : PosSMulReflectLE α β
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ ≠ b₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 1 ↔ NoTopOrder α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α ≤ 1 ↔ ∃ x, IsTop x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b✝ b₁ b₂ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : SMulPosReflectLE α β
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ ≠ a₂

Tactic:
by

Goal state after: