mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr.inl
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
hι : IsEmpty ι
⊢ a * ⨆ i, f i ≤ d

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr.inr.top
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
h : ∀ (i : ι), a * f i ≤ ⊤
⊢ a * ⨆ i, f i ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
htop : ⨆ i, f i = ⊤
⊢ ↑d < ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
a : ↥p
b : ↥q
hab : ↑a + ↑b = x
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = a ∧ s = b
⊢ ((ofIsComplProd h).toFun ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) φ)) (↑a + ↑b) = φ (↑a + ↑b)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ∀ (u : ↥T.ker), 0 u = T ↑u

Tactic:
simp

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

Goal state before:
pp: case refine_2.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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x✝ : M
⊢ f x✝ = (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝¹ x✝ : α
⊢ (x✝¹, x✝) ∈ ∅ → (x✝, x✝¹) ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝¹ x✝ : α
⊢ (x✝¹, x✝) ∈ Set.univ → (x✝, x✝¹) ∈ Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length
⊢ (x.toList[i], x.toList[i + 1]) ∈ r

Tactic:
convert! x.step ⟨i, by simpa [toList] using h⟩ <;> apply List.get_ofFn

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ ∅ → (x✝¹, x✝) ∈ ∅ → (x✝², x✝) ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ Set.univ → (x✝¹, x✝) ∈ Set.univ → (x✝², x✝) ∈ Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
⊢ s.toFun 0 ∈ {x | x ∈ s}

Tactic:
simp [mem_def]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
⊢ s.toFun 1 ∈ {x | x ∈ s}

Tactic:
simp [mem_def]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
right✝ : ∀ (y : α → β), (fun f_1 ↦ Function.graph f_1 = Function.graph f) y → y = f
x : α
⊢ ∃! b, (x, b) ∈ Function.graph f

Tactic:
simp

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

Goal state before:
pp: case refine_4
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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
x✝¹ : { l // g ∘ₗ l = LinearMap.id }
x✝ : P
⊢ ↑((fun e ↦ ⟨↑(↑e).symm ∘ₗ inr R M P, ⋯⟩)
          ((fun l ↦ ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩) x✝¹))
      x✝ =
    ↑x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case refine_5.fst
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
e : N ≃ₗ[R] M × P
hf : Injective ⇑(↑e.symm ∘ₗ inl R M P)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x✝ : M × P
⊢ (e
        ((↑((fun l ↦ ⟨(LinearEquiv.ofBijective ((↑e.symm ∘ₗ inl R M P) ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩)
                ((fun e_1 ↦ ⟨↑(↑e_1).symm ∘ₗ inr R M P, ⋯⟩) ⟨e, ⋯⟩))).symm
          x✝)).1 =
    (e ((↑⟨e, ⋯⟩).symm x✝)).1

Tactic:
simp

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

Goal state before:
pp: case refine_5.snd
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
e : N ≃ₗ[R] M × P
hf : Injective ⇑(↑e.symm ∘ₗ inl R M P)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x✝ : M × P
⊢ (e
        ((↑((fun l ↦ ⟨(LinearEquiv.ofBijective ((↑e.symm ∘ₗ inl R M P) ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm, ⋯⟩)
                ((fun e_1 ↦ ⟨↑(↑e_1).symm ∘ₗ inr R M P, ⋯⟩) ⟨e, ⋯⟩))).symm
          x✝)).2 =
    (e ((↑⟨e, ⋯⟩).symm x✝)).2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B✝) * #(map f A✝)
p1 : Gᵐᵒᵖ × Gᵐᵒᵖ
h1 : p1 ∈ map f B✝ ×ˢ map f A✝
p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
h2 : p2 ∈ map f B✝ ×ˢ map f A✝
hne : p1 ≠ p2
hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2
hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2
⊢ ∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2

Tactic:
simp_rw [mem_product] at h1 h2 ⊢

Goal state after:
G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B✝) * #(map f A✝)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2
hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2
h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝
h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝
⊢ ∃ p1,
    (p1.1 ∈ A✝ ∧ p1.2 ∈ B✝) ∧
      ∃ p2, (p2.1 ∈ A✝ ∧ p2.2 ∈ B✝) ∧ p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case hl
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).toList.length = (p.toList ++ q.toList).length

Tactic:
simp

Goal state after:
case hl
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ p.length + q.length + 1 + 1 = p.length + 1 + (q.length + 1)
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
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 : ↑m < ↑i
⊢ ⋯ ▸ p.toFun (m.castSucc.castPred ⋯) = p.toFun ⟨↑m, ⋯⟩.castSucc

Tactic:
simp

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
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 : ↑m < ↑i
⊢ ⋯ ▸ p.toFun (m.succ.castPred ⋯) = p.toFun ⟨↑m, ⋯⟩.succ

Tactic:
simp

Goal state after:
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 : ↑m < ↑i
⊢ p.toFun (m.succ.castPred ⋯) = p.toFun ⟨↑m + 1, ⋯⟩
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2.right
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✝ : N
⊢ g x✝ = (snd R M P ∘ₗ ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯)) x✝

Tactic:
simp

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
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 : ↑m = ↑i
⊢ ⋯ ▸ p.toFun (m.castSucc.castPred ⋯) = p.toFun m

Tactic:
simp

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

Goal state before:
pp: case refine_4
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
x✝¹ : { l // l ∘ₗ f = LinearMap.id }
x✝ : N
⊢ ↑((fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) ((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩) x✝¹)) x✝ = ↑x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case refine_5.fst
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
e : N ≃ₗ[R] M × P
hg : Surjective ⇑(snd R M P ∘ₗ ↑e)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x : N
⊢ (↑((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod (snd R M P ∘ₗ ↑e)) ⋯, ⋯⟩)
            ((fun e_1 ↦ ⟨fst R M P ∘ₗ ↑↑e_1, ⋯⟩) ⟨e, ⋯⟩))
        x).1 =
    (↑⟨e, ⋯⟩ x).1

Tactic:
simp

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

Goal state before:
pp: case refine_5.snd
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
e : N ≃ₗ[R] M × P
hg : Surjective ⇑(snd R M P ∘ₗ ↑e)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x : N
⊢ (↑((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod (snd R M P ∘ₗ ↑e)) ⋯, ⋯⟩)
            ((fun e_1 ↦ ⟨fst R M P ∘ₗ ↑↑e_1, ⋯⟩) ⟨e, ⋯⟩))
        x).2 =
    (↑⟨e, ⋯⟩ x).2

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝⁸ : Monoid R
inst✝⁷ : Monoid S
inst✝⁶ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction S B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction T C
⊢ ∀ (x y : A),
    (DistribMulActionHom.toMulActionHom 0).toFun (x * y) =
      (DistribMulActionHom.toMulActionHom 0).toFun x * (DistribMulActionHom.toMulActionHom 0).toFun y

Tactic:
simp

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
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
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun i.succ

Tactic:
simp only [Fin.pred_succ, eq_rec_constant]

Goal state after:
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
⊢ p.toFun m = p.toFun i.succ
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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case toFun_eq
α : Type u_1
r : SetRel α α
p : RelSeries r
x✝ : Fin (p.reverse.reverse.length + 1)
⊢ p.reverse.reverse.toFun x✝ = (p.toFun ∘ Fin.cast ⋯) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
a : α
h : (a, s.head) ∈ r
i : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (s.cons a h).length + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ (singleton r x).toList ++ p.toList = x :: p.toList

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ x :: l ≠ []

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ (fromListIsChain (x :: l) ⋯ ⋯).toList = ((fromListIsChain l l_ne_nil hl).cons x ⋯).toList

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
a : α
h : (s.last, a) ∈ r
i : Fin (s.length + 1)
⊢ s.length + 1 + 1 = (s.snoc a h).length + 1

Tactic:
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.tail hp).toList.length = p.toList.tail.length

Tactic:
simp

Goal state after:
case refine_1
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ (p.cons x hx).length ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ ((p.cons x hx).tail ⋯).toList = p.toList

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
hi : i < p.eraseLast.toList.length
h2 : i < p.toList.dropLast.length
⊢ p.eraseLast.toList[i] = p.toList.dropLast[i]

Tactic:
simp

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
⊢ motive p

Tactic:
let {n : ℕ} (heq : p.length = n) : motive p := by
    induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      · simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have ne0 : p.length ≠ 0 := by simp [heq]
      have len : p.eraseLast.length = d := by simp [heq]
      convert! snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)
      exact (p.snoc_self_eraseLast ne0).symm

Goal state after:
α : 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
this : {n : ℕ} → p.length = n → motive p :=
  fun {n} heq ↦
    Nat.recAux (motive := fun {n} ↦ (p : RelSeries r) → p.length = n → motive p) (fun p heq ↦ ⋯.mpr (singleton p.head))
      (fun d hd p heq ↦
        have ne0 := ⋯;
        have len := ⋯;
        ⋯.mpr (snoc p.eraseLast p.last ⋯ (hd p.eraseLast len)))
      n p heq
⊢ motive p
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (x : RelSeries {(a, b) | a < b}),
    ⨆ (_ : ({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).head = a),
        ↑({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).length =
      ⨆ (_ : x.last = a), ↑x.length

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
h : p.last = q.head
i : Fin (p.length + 1)
⊢ p.length + 1 ≤ (p.smash q h).length + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∀ (i : Fin 0), (![inst✝.some] i.castSucc, ![inst✝.some] i.succ) ∈ r

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ { length := 0, toFun := ![inst✝.some], step := ⋯ }.length = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
⊢ coheight a + 1 ≤ coheight b

Tactic:
by
  cases hfin : coheight a with
  | top =>
    have : ⊤ ≤ coheight b := by
      rw [← hfin]
      gcongr
    simp [this]
  | coe n =>
    apply Order.add_one_le_of_lt
    rw [← hfin]
    gcongr
    simp [hfin]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ↑(p.map f hf).length

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case singleton
α : 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
x : β
a : α
hp : (RelSeries.singleton {(a, b) | a < b} x).head = f a
⊢ ↑(RelSeries.singleton {(a, b) | a < b} x).length ≤ coheight a

Tactic:
simp

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
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = RelSeries.last p

Tactic:
simp

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
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
simp

Goal state after: