mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
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:
simpa using

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

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

Goal state after:
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))
⊢ (f ^ (n + m)) x = 0
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
h : IsCofinal ∅
a : α
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LE α
h : IsCofinal ∅
a : α
⊢ False
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:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set α
hs : IsCofinal (⇑e '' s)
⊢ IsCofinal s
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:
simpa using

Goal state after:
α : 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₁
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
obtain ⟨b, hb, hb'⟩ := hs a
  rwa [ha.eq_of_ge hb'] at hb

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:
simpa using

Goal state after:
α : 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₁
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
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
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case intro
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
val✝ : Fintype (PLift ι)
⊢ (iSup N).FG

Tactic:
simpa using

Goal state after:
case intro
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
val✝ : Fintype (PLift ι)
⊢ (iSup N).FG
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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✝²
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:
simpa using

Goal state after:
α : Type u
inst✝ : Preorder α
c : Cardinal.{u}
⊢ c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Preorder α
⊢ ¬cof α = 0 ↔ Nonempty α
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
exact (smul_lt_smul_of_pos_right ha h₁).trans_le (smul_le_smul_of_nonneg_left hb h₂.le)

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

Goal state before:
pp: case empty
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
⊢ motive (span R ↑∅) ⋯

Tactic:
simpa using

Goal state after:
case empty
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
⊢ motive ⊥ ⋯
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
x : ↑s
⊢ ∃ y, ↑x ≤ f y

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
x : ↑s
⊢ ∃ y, ↑x ≤ f y
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case insert
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R ↑s) ⋯
⊢ motive (span R ↑(insert x s)) ⋯

Tactic:
simpa using

Goal state after:
case insert
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R ↑s) ⋯
⊢ motive (span R ↑s ⊔ R ∙ x) ⋯
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case insert
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R ↑s) ⋯
⊢ motive (span R ↑(insert x s)) ⋯

Tactic:
simpa using

Goal state after:
case insert
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R ↑s) ⋯
⊢ motive (span R ↑s ⊔ R ∙ x) ⋯
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α γ : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder γ
f : α → γ
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ cof α = cof γ

Tactic:
simpa using

Goal state after:
α γ : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder γ
f : α → γ
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ cof α = cof γ
Module: Mathlib.Algebra.Order.Module.Defs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
hb : 0 ≤ b
h : a ≤ 1
⊢ a • b ≤ b
Module: Mathlib.Algebra.Order.Module.Defs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a • b
Module: Mathlib.Algebra.Order.Module.Defs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
hb : 0 < b
h : a < 1
⊢ a • b < b
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
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
s : ↥S
⊢ ↑s ∈ ⨆ k, N k

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
s : ↥S
⊢ ↑s ∈ span R ↑S
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α γ : Type u
inst✝¹ : Preorder α
inst✝ : Preorder γ
f : γ → α
g : α → γ
h : GaloisConnection f g
⊢ cof γ ≤ cof α

Tactic:
simpa using

Goal state after:
α γ : Type u
inst✝¹ : Preorder α
inst✝ : Preorder γ
f : γ → α
g : α → γ
h : GaloisConnection f g
⊢ cof γ ≤ cof α
Module: Mathlib.Algebra.Order.Module.Defs

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

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
hb : 0 < b
h : 1 < a
⊢ b < a • b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α γ : Type u
inst✝¹ : Preorder α
inst✝ : Preorder γ
f : α ≃o γ
⊢ cof α = cof γ

Tactic:
simpa using

Goal state after:
α γ : Type u
inst✝¹ : Preorder α
inst✝ : Preorder γ
f : α ≃o γ
⊢ cof α = cof γ
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Semiring α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_a : α
ha : 0 ≤ _a
b₁ b₂ : β
⊢ b₁ ≤ b₂ → _a • b₁ ≤ _a • b₂

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Semiring α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_a : α
ha : 0 ≤ _a
b₁ b₂ : β
⊢ b₁ ≤ b₂ → _a • b₁ ≤ _a • b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Ring α
inst✝⁵ : AddCommGroup β
inst✝⁴ : Module α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
⊢ a₁ ≤ a₂ → a₁ • _b ≤ a₂ • _b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : Ring α
inst✝⁵ : AddCommGroup β
inst✝⁴ : Module α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
⊢ a₁ ≤ a₂ → a₁ • _b ≤ a₂ • _b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → x ∈ s → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
a b : α
hab : a ≤ b
t : Set α
ht : t ∈ s
hb : b ∈ t
⊢ ∃ y ∈ range fun x ↦ f ↑x ⋯, a ≤ y

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → x ∈ s → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
a b : α
hab : a ≤ b
t : Set α
ht : t ∈ s
hb : b ∈ t
⊢ ∃ a_1, ∃ (h : a_1 ∈ s), a ≤ f a_1 ⋯
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupClosed x
⊢ DirSupClosed (⋂₀ s)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupClosed x
⊢ DirSupClosed (⋂₀ s)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInacc x
⊢ DirSupInacc (⋃₀ s)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInacc x
⊢ DirSupInacc (⋃₀ s)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
p : P
x✝ : p ∈ ⊤
⊢ p ∈ ⇑f '' ↑(span R s)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
p : P
x✝ : p ∈ ⊤
⊢ ∃ y, f y = p
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupClosed s
ht : DirSupClosed t
⊢ DirSupClosed (s ∩ t)

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupClosed s
ht : DirSupClosed t
⊢ DirSupClosed (s ∩ t)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∪ t)

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∪ t)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ 0 < a • b ↔ b < 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ 0 < a • b ↔ b < 0
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ Ideal.span ↑{1} = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ Ideal.span {1} = ⊤