mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
⊢ (hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd = liftedConeElement F

Tactic:
apply (preservesLimitIso A (F ⋙ π A)).toEquiv.injective

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
⊢ (preservesLimitIso A (F ⋙ π A)).toEquiv ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd) =
    (preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : ⨆ i, U ↑i = ⊤
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
⊢ ⨆ i, ⨆ j, PrimeSpectrum.basicOpen (a ⟨i, j⟩.fst ⟨i, j⟩.snd) = ⊤

Tactic:
← hs

Goal state after:
case refine_1
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : ⨆ i, U ↑i = ⊤
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
⊢ ⨆ i, ⨆ j, PrimeSpectrum.basicOpen (a ⟨i, j⟩.fst ⟨i, j⟩.snd) = ⨆ i, U ↑i
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
⊢ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf M ≤ (tilde.functor R).essImage M

Tactic:
(h : M.IsQuasicoherent)

Goal state after:
case refine_2
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
h : SheafOfModules.IsQuasicoherent M
⊢ (tilde.functor R).essImage M
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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ presheafMap data G₀ g ≫ restriction data G₀ f ≫ G₀.obj.map (c ≫ d).op =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map (c ≫ d).op

Tactic:
restriction_map (i := Sieve.ofArrows.i hd)
    (p := F.map c ≫ Sieve.ofArrows.h hd) (fac := by simp; grind),

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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ presheafMap data G₀ g ≫
      presheafObjπ data G₀ X (Sieve.ofArrows.i hd) ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map (c ≫ d).op
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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₁ ≫ F.map a = F.map (p₁ ≫ a)

Tactic:
map_comp

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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₁ ≫ F.map a = F.map p₁ ≫ F.map a
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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₂ ≫ F.map b = F.map (p₂ ≫ b)

Tactic:
map_comp

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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₂ ≫ F.map b = F.map p₂ ≫ F.map b
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₀ W₀ : C₀
a : W₀ ⟶ X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = F.map a
ha : (Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀).arrows a
⊢ hom data G₀ X₀ ≫ G₀.obj.map a.op = presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
exact (G₀.2.amalgamate_map _ _ _ ⟨W₀, a, ha⟩).trans
    (presheafObj_mapPreimage_condition _ _ _ _ _ _ _
      ((Sieve.ofArrows.fac ha).trans fac.symm))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
⊢ z ≫ cokernel.map t b l r ⋯ = 0 → z = 0

Tactic:
hz

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
⊢ z = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u'
inst✝⁶ : Category.{v', u'} D
J : Type w
inst✝⁵ : LinearOrder J
inst✝⁴ : OrderBot J
X Y : C
f : X ⟶ Y
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
F : C ⥤ D
inst✝¹ : PreservesWellOrderContinuousOfShape J F
inst✝ : PreservesColimitsOfShape J F
⊢ (F.mapIso c.isoBot).inv ≫ (Functor.whiskerRight c.incl F ≫ (Functor.constComp J Y F).hom).app ⊥ = F.map f

Tactic:
by simp [← Functor.map_comp]

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

Goal state before:
pp: case succ.inr.inr
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
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
by_cases h' : k₁ ≤ j

Goal state after:
case pos
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₂

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₂
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: 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
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
  · simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)]
  rw [Subsingleton.elim iter₁ (iter₂.trunc hj)]
  rfl

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

Goal state before:
pp: 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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) k i ⋯ hij =
    arrowι (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij) hi k hk

Tactic:
rw [arrowMap_extendToSucc _ _ _ _ _ _ hij', arrowMap_limit _ _ hi _ _ hk]

Goal state after:
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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ arrowι (restrictionLT iter.F hij') hi k hk =
    arrowι (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
            (d.lift j hj
              ⟨fun x ↦
                match x with
                | op ⟨i, hi⟩ => (e i hi).val,
                ⋯⟩),
        ⋯⟩

Tactic:
by
    obtain hij' | rfl := hij.lt_or_eq
    · have := (e i hij').map_limit i hi (by rfl)
      dsimp at this ⊢
      rw [map_id, id_apply] at this
      rw [d.map_lift _ _ _ _ hij']
      dsimp
      rw [this]
      congr
      ext ⟨⟨l, hl⟩⟩
      rw [map_lift _ _ _ _ _ (hl.trans hij')]
      apply compatibility
    · dsimp
      rw [map_id, id_apply]
      congr
      ext ⟨⟨l, hl⟩⟩
      rw [d.map_lift _ _ _ _ hl]

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

Goal state before:
pp: case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
hi : IsMin ⊥
⊢ Nonempty (d.Extension val₀ ⊥)

Tactic:
exact ⟨zero d val₀⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ ∃ A', ∃ (h : A < A'), (generatingMonomorphisms G).pushouts (A.ofLE A' ⋯)

Tactic:
by
  induction A using Subobject.ind with | _ f
  obtain ⟨X', i, p', hi, hi', hp', fac⟩ := exists_pushouts hG f
    (by simpa only [Subobject.isIso_iff_mk_eq_top] using hA)
  refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',
    (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩
  refine Arrow.isoMk (Subobject.underlyingIso f) (Subobject.underlyingIso p') ?_
  dsimp
  simp only [← cancel_mono p', assoc, fac,
    Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow]

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

Goal state before:
pp: p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p b - padicValNat p p = padicValNat p b - 1

Tactic:
padicValNat_self

Goal state after:
p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p b - 1 = padicValNat p b - 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ padicValNat p p + padicValNat p k + p ≤ p * k

Tactic:
padicValNat_self

Goal state after:
case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ 1 + padicValNat p k + p ≤ p * k
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) ≤ n
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False

Tactic:
← Nat.lt_add_one_iff,

Goal state after:
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) < n + 1
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p n < b
⊢ padicValNat p n ! = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Tactic:
by
  exact_mod_cast ((padicValNat_eq_emultiplicity (p := p) <| factorial_ne_zero _) ▸
      Prime.emultiplicity_factorial hp.out hnb)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False

Tactic:
by
  have hpn : 0 < padicNorm p (f (stationaryPoint hf)) - padicNorm p (g (stationaryPoint hg)) :=
    sub_pos_of_lt hlt
  obtain ⟨N, hN⟩ := hfg _ hpn
  let i := max N (max (stationaryPoint hf) (stationaryPoint hg))
  have hi : N ≤ i := le_max_left _ _
  have hN' := hN _ hi
  -- Porting note: originally `padic_index_simp [N, hf, hg] at hN' h hlt`
  rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)]
    at hN' h hlt
  have hpne : padicNorm p (f i) ≠ padicNorm p (-g i) := by rwa [← padicNorm.neg (g i)] at h
  rw [CauSeq.sub_apply, sub_eq_add_neg, add_eq_max_of_ne hpne, padicNorm.neg, max_eq_left_of_lt hlt]
    at hN'
  have : padicNorm p (f i) < padicNorm p (f i) := by
    apply lt_of_lt_of_le hN'
    apply sub_le_self
    apply padicNorm.nonneg
  exact lt_irrefl _ this

Goal state after:
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
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
⊢ ∃ Z p₁ p₂ z,
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧ (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁ ∧ (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂

Tactic:
let α₁ : Φ.fiber.elementsMk _ y₁ ⟶ Φ.fiber.elementsMk _ x := ⟨f₁, hy₁⟩

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
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x := ⟨f₁, hy₁⟩
⊢ ∃ Z p₁ p₂ z,
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧ (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁ ∧ (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
⊢ f.norm = g.norm

Tactic:
exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
    simp only [hf, hg, norm, dif_pos]
  else by
    have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
    simp only [hg, hf, norm, dif_neg, not_false_iff]
    let i := max (stationaryPoint hf) (stationaryPoint hg)
    have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
    have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
    rw [hpf, hpg, h]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ ∃ b snd fst, IsPullback fst (F.map snd) g' h

Tactic:
by
    refine ⟨hg.pullback (h ≫ f), hg.snd (h ≫ f), ?_, ?_⟩
    · apply P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) (by simpa using hg.w (h ≫ f))
    · apply IsPullback.of_right' (hg.isPullback (h ≫ f)) P₁

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : D
P : MorphismProperty C
inst✝³ : F.Faithful
inst✝² : F.Full
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : D
Y : C
g : F.obj Y ⟶ X
⊢ IsPullback g (F.map (𝟙 Y)) (𝟙 X) g

Tactic:
simpa using IsPullback.of_id_snd

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ‖↑q‖ = ↑(padicNorm p q)

Tactic:
dsimp [norm]
  rw [← padicNormE.eq_padic_norm']

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ↑(padicNorm p ↑k) ≤ ↑↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X✝ X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C).map f ≫ PInfty = PInfty ≫ (alternatingFaceMapComplex C).map f

Tactic:
ext n
    exact PInfty_f_naturality n f

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑(padicNorm p q) = ↑(↑p ^ (-padicValRat p q))

Tactic:
Rat.cast_inj

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)