mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
x✝ : ι
i✝ : ↑(g ⁻¹' {x✝})
j✝ : ↑(f ⁻¹' {x✝})
⊢ o.matrixDecomposition.toFun (w + z) x✝ i✝ j✝ =
    (o.matrixDecomposition.toFun w + o.matrixDecomposition.toFun z) x✝ i✝ j✝

Tactic:
dsimp [biproduct.components]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
x✝ : ι
i✝ : ↑(g ⁻¹' {x✝})
j✝ : ↑(f ⁻¹' {x✝})
⊢ eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ (w + z) ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ w ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯ +
      eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ z ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w : R
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
x✝ : ι
i✝ : ↑(g ⁻¹' {x✝})
j✝ : ↑(f ⁻¹' {x✝})
⊢ o.matrixDecompositionAddEquiv.toFun (w • z) x✝ i✝ j✝ =
    ((RingHom.id R) w • o.matrixDecompositionAddEquiv.toFun z) x✝ i✝ j✝

Tactic:
dsimp [biproduct.components]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w : R
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
x✝ : ι
i✝ : ↑(g ⁻¹' {x✝})
j✝ : ↑(f ⁻¹' {x✝})
⊢ eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ (w • z) ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯ =
    w • eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ z ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ HasColimitsOfShape J (CardinalDirectedPoset κ)

Tactic:
by
    have := isFiltered_of_isCardinalFiltered J κ
    infer_instance

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

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D₁ D₂ : DiagramWithUniqueTerminal J κ
hW : D₁.W = D₂.W
hP : D₁.P = D₂.P
⊢ D₁ = D₂

Tactic:
obtain ⟨D₁, top, h₁, h₁'⟩ := D₁
  obtain ⟨D₂, top', h₂, h₂'⟩ := D₂
  obtain rfl : D₁ = D₂ := by aesop
  obtain rfl : top = top' := h₂' _ h₁
  obtain rfl : h₁ = h₂ := by subsingleton
  rfl

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) ((hom f) x) = (hom (F.map (a x))) ((hom g) x)
⊢ ∃ l c b, ∀ (x : ToType X), a x ≫ b x = c

Tactic:
by
          let φ (x : X) : j ⟶ IsCardinalFiltered.max k hX :=
            a x ≫ IsCardinalFiltered.toMax k hX x
          exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩

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

Goal state before:
pp: ⊢ (ObjectProperty.singleton PUnit.{u + 1}).IsSeparating ∧
    ∀ ⦃X Y : Type u⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → Function.Surjective fun f ↦ f ≫ i) → IsIso i

Tactic:
refine ⟨isSeparator_punit, fun _ _ i hi₁ hi₂ ↦ ?_⟩

Goal state after:
x✝¹ x✝ : Type u
i : x✝¹ ⟶ x✝
hi₁ : Mono i
hi₂ : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    IsIso ((uliftYonedaEquiv.symm { down := x }).app (op Y))

Tactic:
rw [isIso_iff_bijective, ← Function.Bijective.of_comp_iff _ Equiv.ulift.{w}.symm.bijective,
    ← Function.Bijective.of_comp_iff' Equiv.ulift.{v}.bijective]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    Function.Bijective
      (⇑Equiv.ulift ∘ ⇑(ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := x }).app (op Y))) ∘ ⇑Equiv.ulift.symm)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
E : D
⊢ Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))

Tactic:
rw [Presieve.isSheaf_iff_preservesFiniteProducts]

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
E : D
⊢ PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app { as := a }))
      ((ConcreteCategory.hom (f.app (op X))) ((ConcreteCategory.hom i.hom) y)) =
    (ConcreteCategory.hom
        ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app { as := a }))
      x

Tactic:
simp only [Functor.comp_obj, Discrete.opposite_inverse_obj, Functor.op_obj, Discrete.functor_obj,
    Functor.mapCone_pt, Cone.whisker_pt, Cocone.op_pt, Cofan.mk_pt, Functor.const_obj_obj,
    Functor.mapCone_π_app, Cone.whisker_π, Cocone.op_π, Functor.whiskerLeft_app, NatTrans.op_app,
    Cofan.mk_ι_app]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (G.map (π a).op)) ((ConcreteCategory.hom (f.app (op X))) ((ConcreteCategory.hom i.hom) y)) =
    (ConcreteCategory.hom (G.map (π a).op)) x
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
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : IsSheaf (coherentTopology C) F
⊢ IsSheaf (coherentTopology C) (F ⋙ s)

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
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
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
⊢ IsSheaf (coherentTopology C) F

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
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
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
obtain ⟨_, hF₂⟩ := hF

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ ⦃Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ⦄
    (i j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a

Tactic:
intro ⟨Z⟩ ⟨i⟩ ⟨j⟩
    have hi := Over.w i.hom
    have hj := Over.w j.hom
    dsimp at hi hj
    let ij := PullbackCone.IsLimit.lift hc i.hom.left j.hom.left (by simp [hi, hj])
    refine ⟨Quiver.Hom.op (ObjectProperty.homMk (Over.homMk ij)), ?_, ?_⟩
    all_goals congr; aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ F.IsStackFor R.arrows

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.rwSeq "rw" (Tactic.optConfig []) (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] `isStackFor_iff)] "]") [])
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId `hF)
     []
     []
     ":="
     (Term.proj
      (Term.paren
       (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
       (Term.app `F.isPrestackFor' [(Term.hole "_") `hR])
       ")")
      "."
      `fullyFaithful))))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hF.full)))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hF.faithful)))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId (hygieneInfo `[anonymous]))
     []
     []
     ":="
     (Term.app `IsStack.essSurj_of_sieve [`F (Term.hole "_") `hR]))))
  []
  (Tactic.exact
   "exact"
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    F.map f ≫ (↑s Y).app (op (Over.mk (𝟙 (unop Y)))) = (↑s X).app (op (Over.mk (𝟙 (unop X)))) ≫ G.map f

Tactic:
rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f : X₂ ⟶ X₁⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ F.map (op f) ≫ (↑s (op X₂)).app (op (Over.mk (𝟙 (unop (op X₂))))) =
    (↑s (op X₁)).app (op (Over.mk (𝟙 (unop (op X₁))))) ≫ G.map (op f)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ (pullFunctor F ⋯).FullyFaithful

Tactic:
exact fullyFaithfulPullFunctor F hp h₁

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type (max u v)
w✝¹ : ι → C
f : (i : ι) → w✝¹ i ⟶ S
hR₁ : F.IsStackFor (Presieve.ofArrows w✝¹ f)
hR₂ : Sieve.generate (Presieve.ofArrows w✝¹ f) ∈ J S
ι' : Type (max u v)
w✝ : ι' → C
f' : (i : ι') → w✝ i ⟶ S
h : Presieve.ofArrows w✝¹ f ≤ Presieve.ofArrows w✝ f'
⊢ F.IsStackFor (Presieve.ofArrows w✝ f')

Tactic:
rw [isStackFor_ofArrows_iff] at hR₁ ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type (max u v)
w✝¹ : ι → C
f : (i : ι) → w✝¹ i ⟶ S
hR₁ : (F.toDescentData f).IsEquivalence
hR₂ : Sieve.generate (Presieve.ofArrows w✝¹ f) ∈ J S
ι' : Type (max u v)
w✝ : ι' → C
f' : (i : ι') → w✝ i ⟶ S
h : Presieve.ofArrows w✝¹ f ≤ Presieve.ofArrows w✝ f'
⊢ (F.toDescentData f').IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: case amalgamate
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
ih : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), ∃ i, Witness.eval hF ι t i = some (y✝ r hr)
⊢ ∃ i, Witness.eval hF ι t i = some t✝

Tactic:
choose x hx using ih

Goal state after:
case amalgamate
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x✝ : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
x : ⦃W : C⦄ → (r : W ⟶ Z✝) → R✝ r → Witness K ι W
hx : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), Witness.eval hF ι t (x r hr) = some (y✝ r hr)
⊢ ∃ i, Witness.eval hF ι t i = some t✝
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows (↾fun x_1 ↦ x)
this : (↾fun x ↦ { down := true }) = ↾fun x ↦ { down := false }
⊢ False

Tactic:
simp [ConcreteCategory.hom_ext_iff] at this

Goal state after:
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
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app U✝)) (S.obj U✝) ≤
    Submonoid.comap (MonCat.Hom.hom (M'.map i)) (Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝))

Tactic:
by
    rw [← Submonoid.map_le_iff_le_comap, Submonoid.map_map, ← MonCat.hom_comp, ← p.naturality,
      MonCat.hom_comp, ← Submonoid.map_map]
    grw [S.map_le]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ χ' = h.χ m

Tactic:
by
    have : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow :=
      sq.of_iso (Iso.refl _) (Iso.refl _) (h.isoΩ₀.symm) (Iso.refl _)
        (by simp) (h.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
    exact h.uniq this

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ IsPullback m (from' F) (𝒞.χ m ≫ eΩ.hom) t

Tactic:
rw [eΩ₀.comp_inv_eq.mp (Subsingleton.elim (from' F ≫ eΩ₀.inv) (𝒞.χ₀ F))]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ IsPullback m (𝒞.χ₀ F ≫ eΩ₀.hom) (𝒞.χ m ≫ eΩ.hom) t
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
    (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
        (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
      x₁ = y₁

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃

Tactic:
· simpa using! (mono_iff_injective (m.app X)).mp (inferInstance)

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
X : C
D D' : ComposableArrows EInt 2
φ : D ⟶ D'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ (evaluation C C).obj X).map φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ (evaluation C C).obj X) ⋙ shiftFunctor C 1).map
        φ

Tactic:
by
    obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D
    obtain ⟨a', b', c', f', g', rfl⟩ := mk₂_surjective D'
    exact NatTrans.congr_app (t.ω₁δ_naturality a b c (leOfHom f) (leOfHom g)
      a' b' c' (leOfHom f') (leOfHom g') φ) X

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree (↑u ×ˢ ↑v)

Tactic:
exact hu.prod hv

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Tactic:
by
  have h₁ := ceil_lt_add_one hx.le
  have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith
  calc
    _ ≤ exp (1 - x) / (x + 1) := ?_
    _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr
    _ < _ := by gcongr
  rw [le_div_iff₀ (add_pos hx zero_lt_one), ← le_div_iff₀' (exp_pos _), ← exp_sub, neg_mul,
    sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x]
  exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)

Goal state after: