mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

Tactic:
Preadditive.comp_zsmul,

Goal state after:
case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ (-1) ^ ↑b • PInfty.f (n + 1) ≫ X.δ b = 0
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.sup' H f) = s.sup' H fun i ↦ ⇑(f i)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.sup' H f) x✝ = s.sup' H (fun i ↦ ⇑(f i)) x✝
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i ↦ ⇑(f i)) x✝
Module: Mathlib.Topology.Homotopy.TopCat.Basic

Goal state before:
pp: X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
⊢ (G.comp F).h = X ◁ lift (𝟙 I) (𝟙 I) ≫ (α_ X I I).inv ≫ F.h ▷ I ≫ G.h

Tactic:
ext

Goal state after:
X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
x✝ : ↑(X ⊗ I)
⊢ (ConcreteCategory.hom (G.comp F).h) x✝ =
    (ConcreteCategory.hom (X ◁ lift (𝟙 I) (𝟙 I) ≫ (α_ X I I).inv ≫ F.h ▷ I ≫ G.h)) x✝
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Tactic:
rw [comp_id, Iso.inv_hom_id_app_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) = 0 ≫ Φ.f j
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.curry 0 = f₀

Tactic:
ext

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
a✝ : X
⊢ (F.curry 0) a✝ = f₀ a✝
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.curry 1 = f₁

Tactic:
ext

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
a✝ : X
⊢ (F.curry 1) a✝ = f₁ a✝
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.symm.symm = F

Tactic:
ext

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
x✝ : ↑I × X
⊢ F.symm.symm x✝ = F x✝
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft (Quotient.mk a✝)) (projRight (Quotient.mk a✝)) = Quotient.mk a✝

Tactic:
simp only [projLeft, projRight, ← Path.Homotopic.Quotient.mk_map]

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mk (a✝.map ⋯)) (Quotient.mk (a✝.map ⋯)) = Quotient.mk a✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ =
    CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫ CategoryTheory.eqToHom ⋯

Tactic:
ext

Goal state after:
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
i✝ : I
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ i✝ =
    (CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫ CategoryTheory.eqToHom ⋯) i✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝ = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝

Tactic:
ext

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝).1 = ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝).2 = ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit

Goal state before:
pp: x y : Path PUnit.unit PUnit.unit
⊢ x = y

Tactic:
ext

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic

Tactic:
constructor

Goal state after:
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → (ContinuousMap.id Y).Nullhomotopic

case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic → ContractibleSpace Y
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ pathComponent p = Set.univ

Tactic:
ext

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
x✝ : X
⊢ x✝ ∈ pathComponent p ↔ x✝ ∈ Set.univ
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Tactic:
constructor

Goal state after:
case left
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y

case right
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) ↔
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
constructor

Goal state after:
case mp
Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂) →
    PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)) →
    PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
            hcast ⋯ =
      H.diagonalPath' p

Tactic:
constructor

Goal state after:
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast ⋯ =
    H.diagonalPath' p

case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
          hcast ⋯ =
    H.diagonalPath' p
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ∈ I

Tactic:
constructor

Goal state after:
case pos.left
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2 * ↑x.2

case pos.right
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I

Tactic:
constructor

Goal state after:
case neg.left
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * (2 - 2 * ↑x.2)

case neg.right
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ≤ 1
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ weakEquivalences (CofibrantObject C) (homMk P.ι)

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance

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

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ I

Tactic:
constructor

Goal state after:
case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t

case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ∈ I

Tactic:
constructor

Goal state after:
case neg.left
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1

case neg.right
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.trans (Path.refl x₁) = p.reparam (fun t ↦ ⟨transReflReparamAux t, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t ↦ ⟨transReflReparamAux t, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯) x✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ∈ I

Tactic:
constructor

Goal state after:
case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t

case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ∈ I

Tactic:
constructor

Goal state after:
case pos.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4

case pos.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ∈ I

Tactic:
constructor

Goal state after:
case neg.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)

case neg.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A → A ≤ Subfunctor.equalizer f g

case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ A ≤ Subfunctor.equalizer f g → Subfunctor.equalizer f g = A
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : k = J.fst default ∨ k = J.snd default
⊢ c.π k ≫ m = c.π k ≫ hc.desc (isPushout.multicofork h h' s)

Tactic:
obtain rfl | rfl := this

Goal state after:
case inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.fst default) ≫ m = c.π (J.fst default) ≫ hc.desc (isPushout.multicofork h h' s)

case inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.snd default) ≫ m = c.π (J.snd default) ≫ hc.desc (isPushout.multicofork h h' s)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
constructor

Goal state after:
case mp
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
⊢ c.IsColimit →
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

case mpr
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
⊢ ((∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x) →
    c.IsColimit
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] = ⨆ i, stdSimplex.face {i}ᶜ

Tactic:
ext

Goal state after:
n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ x✝ ∈ ∂Δ[n].obj x✝¹ ↔ x✝ ∈ (⨆ i, stdSimplex.face {i}ᶜ).obj x✝¹
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) ↔ ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1

Tactic:
constructor

Goal state after:
case mp
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1

case mpr
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) ↔ ∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1

Tactic:
constructor

Goal state after:
case mp
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) → ∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1

case mpr
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
⊢ A = ∂Δ[n] ↔ ∂Δ[n] ≤ A ∧ A ≠ ⊤

Tactic:
constructor

Goal state after:
case mp
n : ℕ
A : Δ[n].Subcomplex
⊢ A = ∂Δ[n] → ∂Δ[n] ≤ A ∧ A ≠ ⊤

case mpr
n : ℕ
A : Δ[n].Subcomplex
⊢ ∂Δ[n] ≤ A ∧ A ≠ ⊤ → A = ∂Δ[n]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
this : 0 = i ∨ 0 = k
⊢ False

Tactic:
obtain rfl | rfl := this

Goal state after:
case neg.inl
n k : ℕ
h : k < n + 2
hk : ¬k = 0
hi : 0 < n + 4
h₀ : 0 < ⟨0, hi⟩
hₙ : ⟨0, hi⟩ < Fin.last (n + 3)
hS : {⟨0, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ False

case neg.inr
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
hk : ¬0 = 0
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔
    x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀

Tactic:
constructor

Goal state after:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) →
    x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ (x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀) →
    Rel' f g (Sum.inl x₁) (Sum.inl y₁)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s

Tactic:
constructor

Goal state after:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ (∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

Tactic:
constructor

Goal state after:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: n : ℕ
⊢ I ∂Δ[n].ι

Tactic:
constructor

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
sq : CommSq hf.desc Λ[n + 1, i].ι p b
⊢ ∃ φ, (∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj) ∧ φ ≫ p = b

Tactic:
exact ⟨sq.lift, fun j hj ↦ by simp [← ι_ι_assoc i j hj], by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Rel f g (Sum.inl ((ConcreteCategory.hom f) y₀)) (Sum.inr ((ConcreteCategory.hom g) y₀))

Tactic:
apply Rel.inl_inr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Rel.inl_inr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Rel.inl_inr

Goal state after: