mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ x ∈ s

Tactic:
]

Goal state after:
case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ x ∈ s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ y ∈ s

Tactic:
]

Goal state after:
case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ y ∈ s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
]

Goal state after:
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop

Tactic:
]

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirectedOrder ↑s

Tactic:
]

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirectedOrder ↑s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) id

Tactic:
]

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) id
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case inr
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
⊢ atTop = atTop

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop = atTop

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto (fun x ↦ ↑(f x)) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (fun x ↦ ↑(f x)) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (fun x ↦ f ↑x) atTop l

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (fun x ↦ f ↑x) atTop l

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k a : ℕ
h : k ≤ a
⊢ a ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k b : ℕ
x✝ : 0 ≤ b
⊢ b ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto f atTop l ↔ Tendsto f atTop l

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k : ℕ
hk : 0 < k
a b : ℕ
x✝ : 1 ≤ b
⊢ a ≤ k * b + (k - 1) ↔ a ≤ k * b + (k - 1)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ b

pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ k - 1 < k

Tactic:
]

Goal state after:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ k - 1 < k
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeInf α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a
hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a

Tactic:
]

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : SemilatticeInf α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a
hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b
hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b

Tactic:
]

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b
hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩

Tactic:
]

Goal state after:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩

Tactic:
]

Goal state after:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩
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 simpa [← span_int_eq_addSubgroupClosure] using 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
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mp.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ ↑s'' ⊆ ↑(span R ↑s')

Tactic:
]

Goal state after:
case mp.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ ↑s'' ⊆ ↑(span R ↑s')
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ ↑s' ⊆ ↑(span R s)

Tactic:
]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ ↑s' ⊆ ↑(span R s)
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
⊢ Module.Finite A B ↔ Module.Finite A B

Tactic:
]

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
⊢ WellFoundedGT (Submodule R M) ↔ IsWellFounded (Submodule R M) fun x1 x2 ↦ x1 > x2

Tactic:
]

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₀
⊢ R ∙ x = R ∙ x

Tactic:
]

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₀
⊢ x ∈ R ∙ x ⊔ N₀

Tactic:
]

Goal state after:
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₀
⊢ x ∈ R ∙ x ⊔ N₀
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) ↔
    ∀ (s : Set (Submodule R M)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x > m

Tactic:
]

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) ↔
    ∀ (a : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
]

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 ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0

Tactic:
]

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 ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0
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 : x ∈ LinearMap.ker (f ^ n)
⊢ (f ^ n) x = 0

Tactic:
]

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 : x ∈ LinearMap.ker (f ^ n)
⊢ (f ^ n) x = 0
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 : f x✝¹ = f x✝
⊢ f (r • x✝¹) = f (r • x✝)

Tactic:
]

Goal state after:
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 : f x✝¹ = f x✝
⊢ f (r • x✝¹) = f (r • x✝)
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case inl
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 : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : m ≤ l
⊢ (f ^ m).ker ≤ (f ^ m).ker

Tactic:
]

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
⊢ ⊥ = ⊥

Tactic:
]

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 s = span R s

Tactic:
]

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
⊢ 0 < a • b

Tactic:
]

Goal state after:
α : 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
⊢ 0 < a • b
Module: Mathlib.Order.Cofinal

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ ⋃ i ∈ s, Iio i ⊆ ⋃ i ∈ s, Iic i
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 < 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : a ∈ s
hb' : a ≤ b
⊢ a ∈ s
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₂
⊢ N₁ ⊔ N₂ = N₁ ⊔ N₂

Tactic:
]

Goal state after:
Module: Mathlib.Order.Cofinal

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ∃ x, ∀ y ∈ s, y < x
⊢ BddAbove s
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 < a • b

Tactic:
]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ∃ x, ∀ y ∈ s, y < x

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ∃ x, ∀ y ∈ s, y < x
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

Tactic:
]

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

Goal state after:
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, ⋯⟩
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:
]

Goal state after:
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, ⋯⟩
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:
]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : f b ⋖ f a
⊢ False

Tactic:
]

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : f b ⋖ f a
⊢ False
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
c : α
hb : c ⋖ a
⊢ False

Tactic:
]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
c : α
hb : c ⋖ a
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ (∀ (i : { s // IsCofinal s }), c ≤ lift.{v, u} #↑↑i) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s
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
⊢ Submodule.map f N = Submodule.map f N

Tactic:
]

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
⊢ (map f ⊤).FG

Tactic:
]

Goal state after:
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
⊢ (map f ⊤).FG
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ x, s = {x}
⊢ ∃ x, IsTop x

Tactic:
]

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ x, s = {x}
⊢ ∃ x, IsTop x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case h
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsTop t
⊢ IsTop t

Tactic:
]

Goal state after:
case h
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsTop t
⊢ IsTop t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ IsTop t

Tactic:
]

Goal state after:
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ IsTop t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ Nonempty α

Tactic:
]

Goal state after:
case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ Nonempty α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x

Tactic:
]

Goal state after:
α : Type u
inst✝ : Preorder α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (cof α = 0 ∨ ∃ x, IsTop x) ↔ ∃ x, IsTop x

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (cof α = 0 ∨ ∃ x, IsTop x) ↔ ∃ x, IsTop x