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

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f.hom) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 0 } = { down := 1 }

pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : ¬(LinOrd.Hom.hom f.hom) a < m
h₂ : (LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 1 } = { down := 0 }

Tactic:
·

Goal state after:
case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f.hom) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 0 } = { down := 1 }
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0

Tactic:
·

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : ¬(LinOrd.Hom.hom f.hom) a < m
h₂ : (LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 1 } = { down := 0 }

Tactic:
·

Goal state after:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : ¬(LinOrd.Hom.hom f.hom) a < m
h₂ : (LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 1 } = { down := 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
⊢ ⊤.Factors (⊤.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✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).Factors
    ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).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
⊢ ⊤.Factors (⊤.arrow ≫ f.app (op ⦋0⦌))
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
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✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).Factors
    ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌))

Tactic:
·

Goal state after:
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✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).Factors
    ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌))
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case mpr
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
·

Goal state after:
case mpr
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f = 𝟙 Y

pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ

Tactic:
·

Goal state after:
case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f = 𝟙 Y
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ

Tactic:
·

Goal state after:
case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι

pp: case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e

Tactic:
·

Goal state after:
case left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e

Tactic:
·

Goal state after:
case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
have : HasEqualizer (𝟙 X) p := h X p hp

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ j ≤ j

Tactic:
by lia

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ j < n + 1

Tactic:
by lia

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ j + l < n + 1

Tactic:
by lia

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j < n + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)

pp: case h.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Tactic:
·

Goal state after:
case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Tactic:
·

Goal state after:
case h.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)

pp: case h.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p

Tactic:
·

Goal state after:
case h.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p

Tactic:
·

Goal state after:
case h.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
·

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
·

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖᵒᵖ

Tactic:
rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.succ
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h.left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ i ≫ e = 𝟙 Y

pp: case h.right
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ e ≫ i = p

Tactic:
·

Goal state after:
case h.left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ i ≫ e = 𝟙 Y
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
·

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.castSucc