mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 < ↑m
⊢ y = p.toFun ⟨↑m - 1, ⋯⟩.succ

Tactic:
change Fin.insertNth _ _ _ _ = _
          rw [Fin.insertNth_apply_above]
          swap
          · exact hm.trans (lt_add_one _)
          simp only [Fin.pred_succ, eq_rec_constant, Fin.succ_mk]
          congr
          exact Fin.ext <| Eq.symm <| Nat.succ_pred_eq_of_pos (lt_trans (Nat.zero_lt_succ _) hm)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.h
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ ↑i + 1 < ↑m + 1

Tactic:
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
⊢ ↑i + 1 ≤ p.length

Tactic:
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
hi : ↑i + 1 ≤ p.length
⊢ 0 < ↑i + 1

Tactic:
lia

Goal state after:
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
⊢ p.length + 1 - (↑i + 1) = p.length - (↑i + 1) + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.reverse.reverse = p

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_1
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : 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)
⊢ n = 0

Tactic:
lia

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
⊢ comap g r.mkQ.ker = comap q.mkQ (q.mkQ ∘ₗ f).range ↔ g.range ⊓ r ≤ map g q

Tactic:
range_comp,

Goal state after:
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
⊢ comap g r.mkQ.ker = comap q.mkQ (map q.mkQ f.range) ↔ g.range ⊓ r ≤ map g q
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:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.e'_2
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
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' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc a ⋯
⊢ p.length = p.length - 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : 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)
⊢ n = 0

Tactic:
lia

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

Goal state after:
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 + 1 = p.length

Tactic:
lia

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.flip q p = map₂ f p q

Tactic:
by
  rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]
  rfl

Goal state after:
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' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ p.length = p.length - 1 + 1

Tactic:
lia

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

Goal state before:
pp: ι : Sort uι
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
t : Submodule R N
⊢ map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, span R (image2 (fun m n ↦ (f m) n) ↑(s i) ↑t)

Tactic:
← span_iUnion,

Goal state after:
ι : Sort uι
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
t : Submodule R N
⊢ map₂ f (span R (⋃ i, ↑(s i))) (span R ↑t) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑(s i) ↑t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
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
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, span R (image2 (fun m n ↦ (f m) n) ↑s ↑(t i))

Tactic:
← span_iUnion,

Goal state after:
ι : Sort uι
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
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (span R (⋃ i, ↑(t i))) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑s ↑(t i))
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:
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:
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:
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:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.e'_4.e'_2
α : 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 + 1 + ↑i = j + ↑i + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : p'.length + (p.length - ↑i) ≤ p.length
⊢ p'.length ≤ ↑i

Tactic:
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

Tactic:
intro hfg

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
hfg : ∀ (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: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ p.length - ↑i + ↑i = p.length

Tactic:
lia

Goal state after:
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:
intro hfg

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
hfg : ∀ (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:
· intro H l
    obtain ⟨l', hl'⟩ := H (l.length + 1)
    exact ⟨l', by simp [hl']⟩

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

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:
lia

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
⊢ p.length - (m - n) = n

Tactic:
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:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : 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 - (m - n) = n

Tactic:
lia

Goal state after:
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
⊢ p.length ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply height_le
    intro p hp
    cases hlen : p.length with
    | zero => simp
    | succ n =>
      apply le_iSup_of_le p.eraseLast.last
      apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by lia))
      rw [height_add_const]
      apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ n < p.length + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ n < p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ a✝ < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
by_cases! hfin : height a < ⊤

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ p.length ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
⊢ j < p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
step : p.toFun ⟨j, ⋯⟩ < p.toFun ⟨j + 1, ⋯⟩
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, ⋯⟩ + ↑i
⊢ j < p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
p : LTSeries ℤ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, ⋯⟩ + ↑i
step : p.toFun ⟨j, ⋯⟩ < p.toFun ⟨j + 1, ⋯⟩
⊢ p.toFun ⟨i, hi⟩ + ↑(j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + ↑i

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ Fintype.card α < s.length + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ j < i

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ i < i + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ i + 1 < p.length + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
i : Fin (p.length - 1)
⊢ ↑i + 1 < p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ p.length - 1 + 1 = p.length

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
S : Type u_4
inst✝⁴ : CommSemiring S
inst✝³ : Module S A
inst✝² : SMulCommClass S A A
inst✝¹ : IsScalarTower S A A
inst✝ : CompatibleSMul A A R S
a : A
⊢ ↑R ((mul S A) a) = (mul R A) a

Tactic:
by
  ext x
  simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f x ≤ f (p.toFun i)
q' : LTSeries α := RelSeries.drop p i
q : LTSeries ↑(⇑f ⁻¹' {f x}) := { length := q'.length, toFun := fun j ↦ ⟨q'.toFun j, ⋯⟩, step := ⋯ }
this✝ : p.length ≤ m + (p.length - (m + 1))
this : p.length > m
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ lTensor M (f - g) = lTensor M f - lTensor M g

Tactic:
← coe_lTensorHom

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M) (f - g) = (lTensorHom M) f - (lTensorHom M) g
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1, ∃ z ∈ a, a_1 • z = x) ↔ x ∈ a

Tactic:
refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1, ∃ z ∈ a, a_1 • z = x) → x ∈ a
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 * x = 1

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
⊢ 1 + 0 * x = 1

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
⊢ 1 + 0 = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
⊢ 0 * x + 1 = 1

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
⊢ 0 + 1 = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime x (y + x * z)
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at h ⊢
  exact h.of_add_mul_left_left

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

Goal state before:
pp: case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1

Tactic:
Nat.add_eq_one_iff,

Goal state after:
case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m = 0 ∧ b * n = 1 ∨ a * m = 1 ∧ b * n = 0
⊢ m = 1 ∨ n = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
n : ℕ
⊢ ↑n • 1 = ↑n

Tactic:
rw [Nat.cast_smul_eq_nsmul, nsmul_one]

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap 1 = 1

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ comap (↑(opLinearEquiv R)) 1 = 1

Tactic:
ext
  simp

Goal state after: