mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : IsMax i
⊢ lastCases (last n) succ i = i

Tactic:
obtain rfl : i = Fin.last n := by simpa using! hi

Goal state after:
n : ℕ
hi : IsMax (last n)
⊢ lastCases (last n) succ (last n) = last n
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
⊢ J.Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun Y ↦ ?_
  suffices h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v'}.obj Y) by
    rwa [Presieve.isSheaf_iff_of_nat_equiv]
    · intro
      exact Equiv.ulift.symm
    · intros
      rfl
  rw [← isSheaf_iff_isSheaf_of_type, Presheaf.isSheaf_of_iso_iff
    ((Functor.FullyFaithful.ofFullyFaithful F).compUliftYonedaCompWhiskeringLeft.app Y).symm]
  refine F.op_comp_isSheaf_of_isSheaf J K _ ?_
  rw [isSheaf_iff_isSheaf_of_type]
  apply GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
F : J ⥤ C
G : C ⥤ D
inst✝¹ : F.IsWellOrderContinuous
inst✝ : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
⊢ IsColimit ((Set.principalSegIio j).cocone (F ⋙ G))

Tactic:
by
    have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G j hj
    exact isColimitOfPreserves G (F.isColimitOfIsWellOrderContinuous j hj)

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

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯))

Tactic:
rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]

Goal state after:
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯) ≫ hf.F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso W
      (orderIsoShrink.{w'} J)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape (Shrink.{w', w} J)
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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := hasColimitsOfShape_of_isSuccLimit C i hi
⊢ ∀ (j_1 : ↑(Set.Iio i)),
    (colimit.cocone (restrictionLT iter.F hij)).ι.app j_1 ≫ (eqToIso ⋯).hom = (coconeOfLE iter.F hij).ι.app j_1

Tactic:
rintro ⟨k, hk⟩

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
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := hasColimitsOfShape_of_isSuccLimit C i hi
k : J
hk : k ∈ Set.Iio i
⊢ (colimit.cocone (restrictionLT iter.F hij)).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom = (coconeOfLE iter.F hij).ι.app ⟨k, hk⟩
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: 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
⊢ ¬↑⟨Order.succ j, ⋯⟩ ≤ j

Tactic:
simpa only [Order.succ_le_iff_isMax] using hj

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

Goal state before:
pp: 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
⊢ ¬Order.succ j ≤ j

Tactic:
simpa only [Order.succ_le_iff_isMax] using hj

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

Goal state before:
pp: 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
⊢ (objIso F X ⟨j, ⋯⟩).hom ≫ 𝟙 (F.obj ⟨j, ⋯⟩) ≫ τ ≫ (objSuccIso hj F X).inv =
    (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
id_comp

Goal state after:
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
⊢ (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv = (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv
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 } ≫ functorMapSrc f τ ≫ functorObjTop f πY =
    Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjTop f πX ≫ Arrow.Hom.left τ

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

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

Goal state before:
pp: 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
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ ¬Order.succ j ≤ j

Tactic:
simpa only [Order.succ_le_iff_isMax] using hj

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

Goal state before:
pp: case inr
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₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = 𝟙 (obj c i₁) ≫ map c i₁ i₃ hi' hi₃

Tactic:
id_comp

Goal state after:
case inr
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₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₃ hi' hi₃
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 ⋯) ⋯
⊢ ∀ (j : ↑(Set.Iio i)),
    (coconeOfLE (Φ.iter i).F ⋯).ι.app j ≫ (eqToIso ⋯).hom =
      ((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))).ι.app j

Tactic:
rintro ⟨k, hk⟩

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 ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
⊢ (coconeOfLE (Φ.iter i).F ⋯).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom =
    ((Cocone.precompose e.inv).obj ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))).ι.app ⟨k, hk⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

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

Tactic:
by
    obtain rfl : i = ⊥ := by simpa using hij
    simpa using hi.not_isMin

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) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val

Tactic:
← homOfLE_comp (Order.succ_le_of_lt hij) (Order.le_succ j),

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 ⋯ ≫ homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val
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 A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom =
    𝟙 ((relativeCellComplexιObj I κ f).F.obj j) ≫
      (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom

Tactic:
id_comp

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 A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom =
    (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).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
⊢ q * r = q.num * r.num /. (↑q.den * ↑r.den)

Tactic:
rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
⊢ (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

Tactic:
by_cases hA : A = ⊤
  · subst hA
    have := (Subobject.isIso_arrow_iff_eq_top (largerSubobject hG (⊤ : Subobject X))).2 (by simp)
    exact (MorphismProperty.arrow_mk_iso_iff _
      (Arrow.isoMk (asIso (Subobject.arrow _)) (asIso (Subobject.arrow _)) (by simp))).2
        (isomorphisms_le_pushouts_generatingMonomorphisms G (𝟙 X)
          (MorphismProperty.isomorphisms.infer_property _))
  · refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1
      (exists_larger_subobject hG A hA).choose_spec.choose_spec
    exact Arrow.isoMk (Iso.refl _)
      (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA])))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (Ideal.span {↑p}).IsPrime

pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0

Tactic:
← maximalIdeal_eq_span_p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (maximalIdeal ℤ_[p]).IsPrime

p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ 0 ≤ -x.valuation

Tactic:
Right.nonneg_neg_iff

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0
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 ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint ⋯)) =
    padicNorm p (↑f (stationaryPoint ⋯)) * padicNorm p (↑g (stationaryPoint ⋯))

Tactic:
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (max (stationaryPoint hfg) (max ?v2✝ ?v3✝))) =
    padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) *
      padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : a.norm = padicNorm p k
hk' : k ≠ 0
⊢ ∃ z, a.norm = ↑p ^ (-z)

Tactic:
simpa [hk] using padicNorm.values_discrete hk'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ (c.fst ≫ φ) ≫ c.snd = 𝟙 c.pt ≫ c.snd

Tactic:
· simp only [assoc, hφ₂, id_comp, comp_id, h]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) ≤
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))

Tactic:
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2✝ ?v3✝))) ≤
    max (padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))))
      (padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg)))))

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) j))) •
        (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) j))) ≫ X.σ ⟨a, ⋯⟩ =
      0

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) ⟨k, hk⟩))) •
      (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) ⟨k, hk⟩))) ≫ X.σ ⟨a, ⋯⟩ =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 3) j)) * (-1) ^ (a + 1)) •
        (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) j)) =
      0

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)) * (-1) ^ (a + 1)) •
      (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩)) =
    0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ‖q‖ ≠ ‖r‖
⊢ ‖q + r‖ = max ‖q‖ ‖r‖

Tactic:
by
  dsimp [norm] at h ⊢
  have : padicNormE q ≠ padicNormE r := mod_cast h
  exact mod_cast padicNormE.add_eq_max_of_ne' this

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

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

Tactic:
simpa using norm_int_le_one _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
  have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
  have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
  rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
        exact le_valuation_add hxy

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

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ X.δ 0 ≫ X.σ 0 + -X.σ 0 ≫ X.δ 1 ≫ X.σ 0 +
        (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 ≫ 𝟙 (X _⦋1⦌) + -X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.succ 1)))) =
    0

Tactic:
← Fin.castSucc_zero (n := 1),

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ X.δ (Fin.castSucc 0) ≫ X.σ 0 + -X.σ 0 ≫ X.δ 1 ≫ X.σ 0 +
        (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 + (X.σ 0 ≫ 𝟙 (X _⦋1⦌) + -X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.succ 1)))) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 + (X.σ 0 + -X.σ 0 ≫ X.δ (Fin.succ 0) ≫ X.σ 0 + (-X.σ 0 ≫ X.δ 0 ≫ X.σ 0 + (X.σ 0 + -X.σ 0))) = 0

Tactic:
← Fin.castSucc_zero (n := 1),

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 + (X.σ 0 + -X.σ 0 ≫ X.δ (Fin.succ 0) ≫ X.σ 0 + (-X.σ 0 ≫ X.δ (Fin.castSucc 0) ≫ X.σ 0 + (X.σ 0 + -X.σ 0))) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ (f.postComp h).φ = f.φ ≫ h

Tactic:
unfold φ postComp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
h : Z ⟶ Z'
⊢ PInfty.f (n + 1) ≫ { a := f.a ≫ h, b := fun i ↦ f.b i ≫ h }.a +
      ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ { a := f.a ≫ h, b := fun i ↦ f.b i ≫ h }.b i.rev =
    (PInfty.f (n + 1) ≫ f.a + ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev) ≫ h
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ A.pull θ = Splitting.IndexSet.mk e

Tactic:
dsimp only [SimplicialObject.Splitting.IndexSet.pull]

Goal state after:
case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ A.e)) = Splitting.IndexSet.mk e