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

Goal state before:
pp: case refine_3
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))
⊢ Presieve.IsSheaf (propQCTopology P) F

Tactic:
rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small.{u}]

Goal state after:
case refine_3
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))
⊢ ∀ ⦃X : Scheme⦄ (E : (propQCPrecoverage P).ZeroHypercover X), Presieve.IsSheafFor F E.presieve₀
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ S.pt
⊢ (∀ (j : (Sieve.generateSingleton f).arrows.category),
      (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
    m = Hf.desc (S.ι.app { obj := Over.mk f, property := ⋯ }) ⋯

Tactic:
hm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
m : (Sieve.generateSingleton f).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateSingleton f).arrows.category), (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = S.ι.app j
⊢ m = Hf.desc (S.ι.app { obj := Over.mk f, property := ⋯ }) ⋯
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ ∀ {Y Z : C} {f : Y ⟶ B}, (∃ a g, g ≫ π a = f) → ∀ (g : Z ⟶ Y), ∃ a g_1, g_1 ≫ π a = g ≫ f

Tactic:
rintro Y₁ Y₂ g₁ ⟨a, q, rfl⟩ e

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y₁ Y₂ : C
a : α
q : Y₁ ⟶ X a
e : Y₂ ⟶ Y₁
⊢ ∃ a_1 g, g ≫ π a_1 = e ≫ q ≫ π a
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
⊢ (∀ (j : (Sieve.generateFamily X π).arrows.category),
      (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j) →
    m = H.desc (fun a ↦ S.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯

Tactic:
hm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
⊢ m = H.desc (fun a ↦ S.ι.app { obj := Over.mk (π a), property := ⋯ }) ⋯
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
⊢ x₄ = 0

Tactic:
obtain ⟨T₁, π, _, x₂, x₃, eq⟩ := hom_eq_add_up_to_refinements h₁ x₄

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
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
⊢ Mono (c.ι.app j₀)

Tactic:
let f : (Functor.const _).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
    { app j := X.map j.hom
      naturality _ _ g := by
        dsimp
        simp only [Category.id_comp, ← X.map_comp, Under.w] }

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j ↦ X.map j.hom, naturality := ⋯ }
⊢ Mono (c.ι.app j₀)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

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

Tactic:
rw [le_iSup_iff]
    intro s H
    induction s using Subobject.ind with | _ g
    let c' : Cocone (F ⋙ MonoOver.forget _ ⋙ Over.forget _) := Cocone.mk _
      { app j := Subobject.ofMkLEMk _ _ (H j)
        naturality j j' f := by
          dsimp
          simpa only [← cancel_mono g, Category.assoc, Subobject.ofMkLEMk_comp,
            Category.comp_id] using MonoOver.w (F.map f) }
    exact Subobject.mk_le_mk_of_comm (hc.desc c')
      (hc.hom_ext (fun j ↦ by rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]))

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case le_succ
a : Fin 0
⊢ a ≤ ?succ

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case max_of_succ_le
a : Fin 0
⊢ ?succ ≤ a → IsMax a

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case succ_le_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → ?succ ≤ b

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case succ
a : Fin 0
⊢ Fin 0

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case pred_le
a : Fin 0
⊢ ?pred a ≤ a

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case min_of_le_pred
a : Fin 0
⊢ a ≤ ?pred a → IsMin a

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case le_pred_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → a ≤ ?pred b

Tactic:
exact elim0 a

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case pred
a : Fin 0
⊢ Fin 0

Tactic:
exact elim0 a

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

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

Tactic:
NatTrans.comp_app,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ z =
    (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ ((Functor.const J).map z).app j
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
α : Type u_1
inst✝ : PartialOrder α
h : α <i J
hα : Order.IsSuccLimit h.top
this : HasColimitsOfShape (↑(Set.Iio h.top)) C
⊢ HasColimitsOfShape α C

Tactic:
exact hasColimitsOfShape_of_equivalence h.orderIsoIio.equivalence.symm

Goal state after:
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, ⋯⟩ ∈ Set.Iio m

Tactic:
by_contra h'

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) :=
  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' : ⟨j, ⋯⟩ ∉ Set.Iio m
⊢ False
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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjLeft f πX ≫ functorMapTgt f τ =
    Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f τ ≫ functorObjLeft f πY

Tactic:
simp [ι_functorMapTgt f τ i t b w _ rfl, ι_functorMapSrc_assoc f τ i t b w _ rfl]

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

Goal state before:
pp: case 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
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂),
    j₁ ≤ j₂ → arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
hj : ¬j₁ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

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

Tactic:
· simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)]

Goal state after:
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
k₁ k₂ : J
h : k₁ ≤ k₂
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
⊢ IsColimit ((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J)))

Tactic:
refine IsColimit.ofIsoColimit ((Φ.iter i).isColimit i hi (by simp)) ?_

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
e : ⋯.functor ⋙ Φ.iterationFunctor J ≅ restrictionLT (Φ.iter i).F ⋯ := NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯
⊢ coconeOfLE (Φ.iter i).F ⋯ ≅ (Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
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
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (fun x ↦
      match x with
      | op ⟨k_1, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val) =
    fun x ↦
    match x with
    | op ⟨k_1, hk⟩ =>
      (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val)

Tactic:
ext ⟨l, hl⟩

Goal state after:
case e_x
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
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ (match op ⟨l, hl⟩ with
    | op ⟨k_1, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val) =
    match op ⟨l, hl⟩ with
    | op ⟨k_1, hk⟩ =>
      (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val)
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
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this✝ : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ IsColimit ((Set.principalSegIio m).cocone (functor hG A₀ J))

Tactic:
apply IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup
      ((Set.principalSegIio m).monotone.functor ⋙ functorToMonoOver hG A₀ J) c

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this✝ : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) := ⋯
this : Mono c.pt.hom
⊢ Subobject.mk c.pt.hom = ⨆ j, Subobject.mk ((⋯.functor ⋙ functorToMonoOver hG A₀ J).obj j).obj.hom
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
by
  obtain rfl | hz := eq_or_ne z 0
  · simp
  · rw [padicNorm, if_neg (mod_cast hz)]
    exact zpow_le_one_of_nonpos₀ (mod_cast hp.1.one_le) (by simp)

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

Goal state before:

Tactic:
_ ≤ min (emultiplicity ↑p (q.num * r.den * q.den))
                (emultiplicity ↑p (q.den * r.num * q.den)) :=
          le_min
            (by rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm])
            (by grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h])
        _ ≤ _ := min_le_emultiplicity_add

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
obtain rfl | hs := Finset.eq_empty_or_nonempty s

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ i ∈ ∅, padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ ∅, F i) < t

case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
obtain rfl | hs := Finset.eq_empty_or_nonempty s

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ i ∈ ∅, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ ∅, F i) ≤ t

case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t
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:
by rw [Subtype.ext_iff] at h; norm_cast at h

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (p ^ n * q ^ m) = m

Tactic:
mul_comm (p ^ n) (q ^ m)

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (q ^ m * p ^ n) = m
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖1‖ ≤ ‖z‖
⊢ 1 ≤ ‖z‖

Tactic:
norm_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : 1 ≤ ‖z‖
⊢ 1 ≤ ‖z‖
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 G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Ext.addEquiv₀ ((map f 0) x) = Ext.addEquiv₀ x ≫ f

Tactic:
delta Ext.addEquiv₀

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ (let __Equiv := Ext.homEquiv₀;
      { toEquiv := __Equiv, map_add' := ⋯ })
      ((map f 0) x) =
    (let __Equiv := Ext.homEquiv₀;
        { toEquiv := __Equiv, map_add' := ⋯ })
        x ≫
      f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
by
  apply stationaryPoint_spec hf
  · apply le_trans
    · apply le_max_left _ v3
    · apply le_max_right
  · exact le_rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (f + g).norm = max f.norm g.norm

Tactic:
unfold norm at hfgne ⊢; split_ifs at hfgne ⊢
      -- Porting note: originally `padic_index_simp [hfg, hf, hg] at hfgne ⊢`
      rw [lift_index_left hf, lift_index_right hg] at hfgne
      · rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
        exact padicNorm.add_eq_max_of_ne hfgne

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

Tactic:
have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq :
  ((G.mapHomologicalComplex c).map (nullHomotopicMap' (hσ' q))).f n =
    (nullHomotopicMap' fun i j hij ↦ G.map (hσ' q i j hij)).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 ↔ ↑p ∣ k

Tactic:
constructor
  · intro h
    contrapose! h
    apply le_of_eq
    rw [eq_comm]
    calc
      ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
      _ = padicNorm p k := eq_padicNorm _
      _ = 1 := mod_cast (int_eq_one_iff k).mpr h
  · rintro ⟨x, rfl⟩
    push_cast
    rw [padicNormE.mul]
    calc
      _ ≤ ‖(p : ℚ_[p])‖ * 1 :=
        mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
      _ < 1 := by
        rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z2 - z1‖ < ‖z1‖

Tactic:
simpa [← norm_neg (z1 - _)] using h

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : a = ↑j
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ ≫ X.δ j.succ

Tactic:
simp only [hj₂, Fin.eta, δ_comp_σ_succ, comp_id]
    rfl

Goal state after: