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

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
i : ℕ
hi : i < p.toList.length
⊢ i < p.length + 1

Tactic:
simpa using

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
i : ℕ
hi : i < p.toList.length
⊢ i < p.length + 1
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
⊢ g (x - y) = 0

Tactic:
simpa using

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
⊢ g x = g y
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1.left
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
z : M
hz : f z = x - y
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]

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

Goal state before:
pp: R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
⊢ (∃ l, g ∘ₗ l = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e

Tactic:
simpa using

Goal state after:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
⊢ (∃ l, g ∘ₗ l = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
tfae_1_iff_3 : (∃ l, g ∘ₗ l = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ (∃ l, l ∘ₗ f = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e

Tactic:
simpa using

Goal state after:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
tfae_1_iff_3 : (∃ l, g ∘ₗ l = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ (∃ l, l ∘ₗ f = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 0 < p.length.sub 0

Tactic:
simpa using

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ ¬p.length = 0
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : 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
⊢ motive p

Tactic:
convert! singleton p.head
      ext n
      · exact heq
      simp [show n = 0 by lia, apply_zero]

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

Tactic:
simpa using

Goal state after:
case hl
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length
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:
exact height_le

Goal state after:
Module: Mathlib.Order.RelSeries

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

Goal state after:
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
⊢ (q.toFun i.castSucc, q.toFun i.succ) ∈ r
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
this : map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Tactic:
simpa using

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
this : map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (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
this : map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))
⊢ map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)

Tactic:
simpa using

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
this : map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))
⊢ map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)
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
hfg : ∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0
x : N
⊢ g x = 0 ↔ ∃ y, f y = x

Tactic:
simpa using

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.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
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N
⊢ (f.range.liftQ g h) (Submodule.Quotient.mk x) = 0 ↔ Submodule.Quotient.mk x = 0

Tactic:
simpa using

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
⊢ g x = 0 ↔ ∃ y, f y = x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
l' : RelSeries r
hl' : l.length < l'.length
⊢ n + 1 < l'.length + 1

Tactic:
simpa using

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
l' : RelSeries r
hl' : l.length < l'.length
⊢ n < l'.length
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.Injective ⇑(f.range.liftQ g ⋯)

Tactic:
simpa using

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
h : Function.Exact ⇑f ⇑g
⊢ g.ker = f.range
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
this : ↑(RelSeries.snoc p y ⋯).length ≤ height (RelSeries.snoc p y ⋯).last
⊢ ↑p.length + 1 ≤ height y

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
this : ↑(RelSeries.snoc p y ⋯).length ≤ height (RelSeries.snoc p y ⋯).last
⊢ ↑p.length + 1 ≤ height y
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
⊢ ↑n + 1 ≤ height b

Tactic:
| coe n =>

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
⊢ ↑n + 1 ≤ coheight b

Tactic:
| coe n =>

Goal state after:
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
⊢ ↑(p.cons x hx).length ≤ coheight a

Tactic:
obtain ⟨a', haa', ha'⟩ := h a p.head (by grind)

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
⊢ ↑(p.cons x hx).length ≤ coheight a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b
a : α
this : coheight (OrderDual.toDual a) = coheight (OrderDual.toDual (f a))
⊢ height a = height (f a)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b
a : α
this : coheight (OrderDual.toDual a) = coheight (OrderDual.toDual (f a))
⊢ height a = height (f a)
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

Tactic:
simpa using

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.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 using

Goal state after:
α : 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
⊢ p.toFun i < p.toFun j
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = 0 ↔ IsMin x

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = 0 ↔ ∀ (b : α), ¬b < x
Module: Mathlib.Order.KrullDimension

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

Tactic:
simpa using

Goal state after:
case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

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

Tactic:
cases hn : n with

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case right
α : 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
⊢ ↑n ≤ height (RelSeries.eraseLast p).last

Tactic:
simpa using

Goal state after:
case right
α : 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
⊢ ↑n ≤ height (p.toFun ⟨n, ⋯⟩)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Preorder α
⊢ (∃ x, (∃ b, b < x) ∧ ∃ b, x < b) → ∃ i, 1 < ↑i.length

Tactic:
· rintro ⟨x, ⟨y, hxy⟩, z, hzx⟩
    exact ⟨⟨2, ![y, x, z], fun i ↦ by fin_cases i <;> simpa⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
n : ℕ
⊢ ↑n ≤ m

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
n : ℕ
⊢ ↑n ≤ m
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
simpa using

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
⊢ ↑n + coheight a ≤ ⨆ p, ↑p.length

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, height a + coheight a)

Tactic:
by
  apply le_antisymm
  · rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_le_coe]
    apply ciSup_mono (by bddDefault) (by simp)
  · wlog hnottop : krullDim α < ⊤
    · simp_all
    rw [krullDim_eq_iSup_length, WithBot.coe_le_coe]
    apply iSup_le
    intro a
    have : height a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (height_le_krullDim a) hnottop)
    have : coheight a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (coheight_le_krullDim a) hnottop)
    cases hh : height a with
    | top => simp_all
    | coe n =>
      cases hch : coheight a with
      | top => simp_all
      | coe m =>
        obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
        obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
        apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ krullDim α < ↑⊤

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ krullDim α < ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin p.length
⊢ ((p.toFun i.castSucc).untop ⋯, (p.toFun i.succ).untop ⋯) ∈ {(a, b) | a < b}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin p.length
⊢ p.toFun i.castSucc < p.toFun i.succ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : CommSemiring A
inst✝⁷ : Module A M
inst✝⁶ : Module A N
inst✝⁵ : SMulCommClass R A M
inst✝⁴ : CommSemiring S
inst✝³ : Module S M
inst✝² : SMulCommClass R S M
inst✝¹ : SMulCommClass A S M
inst✝ : CompatibleSMul R A M N
x✝⁴ x✝³ x✝² : M ⊗[R] N
x✝¹ : ∃ a, (mapOfCompatibleSMul R A S M N) a = x✝³
x✝ : ∃ a, (mapOfCompatibleSMul R A S M N) a = x✝²
x : M ⊗[A] N
hx : (mapOfCompatibleSMul R A S M N) x = x✝³
y : M ⊗[A] N
hy : (mapOfCompatibleSMul R A S M N) y = x✝²
⊢ (mapOfCompatibleSMul R A S M N) (x + y) = x✝³ + x✝²

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : CommSemiring A
inst✝⁷ : Module A M
inst✝⁶ : Module A N
inst✝⁵ : SMulCommClass R A M
inst✝⁴ : CommSemiring S
inst✝³ : Module S M
inst✝² : SMulCommClass R S M
inst✝¹ : SMulCommClass A S M
inst✝ : CompatibleSMul R A M N
x✝⁴ x✝³ x✝² : M ⊗[R] N
x✝¹ : ∃ a, (mapOfCompatibleSMul R A S M N) a = x✝³
x✝ : ∃ a, (mapOfCompatibleSMul R A S M N) a = x✝²
x : M ⊗[A] N
hx : (mapOfCompatibleSMul R A S M N) x = x✝³
y : M ⊗[A] N
hy : (mapOfCompatibleSMul R A S M N) y = x✝²
⊢ (mapOfCompatibleSMul R A S M N) x + (mapOfCompatibleSMul R A S M N) y = x✝³ + x✝²
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
n : ℕ
⊢ height ↑n = ↑n

Tactic:
| coe n =>

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
r✝ : ℤ
m : M
p : P
r : ℕ
ih : (↑r • m) ⊗ₜ[R] p = m ⊗ₜ[R] (↑r • p)
⊢ ((↑r + 1) • m) ⊗ₜ[R] p = m ⊗ₜ[R] ((↑r + 1) • p)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
r✝ : ℤ
m : M
p : P
r : ℕ
ih : (↑r • m) ⊗ₜ[R] p = m ⊗ₜ[R] (↑r • p)
⊢ (r • m) ⊗ₜ[R] p = r • m ⊗ₜ[R] p
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
r✝ : ℤ
m : M
p : P
r : ℕ
ih : (-↑r • m) ⊗ₜ[R] p = m ⊗ₜ[R] (-↑r • p)
⊢ ((-↑r - 1) • m) ⊗ₜ[R] p = m ⊗ₜ[R] ((-↑r - 1) • p)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
r✝ : ℤ
m : M
p : P
r : ℕ
ih : (-↑r • m) ⊗ₜ[R] p = m ⊗ₜ[R] (-↑r • p)
⊢ (-(r • m)) ⊗ₜ[R] p = m ⊗ₜ[R] (-(r • p))
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ∀ (x : R) (y : M), (lift (lsmul R M ∘ₗ (mul R R) r)) (x ⊗ₜ[R] y) = ((lsmul R M) r ∘ₗ lift (lsmul R M)) (x ⊗ₜ[R] y)

Tactic:
intro x a

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r x : R
a : M
⊢ (lift (lsmul R M ∘ₗ (mul R R) r)) (x ⊗ₜ[R] a) = ((lsmul R M) r ∘ₗ lift (lsmul R M)) (x ⊗ₜ[R] a)
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n✝ n : ℕ
⊢ mulLeft R a ^ n * mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a

Tactic:
Module.End.mul_eq_comp,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n✝ n : ℕ
⊢ (mulLeft R a ^ n) ∘ₗ mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a