mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) k) = F.Y (e.hom.s₁ (e.inv.s₁ k))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ e.inv.h₁ k ≫ e.hom.h₁ (e.inv.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ E.X (e.inv.s₀ (e.hom.s₀ i)) = E.X i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ IsIso (e.hom.h₀ i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ E.Y (e.inv.s₁ (e.hom.s₁ k)) = E.Y ((congrIndexOneOfEq ?m.87 ?m.88) k)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.s₁ (e.hom.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ IsIso (e.hom.h₁ k)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.leftOp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f : E.Hom F
X✝ Y✝ Z✝ x✝² x✝¹ : WalkingMulticospan E.multicospanShape
x✝ : x✝¹ ⟶ x✝²
⊢ (match x✝¹, x✝², WalkingMulticospan.Hom.id x✝¹ ≫ x✝ with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      WalkingMulticospan.Hom.id
        (match x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
    | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) =
    (match x✝¹, x✝¹, WalkingMulticospan.Hom.id x✝¹ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) ≫
      match x✝¹, x✝², x✝ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ D
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.rightOp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.leftOp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.rightOp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f : E.Hom F
X✝ Y✝ Z✝ : WalkingMulticospan E.multicospanShape
a✝ : E.multicospanShape.R
⊢ (match WalkingMulticospan.left (E.multicospanShape.fst a✝), WalkingMulticospan.right a✝,
      WalkingMulticospan.Hom.fst a✝ ≫ WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      WalkingMulticospan.Hom.id
        (match x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
    | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) =
    (match WalkingMulticospan.left (E.multicospanShape.fst a✝), WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.fst a✝ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) ≫
      match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : (Functor.const J).obj (K.obj c.pt) ⟶ (Functor.const J).obj B :=
  (Functor.constComp J c.pt K).inv ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
⊢ K.map (c.π.app j) ≫ (F.obj j).hom =
    (((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).obj
        j).hom

Tactic:
convert! (nat_trans_from_is_connected z j (Classical.arbitrary J)) <;> simp [z]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
⊢ K.map (c.π.app j) ≫ (F.obj j).hom =
    (((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).obj
        j).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
      homMk (c.π.app Y) ⋯ =
    homMk (c.π.app X) ⋯ ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f : E.Hom F
X✝ Y✝ Z✝ : WalkingMulticospan E.multicospanShape
a✝ : E.multicospanShape.R
⊢ (match WalkingMulticospan.left (E.multicospanShape.snd a✝), WalkingMulticospan.right a✝,
      WalkingMulticospan.Hom.snd a✝ ≫ WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      WalkingMulticospan.Hom.id
        (match x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
    | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) =
    (match WalkingMulticospan.left (E.multicospanShape.snd a✝), WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.snd a✝ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) ≫
      match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
⊢ (proj K B).mapCone (raiseCone c) = c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
t : IsLimit c
s : Cone F
⊢ K.map (t.lift ((proj K B).mapCone s)) ≫ (raiseCone c).pt.hom = s.pt.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
⊢ ∀ (i : E.multicospanShape.L),
    (𝟭 (WalkingMulticospan E.multicospanShape)).obj (WalkingMulticospan.left i) =
      (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).obj (WalkingMulticospan.left i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K✝ : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K✝ B
c : Cone (F ⋙ proj K✝ B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ m = homMk (t.lift ((proj K✝ B).mapCone s)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x✝¹)) ≫ ((proj K B).mapCone c✝).π.app x✝ = x✝¹.π.app x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
s : Cone (K✝ ⋙ proj K B)
m : s.pt ⟶ ((proj K B).mapCone c✝).pt
fac : ∀ (j : J), m ≫ ((proj K B).mapCone c✝).π.app j = s.π.app j
⊢ K.map m ≫ c✝.pt.hom = (CreatesConnected.raiseCone s).pt.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
⊢ PreservesColimitsOfShape J (proj B K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
D✝ : Type u_1
inst✝³ : Category.{v_1, u_1} D✝
K : C ⥤ D✝
X : C
B : D✝
inst✝² : IsConnected J
inst✝¹ : HasLimitsOfShape J C
inst✝ : PreservesLimitsOfShape J K
D : J ⥤ CostructuredArrow K B
⊢ PreservesLimit D (CostructuredArrow.toOver K B)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
D✝ : Type u_1
inst✝³ : Category.{v_1, u_1} D✝
K : C ⥤ D✝
X : C
B : D✝
inst✝² : IsConnected J
inst✝¹ : HasColimitsOfShape J C
inst✝ : PreservesColimitsOfShape J K
D : J ⥤ StructuredArrow B K
⊢ PreservesColimit D (StructuredArrow.toUnder B K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).obj (WalkingMulticospan.right x✝) =
    (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).obj (WalkingMulticospan.right x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePullbackShape J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePushoutShape J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).map (WalkingMulticospan.Hom.fst x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).map (WalkingMulticospan.Hom.fst x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).map (WalkingMulticospan.Hom.snd x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).map (WalkingMulticospan.Hom.snd x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
⊢ ∀ (i : F.multicospanShape.L),
    (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left i) =
      (𝟭 (WalkingMulticospan F.multicospanShape)).obj (WalkingMulticospan.left i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right x✝) =
    (𝟭 (WalkingMulticospan F.multicospanShape)).obj (WalkingMulticospan.right x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g

Tactic:
by

Goal state after: