mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
⊢ ∀ ⦃X : Q.Over ⊤ S⦄ (S_1 : Presieve X) (Ti : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → S_1 f → Presieve Y),
    S_1 ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h} →
      (∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : S_1 f),
          Ti f H ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}) →
        S_1.bind Ti ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}

Tactic:
by
    rintro X _ T ⟨𝒰, h, p, rfl⟩ H
    choose V h pV hV using H
    let 𝒱j (j : 𝒰.I₀) : (Cover (precoverage P) ((𝒰.X j).asOverProp S (p j)).left) :=
      V ((𝒰.f j).asOverProp S) ⟨j⟩
    refine ⟨𝒰.bind (fun j ↦ 𝒱j j), inferInstance, fun j ↦ pV _ _ _, ?_⟩
    convert!
      Presieve.ofArrows_bind _ (fun j ↦ ((𝒰.f j).asOverProp S)) _
        (fun Y f H j ↦ ((V f H).X j).asOverProp S (pV _ _ _))
        (fun Y f H j ↦ ((V f H).f j).asOverProp S)
    apply hV

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

Goal state before:
pp: case mpr
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows

Tactic:
· rintro ⟨T, ⟨𝒰, h, p, rfl⟩, le⟩
    use 𝒰, h
    rintro - - ⟨i⟩
    exact ⟨(𝒰.X i).asOverProp S (p i), (𝒰.f i).asOverProp S, 𝟙 _, le _ _ ⟨i⟩, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯ ≫ homOfLE hf).op)) t = 0

Tactic:
op_comp,

Goal state after:
case refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map ((homOfLE hf).op ≫ (homOfLE ⋯).op))) t = 0
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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
⊢ { I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
          Y := fun i j ↦ U (pullback (f S i) (f S j)),
          p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
          p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)), w := ⋯ }.sieve₁₀
      p₁ p₂ ∈
    J₀ W₀

Tactic:
← functorPushforward_mem_iff J₀ J F

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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
⊢ Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
            Y := fun i j ↦ U (pullback (f S i) (f S j)),
            p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ }.sieve₁₀
        p₁ p₂) ∈
    J (F.obj W₀)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ IsUnit ((algebraMap (↑R) (Module.End ↑R ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))))) f)

pp: case refine_3
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f)))),
    ∃ n y, f ^ n • x = (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) y

pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))),
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0

Tactic:
· exact Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen f le_rfl

Goal state after:
case refine_3
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f)))),
    ∃ n y, f ^ n • x = (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) y

case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))),
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
⊢ data.sieve f ∈ J₀ X₀

Tactic:
← functorPushforward_mem_iff J₀ J F

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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
⊢ Sieve.functorPushforward F (data.sieve f) ∈ J (F.obj X₀)
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ ∀ {Y_1 Z : C} {f_1 : Y_1 ⟶ X}, (∃ e, e ≫ f = f_1) → ∀ (g : Z ⟶ Y_1), ∃ e, e ≫ f = g ≫ f_1

Tactic:
rintro W Z g ⟨e, rfl⟩ q

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
W Z : C
e : W ⟶ Y
q : Z ⟶ W
⊢ ∃ e_1, e_1 ≫ f = q ≫ e ≫ 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 Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
⊢ presheafMap data G₀ g ≫ restriction data G₀ f = restriction data G₀ (f ≫ g)

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property ⟨_, GrothendieckTopology.bind_covering
    (hS := cover_lift F J₀ J (J.pullback_stable f (data X).mem₀)) (hR := fun Y₀ a ha ↦
      cover_lift F J₀ J (J.pullback_stable
        (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g) (data Y).mem₀))⟩ _ _ ?_

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
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.bind (Sieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀)).arrows fun Y₀ a ha ↦
            Sieve.functorPullback F
              (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
                (data Y).toPreOneHypercover.sieve₀),
          ⋯⟩),
    (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map I.f.op =
      restriction data G₀ (f ≫ g) ≫ G₀.obj.map I.f.op
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: ⊢ fppfPrecoverage ≤ fpqcPrecoverage

Tactic:
by
  rw [fpqcPrecoverage, propQCPrecoverage, le_inf_iff]
  refine ⟨?_, precoverage_mono fun X Y f ⟨hf, _⟩ ↦ inferInstance⟩
  exact precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f ⟨_, _⟩ ↦ f.isOpenMap

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 : IsPushout t l r b
⊢ Epi (kernel.map t b l r ⋯)

Tactic:
rw [epi_iff_surjective_up_to_refinements]
  intro A₀ z
  obtain ⟨A₁, π₁, _, x₁, hx₁⟩ := ((ShortComplex.mk _ _
    sq.cokernelCofork.condition).exact_of_g_is_cokernel
      sq.isColimitCokernelCofork).exact_up_to_refinements
        (z ≫ kernel.ι _ ≫ biprod.inr) (by simp)
  refine ⟨A₁, π₁, inferInstance, -kernel.lift _ x₁ ?_, ?_⟩
  · simpa using hx₁.symm =≫ biprod.fst
  · ext
    simpa using hx₁ =≫ biprod.snd

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ J.yoneda.map f ≫ J.yonedaEquiv.symm x = J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

Tactic:
apply J.yonedaEquiv.injective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ J.yonedaEquiv (J.yoneda.map f ≫ J.yonedaEquiv.symm x) =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x)

Tactic:
apply J.yonedaEquiv.injective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.yonedaEquiv (J.yonedaEquiv.symm x ≫ f) =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x))
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)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ (colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom ⋯) ≫ c.pt.hom =
    Over.Hom.left (c.ι.app j) ≫ c.pt.hom

Tactic:
rw [Category.assoc, Subobject.ofMkLEMk_comp, Over.w]

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
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ f = (F.obj j).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
⊢ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
ext j

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 ≫ 𝟙 (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
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : α ≤i J
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Tactic:
have := hj.nonempty_Iio.to_subtype

Goal state after:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : α ≤i J
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
this : Nonempty ↑(Set.Iio j)
⊢ HasColimitsOfShape (↑(Set.Iio j)) C
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case isMin
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
h : IsMin j
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F

Tactic:
| isMin j h =>

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

Goal state before:
pp: case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (if h₂ : i₃ < i₃ then (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else if h₁ : i₁ < i₃ then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯) =
    (if h₂ : i₂ < i₃ then (objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else if h₁ : i₁ < i₃ then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      if h₂ : i₃ < i₃ then (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else if h₁ : i₂ < i₃ then (objIso c i₂ h₁).hom ≫ c.ι.app ⟨i₂, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
· rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
          Cocone.w_assoc]

Goal state after:
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₂
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯

Tactic:
have := (Arrow.mk_eq_mk_iff _ _).1 (congr_arrowMap iter₁ iter₂ h h₁ h₂)
  tauto

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₁✝ : i < Order.succ j
hi₁ : i ≤ j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
obtain hi₁ | rfl := hi₁.lt_or_eq

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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i hi₁✝¹ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

case inr
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
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))).obj ⟨i, ⋯⟩)
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 ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
⊢ i = ⊥

Tactic:
simpa using hij

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)) (d.succ j hj e.val) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯ ≫ homOfLE ⋯).op)) (d.succ j hj e.val))

Tactic:
op_comp,

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)) (d.succ j hj e.val) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) (d.succ j hj e.val))
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 ⋯ ≫ homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val

Tactic:
op_comp,

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 ≫ (homOfLE ⋯).op))) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
⊢ padicValRat p 0 = 0

Tactic:
simp [padicValRat]

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

Goal state before:
pp: p : ℕ
⊢ padicValRat p 1 = 0

Tactic:
simp [padicValRat]

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

Goal state before:
pp: p : ℕ
z : ℤ
⊢ padicValRat p ↑z = ↑(padicValInt p z)

Tactic:
simp [padicValRat]

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

Goal state before:
pp: p n : ℕ
⊢ padicValRat p ↑n = ↑(padicValNat p n)

Tactic:
simp [padicValRat]

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
⊢ 1 ≤ padicValNat p n

Tactic:
rwa [← ENat.natCast_le_natCast, padicValNat_eq_emultiplicity hn,
    ← pow_dvd_iff_le_emultiplicity, pow_one]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n

Tactic:
rw [Subtype.ext_iff] at h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
m n : ℕ
h : ↑↑m = ↑↑n
⊢ ↑m = ↑n
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ
p n : ℕ
⊢ padicValNat p (n + 1) ≤ log p (n + 1)

Tactic:
rcases p with _ | _ | p

Goal state after:
case succ.zero
n : ℕ
⊢ padicValNat 0 (n + 1) ≤ log 0 (n + 1)

case succ.succ.zero
n : ℕ
⊢ padicValNat (0 + 1) (n + 1) ≤ log (0 + 1) (n + 1)

case succ.succ.succ
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑n‖ = 1 ↔ p.Coprime n

Tactic:
rw [norm_def, coe_natCast, Padic.norm_natCast_eq_one_iff]

Goal state after: