mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (M.actRight ▷ Q.X)
            ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ((M.X ⊗ Y.X) ◁ g.hom) (M.X ◁ g.hom) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)

Tactic:
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (M.X ◁ g.hom ≫
        colimit.ι (parallelPair (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
          ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
⊢ { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x ≤
      { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y →
    x ≤ y

Tactic:
rintro ⟨k, x', y', hx, hy, h⟩

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
h : x' ≤ y'
⊢ x ≤ y
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
⊢ ∀ {i j : J} {f : i ⟶ j}, (D₁.W ⊔ D₂.W) f → (D₁.P ⊔ D₂.P) i

Tactic:
rintro _ _ _ (h | h)

Goal state after:
case inl
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₁.W f✝
⊢ (D₁.P ⊔ D₂.P) i✝

case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₂.W f✝
⊢ (D₁.P ⊔ D₂.P) i✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
⊢ ∀ {i j : J} {f : i ⟶ j}, (D₁.W ⊔ D₂.W) f → (D₁.P ⊔ D₂.P) j

Tactic:
rintro _ _ _ (h | h)

Goal state after:
case inl
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₁.W f✝
⊢ (D₁.P ⊔ D₂.P) j✝

case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₂.W f✝
⊢ (D₁.P ⊔ D₂.P) j✝
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
x : X
⊢ (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x

Tactic:
← hy,

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
x : X
⊢ (ConcreteCategory.hom (p.ι.app j')) (y' x) = (ConcreteCategory.hom (p.ι.app (j x))) (y x)
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁵ : HasPushouts C
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝³ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝² : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : HasIterationOfShape κ.ord.ToType C
Z₀ X Y : C
⊢ W.isLocal.isLocal ((succStruct W Z).toSucc Z₀)

Tactic:
exact isLocal_isLocal_toSucc W Z₀

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.F.obj j
h : f ≫ g₁ ≫ H.incl.app j = f ≫ g₂ ≫ H.incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk : (f ≫ g₁) ≫ H.F.map u = (f ≫ g₂) ≫ H.F.map u
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app j

Tactic:
have hg := iteration_map_succ_injectivity f hf
      (g₁ ≫ H.F.map u) (g₂ ≫ H.F.map u) (by simpa using hk)

Goal state after:
case refine_1
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.F.obj j
h : f ≫ g₁ ≫ H.incl.app j = f ≫ g₂ ≫ H.incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk : (f ≫ g₁) ≫ H.F.map u = (f ≫ g₂) ≫ H.F.map u
hg : (g₁ ≫ H.F.map u) ≫ (iteration W Z κ).map (homOfLE ⋯) = (g₂ ≫ H.F.map u) ≫ (iteration W Z κ).map (homOfLE ⋯)
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app j
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ EffectiveEpiFamily X_1 π},
      ∃ T ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π},
        T.FactorsThruAlong S f

Tactic:
rintro B₁ B₂ f S ⟨α, _, X₁, π₁, rfl, hS⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
⊢ ∃ T ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π},
    T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
⊢ ∃ c' t, f₁ ≫ (functor J κ).map t = f₂ ≫ (functor J κ).map t

Tactic:
let D₄' : DiagramWithUniqueTerminal J κ :=
    { toDiagram := D₄ D φ
      top := m₁
      isTerminal := hm₁
      uniq_terminal j hj := by
        obtain (hj' | ⟨⟨⟩⟩) := hj.prop
        · exact hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift hj')
        · rfl }

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
D₄' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₄ D φ;
  { toDiagram := __Diagram, top := m₁, isTerminal := hm₁, uniq_terminal := ⋯ }
⊢ ∃ c' t, f₁ ≫ (functor J κ).map t = f₂ ≫ (functor J κ).map t
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
⊢ Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck R

Tactic:
apply pullback_stable

Goal state after:
case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck (∐ fun i ↦ X i)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
rw [← extensive_regular_generate_coherent]
  exact isSheaf_sup (extensiveCoverage C) (regularCoverage C) F

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
intro X B π _ _

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ (Presieve.ofArrows (cylinder f g).Y fun j_1 ↦ (cylinder f g).toPullback j_1) ≤
    (Sieve.pullback
        (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
          (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
          (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
        (E.sieve₁' i.fst j.fst)).arrows

Tactic:
rintro - - ⟨k⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y : C
k : (cylinder f g).I₁ i j
⊢ (Sieve.pullback
        (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
          (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
          (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
        (E.sieve₁' i.fst j.fst)).arrows
    ((cylinder f g).toPullback k)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ pullHom (pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = pullFunctorObjHom w D (gf₁ ≫ f' j₁) gf₁ gf₂ ⋯ ⋯

Tactic:
by
    rw [pullFunctorObjHom_eq _ _ _ _ _ (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)]
    rw [← D.pullHom_hom g (q ≫ p) (q' ≫ p) (by rw [reassoc_of% hq])
      (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) (by rw [Category.assoc, w, reassoc_of% hf₁])
      (by rw [Category.assoc, w, reassoc_of% hf₂]) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂)
      (by cat_disch) (by cat_disch)]
    dsimp [pullHom]
    simp only [Functor.map_comp, Category.assoc]
    rw [F.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc _ _ _ _ _ _ _ _ (by cat_disch),
      mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app _ _ _ _ _ _ _ _ _ (by cat_disch)]

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

Goal state before:
pp: case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

Tactic:
· obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
            rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
⊢ ∃ φ,
    ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
let c : Cone ((Presieve.diagram (Sieve.pullback g S).arrows).op ⋙ G) :=
    { pt := F.obj (op Y)
      π :=
        { app := fun ⟨Z, hZ⟩ => F.map Z.hom.op ≫ (x _ hZ).app (op (Over.mk (𝟙 _)))
          naturality := by
            rintro ⟨Z₁, hZ₁⟩ ⟨Z₂, hZ₂⟩ ⟨⟨f : Z₂ ⟶ Z₁⟩⟩
            dsimp
            rw [id_comp, assoc]
            have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by simp)
            simp only [op_id, Functor.map_id, id_apply] at H
            let φ : Over.mk f.left ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk f.left
            have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op
            dsimp at H H' ⊢
            erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f] } }
  use (hG g).lift c
  intro Z p hp
  exact ((hG g).fac c ⟨Over.mk p, hp⟩)

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
⊢ (fun g ↦ end_.lift (fun j ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
      ((fun f ↦
          {
            app := fun j ↦
              uncurry
                (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
            naturality := ⋯ })
        f) =
    f

Tactic:
dsimp
    ext j
    dsimp
    simp only [curry_uncurry, end_.lift_π]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M ≫
          (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
            ((F.map p.op.toLoc).toFunctor.obj M) =
    pullFunctorObjHom w (ofObj M) (f₁ ≫ f' i₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map
          ((F.mapComp' (f (α i₂)).op.toLoc (p' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((F.mapComp' p.op.toLoc (f' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).hom.toNatTrans.app M)

Tactic:
pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' i₁) (f₂ ≫ p' i₂),

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M ≫
          (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
            ((F.map p.op.toLoc).toFunctor.obj M) =
    ((F.mapComp' (p' i₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' i₁).op.toLoc ⋯).inv.toNatTrans.app ((ofObj M).obj (α i₁)) ≫
        (ofObj M).hom (q ≫ p) (f₁ ≫ p' i₁) (f₂ ≫ p' i₂) ⋯ ⋯ ≫
          (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' i₂).op.toLoc ⋯).hom.toNatTrans.app ((ofObj M).obj (α i₂))) ≫
      (F.map f₂.op.toLoc).toFunctor.map
          ((F.mapComp' (f (α i₂)).op.toLoc (p' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((F.mapComp' p.op.toLoc (f' i₂).op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) ⋯).hom.toNatTrans.app M)
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
R : Sieve U
hR : R ∈ ⊥ U
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.flip.obj (op X)).map f)) y = x

Tactic:
by
    obtain rfl : R = ⊤ := by simpa using hR
    exact ⟨U, 𝟙 _, by simp, x, by simp⟩

Goal state after: