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

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ 0 < ↑i + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.succ.rev = ⟨p.length - (↑i + 1), ⋯⟩.castSucc

pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.castSucc.rev = ⟨p.length - (↑i + 1), ⋯⟩.succ

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.succ.rev = ⟨p.length - (↑i + 1), ⋯⟩.castSucc
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.castSucc.rev = ⟨p.length - (↑i + 1), ⋯⟩.succ

Tactic:
·

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.castSucc.rev = ⟨p.length - (↑i + 1), ⋯⟩.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ (∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = x) → (∃ y, p.toFun y = x) ∨ x = newLast

pp: case mpr
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ (∃ y, p.toFun y = x) ∨ x = newLast → ∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = x

Tactic:
·

Goal state after:
case mp
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ (∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = x) → (∃ y, p.toFun y = x) ∨ x = newLast
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ (∃ y, p.toFun y = x) ∨ x = newLast → ∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = x

Tactic:
·

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ (∃ y, p.toFun y = x) ∨ x = newLast → ∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr.inl
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
i : Fin (p.length + 1)
⊢ ∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = p.toFun i

pp: case mpr.inr
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
rel : (p.last, x) ∈ r
⊢ ∃ y, (Fin.append p.toFun (singleton r x).toFun ∘ Fin.cast ⋯) y = x

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
i : Fin (p.length + 1)
⊢ ∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = p.toFun i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr.inr
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
rel : (p.last, x) ∈ r
⊢ ∃ y, (Fin.append p.toFun (singleton r x).toFun ∘ Fin.cast ⋯) y = x

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
rel : (p.last, x) ∈ r
⊢ ∃ y, (Fin.append p.toFun (singleton r x).toFun ∘ Fin.cast ⋯) y = x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_1
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ (p.tail hp).toList.length = p.toList.tail.length

pp: case refine_2
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
h1 : i < (p.tail hp).toList.length
h2 : i < p.toList.tail.length
⊢ (p.tail hp).toList[i] = p.toList.tail[i]

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ (p.tail hp).toList.length = p.toList.tail.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_2
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
h1 : i < (p.tail hp).toList.length
h2 : i < p.toList.tail.length
⊢ (p.tail hp).toList[i] = p.toList.tail[i]

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
h1 : i < (p.tail hp).toList.length
h2 : i < p.toList.tail.length
⊢ (p.tail hp).toList[i] = p.toList.tail[i]
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case length_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
heq : p.length = 0
⊢ p.length = (RelSeries.singleton r p.head).length

pp: case toFun_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
heq : p.length = 0
n : Fin (p.length + 1)
⊢ p.toFun n = ((RelSeries.singleton r p.head).toFun ∘ Fin.cast ⋯) n

Tactic:
·

Goal state after:
case length_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
heq : p.length = 0
⊢ p.length = (RelSeries.singleton r p.head).length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
    (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) →
      ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → p.length ≠ 0 → ↑p.length ≤ n
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ n

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ n

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
    (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) →
      ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → p.length ≠ 0 → ↑p.length ≤ n
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length - 1 < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case hl
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ p.eraseLast.toList.length = p.toList.dropLast.length

pp: case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ ∀ (i : ℕ) (h₁ : i < p.eraseLast.toList.length) (h₂ : i < p.toList.dropLast.length),
    p.eraseLast.toList[i] = p.toList.dropLast[i]

Tactic:
·

Goal state after:
case hl
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ p.eraseLast.toList.length = p.toList.dropLast.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ ∀ (i : ℕ) (h₁ : i < p.eraseLast.toList.length) (h₂ : i < p.toList.dropLast.length),
    p.eraseLast.toList[i] = p.toList.dropLast[i]

Tactic:
·

Goal state after:
case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ ∀ (i : ℕ) (h₁ : i < p.eraseLast.toList.length) (h₂ : i < p.toList.dropLast.length),
    p.eraseLast.toList[i] = p.toList.dropLast[i]
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case length_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
⊢ p.length = (RelSeries.singleton r p.head).length

pp: case toFun_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
n : Fin (p.length + 1)
⊢ p.toFun n = ((RelSeries.singleton r p.head).toFun ∘ Fin.cast ⋯) n

Tactic:
·

Goal state after:
case length_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
⊢ p.length = (RelSeries.singleton r p.head).length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case toFun_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
n : Fin (p.length + 1)
⊢ p.toFun n = ((RelSeries.singleton r p.head).toFun ∘ Fin.cast ⋯) n

Tactic:
·

Goal state after:
case toFun_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
n : Fin (p.length + 1)
⊢ p.toFun n = ((RelSeries.singleton r p.head).toFun ∘ Fin.cast ⋯) n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

pp: case mpr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n) → height a ≤ n

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a
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 : Set M
t : Set N
⊢ span R (image2 (fun m n ↦ (f m) n) s t) ≤ map₂ f (span R s) (span R t)

Tactic:
·

Goal state after:
case a
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 : Set M
t : Set N
⊢ span R (image2 (fun m n ↦ (f m) n) s t) ≤ map₂ f (span R s) (span R t)
Module: Mathlib.Order.KrullDimension

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n) → height a ≤ n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case left
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).succ) ∈
    r

pp: case right
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin q.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).succ) ∈
    r

Tactic:
·

Goal state after:
case left
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).succ) ∈
    r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length 0) = p.toFun i.succ

pp: case neg
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : ¬i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd (q.length + 1) ⟨↑i + 1, ⋯⟩) = p.toFun i.succ

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length 0) = p.toFun i.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case neg
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : ¬i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd (q.length + 1) ⟨↑i + 1, ⋯⟩) = p.toFun i.succ

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : ¬i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd (q.length + 1) ⟨↑i + 1, ⋯⟩) = p.toFun i.succ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ↑p.length ≤ height x

pp: case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ↑p.length ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hab
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ (RelSeries.eraseLast p).last < ?b

pp: case hbc
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ?b ≤ x

pp: case b
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ α

Tactic:
·

Goal state after:
case hab
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ (RelSeries.eraseLast p).last < ?b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.length - 1 < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hbc
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1, ⋯⟩.succ ≤ x

Tactic:
·

Goal state after:
case hbc
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1, ⋯⟩.succ ≤ x
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 = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)

Tactic:
by
  rw [← map₂_span_span, span_eq, span_eq]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_1
r : SetRel α α
q : RelSeries r
toFun✝ : Fin (0 + 1) → α
step✝ : ∀ (i : Fin 0), (toFun✝ i.castSucc, toFun✝ i.succ) ∈ r
h : { length := 0, toFun := toFun✝, step := step✝ }.last = q.head
⊢ ({ length := 0, toFun := toFun✝, step := step✝ }.smash q h).head =
    { length := 0, toFun := toFun✝, step := step✝ }.head

pp: case succ
α : Type u_1
r : SetRel α α
q : RelSeries r
n✝ : ℕ
toFun✝ : Fin (n✝ + 1 + 1) → α
step✝ : ∀ (i : Fin (n✝ + 1)), (toFun✝ i.castSucc, toFun✝ i.succ) ∈ r
h : { length := n✝ + 1, toFun := toFun✝, step := step✝ }.last = q.head
⊢ ({ length := n✝ + 1, toFun := toFun✝, step := step✝ }.smash q h).head =
    { length := n✝ + 1, toFun := toFun✝, step := step✝ }.head

Tactic:
·

Goal state after:
case zero
α : Type u_1
r : SetRel α α
q : RelSeries r
toFun✝ : Fin (0 + 1) → α
step✝ : ∀ (i : Fin 0), (toFun✝ i.castSucc, toFun✝ i.succ) ∈ r
h : { length := 0, toFun := toFun✝, step := step✝ }.last = q.head
⊢ ({ length := 0, toFun := toFun✝, step := step✝ }.smash q h).head =
    { length := 0, toFun := toFun✝, step := step✝ }.head
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
⊢ ↑p'.length ≤ height x

Tactic:
refine le_iSup₂_of_le p' ?_ le_rfl

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
⊢ p'.last ≤ x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r✝ : SetRel α α
β : Type u_2
s : SetRel β β
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
x✝ : Fin (↑i + 1)
j : ℕ
h : j < ↑i + 1
⊢ j < p.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r✝ : SetRel α α
β : Type u_2
s : SetRel β β
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
x✝ : Fin ↑i
j : ℕ
h : j < ↑i
⊢ j < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length + 1)
x✝ : Fin (p.length - ↑i + 1)
j : ℕ
h : j < p.length - ↑i + 1
⊢ j + ↑i < p.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length + 1)
x✝ : Fin (p.length - ↑i)
j : ℕ
h : j < p.length - ↑i
⊢ j + ↑i < p.length

Tactic:
by lia

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

Goal state before:
pp: case mp
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 : f.range ≤ g.ker
⊢ (∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0) → ∀ (x : N), g x = 0 ↔ ∃ y, f y = x

pp: case mpr
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 : f.range ≤ g.ker
⊢ (∀ (x : N), g x = 0 ↔ ∃ y, f y = x) → ∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0

Tactic:
·

Goal state after:
case mp
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 : f.range ≤ g.ker
⊢ (∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0) → ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n

pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
·

Goal state after:
case mp
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mpr
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 : f.range ≤ g.ker
⊢ (∀ (x : N), g x = 0 ↔ ∃ y, f y = x) → ∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0

Tactic:
·

Goal state after:
case mpr
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 : f.range ≤ g.ker
⊢ (∀ (x : N), g x = 0 ↔ ∃ y, f y = x) → ∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
·

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r✝ : SetRel α α
β : Type u_2
s : SetRel β β
γ : Type u_3
inst✝¹ : Preorder γ
inst✝ : Unique γ
x : RelSeries {(a, b) | a < b}
r : (RelSeries.singleton {(a, b) | a < b} default).length < x.length
⊢ 0 < x.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) ≤ height x

pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)

Tactic:
·

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)

Tactic:
·

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
p : LTSeries β
f : α → β
comap : ∀ ⦃x y : α⦄, f x < f y → x < y
surjective : Function.Surjective f
i j : Fin (p.length + 1)
h : i < j
⊢ f ((fun i ↦ ⋯.choose) i) < f ((fun i ↦ ⋯.choose) j)

Tactic:
simpa only [(surjective _).choose_spec] using p.strictMono h

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ m - n < p.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ m - n < p.length + 1

Tactic:
by lia

Goal state after: