mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

Tactic:
constructor
  · introv H hαX hαY
    rw [H c' (mapPair αX αY) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> assumption) (.of_discrete _)]
    constructor
    · intro H
      exact ⟨H _, H _⟩
    · rintro H ⟨⟨⟩⟩
      exacts [H.1, H.2]
  · introv H F' hα h
    let X' := F'.obj ⟨WalkingPair.left⟩
    let Y' := F'.obj ⟨WalkingPair.right⟩
    have : F' = pair X' Y' := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X', Y']
    clear_value X' Y'
    subst this
    change BinaryCofan X' Y' at c'
    rw [H c' _ _ _ (NatTrans.congr_app hα ⟨WalkingPair.left⟩)
        (NatTrans.congr_app hα ⟨WalkingPair.right⟩)]
    constructor
    · rintro H ⟨⟨⟩⟩
      exacts [H.1, H.2]
    · intro H
      exact ⟨H _, H _⟩

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.102, ?u.101, v'', v, u'', u} Gr
⊢ ∀ {W X Y Z : D} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen

Tactic:
intro W X Y Z f g h i _ H

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.102, ?u.101, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case h_map
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := ⋯
⊢ ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y), F.map f ≍ (Discrete.functor F').map f

Tactic:
· rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
      simp [F']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ Nonempty (IsColimit c)

Tactic:
have : F = Discrete.functor F' := by
    apply Functor.hext
    · exact fun i ↦ rfl
    · rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
      simp [F']

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
⊢ Nonempty (IsColimit c)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType (F.obj (op V))
ht : (ConcreteCategory.hom (f.app (op V))) t = (ConcreteCategory.hom (G.map i.op)) s
j : W ⟶ V
⊢ (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map j.op)) t) =
    (ConcreteCategory.hom (G.map (j ≫ i).op)) s

Tactic:
rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
⊢ mapPair (α.app { as := 0 }) (Sigma.desc fun b ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι =
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).ι ≫
      (const (Discrete WalkingPair)).map i

Tactic:
ext ⟨⟨⟩⟩
    · simpa only [pair_obj_left, Functor.const_obj_obj, pair_obj_right, Discrete.functor_obj,
        NatTrans.comp_app, mapPair_left, BinaryCofan.ι_app_left, BinaryCofan.mk_pt,
        BinaryCofan.mk_inl, Functor.const_map_app, extendCofan_pt,
        extendCofan_ι_app, Fin.cases_zero] using! congr_app e ⟨0⟩
    · dsimp
      ext j
      simpa only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app,
        Category.assoc, extendCofan_pt, Functor.const_obj_obj, NatTrans.comp_app, extendCofan_ι_app,
        Fin.cases_succ, Functor.const_map_app] using! congr_app e ⟨j.succ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
e₁ e₂ : Ext X Y i
⊢ e₁ = e₂

Tactic:
simp only [hX i hi]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
e : X ≅ Y
⊢ projectiveDimension X = projectiveDimension Y

Tactic:
by
  simp only [projectiveDimension]
  congr! 5
  exact ⟨fun h ↦ hasProjectiveDimensionLT_of_iso e _,
    fun h ↦ hasProjectiveDimensionLT_of_iso e.symm _⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ smul α φ 1 m = m

Tactic:
by
  apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)
  rintro Y f ⟨m₀, hm₀⟩
  rw [← hm₀, map_smul_eq α φ 1 m f.op 1 (by simp) m₀ hm₀, one_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom J j k
⊢ Decidable (f = g)

Tactic:
cases f <;> cases g <;> simp only [diagram.injEq] <;> infer_instance

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | Sieve.generate S ∈ J X}, ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f

Tactic:
by
    intro X Y f S (hS : Sieve.generate S ∈ J X)
    refine ⟨(Sieve.generate S).pullback f, ?_, fun Z g h => h⟩
    dsimp
    rw [Sieve.generate_sieve]
    exact J.pullback_stable _ hS

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

Goal state before:
pp: case refine_1.transitive
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleS : ∃ R ∈ J.coverings X, R ≤ S.arrows
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝² : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝¹ : PreservesLimit (cospan (f i) (f j)) F
this✝ : HasPullback (F.map (f i)) (F.map (f j))
this : Function.Bijective ⇑(ConcreteCategory.hom (P.map (pullbackComparison F (f i) (f j)).op))
⊢ (ConcreteCategory.hom
          (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x i) =
      (ConcreteCategory.hom
          (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)

Tactic:
exact this.1.eq_iff

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : GrothendieckTopology C
S : C
R : Sieve S
⊢ R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ J S

Tactic:
mem_toPrecoverage_iff,

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : GrothendieckTopology C
S : C
R : Sieve S
⊢ Sieve.generate R.arrows ∈ J S ↔ R ∈ J S
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.toPrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.toPrecoverage.coverings S

Tactic:
mem_toPrecoverage_iff,

Goal state after:
C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.toPrecoverage.coverings (X i)
⊢ Sieve.generate (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J S
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ J.toPrecoverage.coverings Y

Tactic:
mem_toPrecoverage_iff,

Goal state after:
C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Sieve.generate (Presieve.ofArrows P p₁) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
⊢ (trivial S).sieve₀ = ⊤

Tactic:
rw [PreZeroHypercover.sieve₀, Sieve.ofArrows, ← PreZeroHypercover.presieve₀]
  simp

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
u₁ : a ≫ b ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
⊢ (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2

Tactic:
simp [← reassoc_of% h₁, w, ← reassoc_of% u₁, ← pullback.condition]

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:
let z : (Functor.const J).obj (K.obj c.pt) ⟶ _ :=
      (CategoryTheory.Functor.constComp J c.pt K).inv ≫ Functor.whiskerRight c.π K ≫
        natTransInCostructuredArrow F

Goal state after:
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
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 ((CreatesConnected.raiseCone x✝¹).π.app x✝) = x✝¹.π.app x✝

Tactic:
CreatesConnected.raiseCone_π_app,

Goal state after:
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 (homMk (x✝¹.π.app x✝) ⋯) = x✝¹.π.app x✝
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
· exact Or.inl (mk_eq_bot_iff_zero.mpr h)

Goal state after:
case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case refine_1
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
h :
  Sieve.ofObjects U ⊤ ∈
    { sieves := fun X ↦ {S | ∀ x ∈ X, ∃ U, (∃ x, S.arrows x) ∧ x ∈ U}, top_mem' := ⋯, pullback_stable' := ⋯,
        transitive' := ⋯ }
      ⊤
x : T
⊢ ∃ i, x ∈ U i

pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1

Tactic:
· obtain ⟨V, ⟨u, ⟨i, ⟨hi⟩⟩⟩, hx⟩ := h x trivial
    use i, leOfHom hi hx

Goal state after:
case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case refine_1
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
    ∃! x,
      ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
        (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j
sf : (i : ι) → ToType (F.obj (op (U i)))
cpt : F.IsCompatible U sf
⊢ ∃! s,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i

pp: case refine_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j

Tactic:
· exact h _ cpt.sectionPairwise.prop

Goal state after:
case refine_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

Tactic:
refine
          ⟨[{   left := ⟨⟨⟩⟩
                right := single i
                hom := ObjectProperty.homMk (homOfLE (a.hom.le.trans (by simp))) },
              { left := ⟨⟨⟩⟩
                right := pair i i'
                hom := ObjectProperty.homMk (homOfLE
                  (le_inf ((a.hom.le).trans (by simp)) b.hom.le)) }, _],
                ?_, rfl⟩

Goal state after:
case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a },
      { left := { as := PUnit.unit }, right := single i, hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i i', hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := single i', hom := b }]