mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
⊢ ⋯.HasLift

Tactic:
have : i₁ (IsLocalRing.closedPoint K) ∈ (⊤ : (Proj 𝒜).Opens) := trivial

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
this : i₁ (IsLocalRing.closedPoint K) ∈ ⊤
⊢ ⋯.HasLift
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₀
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i

Tactic:
presheafMap_π,

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₀
⊢ restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i =
    presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i

Tactic:
presheafMap_π,

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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ restriction data G₀ ((data X).f i ≫ f ≫ g) = presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ restriction data G₀ ((data X).f i ≫ f ≫ g) = presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i

Tactic:
presheafMap_π,

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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ restriction data G₀ ((data X).f i ≫ f ≫ g) = presheafMap data G₀ g ≫ restriction data G₀ ((data X).f i ≫ 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₀
⊢ presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j =
    presheafObjπ data G₀ X i ≫
      (presheafObjObjIso data G₀ ((data X).X i)).inv ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j

Tactic:
presheafMap_π,

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 ≫
      (presheafObjObjIso data G₀ ((data X).X i)).inv ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j
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₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ ∃ x₂', π ≫ x₄ = x₂' ≫ r

Tactic:
refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩

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₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r
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
⊢ F.map (⋯.functor.map f) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ 𝟙 (F.obj f✝.top)

Tactic:
← F.map_comp,

Goal state after:
α : 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
⊢ F.map (⋯.functor.map f ≫ homOfLE ⋯) = F.map (homOfLE ⋯) ≫ 𝟙 (F.obj f✝.top)
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
this : ↑m ≤ j
⊢ False

Tactic:
apply hm.1

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
this : ↑m ≤ j
⊢ IsMin m
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
h' : m ≤ ⟨j, ⋯⟩
⊢ False

Tactic:
apply hm.1

Goal state after:
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) := ⋯
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j' ≤ j
h' : m ≤ ⟨j, ⋯⟩
⊢ IsMin m
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case inl
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
j : Fin n
hj : ¬IsMax j.castSucc
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
replace hF := hF j

Goal state after:
case inl
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : W (F.map (homOfLE ⋯))
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f → Nonempty (AttachCells g f)

Tactic:
rintro ⟨Y₁, Y₂, m, g₁, g₂, h, sq⟩
    rw [coproducts_iff] at h
    obtain ⟨ι, ⟨F₁, F₂, c₁, c₂, h₁, h₂, φ, hφ⟩⟩ := h
    let π (i : ι) : α := ((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose
    let e (i : ι) : Arrow.mk (φ.app ⟨i⟩) ≅ Arrow.mk (g (π i)) :=
      eqToIso (((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose_spec)
    let e₁ (i : ι) : F₁.obj ⟨i⟩ ≅ A (π i) := Arrow.leftFunc.mapIso (e i)
    let e₂ (i : ι) : F₂.obj ⟨i⟩ ≅ B (π i) := Arrow.rightFunc.mapIso (e i)
    exact ⟨{
      ι := ι
      π := π
      cofan₁ := Cofan.mk c₁.pt (fun i ↦ (e₁ i).inv ≫ c₁.ι.app ⟨i⟩)
      cofan₂ := Cofan.mk c₂.pt (fun i ↦ (e₂ i).inv ≫ c₂.ι.app ⟨i⟩)
      isColimit₁ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₁ i)) _).1
          (IsColimit.ofIsoColimit h₁ (Cocone.ext (Iso.refl _) (by simp)))
      isColimit₂ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₂ i)) _).1
          (IsColimit.ofIsoColimit h₂ (Cocone.ext (Iso.refl _) (by simp)))
      hm i := by simp [e₁, e₂]
      isPushout := sq, .. }⟩

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 : J
hi : i < j
⊢ (ofCocone c).map (homOfLE ⋯) = (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv

Tactic:
dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]
  rw [dif_neg (by simp), dif_pos hi, comp_id]

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

Goal state before:
pp: case neg.inl
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₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩) =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, h₂⟩).inv) ≫
      if h₂ : i₂ ≤ j then
        (objIso F X ⟨i₂, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
      else eqToHom ⋯

Tactic:
dif_pos h₂,

Goal state after:
case neg.inl
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₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩) =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, h₂⟩).inv) ≫
      (objIso F X ⟨i₂, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))

Tactic:
πObj_ιIteration_app_right,

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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom
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 + -padicValRat p r = padicValRat p q - padicValRat p r

Tactic:
sub_eq_add_neg

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
rw [sub_eq_add_neg, ← padicNorm.neg r]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑(p ^ n) ∣ ↑a ↔ ↑p ^ n ∣ a

Tactic:
← norm_int_le_pow_iff_dvd,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑(p ^ n) ∣ ↑a ↔ ‖↑a‖ ≤ ↑p ^ (-↑n)
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Subsingleton (F.H n)

Tactic:
by
  rw [← functorH_obj_coe]
  apply AddCommGrpCat.subsingleton_of_isZero
  exact Functor.map_isZero (functorH J n) h

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:
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
P Q : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ (P.map g ≫ Pi.lift fun x ↦ Φ.toPresheafFiber (unop Y) x P ≫ f) =
    (Pi.lift fun x ↦ Φ.toPresheafFiber (unop X) x P ≫ f) ≫ (Φ.skyscraperPresheaf M).map g

Tactic:
dsimp
        ext y
        have := Φ.toPresheafFiber_w g.unop y P
        dsimp at this
        simp [reassoc_of% this]

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
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
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
V : C
g : unop (op V) ⟶ U
this : Sieve.pullback g (Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U))) ∈ J (unop (op V))
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm g) ∈ J V

Tactic:
rw [Presheaf.pullback_imageSieve] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
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
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
V : C
g : unop (op V) ⟶ U
this :
  Presheaf.imageSieve f
      ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))) ∈
    J (unop (op V))
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm g) ∈ J V
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : S.Etale
x : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj X
⊢ ∃ j,
    (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
      Nonempty (j ⟶ ⟨X, x⟩)

Tactic:
cases X with

Goal state after:
case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
x : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj (Etale.mk f)
⊢ ∃ j,
    (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
      Nonempty (j ⟶ ⟨Etale.mk f, x⟩)
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : S.Etale
R : Sieve X
hR : R ∈ S.smallEtaleTopology X
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj X
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f)) y = φ

Tactic:
cases X with

Goal state after:
case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj (Etale.mk f)
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f_1)) y = φ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne)) < ε

Tactic:
cases _root_.le_total N (stationaryPoint hne) with
  | inl hgen =>
    exact hN _ hgen _ hi
  | inr hngen =>
    have := stationaryPoint_spec hne le_rfl hngen
    rw [← this]
    exact hN _ le_rfl _ hi

Goal state after: