mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ ∀ (a b : α), e (a * b) = e a * e b

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ ∀ (a b : α), e (a * b) = e a * e b
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0

pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0

pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
H : f a = 0
⊢ 0 = 1 ↔ f a = 1

pp: case neg
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
H : ¬f a = 0
⊢ ↑⟨Units.mk0 (f a) H, ⋯⟩ = 1 ↔ f a = 1

Tactic:
<;>

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
H : f a = 0
⊢ 0 = 1 ↔ f a = 1

case neg
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
H : ¬f a = 0
⊢ ↑⟨Units.mk0 (f a) H, ⋯⟩ = 1 ↔ f a = 1
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ x = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), x = ↑(valueGroup.mk f r s hr hs)

Tactic:
obtain _ | ⟨x, hx⟩ := x

Goal state after:
case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), none = ↑(valueGroup.mk f r s hr hs)

case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
⊢ some ⟨x, hx⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx⟩ = ↑(valueGroup.mk f r s hr hs)
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ objD X (0 + 1) ≫ objD X 0 = 0

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1 + 1) ≫ objD X (n + 1) = 0

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ objD X (0 + 1) ≫ objD X 0 = 0

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1 + 1) ≫ objD X (n + 1) = 0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (objX Y 0).Factors ((objX X 0).arrow ≫ f.app (op ⦋0⦌))

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (objX Y (n✝ + 1)).Factors ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌))

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (objX Y 0).Factors ((objX X 0).arrow ≫ f.app (op ⦋0⦌))

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (objX Y (n✝ + 1)).Factors ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌))
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
y : ↑Y.toLinOrd
⊢ Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})

Tactic:
exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (objX Y (0 + 1)).factorThru ((objX X (0 + 1)).arrow ≫ f.app (op ⦋0 + 1⦌)) ⋯ ≫ (obj Y).d (0 + 1) 0 =
    (obj X).d (0 + 1) 0 ≫ (objX Y 0).factorThru ((objX X 0).arrow ≫ f.app (op ⦋0⦌)) ⋯

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (objX Y (n✝ + 1 + 1)).factorThru ((objX X (n✝ + 1 + 1)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      (obj Y).d (n✝ + 1 + 1) (n✝ + 1) =
    (obj X).d (n✝ + 1 + 1) (n✝ + 1) ≫ (objX Y (n✝ + 1)).factorThru ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (objX Y (0 + 1)).factorThru ((objX X (0 + 1)).arrow ≫ f.app (op ⦋0 + 1⦌)) ⋯ ≫ (obj Y).d (0 + 1) 0 =
    (obj X).d (0 + 1) 0 ≫ (objX Y 0).factorThru ((objX X 0).arrow ≫ f.app (op ⦋0⦌)) ⋯

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (objX Y (n✝ + 1 + 1)).factorThru ((objX X (n✝ + 1 + 1)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      (obj Y).d (n✝ + 1 + 1) (n✝ + 1) =
    (obj X).d (n✝ + 1 + 1) (n✝ + 1) ≫ (objX Y (n✝ + 1)).factorThru ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:

Tactic:
<;>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ l + j = j + l

Tactic:
<;>

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ l + j = j + l
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : k < j
h✝ : i ≤ k
⊢ False

Tactic:
<;>

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : k < j
h✝ : i ≤ k
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : k + 1 < i
⊢ False

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : k + 1 < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ k = k + 1 + 1

Tactic:
<;>

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ k = k + 1 + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : k < j
h✝ : k < i
⊢ False

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : k < j
h✝ : k < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False

Tactic:
<;>

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² h✝¹ : k < j
h✝ : k < i
⊢ False

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² h✝¹ : k < j
h✝ : k < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : k < j
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False

Tactic:
<;>

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : k < j
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : j ≤ k
h✝¹ : k < j
h✝ : k < i
⊢ k + 1 + 1 = k

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : j ≤ k
h✝¹ : k < j
h✝ : k < i
⊢ k + 1 + 1 = k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : j ≤ k
h✝¹ : k < j
h✝ : i ≤ k
⊢ False

Tactic:
<;>

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : j ≤ k
h✝¹ : k < j
h✝ : i ≤ k
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² h✝¹ : j ≤ k
h✝ : k + 1 < i
⊢ False

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² h✝¹ : j ≤ k
h✝ : k + 1 < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.pred ⋯) = j

pp: case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

pp: case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.pred ⋯) = j

pp: case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.pred ⋯) = j

case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.pred ⋯) = j

case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ j - 1 = j

pp: case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ False

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ j - 1 = j

case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : j < i + 1
h✝ : i < j
⊢ j - 1 = j

pp: case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : i + 1 ≤ j
h✝ : j + 1 ≤ i
⊢ False

Tactic:
<;>

Goal state after:
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : j < i + 1
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : i + 1 ≤ j
h✝ : j + 1 ≤ i
⊢ False
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ f.app (op ⦋n + 1⦌) ≫ (obj Y).d (n + 1) n = (obj X).d (n + 1) n ≫ f.app (op ⦋n⦌)

Tactic:
simp only [obj, ChainComplex.of_d, objD, Int.reduceNeg]
    rw [comp_sum, sum_comp]
    refine Finset.sum_congr rfl fun _ _ => ?_
    rw [comp_zsmul, zsmul_comp]
    congr 1
    symm
    apply f.naturality

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case zero
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ 0
⊢ (Hom.toOrderHom (factor_δ f 0 ≫ δ 0)) k = (Hom.toOrderHom f) k

pp: case succ
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
i✝ : Fin (n + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ i✝.succ
⊢ (Hom.toOrderHom (factor_δ f i✝.succ ≫ δ i✝.succ)) k = (Hom.toOrderHom f) k

Tactic:
<;>

Goal state after:
case zero
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ 0
⊢ (Hom.toOrderHom (factor_δ f 0 ≫ δ 0)) k = (Hom.toOrderHom f) k

case succ
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
i✝ : Fin (n + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ i✝.succ
⊢ (Hom.toOrderHom (factor_δ f i✝.succ ≫ δ i✝.succ)) k = (Hom.toOrderHom f) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ δ 0 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.succ

Tactic:
ext x
  fin_cases x
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ δ 1 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.castSucc

Tactic:
ext x
  fin_cases x
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩))) =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩))) =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩))) =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩))) =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨1, ⋯⟩))