mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ localEpi (fun x ↦ x ∈ Set.range G.obj) f ↔ Epi (F.map f)

Tactic:
rw [← dsimp% (localEpi (· ∈ Set.range G.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),
    dsimp% adj.unit.naturality f,
    dsimp% (localEpi (· ∈ Set.range G.obj)).precomp_iff _ _ (isLocal_adj_unit_app adj X)]
  refine ⟨fun h ↦ ⟨fun {Z} u v huv ↦ ?_⟩, ?_⟩
  · refine G.map_injective ?_
    apply h ⟨Z, rfl⟩
    simp [← Functor.map_comp, huv]
  · rintro h _ ⟨Z, rfl⟩ u v huv
    obtain ⟨u, rfl⟩ := G.map_surjective u
    obtain ⟨v, rfl⟩ := G.map_surjective v
    simp only [← G.map_comp, G.map_injective_iff, cancel_epi] at huv
    rw [huv]

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α β : PartOrdEmb
f : α ⟶ β
hf : IsIso ((forget PartOrdEmb).map f)
⊢ IsIso f

Tactic:
CategoryTheory.isIso_iff_bijective

Goal state after:
α β : PartOrdEmb
f : α ⟶ β
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))
⊢ IsIso f
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
⊢ (isCardinalFiltered κ).colimitsOfShape J ≤ isCardinalFiltered κ

Tactic:
by
    have := isFiltered_of_isCardinalFiltered J κ
    rintro X ⟨p⟩
    simp only [(isCardinalFiltered κ).prop_iff_of_iso
      (p.isColimit.coconePointUniqueUpToIso
        (Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))),
      isCardinalFiltered_iff]
    exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
A : Type u
inst✝¹ : SmallCategory A
inst✝ : IsCardinalFiltered A κ
⊢ PreservesColimitsOfShape A (forget (CardinalDirectedPoset κ))

Tactic:
have := isFiltered_of_isCardinalFiltered A κ
  change PreservesColimitsOfShape A (CardinalDirectedPoset.ι ⋙ forget _)
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
⊢ (fun i j_1 ↦
      (f j).X i ⟶ { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X j_1)
    x y

Tactic:
refine if h : y.1 = j then ?_ else 0
              refine if h' : @Eq.ndrec _ y.1 (fun j => (f j).ι) y.2 _ h = x then ?_ else 0
              apply eqToHom
              subst h h'
              rfl

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : (FintypeCat.of X.ι).obj
⊢ MulOpposite.unop (if h : i✝ = j✝ then eqToHom ⋯ else 0) = if i✝ = j✝ then 1 else 0

Tactic:
split_ifs

Goal state after:
case pos
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : (FintypeCat.of X.ι).obj
h✝ : i✝ = j✝
⊢ MulOpposite.unop (eqToHom ⋯) = 1

case neg
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : (FintypeCat.of X.ι).obj
h✝ : ¬i✝ = j✝
⊢ MulOpposite.unop 0 = 0
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ {i j_1 : J} {f : i ⟶ j_1}, MorphismProperty.ofHoms (fun x ↦ 𝟙 j) f → ObjectProperty.ofObj (fun x ↦ j) i

Tactic:
by rintro _ _ _ ⟨⟩; exact ⟨⟨⟩⟩

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ {i j_1 : J} {f : i ⟶ j_1}, MorphismProperty.ofHoms (fun x ↦ 𝟙 j) f → ObjectProperty.ofObj (fun x ↦ j) j_1

Tactic:
by rintro _ _ _ ⟨⟩; exact ⟨⟨⟩⟩

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ ↔ HasCardinalLT X κ

Tactic:
refine ⟨fun _ ↦ ?_, fun hX ↦ hX.isCardinalPresentable⟩

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
⊢ HasCardinalLT X κ
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
⊢ ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := hP b hb

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
⊢ ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
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.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpiFamily _).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.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝³ : IsLocallySurjective data.i
this✝² : IsLocallyInjective data.p
this✝¹ : Epi data.p
this✝ : Mono data.p
this : IsIso data.p
⊢ IsLocallySurjective φ

Tactic:
rw [← data.fac]

Goal state after:
case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝³ : IsLocallySurjective data.i
this✝² : IsLocallyInjective data.p
this✝¹ : Epi data.p
this✝ : Mono data.p
this : IsIso data.p
⊢ IsLocallySurjective (data.i ≫ data.p)
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 : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)

Tactic:
have := hF.1

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
this : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
Module: Mathlib.CategoryTheory.Sites.Finite

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
u : Y ⟶ X
s : Presieve X
hs : s ∈ (Precoverage.finite C).coverings X
⊢ pullbackArrows u s ∈ (Precoverage.finite C).coverings Y

Tactic:
by simpa using hs.image _

Goal state after:
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 q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
⊢ pullback.snd
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      E.p₂ k.down =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)

Tactic:
by
    have : E.p₂ k.down = pullback.lift _ _ (E.w k.down) ≫ pullback.snd _ _ := by simp
    nth_rw 2 [this]
    rw [← pullback.condition_assoc]
    simp

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
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
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : Over (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ (sieve f f' i).arrows g

Tactic:
rw [show g = Over.homMk Z.hom by ext; simpa using Over.w g]
      exact mem_sieve _ _ fac

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
⊢ (PreOneHypercover.cylinder f g).sieve₁' i j ∈
    J (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))

Tactic:
PreOneHypercover.sieve₁'_cylinder

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
⊢ Sieve.pullback
      (pullback.map ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.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) ∈
    J (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))
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
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
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom

Tactic:
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
D : F.DescentData f
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
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y✝ : C
f : Y✝ ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
T : Over X
a : T ⟶ Over.mk f
Y : C
i : ι
b : (Over.forget X).obj T ⟶ Z i
hb : b ≫ g i = (Over.forget X).map a
z : (Over.forget X ⋙ ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber).obj T
hz₁ :
  z ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      T
hz₂ :
  ↑((ConcreteCategory.hom
          ({
                    obj :=
                      ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.over
                        ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd,
                    property := ⋯ }.obj.fiber.map
            a))
        ⟨z, hz₁⟩) =
    ↑⟨y, ⋯⟩
⊢ ∃ i y_1, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y_1 = y

Tactic:
exact ⟨i, Φ.obj.fiber.map b z,
      (ConcreteCategory.congr_hom (Φ.obj.fiber.map_comp b (g i)) _).symm.trans (by rwa [hb])⟩

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
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ r' k ≫ f ((α ∘ β) k) = f'' k ≫ r

Tactic:
dsimp
        rw [← hr', Category.assoc, w, reassoc_of% w', hr]

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

Goal state before:
pp: case refine_1
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
⊢ Presieve.IsSeparatedFor F S.arrows

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), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
· intro x t₁ t₂ ht₁ ht₂
    let 𝒮 (Z : C) : Set (F.obj (.op Z)) :=
      .range (fun (g : { g : Z ⟶ X | S.arrows g }) ↦ x _ g.2) ∪
      .range (fun (g : Z ⟶ X) ↦ F.map g.op t₁) ∪ .range (fun (g : Z ⟶ X) ↦ F.map g.op t₂)
    let Q : Subfunctor F := K.subsheafify 𝒮
    have (Z : C) : _root_.Small.{max u v} (Q.toFunctor.obj (Opposite.op Z)) :=
      small_subsheafify_of_small H _ inferInstance _
    have hQ : Presieve.IsSheaf J Q.toFunctor :=
      h.isSheaf_of_forall_aux _ fun X R hR ↦ isSheafFor_subsheafify _ hR (H _ hR)
    let x' : S.arrows.FamilyOfElements Q.toFunctor :=
      fun Z g hg ↦ ⟨x g hg, .base <| .inl <| .inl ⟨⟨g, hg⟩, rfl⟩⟩
    have ht₁' : t₁ ∈ Q.obj (.op X) := .base (.inl <| .inr ⟨𝟙 _, by simp⟩)
    have ht₂' : t₂ ∈ Q.obj (.op X) := .base (.inr ⟨𝟙 _, by simp⟩)
    have : (⟨t₁, ht₁'⟩ : Q.obj _) = ⟨t₂, ht₂'⟩ :=
      (hQ _ hS).isSeparatedFor x' ⟨_, ht₁'⟩ ⟨_, ht₂'⟩ (.of_mono Q.ι ht₁) (.of_mono Q.ι ht₂)
    simp_all

Goal state after:
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), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.PreservesLimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
K : Type u_1
inst✝ : Category.{v_1, u_1} K
⊢ ∀ {K_1 : K ⥤ C}, PreservesLimit K_1 (GrothendieckTopology.uliftYoneda.{v', v, u} J)

Tactic:
by
    intro F
    have : PreservesLimitsOfShape K (uliftYoneda J ⋙ sheafToPresheaf J (Type max v v')) :=
      preservesLimitsOfShape_of_natIso (uliftYonedaCompSheafToPresheaf J).symm
    exact preservesLimit_of_reflects_of_preserves (uliftYoneda J)
      (sheafToPresheaf ..)

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
⊢ Presieve.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R

Tactic:
by
  refine ⟨fun h X R hR ↦ ?_, fun h ↦ H.isSheaf_of_forall _ h⟩
  rw [Presieve.isSheafFor_iff_generate]
  exact h _ (H.le_toPrecoverage _ hR)

Goal state after:
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)
⊢ EffectiveEpi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)

Tactic:
suffices EffectiveEpi ((presheafToSheaf J D).map p) by infer_instance

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)
⊢ EffectiveEpi ((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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
S : C
R : Presieve S
hR : Sieve.generate R ∈ J S
⊢ (Sieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ∈ ?m.35 S

Tactic:
rwa [Sieve.ofArrows_category']

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
χ' : X ⟶ Ω
π : U ⟶ underlying.obj h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ χ' = h.χ m

Tactic:
apply h.homEquiv.injective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
χ' : X ⟶ Ω
π : U ⟶ underlying.obj h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ h.homEquiv χ' = h.homEquiv (h.χ m)
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
⊢ m ≫ χ m = (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F ≫ truth C

Tactic:
ext
  apply Sieve.ext
  simp [← NatTrans.naturality_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree (f '' s) ↔ ThreeGPFree t

Tactic:
hf.bijOn.image_eq

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree t ↔ ThreeGPFree t