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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ (i : LTSeries α), RelSeries.head i = a → ↑i.length ≤ n) ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.head p = a → ↑p.length ≤ n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ (f m) n ∈ ⊥

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ (f m) n ∈ ⊥
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ (f m) n = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ (f m) n = 0
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ (f m) n = 0

Tactic:
hm,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ (f 0) n = 0
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ g.range ⊓ r ≤ map g q ↔ g.range ⊓ r ≤ map g q

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = map₂ f p q

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b ↦ (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b ↦ (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ q.toFun (Fin.last q.length) = q.toFun (Fin.last q.length)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
⊢ span R ((fun n ↦ (f m) n) '' ↑s) = span R (⇑(f m) '' ↑s)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
n : N
⊢ map₂ f s (R ∙ n) = map₂ f s (R ∙ n)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
M₂ : Type u_5
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
M₂ : Type u_5
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (¬∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n

Tactic:
]

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (¬∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ ⨆ i, ↑(↑i).length + n = ⨆ x, ↑(↑x).length + n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
M₂ : Type u_5
N₂ : Type u_6
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R M₂
inst✝ : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
M₂ : Type u_5
N₂ : Type u_6
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R M₂
inst✝ : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ height a ≤ height b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ height a ≤ height b
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑f ↔ Function.Surjective ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ height a < height b

Tactic:
]

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ height a < height b
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
⊢ f = 0 ↔ f = 0

Tactic:
]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ coheight a ≤ coheight b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ coheight a ≤ coheight b
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ↔ r.FiniteDimensional

Tactic:
]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ coheight a < coheight b

Tactic:
]

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ coheight a < coheight b
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional

Tactic:
]

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ IsEmpty { f // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }

Tactic:
]

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ IsEmpty { f // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin (↑lg + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lg) g ⋯
leq : lf = lg
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lg, g⟩, mg⟩

Tactic:
]

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin (↑lg + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lg) g ⋯
leq : lf = lg
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lg, g⟩, mg⟩
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' : f a' = p.head
⊢ coheight a' + 1 ≤ coheight a

Tactic:
]

Goal state after:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' : f a' = p.head
⊢ coheight a' + 1 ≤ coheight a
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin (↑lf + 1)), f i = g i
⊢ ∀ (x : Fin (↑lf + 1)), f x = g x

Tactic:
]

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin (↑lf + 1)), f i = g i
⊢ ∀ (x : Fin (↑lf + 1)), f x = g x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬∃ x, ∀ y ∈ Set.range fun x ↦ (↑x).length, y ≤ x
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
]

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬∃ x, ∀ y ∈ Set.range fun x ↦ (↑x).length, y ≤ x
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
]

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
]

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ p_1, ⨆ (_ : RelSeries.last p_1 = (RelSeries.eraseLast p).last), ↑p_1.length + 1

Tactic:
]

Goal state after:
case a.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ p_1, ⨆ (_ : RelSeries.last p_1 = (RelSeries.eraseLast p).last), ↑p_1.length + 1
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_1.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length) j.castSucc
⊢ j.castSucc = Fin.last { length := n + 1, toFun := s, step := h }.length

Tactic:
]

Goal state after:
case succ.refine_1.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length) j.castSucc
⊢ j.castSucc = Fin.last { length := n + 1, toFun := s, step := h }.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = y), ↑p.length + 1 ≤ height x

Tactic:
]

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = y), ↑p.length + 1 ≤ height x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_1.refine_1
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    (Fin.castLE ⋯ ∘ ⇑i) j
⊢ Fin.last { length := n + 1, toFun := s, step := h }.length = j.castSucc

Tactic:
]

Goal state after:
case succ.refine_1.refine_1
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    (Fin.castLE ⋯ ∘ ⇑i) j
⊢ Fin.last { length := n + 1, toFun := s, step := h }.length = j.castSucc
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬∃ x_1, ∀ y ∈ Set.range fun x_2 ↦ (↑x_2).length, y ≤ x_1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬∃ x_1, ∀ y ∈ Set.range fun x_2 ↦ (↑x_2).length, y ≤ x_1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ coheight x = ⊤ ↔ ∀ (n : ℕ), ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
convert! height_eq_top_iff (α := αᵒᵈ) (x := x) using 2 with n
  constructor <;> (intro ⟨p, hp, hl⟩; use p.reverse; constructor <;> simpa)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderBot α
h : ⊥ < x
⊢ ¬IsMin x

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderBot α
h : ⊥ < x
⊢ ¬IsMin x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderTop α
h : x < ⊤
⊢ ¬IsMax x

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderTop α
h : x < ⊤
⊢ ¬IsMax x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
h : ↑n < ↑m
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
h : ↑n < ↑m
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n