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

Goal state before:
pp: case inl
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
val✝ : 𝒰.ulift.I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f (Sum.inl val✝))

pp: case inr
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
val✝ : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f (Sum.inr val✝))

Tactic:
<;>

Goal state after:
case inl
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
val✝ : 𝒰.ulift.I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f (Sum.inl val✝))

case inr
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
val✝ : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f (Sum.inr val✝))
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : P f
inst✝¹ : Surjective f
inst✝ : QuasiCompact f
⊢ Presieve.singleton f ∈ (precoverage P).coverings Y

Tactic:
grind [singleton_mem_precoverage_iff]

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

Goal state before:
pp: case refine_3.inr.refine_2
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate]

Goal state after:
case refine_3.inr.refine_2
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))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
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 : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
| e a

Tactic:
rw [← Category.id_comp (e a)]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
| 𝟙 (X a) ≫ e a
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
⊢ ((Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
        {
          hom :=
            ⋯.extend
              {
                app := fun Y ↦
                  ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
                naturality := ⋯ } }).hom =
    (s.inj j).hom

Tactic:
have (j : ι) : u j ≫ (Sieve.ofArrows _ c.inj).functorInclusion =
      CategoryTheory.yoneda.map (c.inj j) := rfl

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = CategoryTheory.yoneda.map (c.inj j)
⊢ ((Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
        {
          hom :=
            ⋯.extend
              {
                app := fun Y ↦
                  ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
                naturality := ⋯ } }).hom =
    (s.inj j).hom
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a

pp: case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a

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

pp: case succ
⊢ Fin 0 → Fin 0

Tactic:
<;>

Goal state after:
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a

case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a

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

case succ
⊢ Fin 0 → Fin 0
Module: Mathlib.Data.Fin.SuccPredOrder

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

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

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

pp: case succ
a : Fin 0
⊢ Fin 0

Tactic:
<;>

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

case max_of_succ_le
a : Fin 0
⊢ ?succ ≤ a → IsMax a

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

case succ
a : Fin 0
⊢ Fin 0
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a

pp: case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

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

pp: case pred
⊢ Fin 0 → Fin 0

Tactic:
<;>

Goal state after:
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a

case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

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

case pred
⊢ Fin 0 → Fin 0
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x : ↑(Iic j)
k : α
h : k < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ } x
⊢ k ∈ range ⇑{ toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
simpa using h.le.trans x.2

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

Goal state before:
pp: case refine_2
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
⊢ Arrow.mk (colim.map c.ι) ≅ Arrow.mk (𝟙 c.pt)

Tactic:
exact Arrow.isoMk (IsColimit.coconePointUniqueUpToIso (colimit.isColimit Y) hc)
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
        (isColimitConstCocone J c.pt))

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

Goal state before:
pp: case «0»
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'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

pp: case «1»
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'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

Tactic:
<;>

Goal state after:
case «0»
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'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

case «1»
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'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

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

Tactic:
dif_pos (hi₂₃.trans hi₃'),

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

Goal state before:
pp: case inl.e_F
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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ = Arrow.mk ((iter l₁ ⋯).mapObj (iter l₂ ⋯) pf✝ ⋯ ⋯ pf✝)

Tactic:
arrow_mk_mapObj

Goal state after:
case inl.e_F
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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ = arrowMap (iter l₂ ⋯).F l₁ l₂ pf✝ ⋯
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr.e_F
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
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter l₂ pf✝⁷).F l₁ l₂ pf✝⁵ pf✝³ = Arrow.mk ((iter ↑⟨l₁, pf✝²⟩ ⋯).mapObj (iter l₂ hl₂) pf✝ ⋯ ⋯ pf✝)

Tactic:
arrow_mk_mapObj

Goal state after:
case inr.e_F
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
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter l₂ pf✝⁷).F l₁ l₂ pf✝⁵ pf✝³ = arrowMap (iter l₂ hl₂).F (↑⟨l₁, pf✝²⟩) l₂ pf✝ ⋯
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 ⊥)
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
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:
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

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

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
X' : C
i : A✝ ⟶ X'
p' : X' ⟶ X
hi : (generatingMonomorphisms G).pushouts i
hi' : ¬IsIso i
hp' : Mono p'
fac : i ≫ p' = f
⊢ (Subobject.underlyingIso f).hom ≫ i = (Subobject.mk f).ofLE (Subobject.mk p') ⋯ ≫ (Subobject.underlyingIso p').hom

Tactic:
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: case inl.zero
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValRat p (0 ^ 0) = ↑0 * padicValRat p 0

pp: case inl.succ
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
⊢ padicValRat p (0 ^ (n✝ + 1)) = ↑(n✝ + 1) * padicValRat p 0

Tactic:
<;>

Goal state after:
case inl.zero
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValRat p (0 ^ 0) = ↑0 * padicValRat p 0

case inl.succ
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
⊢ padicValRat p (0 ^ (n✝ + 1)) = ↑(n✝ + 1) * padicValRat p 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

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

pp: case inr.succ
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
n✝ : ℕ
a✝ : padicValRat p (q ^ n✝) = ↑n✝ * padicValRat p q
⊢ padicValRat p (q ^ (n✝ + 1)) = ↑(n✝ + 1) * padicValRat p q

Tactic:
<;>

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

case inr.succ
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
n✝ : ℕ
a✝ : padicValRat p (q ^ n✝) = ↑n✝ * padicValRat p q
⊢ padicValRat p (q ^ (n✝ + 1)) = ↑(n✝ + 1) * padicValRat p q
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case nat
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n✝ : ℕ
⊢ padicValRat p (q ^ ↑n✝) = ↑n✝ * padicValRat p q

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
a✝ : ∀ (n : ℕ), padicValRat p (q ^ ↑n) = ↑n * padicValRat p q
n✝ : ℕ
⊢ padicValRat p (q ^ (-↑n✝)) = -↑n✝ * padicValRat p q

Tactic:
<;>

Goal state after:
case nat
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n✝ : ℕ
⊢ padicValRat p (q ^ ↑n✝) = ↑n✝ * padicValRat p q

case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
a✝ : ∀ (n : ℕ), padicValRat p (q ^ ↑n) = ↑n * padicValRat p q
n✝ : ℕ
⊢ padicValRat p (q ^ (-↑n✝)) = -↑n✝ * padicValRat p q
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

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

Tactic:
intro X Y p hp A B i (_ : Mono i)
    obtain ⟨J, _, _, _, _, ⟨h⟩⟩ :=
      generatingMonomorphisms.exists_transfiniteCompositionOfShape hG i
    exact transfiniteCompositionsOfShape_le_llp_rlp _ _ _ h.mem _ (by simpa)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑p ∣ m

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑(p ^ 1) ∣ m
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < ↑p

pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < ↑p

Tactic:
<;>

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < ↑p

case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ -padicValRat p ↑m = 0

pp: case neg.ha₀
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ 0 < ↑p

pp: case neg.ha₁
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ≠ 1

Tactic:
<;>

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ -padicValRat p ↑m = 0

case neg.ha₀
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ 0 < ↑p

case neg.ha₁
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ≠ 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
hne : ⟨fun n ↦ ↑(seq n), h⟩ ≈ 0
⊢ ↑0 ≤ 1

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
hne : ¬⟨fun n ↦ ↑(seq n), h⟩ ≈ 0
⊢ ↑(padicNorm p (↑⟨fun n ↦ ↑(seq n), h⟩ (PadicSeq.stationaryPoint hne))) ≤ 1

Tactic:
<;>

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
hne : ⟨fun n ↦ ↑(seq n), h⟩ ≈ 0
⊢ ↑0 ≤ 1

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n ↦ ↑(seq n)
hne : ¬⟨fun n ↦ ↑(seq n), h⟩ ≈ 0
⊢ ↑(padicNorm p (↑⟨fun n ↦ ↑(seq n), h⟩ (PadicSeq.stationaryPoint hne))) ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε

Tactic:
obtain ⟨k, hk⟩ := @exists_pow_neg_lt p _ ε (mod_cast hε)
  use k
  rw [show (p : ℝ) = (p : ℚ) by simp] at hk
  exact mod_cast hk

Goal state after:
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
⊢ ‖z‖ = 1

Tactic:
refine le_antisymm (norm_le_one _) ?_

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