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

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{v_3, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant K F → IsConstant J ((sheafEquiv J K G D).inverse.obj F)

Tactic:
· exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant' J D K G hT hT').app _ ≪≫
      (sheafEquiv J K G D).inverse.mapIso i⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
X Y : Scheme
⊢ ∀ (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)

Tactic:
f

Goal state after:
case refine_2
S : Scheme
X Y : Scheme
f : X ⟶ Y
⊢ ∀ (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: case refine_2
X : Scheme
R S : CommRingCat
⊢ ∀ (f : R ⟶ S),
    Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
f

Goal state after:
case refine_2
X : Scheme
R S : CommRingCat
f : R ⟶ S
⊢ Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = R

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫
      { hom := presheafObjObjIso.hom data G₀ ((data X).X i), inv := presheafObjObjIso.inv data G₀ ((data X).X i),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
        presheafObjπ data G₀ (F.obj ((data X).X i)) j

Tactic:
presheafObjObjIso.inv_π data G₀

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj ((data X).X i))).f j)
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: X Y : Scheme
⊢ ∀ (f : X ⟶ Y), Etale f → WeaklyEtale f

Tactic:
f

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ Etale f → WeaklyEtale f
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ J.yonedaEquiv (J.yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom ((J.yoneda.map f).hom.app (op X))) (𝟙 X) = f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ⨆ j, Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk f

Tactic:
iSup_le_iff

Goal state after:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ ⨆ j, Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom

Tactic:
iSup_le_iff

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
h' : Function.Surjective fun j ↦ ⟨s j, ⋯⟩
σ : { x // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun j ↦ ⟨s j, ⋯⟩
hs : HasCardinalLT (↑(Set.range s)) κ
⊢ ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj.hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫
      colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
rw [Category.id_comp, ι_colimMap_assoc, colimit.comp_coconePointUniqueUpToIso_hom,
      constCocone_ι, NatTrans.id_app, Category.comp_id]

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z = (pullback.snd c.ι ((Functor.const J).map z)).app j
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ z = (pullback.fst c.ι ((Functor.const J).map z) ≫ c.ι).app j

Tactic:
pullback.condition,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ z =
    (pullback.snd c.ι ((Functor.const J).map z) ≫ (Functor.const J).map z).app j
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
refine ⟨j, hb', ?_⟩

Goal state after:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
⊢ j < ↑m
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
⊢ ∀ (f : A ⟶ B), W.transfiniteCompositionsOfShape J f → transfiniteCompositions.{w, v, u} W f

Tactic:
f

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
f : A ⟶ B
⊢ W.transfiniteCompositionsOfShape J f → transfiniteCompositions.{w, v, u} W f
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
⊢ ∀ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W₁ f → transfiniteCompositions.{w, v, u} W₂ f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
⊢ transfiniteCompositions.{w, v, u} W₁ f → transfiniteCompositions.{w, v, u} W₂ f
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), transfiniteCompositions.{w, v, u} W f → W f

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ transfiniteCompositions.{w, v, u} W f → W f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : J
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : ¬k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
· simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ arrowMap (functor hj iter) k i ⋯ hij✝ = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk

Tactic:
arrowMap_functor _ _ _ _ _ hij,

Goal state after:
case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ Arrow.mk ((iter k ⋯).mapObj (iter i hij) ⋯ ⋯ ⋯ ⋯) = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), transfiniteCompositions.{w, v, u} W f → W.rlp.llp f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ transfiniteCompositions.{w, v, u} W f → W.rlp.llp f
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
⊢ (propArrow I).functorCategory (Arrow C) ((succStruct I κ).toSucc F)

Tactic:
f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ propArrow I (((succStruct I κ).toSucc F).app f)
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
⊢ ∀ (f : X ⟶ Y),
    I.rlp.llp f → ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts f

Tactic:
f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ I.rlp.llp f → ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts f
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
ne : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1

Tactic:
padicNorm,

Goal state after:
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
ne : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-padicValRat p✝ ↑q)) = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q ≠ 0

Tactic:
rw [padicNorm.eq_zpow_of_nonzero hq]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1

Tactic:
padicNorm,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
min_eq_right h,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (q + r)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
⊢ ↑(PadicSeq.norm ⟨fun n ↦ ↑(seq n), h⟩) ≤ 1

Tactic:
rw [PadicSeq.norm]
      split_ifs with hne <;> norm_cast
      apply padicNorm.of_int

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case coe.ofAdd.inl
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : 0 ≤ x
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } a =
      ↑(Multiplicative.ofAdd x)

Tactic:
exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = ↑p ^ (-f.valuation)

Tactic:
norm,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) = ↑p ^ (-f.valuation)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ padicNorm p (↑f (stationaryPoint hf)) = ↑p ^ (-padicValRat p (↑f (stationaryPoint hf)))

Tactic:
padicNorm,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ (if ↑f (stationaryPoint hf) = 0 then 0 else ↑p ^ (-padicValRat p (↑f (stationaryPoint hf)))) =
    ↑p ^ (-padicValRat p (↑f (stationaryPoint hf)))
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : LocallySmall.{w, v, u} C
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
inst✝ : HasSheafify J (Type w)
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
hf : ∀ (Φ : P.FullSubcategory), Epi (↾⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
⊢ Sheaf.IsLocallySurjective ((presheafToSheaf J (Type w)).map (Functor.whiskerRight f (forget A)))

Tactic:
Sheaf.isLocallySurjective_iff_epi,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : LocallySmall.{w, v, u} C
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
inst✝ : HasSheafify J (Type w)
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
hf : ∀ (Φ : P.FullSubcategory), Epi (↾⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
⊢ Epi ((presheafToSheaf J (Type w)).map (Functor.whiskerRight f (forget A)))
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)

Tactic:
← Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i,

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
this :
  (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app X))
      ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
⊢ (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i)))
        ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)) =
    (ConcreteCategory.hom
        (Φ.obj.presheafFiber.map
          (Sigma.ι (fun i ↦ shrinkYoneda.{w, v, u}.obj (U i)) i ≫ Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app (U i))) y)
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
⊢ ∀ (f : P₁ ⟶ P₂), J.W f → IsIso (Φ.presheafFiber.map f)

Tactic:
f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ J.W f → IsIso (Φ.presheafFiber.map f)