mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
h : (ConcreteCategory.hom (F.map (a₁ ≫ d))) x' ≤ (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
| (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'

Tactic:
rw [h₁]

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
h : (ConcreteCategory.hom (F.map (a₁ ≫ d))) x' ≤ (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
| (ConcreteCategory.hom (F.map (a₂ ≫ d'))) y'
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 (𝟙 X i✝ j✝) = 𝟙 (FintypeCat.of X.ι) i✝ j✝

Tactic:
simp only [Mat_.id_def, id_def]

Goal state after:
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
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
inst✝ : HasFiniteCoproducts C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
x✝ : EffectiveEpi g
⊢ ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
by
    have hp := Precoherent.pullback f PUnit (fun () ↦ Z) (fun () ↦ g)
    simp only [exists_const] at hp
    rw [← effectiveEpi_iff_effectiveEpiFamily g] at hp
    obtain ⟨β, _, X₂, π₂, h, ι, hι⟩ := hp inferInstance
    refine ⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩
    ext b
    simpa using hι b

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
Q E : C
e : Q ⟶ E
r : E ⟶ ∐ X
hq : Presieve.ofArrows X (fun i ↦ Sigma.ι X i) r
⊢ Presieve.ofArrows X f (r ≫ Sigma.desc f)

Tactic:
cases hq; simpa using Presieve.ofArrows.mk _

Goal state after:
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
⊢ ∃ a, (ConcreteCategory.hom (f.app (op X))) a = x

Tactic:
let ht' := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse
    (Cocone.op (Cofan.mk X π))).symm h.some.op

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
⊢ ∃ a, (ConcreteCategory.hom (f.app (op X))) a = x
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ Sheaf.IsLocallySurjective (c.π.app (op 0))

Tactic:
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ ∀ (X : C) (y : ToType ((F.obj (op 0)).obj.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((c.π.app (op 0)).hom.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op 0)).obj.map (op φ))) y
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
⊢ f = ΓHomEquiv c.π

Tactic:
replace hf : ((Functor.const Cᵒᵖ).map f) ≫ F.coneΓ.π = c.π := by ext j; exact hf j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : (Functor.const Cᵒᵖ).map f ≫ F.coneΓ.π = c.π
⊢ f = ΓHomEquiv c.π
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ ∀ (E_1 : Multifork (F.multicospanIndex G)) (m : E_1.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E_1.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
· intro t m hm
    refine Multifork.IsLimit.hom_ext hE fun i ↦ ?_
    rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
I : S.Arrow
⊢ IsIso (f.hom.app (op I.Y))

Tactic:
obtain ⟨i, ⟨g⟩⟩ := I.hf

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
I : S.Arrow
i : ι
g : I.Y ⟶ X i
⊢ IsIso (f.hom.app (op I.Y))
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₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (f₂ ≫ p' j₂) ≫ f (α j₂) = q ≫ p

Tactic:
simp [w, reassoc_of% hf₂]

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

Goal state before:
pp: case h
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
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) := ⋯
⊢ ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)),
    (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
intro Z p hp

Goal state after:
case h
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
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun x_1 ↦
          match x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
Z : C
p : Z ⟶ Y
hp : S.arrows (p ≫ g)
⊢ (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
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 ((F.mapId { as := op (X i₁) }).hom.toNatTrans.app (D.obj i₁)) ≫ D.hom q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (𝟙 (X i₁)).op.toLoc f₁.op.toLoc f₁.op.toLoc ⋯).inv.toNatTrans.app (D.obj i₁) ≫
      D.hom q f₁ f₂ ⋯ ⋯ ≫
        (F.mapComp' (𝟙 (X i₂)).op.toLoc f₂.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (D.obj i₂) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₂) }).hom.toNatTrans.app (D.obj i₂))

Tactic:
simp [mapComp'_id_comp_inv_app_assoc, mapComp'_id_comp_hom_app, ← Functor.map_comp]

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
⊢ Epi ((presheafToSheaf J D).map f.hom)

Tactic:
rw [h₁]

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
⊢ Epi ((sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
x✝¹ : S.obj α
x✝ : unop β
⊢ (ConcreteCategory.hom ((ConcreteCategory.hom (S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom)).toFun x✝¹)).toFun x✝ =
    (ConcreteCategory.hom
          ((ConcreteCategory.hom ((evalEquiv S hs (unop α)).toIso.hom ≫ ↾fun g ↦ f.unop ≫ g)).toFun x✝¹)).toFun
      x✝

Tactic:
exact eval_map S (unop α) (unop β) f.unop _ _

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
S : C
R R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ F.IsStackFor R ↔ F.IsStackFor R'

Tactic:
simp only [isStackFor_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence ↔ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
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
⊢ F.IsStackFor (Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence

Tactic:
simp only [isStackFor_iff]

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
⊢ (F.toDescentData fun f_1 ↦ f_1.obj.hom).IsEquivalence ↔ (F.toDescentData f).IsEquivalence
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X : C
φ : X ⟶ 𝒞.Ω
⊢ IsPullback (pullback.fst φ 𝒞.truth) ?m.52 φ 𝒞.truth

Tactic:
by
    convert! IsPullback.of_hasPullback φ 𝒞.truth

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤

Tactic:
rintro ⟨a, h⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
a : F.obj (Opposite.op Y)
h : (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
⊢ (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤
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.obj ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι

Tactic:
· simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

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✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ (commShiftIso F.op n).inv.app X =
    (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
      ((commShiftIso F m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op

Tactic:
← cancel_epi ((F.op.commShiftIso n).hom.app X),

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
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ (commShiftIso F.op n).hom.app X ≫ (commShiftIso F.op n).inv.app X =
    (commShiftIso F.op n).hom.app X ≫
      (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
        ((commShiftIso F m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op
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✝³ : Preadditive C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
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
X Y : A
n : ℤ
f : (shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ (shiftFunctor C (-n)).map f = (shiftFunctor C (-n)).map 0

Tactic:
by
    rw [← cancel_epi ((shiftEquiv C n).unitIso.hom.app _), Functor.map_zero, comp_zero]
    exact hι _ (by lia)

Goal state after:
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
⊢ #s ≤ #t

Tactic:
← mul_one #s,

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
⊢ #s * 1 ≤ #t
Module: Mathlib.Combinatorics.Additive.CovBySMul

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ ↑(#(F₁ • F₂)) ≤ K * L

pp: case refine_2
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ A ⊆ ↑(F₁ • F₂) • C

Tactic:
· calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr

Goal state after:
case refine_2
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ A ⊆ ↑(F₁ • F₂) • C
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n✝ : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h : s.prod = t.prod
n : ℕ
hf : IsMulFreimanHom (n + 1 + 1) A B f
hs : s.card = n + 1
x✝ : t.card = n + 1
a : α
ha : a ∈ s
⊢ ∀ ⦃x : α⦄, x ∈ a ::ₘ s → x ∈ A

Tactic:
by simpa [hsA ha]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n✝ : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h : s.prod = t.prod
n : ℕ
hf : IsMulFreimanHom (n + 1 + 1) A B f
hs : s.card = n + 1
x✝ : t.card = n + 1
a : α
ha : a ∈ s
⊢ ∀ ⦃x : α⦄, x ∈ a ::ₘ t → x ∈ A

Tactic:
by simpa [hsA ha]

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Tactic:
by
  calc
    _ ≤ log (2 ^ 3) * (69 / 50) := by
      gcongr
      · field_simp
        simp (disch := positivity) [exp_one_gt_two]
      · norm_num1
        exact two_div_one_sub_two_div_e_le_eight
    _ ≤ √(log (2 ^ 12)) := by
      simp only [Real.log_pow, Nat.cast_ofNat]
      apply le_sqrt_of_sq_le
      nlinarith [log_two_lt_d9, log_two_gt_d9]
    _ ≤ √(log ↑N) := by
      gcongr
      exact mod_cast hN

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

Goal state before:
pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 1 ≤ x * (1 / 2) - x * (1 / rexp 1)

Tactic:
← mul_sub,

Goal state after:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 1 ≤ x * (1 / 2 - 1 / rexp 1)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hbc
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log ↑N)) ≤ (↑N ^ (2 / ↑n))⁻¹ * ((rexp (↑n - 2))⁻¹ * (↑n)⁻¹)

Tactic:
← exp_neg,

Goal state after:
case hbc
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log ↑N)) ≤ (↑N ^ (2 / ↑n))⁻¹ * (rexp (-(↑n - 2)) * (↑n)⁻¹)