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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ (RelSeries.snoc p x ⋯).last ≤ x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ ↑p.length + 1 ≤ ↑(RelSeries.snoc p x ⋯).length

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ + 1 ≤ ↑n ↔ ⊤ < ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ height ⊥ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ coheight ⊤ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
simp

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

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), False
x : α
⊢ ∀ (i : Fin 0), (x, x) ∈ {(a, b) | a < b}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
t : RelSeries {(a, b) | a ⋖ b}
i : Fin ((RelSeries.cons s ⊥ ⋯).length + 1) ↪ Fin (t.length + 1)
hi : t.toFun ∘ ⇑i = (RelSeries.cons s ⊥ ⋯).toFun
ht : t.head = ⊥ ∧ t.last = ⊤
j : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (RelSeries.cons s ⊥ ⋯).length + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
t : RelSeries {(a, b) | a ⋖ b}
i : Fin ((RelSeries.cons s ⊥ ⋯).length + 1) ↪ Fin (t.length + 1)
hi : t.toFun ∘ ⇑i = (RelSeries.cons s ⊥ ⋯).toFun
ht : t.head = ⊥ ∧ t.last = ⊤
x✝¹ x✝ : Fin (s.length + 1)
⊢ (fun j ↦ i (Fin.cast ⋯ j.succ)) x✝¹ = (fun j ↦ i (Fin.cast ⋯ j.succ)) x✝ → x✝¹ = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ 0 < ↑{ length := 1, toFun := ![x, y], step := ⋯ }.length

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (0 + 1) → α
h : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := 0, toFun := l, step := h }.length ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1) → α
hl : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0, toFun := l, step := hl }.length
⊢ ↑{ length := 0, toFun := l, step := hl }.length ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
⊢ (RelSeries.snoc s ⊤ ⋯).last = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ↑{ length := 0 + 1, toFun := l, step := hl }.length ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin ((RelSeries.snoc s ⊤ ⋯).length + 1) ↪ Fin (t.length + 1)
hi : t.toFun ∘ ⇑i = (RelSeries.snoc s ⊤ ⋯).toFun
ht : t.head = ⊥ ∧ t.last = ⊤
j : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (RelSeries.snoc s ⊤ ⋯).length + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ 1 < ↑{ length := 2, toFun := ![y, x, z], step := ⋯ }.length

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin ((RelSeries.snoc s ⊤ ⋯).length + 1) ↪ Fin (t.length + 1)
hi : t.toFun ∘ ⇑i = (RelSeries.snoc s ⊤ ⋯).toFun
ht : t.head = ⊥ ∧ t.last = ⊤
x✝¹ x✝ : Fin (s.length + 1)
⊢ (fun j ↦ i (Fin.cast ⋯ j.castSucc)) x✝¹ = (fun j ↦ i (Fin.cast ⋯ j.castSucc)) x✝ → x✝¹ = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length = ⊥ ↔ ∀ (l : LTSeries α), l.length < 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (x : α), height x ≤ height x + coheight x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁴ : CommSemiring R
inst✝³³ : CommSemiring R₂
inst✝³² : CommSemiring R₃
inst✝³¹ : Monoid R'
inst✝³⁰ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝²⁹ : AddCommMonoid M
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid P
inst✝²⁶ : AddCommMonoid Q
inst✝²⁵ : AddCommMonoid S
inst✝²⁴ : AddCommMonoid P'
inst✝²³ : AddCommMonoid Q'
inst✝²² : AddCommMonoid M₂
inst✝²¹ : AddCommMonoid N₂
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Q₂
inst✝¹⁸ : AddCommMonoid M₃
inst✝¹⁷ : AddCommMonoid N₃
inst✝¹⁶ : AddCommMonoid P₃
inst✝¹⁵ : AddCommMonoid Q₃
inst✝¹⁴ : DistribMulAction R' M
inst✝¹³ : Module R'' M
inst✝¹² : Module R M
inst✝¹¹ : Module R N
inst✝¹⁰ : Module R S
inst✝⁹ : Module R P'
inst✝⁸ : Module R Q'
inst✝⁷ : Module R₂ M₂
inst✝⁶ : Module R₂ N₂
inst✝⁵ : Module R₂ P₂
inst✝⁴ : Module R₂ Q₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₃ N₃
inst✝¹ : Module R₃ P₃
inst✝ : Module R₃ Q₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (f (s • m, n).1) (s • m, n).2 = (f (m, s • n).1) (m, s • n).2

Tactic:
hf

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁴ : CommSemiring R
inst✝³³ : CommSemiring R₂
inst✝³² : CommSemiring R₃
inst✝³¹ : Monoid R'
inst✝³⁰ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝²⁹ : AddCommMonoid M
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid P
inst✝²⁶ : AddCommMonoid Q
inst✝²⁵ : AddCommMonoid S
inst✝²⁴ : AddCommMonoid P'
inst✝²³ : AddCommMonoid Q'
inst✝²² : AddCommMonoid M₂
inst✝²¹ : AddCommMonoid N₂
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Q₂
inst✝¹⁸ : AddCommMonoid M₃
inst✝¹⁷ : AddCommMonoid N₃
inst✝¹⁶ : AddCommMonoid P₃
inst✝¹⁵ : AddCommMonoid Q₃
inst✝¹⁴ : DistribMulAction R' M
inst✝¹³ : Module R'' M
inst✝¹² : Module R M
inst✝¹¹ : Module R N
inst✝¹⁰ : Module R S
inst✝⁹ : Module R P'
inst✝⁸ : Module R Q'
inst✝⁷ : Module R₂ M₂
inst✝⁶ : Module R₂ N₂
inst✝⁵ : Module R₂ P₂
inst✝⁴ : Module R₂ Q₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₃ N₃
inst✝¹ : Module R₃ P₃
inst✝ : Module R₃ Q₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (f m) (s • (s • m, n).2) = (f (m, s • n).1) (m, s • n).2
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a, (injStrictMono (Fintype.card α)) a = { length := l, toFun := f, step := mf }

Tactic:
Subtype.exists

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a, ∃ (b : StrictMono a.snd), (injStrictMono (Fintype.card α)) ⟨a, b⟩ = { length := l, toFun := f, step := mf }
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : CommSemiring R₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
M : Type u_7
N : Type u_8
P₂ : Type u_17
P₃ : Type u_18
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P₂
inst✝⁵ : AddCommMonoid P₃
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R₂ P₂
inst✝¹ : Module R₃ P₃
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
h : P₂ →ₛₗ[σ₂₃] P₃
x✝¹ : M
x✝ : N
⊢ (h ∘ₛₗ lift f') (x✝¹ ⊗ₜ[R] x✝) = ((f'.compr₂ₛₗ h) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N →ₗ[R] P
g : P →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (g ∘ₗ lift f) (x✝¹ ⊗ₜ[R] x✝) = ((f.compr₂ g) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N) = LinearMap.id

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁹ : CommSemiring R
inst✝⁴⁸ : CommSemiring R₂
inst✝⁴⁷ : CommSemiring R₃
inst✝⁴⁶ : Monoid R'
inst✝⁴⁵ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁴ : AddCommMonoid M✝
inst✝⁴³ : AddCommMonoid N✝
inst✝⁴² : AddCommMonoid P
inst✝⁴¹ : AddCommMonoid Q
inst✝⁴⁰ : AddCommMonoid S✝
inst✝³⁹ : AddCommMonoid P'
inst✝³⁸ : AddCommMonoid Q'
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N₂
inst✝³⁵ : AddCommMonoid P₂
inst✝³⁴ : AddCommMonoid Q₂
inst✝³³ : AddCommMonoid M₃
inst✝³² : AddCommMonoid N₃
inst✝³¹ : AddCommMonoid P₃
inst✝³⁰ : AddCommMonoid Q₃
inst✝²⁹ : DistribMulAction R' M✝
inst✝²⁸ : Module R'' M✝
inst✝²⁷ : Module R M✝
inst✝²⁶ : Module R N✝
inst✝²⁵ : Module R S✝
inst✝²⁴ : Module R P'
inst✝²³ : Module R Q'
inst✝²² : Module R₂ M₂
inst✝²¹ : Module R₂ N₂
inst✝²⁰ : Module R₂ P₂
inst✝¹⁹ : Module R₂ Q₂
inst✝¹⁸ : Module R₃ M₃
inst✝¹⁷ : Module R₃ N₃
inst✝¹⁶ : Module R₃ P₃
inst✝¹⁵ : Module R₃ Q₃
inst✝¹⁴ : Module R P
inst✝¹³ : Module R Q
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✝ : M
⊢ ∀ (x : N),
    (let __spread.0 := (mk R M N) (x✝¹ + x✝);
        { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
        x =
      ((let __spread.0 := (mk R M N) x✝¹;
          { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }) +
          let __spread.0 := (mk R M N) x✝;
          { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
        x

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁹ : CommSemiring R
inst✝⁴⁸ : CommSemiring R₂
inst✝⁴⁷ : CommSemiring R₃
inst✝⁴⁶ : Monoid R'
inst✝⁴⁵ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁴ : AddCommMonoid M✝
inst✝⁴³ : AddCommMonoid N✝
inst✝⁴² : AddCommMonoid P
inst✝⁴¹ : AddCommMonoid Q
inst✝⁴⁰ : AddCommMonoid S✝
inst✝³⁹ : AddCommMonoid P'
inst✝³⁸ : AddCommMonoid Q'
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N₂
inst✝³⁵ : AddCommMonoid P₂
inst✝³⁴ : AddCommMonoid Q₂
inst✝³³ : AddCommMonoid M₃
inst✝³² : AddCommMonoid N₃
inst✝³¹ : AddCommMonoid P₃
inst✝³⁰ : AddCommMonoid Q₃
inst✝²⁹ : DistribMulAction R' M✝
inst✝²⁸ : Module R'' M✝
inst✝²⁷ : Module R M✝
inst✝²⁶ : Module R N✝
inst✝²⁵ : Module R S✝
inst✝²⁴ : Module R P'
inst✝²³ : Module R Q'
inst✝²² : Module R₂ M₂
inst✝²¹ : Module R₂ N₂
inst✝²⁰ : Module R₂ P₂
inst✝¹⁹ : Module R₂ Q₂
inst✝¹⁸ : Module R₃ M₃
inst✝¹⁷ : Module R₃ N₃
inst✝¹⁶ : Module R₃ P₃
inst✝¹⁵ : Module R₃ Q₃
inst✝¹⁴ : Module R P
inst✝¹³ : Module R Q
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
s : S
⊢ (lift
          {
            toFun := fun m ↦
              let __spread.0 := (mk R M N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }).toFun
      (s • 0) =
    (RingHom.id S) s •
      (lift
            {
              toFun := fun m ↦
                let __spread.0 := (mk R M N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ }).toFun
        0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ (⊥, RelSeries.head (p.map (fun a ↦ ↑a) ⋯)) ∈ {(a, b) | a < b}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (x : α), height ↑(Equiv.withTopSubtypeNe.symm x) + 1 = height x + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
h' : height (f x) = ⊤
⊢ height x ≤ (↑m + 1) * ⊤ + ↑m

Tactic:
simp

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
⊢ ∀ (a : M ⊗[R] N), 0 • a = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴¹ : CommSemiring R
inst✝⁴⁰ : CommSemiring R₂
inst✝³⁹ : CommSemiring R₃
inst✝³⁸ : Monoid R'
inst✝³⁷ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁶ : AddCommMonoid M
inst✝³⁵ : AddCommMonoid N
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid Q
inst✝³² : AddCommMonoid S
inst✝³¹ : AddCommMonoid P'
inst✝³⁰ : AddCommMonoid Q'
inst✝²⁹ : AddCommMonoid M₂
inst✝²⁸ : AddCommMonoid N₂
inst✝²⁷ : AddCommMonoid P₂
inst✝²⁶ : AddCommMonoid Q₂
inst✝²⁵ : AddCommMonoid M₃
inst✝²⁴ : AddCommMonoid N₃
inst✝²³ : AddCommMonoid P₃
inst✝²² : AddCommMonoid Q₃
inst✝²¹ : DistribMulAction R' M
inst✝²⁰ : Module R'' M
inst✝¹⁹ : Module R M
inst✝¹⁸ : Module R N
inst✝¹⁷ : Module R S
inst✝¹⁶ : Module R P'
inst✝¹⁵ : Module R Q'
inst✝¹⁴ : Module R₂ M₂
inst✝¹³ : Module R₂ N₂
inst✝¹² : Module R₂ P₂
inst✝¹¹ : Module R₂ Q₂
inst✝¹⁰ : Module R₃ M₃
inst✝⁹ : Module R₃ N₃
inst✝⁸ : Module R₃ P₃
inst✝⁷ : Module R₃ Q₃
inst✝⁶ : SMulCommClass R R' M
inst✝⁵ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁴ : Monoid R'₂
inst✝³ : DistribMulAction R'₂ M
inst✝² : SMulCommClass R R'₂ M
inst✝¹ : SMul R'₂ R'
inst✝ : IsScalarTower R'₂ R' M
s : R'₂
r : R'
x : M ⊗[R] N
⊢ (s • r) • 0 = s • r • 0

Tactic:
simp

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
⊢ (0 • m) ⊗ₜ[R] p = m ⊗ₜ[R] (0 • p)

Tactic:
simp

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 x : A
⊢ (↑R ((mul S A) a)) x = ((mul R A) a) x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toSpanSingleton R A 1) 1 = (Algebra.linearMap R A) 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
x : A ⊗[R] A
⊢ (mul' R A).toFun (a • 0) = (RingHom.id A) a • (mul' R A).toFun 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
f : A →ₙₐ[R] B
⊢ ∀ (x y : A), (↑f ∘ₗ LinearMap.mul' R A) (x ⊗ₜ[R] y) = (LinearMap.mul' R B ∘ₗ (↑f ⊗ₘ ↑f)) (x ⊗ₜ[R] y)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (x y : A),
    (f.toLinearMap ∘ₗ LinearMap.mul' R A) (x ⊗ₜ[R] y) =
      (LinearMap.mul' R B ∘ₗ (f.toLinearMap ⊗ₘ f.toLinearMap)) (x ⊗ₜ[R] y)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁵ : CommSemiring R
inst✝⁴⁴ : CommSemiring R₂
inst✝⁴³ : CommSemiring R₃
inst✝⁴² : Monoid R'
inst✝⁴¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁰ : AddCommMonoid M
inst✝³⁹ : AddCommMonoid N
inst✝³⁸ : AddCommMonoid P
inst✝³⁷ : AddCommMonoid Q
inst✝³⁶ : AddCommMonoid S
inst✝³⁵ : AddCommMonoid P'
inst✝³⁴ : AddCommMonoid Q'
inst✝³³ : AddCommMonoid M₂
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid P₂
inst✝³⁰ : AddCommMonoid Q₂
inst✝²⁹ : AddCommMonoid M₃
inst✝²⁸ : AddCommMonoid N₃
inst✝²⁷ : AddCommMonoid P₃
inst✝²⁶ : AddCommMonoid Q₃
inst✝²⁵ : DistribMulAction R' M
inst✝²⁴ : Module R'' M
inst✝²³ : Module R M
inst✝²² : Module R N
inst✝²¹ : Module R S
inst✝²⁰ : Module R P'
inst✝¹⁹ : Module R Q'
inst✝¹⁸ : Module R₂ M₂
inst✝¹⁷ : Module R₂ N₂
inst✝¹⁶ : Module R₂ P₂
inst✝¹⁵ : Module R₂ Q₂
inst✝¹⁴ : Module R₃ M₃
inst✝¹³ : Module R₃ N₃
inst✝¹² : Module R₃ P₃
inst✝¹¹ : Module R₃ Q₃
inst✝¹⁰ : SMulCommClass R R' M
inst✝⁹ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁸ : Monoid R'₂
inst✝⁷ : DistribMulAction R'₂ M
inst✝⁶ : SMulCommClass R R'₂ M
inst✝⁵ : SMul R'₂ R'
inst✝⁴ : DistribMulAction R'₂ N
inst✝³ : DistribMulAction R' N
inst✝² : CompatibleSMul R R'₂ M N
inst✝¹ : CompatibleSMul R R' M N
inst✝ : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x : M ⊗[R] N
⊢ (s • r) • 0 = s • r • 0

Tactic:
simp

Goal state after: