mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    D₁.hom (q ≫ f i) q (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯

Tactic:
this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
        D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯ =
    D₁.hom (q ≫ f i) q (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : F.p₁ p.snd = pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫ F.p₁ p.snd =
    ((cylinderHom f g).comp f).h₀ p

Tactic:
this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : F.p₁ p.snd = pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫
      pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst)) =
    ((cylinderHom f g).comp f).h₀ p
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯ ≫ pullback.snd (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫ F.p₂ p.snd =
    pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫ g.h₀ p.fst

Tactic:
this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯ ≫ pullback.snd (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫ F.p₂ p.snd =
    pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫
      pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯ ≫ pullback.snd (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
⊢ pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ =
    𝟙 ((F.map (𝟙 (X i)).op.toLoc).toFunctor.obj (D.obj i))

Tactic:
obtain ⟨p, h₁, h₂⟩ := (sq i i).isPullback.exists_lift (𝟙 _) (𝟙 _) (by simp)

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ =
    𝟙 ((F.map (𝟙 (X i)).op.toLoc).toFunctor.obj (D.obj i))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ IsIso (pullback.lift fst snd h)

Tactic:
[

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ IsIso (pullback.lift fst snd h)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ pullHom (mor w φ Y₁.hom a₁ fac₁) g₁ Z.hom Z.hom ⋯ ⋯ = pullHom (mor w φ Y₂.hom a₂ fac₂) g₂ Z.hom Z.hom ⋯ ⋯

Tactic:
← dsimp% mor_precomp w φ Y₁.hom a₁ fac₁ _ _ _ hg₁ rfl,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ mor w φ Z.hom (g₁ ≫ a₁) ⋯ = pullHom (mor w φ Y₂.hom a₂ fac₂) g₂ Z.hom Z.hom ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| (α_ P₁ P₂ P₃).hom.app (Opposite.op X) ≫
    Φ.toPresheafFiber X x P₁ ▷ (P₂.obj (Opposite.op X) ⊗ P₃.obj (Opposite.op X)) ≫
      Φ.presheafFiber.obj P₁ ◁ (Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃)

Tactic:
← tensorHom_def

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| (α_ P₁ P₂ P₃).hom.app (Opposite.op X) ≫
    (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃)
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 : C
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ IsIso ((pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (𝟙 X)))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  exact fun _ ↦ (colimit.isColimit _).isIso_ι_app_of_isTerminal _
    (Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId X).op

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F R

Tactic:
exact H _ hR

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₁.op))
        ((ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
          (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))))) =
    (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₂.op))
        ((ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
          (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))))

Tactic:
[

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₁.op))
        ((ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
          (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))))) =
    (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₂.op))
        ((ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
          (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (eval S β ((ConcreteCategory.hom (S.map f.op)) s))) x =
    (ConcreteCategory.hom (eval S α s)) ((ConcreteCategory.hom f) x)

Tactic:
[

Goal state after:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (eval S β ((ConcreteCategory.hom (S.map f.op)) s))) x =
    (ConcreteCategory.hom (eval S α s)) ((ConcreteCategory.hom f) x)
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S'✝ : SubmonoidFunctor M'
p : M ⟶ M'
S'' : SubmonoidFunctor M''
S' : SubmonoidFunctor M'
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : ↑(M.obj U✝)
h : x✝ ∈ Submonoid.comap (MonCat.Hom.hom (p.app U✝)) (S'.obj U✝)
⊢ x✝ ∈ Submonoid.comap (MonCat.Hom.hom (M.map x✝¹)) (Submonoid.comap (MonCat.Hom.hom (p.app V✝)) (S'.obj V✝))

Tactic:
[

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S'✝ : SubmonoidFunctor M'
p : M ⟶ M'
S'' : SubmonoidFunctor M''
S' : SubmonoidFunctor M'
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : ↑(M.obj U✝)
h : x✝ ∈ Submonoid.comap (MonCat.Hom.hom (p.app U✝)) (S'.obj U✝)
⊢ x✝ ∈ Submonoid.comap (MonCat.Hom.hom (M.map x✝¹)) (Submonoid.comap (MonCat.Hom.hom (p.app V✝)) (S'.obj V✝))
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsColimit (Cofork.ofπ ((presheafToSheaf J D).map p) ⋯)

Tactic:
have := IsRegularEpiCategory.regularEpiOfEpi p

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝² : Epi ((presheafToSheaf J D).map f.hom)
this✝¹ : Epi ((presheafToSheaf J D).map i)
this✝ : IsIso ((presheafToSheaf J D).map i)
this : IsRegularEpi p
⊢ IsColimit (Cofork.ofπ ((presheafToSheaf J D).map p) ⋯)
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
α : ι' → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
exact ⟨pullFunctorEquivalence (p' := p') (q' := q') F (Iso.refl _)
    (by cat_disch) (by cat_disch), ⟨toDescentDataCompPullFunctorIso _ _ ≪≫
    Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _ ≪≫ Functor.leftUnitor _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : C
f : X ⟶ Y
⊢ (inverseAssociator C D E).map ((inl_ C (D ⊕ E)).map f) = (inl_ (C ⊕ D) E).map ((inl_ C D).map f)

Tactic:
by
  simp [inverseAssociator]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : D
f : X ⟶ Y
⊢ (inverseAssociator C D E).map ((inr_ C (D ⊕ E)).map ((inl_ D E).map f)) = (inl_ (C ⊕ D) E).map ((inr_ C D).map f)

Tactic:
by
  simp [inverseAssociator]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
⊢ πQ f₂ β = 0

Tactic:
← cancel_epi π,

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
⊢ π ≫ πQ f₂ β = π ≫ 0
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → b = c

Tactic:
by
  rintro a ha b hb c hc habc
  obtain rfl := hs ha hb hc habc
  simpa using habc.symm

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : CommMonoid R
f : α → β → R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∏ a ∈ s, ∏ b ∈ bipartiteAbove r t a, f a b = ∏ b ∈ t, ∏ a ∈ bipartiteBelow r s b, f a b

Tactic:
[

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : CommMonoid R
f : α → β → R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∏ a ∈ s, ∏ b ∈ bipartiteAbove r t a, f a b = ∏ b ∈ t, ∏ a ∈ bipartiteBelow r s b, f a b
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a ∈ s, #(bipartiteAbove r t a) = ∑ b ∈ t, #(bipartiteBelow r s b)

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a ∈ s, #(bipartiteAbove r t a) = ∑ b ∈ t, #(bipartiteBelow r s b)
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = b → a = c

pp: case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = c → a = b

Tactic:
· rintro rfl
    exact (add_left_cancel habc).symm

Goal state after:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = c → a = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b

Tactic:
[

Goal state after:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ↑(#s)
⊢ ∃ y ∈ t, b < ↑(#({x ∈ s | f x = y}))

Tactic:
[

Goal state after:
α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ↑(#s)
⊢ ∃ y ∈ t, b < ↑(#({x ∈ s | f x = y}))
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
ht : ↑(#s) < #t • b
⊢ ∃ y ∈ t, ↑(#({x ∈ s | f x = y})) < b

Tactic:
[

Goal state after:
α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
ht : ↑(#s) < #t • b
⊢ ∃ y ∈ t, ↑(#({x ∈ s | f x = y})) < b
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ↑(#s)
⊢ ∃ y ∈ t, b ≤ ↑(#({x ∈ s | f x = y}))

Tactic:
[

Goal state after:
α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ↑(#s)
⊢ ∃ y ∈ t, b ≤ ↑(#({x ∈ s | f x = y}))