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

Tactic:
;

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

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

Goal state before:
pp: case 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 : ↑m = ↑i
⊢ ↑m < ↑i + 1

Tactic:
;

Goal state after:
case 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 : ↑m = ↑i
⊢ ↑m < ↑i + 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 : α := ⋯
y : α := ⋯
hm : ↑m = ↑i
⊢ ↑m = ↑i.castSucc

Tactic:
;

Goal state after:
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 : α := ⋯
y : α := ⋯
hm : ↑m = ↑i
⊢ ↑m = ↑i.castSucc
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_3
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
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ fst R M P ∘ₗ inl R M P = LinearMap.id

Tactic:
;

Goal state after:
case refine_3
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
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ fst R M P ∘ₗ inl R M P = LinearMap.id
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 : α := ⋯
y : α := ⋯
hm : ↑m = ↑i
⊢ ↑m.succ = ↑i.succ.castSucc

Tactic:
;

Goal state after:
α : 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 : α := ⋯
y : α := ⋯
hm : ↑m = ↑i
⊢ ↑m.succ = ↑i.succ.castSucc
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
⊢ ↑m + 1 = ↑i + 1

Tactic:
;

Goal state after:
α : 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
⊢ ↑m + 1 = ↑i + 1
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 }
⊢ (fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) ((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩) x✝) = x✝

Tactic:
;

Goal state after:
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 }
⊢ (fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) ((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩) x✝) = x✝
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:
;

Goal state after:
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✝
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
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝³ : NonUnitalNonAssocSemiring B₁
inst✝² : DistribMulAction R B₁
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
x y : A
⊢ Function.prod (⇑f) (⇑g) (x * y) = Function.prod (⇑f) (⇑g) x * Function.prod (⇑f) (⇑g) y

Tactic:
by simp only [Function.prod_apply, Prod.mk_mul_mk, map_mul]

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

Goal state before:
pp: R✝ : Type u
S✝ : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : MulAction R S
inst✝⁵ : DistribMulAction S A
inst✝⁴ : DistribMulAction S B
inst✝³ : DistribMulAction R A
inst✝² : DistribMulAction R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₙₐ[S] B
r : R
x : A
this : f ((r • 1) • x) = (r • 1) • f x
⊢ (↑f).toFun (r • x) = (MonoidHom.id R) r • (↑f).toFun x

Tactic:
;

Goal state after:
R✝ : Type u
S✝ : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : MulAction R S
inst✝⁵ : DistribMulAction S A
inst✝⁴ : DistribMulAction S B
inst✝³ : DistribMulAction R A
inst✝² : DistribMulAction R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₙₐ[S] B
r : R
x : A
this : f ((r • 1) • x) = (r • 1) • f x
⊢ (↑f).toFun (r • x) = (MonoidHom.id R) r • (↑f).toFun x
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:
;

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

Tactic:
;

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
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
⊢ m = i.succ
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 : α := ⋯
y : α := ⋯
hm : ↑i + 1 = ↑m
⊢ ↑m = ↑i.succ

Tactic:
;

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := ⋯
y : α := ⋯
hm : ↑i + 1 = ↑m
⊢ ↑m = ↑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:
;

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

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
⊢ (p.append (singleton r newLast) rel).head = p.head

Tactic:
;

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
⊢ (p.append (singleton r newLast) rel).head = p.head
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:
;

Goal state after:
case e'_4.e'_2
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1
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:
;

Goal state after:
α✝ : 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
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.mem.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.mem.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x y : N),
    x ∈ span R t →
      y ∈ span R t →
        (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) →
          (f a) y ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (x + y) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.mem.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R),
    ∀ x ∈ span R t,
      (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (a_1 • x) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ n ∈ span R t, (f 0) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (x y : M),
    x ∈ span R s →
      y ∈ span R s →
        (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
          (∀ n ∈ span R t, (f y) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
            ∀ n ∈ span R t, (f (x + y)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (a : R),
    ∀ x ∈ span R s,
      (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
        ∀ n ∈ span R t, (f (a • x)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
all_goals
      intros
      simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

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
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥

Tactic:
;

Goal state after:
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
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥
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:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin (p.length + 1)
x✝ : Fin p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castLE ⋯ x✝.castSucc) = p.toFun x✝.castSucc

Tactic:
;

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin (p.length + 1)
x✝ : Fin p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castLE ⋯ x✝.castSucc) = p.toFun x✝.castSucc
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective ⇑τ₁
h₂ : Function.Bijective ⇑τ₂
h₃ : Function.Injective ⇑τ₃
x✝ : M₁
⊢ (f'.toAddMonoidHom.comp τ₁.toAddMonoidHom) x✝ = (τ₂.toAddMonoidHom.comp f.toAddMonoidHom) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹² : Ring R
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective ⇑τ₁
h₂ : Function.Bijective ⇑τ₂
h₃ : Function.Injective ⇑τ₃
x✝ : M₁
⊢ (f'.toAddMonoidHom.comp τ₁.toAddMonoidHom) x✝ = (τ₂.toAddMonoidHom.comp f.toAddMonoidHom) x✝
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective ⇑τ₁
h₂ : Function.Bijective ⇑τ₂
h₃ : Function.Injective ⇑τ₃
x✝ : M₂
⊢ (g'.toAddMonoidHom.comp τ₂.toAddMonoidHom) x✝ = (τ₃.toAddMonoidHom.comp g.toAddMonoidHom) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹² : Ring R
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective ⇑τ₁
h₂ : Function.Bijective ⇑τ₂
h₃ : Function.Injective ⇑τ₃
x✝ : M₂
⊢ (g'.toAddMonoidHom.comp τ₂.toAddMonoidHom) x✝ = (τ₃.toAddMonoidHom.comp g.toAddMonoidHom) x✝
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
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:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
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
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:
;

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