mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i

Tactic:
by
    refine Presheaf.IsSheaf.hom_ext hG₀
      ⟨_, cover_lift F J₀ _ (J.pullback_stable ((data X).f i) S.2)⟩ _ _ ?_
    rintro ⟨X₀, a, ha⟩
    dsimp
    simp only [assoc, ← Functor.map_comp]
    exact h ⟨_, _, ha⟩

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

Goal state before:
pp: 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
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))

Tactic:
rw [← constantSheafAdj_counit_w]

Goal state after:
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
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsIso
    ((constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T)) ≫
      (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F))
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)

Tactic:
rw [Sieve.generateSingleton_eq]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generateSingleton f).arrows.cocone)
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows
      (fun i_1 ↦ pullback ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f i_1) (V.affineOneHypercover.f i)) fun x ↦
      pullback.snd ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f x) (V.affineOneHypercover.f i))

Tactic:
let 𝒰' := (𝒱.cover.pullback₂ f).pullback₂ (V.affineCover.f i)

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i : V.affineOneHypercover.I₀
𝒰' : (precoverage P).ZeroHypercover (V.affineCover.X i) :=
  Precoverage.ZeroHypercover.pullback₂ (V.affineCover.f i) (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover)
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows
      (fun i_1 ↦ pullback ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f i_1) (V.affineOneHypercover.f i)) fun x ↦
      pullback.snd ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f x) (V.affineOneHypercover.f i))
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z✝ : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z✝
hR : Sieve.ofArrows T g ∈ (J.over X) Z✝
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : gi ≫ (fun i ↦ Over.Hom.left (g i)) i = gj ≫ (fun i ↦ Over.Hom.left (g i)) j
⊢ Over.homMk gi ⋯ ≫ g i = Over.homMk gj ⋯ ≫ g j

Tactic:
by ext; exact hgij

Goal state after:
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
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
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ }
this : Mono α
⊢ ∀ (j : J), c.ι.app j ≫ f = α.app j ≫ (constCocone J X).ι.app j

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f✝ : α <i β
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : β ⥤ C
i j : α
f : i ⟶ j
⊢ (⋯.functor ⋙ F).map f ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ ((Functor.const α).obj (F.obj f✝.top)).map f

Tactic:
by
        dsimp
        rw [← F.map_comp, comp_id]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj' : j' ∈ Set.Iio ↑m
⊢ ∃ j₁, ⟨j', hj'⟩ ≤ f j₁

Tactic:
push _ ∈ _ at hj'

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ f j₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j' ≤ j
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ ⟨↑j₁.1, ⋯⟩

Tactic:
refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
        by_contra h'
        simp only [Set.mem_Iio, not_lt] at h'
        apply hm.1
        rintro ⟨k, hk⟩ hkm
        exact h'.trans hk

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : ¬i₁ < j
h₁' : i₁ = j
⊢ obj c i₁ = obj c i₂

Tactic:
subst h₁' h₂'; rfl

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
φ : FunctorObjIndex f πX →
  (i : Shrink.{t, w} I) × Shrink.{t, v} ((A ((equivShrink I).symm i) ⟶ X) × (B ((equivShrink I).symm i) ⟶ S)) :=
  fun x ↦
    ⟨(equivShrink I) x.i,
      (equivShrink
          ((A ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ X) × (B ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b)⟩
⊢ Small.{t, max v w} (FunctorObjIndex f πX)

Tactic:
have hφ : Function.Injective φ := by
    rintro ⟨i₁, t₁, b₁, _⟩ ⟨i₂, t₂, b₂, _⟩ h
    obtain rfl : i₁ = i₂ := by simpa [φ] using congr_arg Sigma.fst h
    simpa [cancel_epi, φ] using h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
φ : FunctorObjIndex f πX →
  (i : Shrink.{t, w} I) × Shrink.{t, v} ((A ((equivShrink I).symm i) ⟶ X) × (B ((equivShrink I).symm i) ⟶ S)) :=
  fun x ↦
    ⟨(equivShrink I) x.i,
      (equivShrink
          ((A ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ X) × (B ((equivShrink I).symm ((equivShrink I) x.i)) ⟶ S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b)⟩
hφ : Function.Injective φ
⊢ Small.{t, max v w} (FunctorObjIndex f πX)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h

Tactic:
obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
    obtain h₂ | rfl := h₂₃.lt_or_eq
    · rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
      rw [map_eq hj F τ i₁ i₂ _ h₂]
      dsimp [map]
      rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, assoc, assoc,
        Iso.inv_hom_id_assoc, comp_id, ← Functor.map_comp_assoc, homOfLE_comp]
    · rw [map_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : i < Order.succ j
hij : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val

Tactic:
d.map_succ

Goal state after:
case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : i < Order.succ j
hij : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

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
⊢ ((coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp

Tactic:
le_llp_iff_le_rlp,

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
⊢ W.rlp ≤ ((coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts.rlp
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts).retracts ≤ W.rlp.llp

Tactic:
le_llp_iff_le_rlp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W.rlp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts).retracts.rlp
Module: Mathlib.CategoryTheory.Adjunction.Additive

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (G ⋙ preadditiveYoneda ⋙ (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).map f ≫
      (NatIso.ofComponents
          (fun X ↦
            (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X) Y✝).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
          ⋯).hom =
    (NatIso.ofComponents
          (fun X ↦
            (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X) X✝).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
          ⋯).hom ≫
      (preadditiveYoneda ⋙
            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).map
        f

Tactic:
ext _ ⟨x⟩

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
x✝ : Cᵒᵖ
x : ↑((preadditiveYoneda.obj (G.obj X✝)).obj x✝)
⊢ (AddCommGrpCat.Hom.hom
        (((G ⋙ preadditiveYoneda ⋙ (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).map
                f ≫
              (NatIso.ofComponents
                  (fun X ↦
                    (AddEquiv.ulift.trans
                        ((adj.homAddEquiv (unop X) Y✝).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
                  ⋯).hom).app
          x✝))
      { down := x } =
    (AddCommGrpCat.Hom.hom
        (((NatIso.ofComponents
                  (fun X ↦
                    (AddEquiv.ulift.trans
                        ((adj.homAddEquiv (unop X) X✝).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
                  ⋯).hom ≫
              (preadditiveYoneda ⋙
                    (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                      (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).map
                f).app
          x✝))
      { down := x }
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r

Tactic:
rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ↑(multiplicity (↑p) n₁) - ↑(multiplicity (↑p) d₁) ≤ ↑(multiplicity (↑p) n₂) - ↑(multiplicity (↑p) d₂)

Tactic:
sub_le_iff_le_add',

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ↑(multiplicity (↑p) n₁) ≤ ↑(multiplicity (↑p) d₁) + (↑(multiplicity (↑p) n₂) - ↑(multiplicity (↑p) d₂))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤ (coproducts.{w, v, u} (monomorphisms C)).pushouts

Tactic:
apply pushouts_monotone

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ coproducts.{w, v, u} (generatingMonomorphisms G) ≤ coproducts.{w, v, u} (monomorphisms C)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD maximalIdeal ℤ_[p] ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD maximalIdeal ℤ_[p] ^ n • ⊤]

Tactic:
simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.sub_mem, maximalIdeal_eq_span_p,
      Ideal.span_singleton_pow, ← norm_le_pow_iff_mem_span_pow] at hx ⊢
    let x' : CauSeq ℤ_[p] norm := ⟨x, ?_⟩; swap
    · intro ε hε
      obtain ⟨m, hm⟩ := exists_pow_neg_lt p hε
      refine ⟨m, fun n hn => lt_of_le_of_lt ?_ hm⟩
      rw [← neg_sub, norm_neg]
      exact hx hn
    · refine ⟨x'.lim, fun n => ?_⟩
      have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := zpow_pos (mod_cast hp.out.pos) _
      obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this
      by_cases! hin : i ≤ n
      · exact (hi i le_rfl n hin).le
      · specialize hi i le_rfl i le_rfl
        specialize hx hin.le
        have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
        rw [sub_add_sub_cancel] at this
        exact this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → IsIso c.inl

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ IsIso c.inl → c.inl = c.inr

Tactic:
· intro h
    obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
    refine ⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩
    · simp only [comp_id, reassoc_of% hφ₁]
    · simp only [comp_id, h, reassoc_of% hφ₂]

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ IsIso c.inl → c.inl = c.inr
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
    simpa only [hfg, norm]

Goal state after:
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
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : HasSheafify J (Type w)
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ Epi f

Tactic:
rw [← Sheaf.isLocallySurjective_iff_epi]

Goal state after:
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)
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ Sheaf.IsLocallySurjective f
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
⊢ ∀ (i j : (glueData hf).J),
    (ConcreteCategory.hom (F.obj.map ((glueData hf).f i j).op)) (yonedaEquiv (f i)) =
      (ConcreteCategory.hom (F.obj.map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op))) (yonedaEquiv (f j))

Tactic:
intro i j

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
i j : (glueData hf).J
⊢ (ConcreteCategory.hom (F.obj.map ((glueData hf).f i j).op)) (yonedaEquiv (f i)) =
    (ConcreteCategory.hom (F.obj.map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op))) (yonedaEquiv (f j))
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)
⊢ γ ≫ α = γ ≫ β

Tactic:
rw [← fac₁, ← fac₂] at h ⊢

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (a ≫ (glueData hf).openCover.f i) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (b ≫ (glueData hf).openCover.f j)
⊢ a ≫ (glueData hf).openCover.f i = b ≫ (glueData hf).openCover.f j