mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
x y : ↑(Opposite.unop (Opposite.op J)).1
h : φ x = φ y
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) y

Tactic:
by simpa [hφ]

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
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

Goal state after:
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
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
⊢ j = m

Tactic:
exfalso

Goal state after:
case inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
⊢ False
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 κ) κ
⊢ (functor J κ).Final

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

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
⊢ (functor J κ).Final
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 κ)
⊢ (functor J κ).Final

Tactic:
Functor.final_iff_of_isFiltered

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 κ)
⊢ (∀ (d : J), ∃ c, Nonempty (d ⟶ (functor J κ).obj c)) ∧
    ∀ {d : J} {c : DiagramWithUniqueTerminal J κ} (s s' : d ⟶ (functor J κ).obj c),
      ∃ c' t, s ≫ (functor J κ).map t = s' ≫ (functor J κ).map t
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
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
h : IsSheaf (extensiveTopology C) F
⊢ PreservesFiniteProducts F

Tactic:
rw [IsSheaf] at h

Goal state after:
case mp
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
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ PreservesFiniteProducts F
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
obtain ⟨Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpi _).mp hS

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔ Presheaf.IsSheaf (regularCoverage C).toGrothendieck F

Tactic:
rw [Presheaf.isSheaf_iff_isLimit_coverage]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).hom.toNatTrans.app
          ((F.map f₁.op.toLoc).toFunctor.obj M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map ((F.map g.op.toLoc).toFunctor.map φ) ≫
          (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).inv.toNatTrans.app
              ((F.map f₂.op.toLoc).toFunctor.obj M₂) ≫
            (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂

Tactic:
simp [mapComp'_inv_naturality_assoc, ← reassoc_of% Cat.Hom₂.comp_app]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ pullHom (pullHom φ g gf₁ gf₂ hgf₁ hgf₂) g' g'f₁ g'f₂ hg'f₁ hg'f₂ = pullHom φ (g' ≫ g) g'f₁ g'f₂ ⋯ ⋯

Tactic:
dsimp [pullHom]
  rw [Functor.map_comp_assoc, Functor.map_comp_assoc,
    F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app _ _ _ _ _ _ _ rfl (by aesop),
    F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc _ _ _ _ _ _ _ rfl (by aesop)]
  simp [mapComp'_inv_naturality_assoc, ← reassoc_of% Cat.Hom₂.comp_app]

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
hF : ∀ (S : C), ∀ R ∈ J S, F.IsStackFor R.arrows
S✝ : C
R : Sieve S✝
hR : R ∈ J S✝
⊢ (F.toDescentData fun f ↦ f.obj.hom).EssSurj

Tactic:
have := (isStackFor_iff _ _).1 (hF _ _ hR)
    infer_instance

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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
⊢ (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
      D.hom ((g ≫ f' j) ≫ p) (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫
        (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j)) =
    𝟙 ((F.map g.op.toLoc).toFunctor.obj ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))))

Tactic:
D.hom_self _ _ (by cat_disch)

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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
⊢ (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
      𝟙 ((F.map (g ≫ p' j).op.toLoc).toFunctor.obj (D.obj (α j))) ≫
        (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j)) =
    𝟙 ((F.map g.op.toLoc).toFunctor.obj ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))))
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₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  ((Over.forget (unop (op Z₁.left))).op ⋙ F).map φ.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ ((Over.forget (unop (op Z₁.left))).op ⋙ G).map φ.op
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op

Tactic:
dsimp at H H' ⊢

Goal state after:
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₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
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
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
hx : x.Compatible
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) := fun Z ↦ Set.range fun g ↦ x ↑g ⋯
Q : Subfunctor F := K.subsheafify 𝒮
this : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
t : Q.toFunctor.obj (Opposite.op X)
ht : Presieve.FamilyOfElements.IsAmalgamation (fun Z g hg ↦ ⟨x g hg, ⋯⟩) t
right✝ :
  ∀ (y : Q.toFunctor.obj (Opposite.op X)),
    (fun t ↦ Presieve.FamilyOfElements.IsAmalgamation (fun Z g hg ↦ ⟨x g hg, ⋯⟩) t) y → y = t
⊢ ∃ t, x.IsAmalgamation t

Tactic:
exact ⟨t.val, ht.map Q.ι⟩

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) (χ'.hom ≫ (closedSieves J).ι)
    (Presheaf.truth C)

Tactic:
have pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι)
    (closedSieves J).ι := IsPullback.of_horiz_isIso_mono (by simp)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
⊢ IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) (χ'.hom ≫ (closedSieves J).ι)
    (Presheaf.truth C)
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
r : Retract X Y
hY : P.triangEnvelope Y
⊢ P.triangEnvelope X

Tactic:
prop_triangEnvelope_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
r : Retract X Y
hY : ∃ n, P.triangEnvelopeIter n Y
⊢ ∃ n, P.triangEnvelopeIter n X
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
hX : P.triangEnvelope X
⊢ P.triangEnvelope.shift a X

Tactic:
prop_triangEnvelope_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
hX : ∃ n, P.triangEnvelopeIter n X
⊢ P.triangEnvelope.shift a X
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ P.triangEnvelope ((shiftFunctor C a).obj X)

Tactic:
prop_triangEnvelope_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ ∃ n, P.triangEnvelopeIter n ((shiftFunctor C a).obj X)
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : P.triangEnvelope T.obj₁
h₂ : P.triangEnvelope T.obj₃
⊢ P.triangEnvelope T.obj₂

Tactic:
prop_triangEnvelope_iff

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : ∃ n, P.triangEnvelopeIter n T.obj₁
h₂ : ∃ n, P.triangEnvelopeIter n T.obj₃
⊢ ∃ n, P.triangEnvelopeIter n T.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : Category.{v_2, u_2} D
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
E : C ≌ D
inst✝² : E.functor.CommShift ℤ
inst✝¹ : E.inverse.CommShift ℤ
inst✝ : E.CommShift ℤ
⊢ Equivalence.refl.IsTriangulated

Tactic:
by
  dsimp [Equivalence.IsTriangulated]
  rw [refl_toAdjunction]
  infer_instance

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✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
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
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
⊢ Nonempty (Abelian.AbelianStruct f₁)

Tactic:
obtain ⟨m₁, hm₁⟩ : ∃ (m₁ : X₁ ⟶ I), (shiftFunctor C (1 : ℤ)).map (ι.map m₁) = H.m₁ :=
      ⟨(ι ⋙ shiftFunctor C (1 : ℤ)).preimage H.m₁, Functor.map_preimage (ι ⋙ _) _⟩

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✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
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
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ (shiftFunctor C 1).obj (ι.obj I)
hI : Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : (shiftFunctor C 1).map (ι.map m₁) = H.m₁
⊢ Nonempty (Abelian.AbelianStruct f₁)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ √(log (2 ^ 12)) ≤ √(log ↑N)

Tactic:
gcongr
      exact mod_cast hN

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

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 8 ≤ log ↑N

Tactic:
exact log_le_log (by simp) (mod_cast hN₃)

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

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (2 * ↑(dValue N)) ^ nValue N ≤ ↑N

Tactic:
rw [← rpow_natCast]
    apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
    rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]
    rw [cast_ne_zero]
    apply (nValue_pos hN).ne'

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
x : G
hx : x ∈ A / C
⊢ #B ≤
    #(bipartiteAbove
        (fun b x ↦
          match x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) x)

Tactic:
obtain ⟨a, ha, c, hc, rfl⟩ := mem_div.1 hx
    refine card_le_card_of_injOn (fun b ↦ (a / b, c / b)) (fun b hb ↦ ?_) fun b₁ _ b₂ _ h ↦ ?_
    · rw [mem_coe, mem_bipartiteAbove]
      exact ⟨mk_mem_product (div_mem_div ha hb) (div_mem_div hc hb), div_div_div_cancel_right ..⟩
    · exact div_right_injective (Prod.ext_iff.1 h).1

Goal state after:
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: G : Type u_1
inst✝² : DecidableEq G
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
s t : Finset G
hs : s.Nonempty
ht : t.Nonempty
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
by
  simpa only [Monoid.minOrder_eq_top, min_eq_right, le_top, Nat.cast_le]
    using cauchy_davenport_minOrder_mul hs ht

Goal state after: