mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ b ≤ a

Tactic:
← s.le_iff_le

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✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ s.toRelEmbedding b ≤ s.toRelEmbedding a
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} W ≤ W

Tactic:
intro _ _ f hf
  rw [transfiniteCompositions_iff] at hf
  obtain ⟨J, _, _, _, _, hf⟩ := hf
  exact W.transfiniteCompositionsOfShape_le J _ hf

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case mk
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
val✝ : F.obj (op j)
map_zero✝ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = val₀
map_succ✝ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (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✝,
          ⋯⟩
h : { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }.val = e'.val
⊢ { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ } = e'

Tactic:
cases e'

Goal state after:
case mk.mk
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
val✝¹ : F.obj (op j)
map_zero✝¹ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹ = val₀
map_succ✝¹ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹ =
      d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (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✝¹,
          ⋯⟩
val✝ : F.obj (op j)
map_zero✝ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = val₀
map_succ✝ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (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✝,
          ⋯⟩
h :
  { val := val✝¹, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
    { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }.val
⊢ { val := val✝¹, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ } =
    { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: case right
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ isomorphisms C (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))

Tactic:
rw [MorphismProperty.isomorphisms.iff]
    dsimp [succStruct]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ RelativeCellComplex (fun x ↦ I.homFamily) (ιObj I κ f)

Tactic:
by
  have := hasIterationOfShape I κ
  let h := transfiniteCompositionOfShapeSuccStructPropιIteration I κ
  exact
  { toTransfiniteCompositionOfShape :=
      h.toTransfiniteCompositionOfShape.map ((evaluation _ _).obj f ⋙ Arrow.leftFunc)
    attachCells j hj :=
      attachCellsOfSuccStructProp I κ (h.map_mem j hj) f }

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 Y : C
p : X ⟶ Y
inst✝ : Mono p
hp :
  ¬∀ (G_1 : C),
      ObjectProperty.singleton G G_1 →
        Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (Opposite.op G_1)).map p))
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Tactic:
simp only [ObjectProperty.singleton_iff, Function.Surjective, Functor.flip_obj_map, forall_eq',
    not_forall, not_exists] at hp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
hp :
  ∃ x,
    ∀ (x_1 : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x_1 = x
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p
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))
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift

Tactic:
intro g

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
⊢ ∀ {g_1 : B ⟶ Y} (sq : CommSq g i (πObj I κ f) g_1), sq.HasLift
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
⊢ Subobject.mk (transfiniteIterate (largerSubobject hG) m A₀).arrow =
    ⨆ j, Subobject.mk (transfiniteIterate (largerSubobject hG) (↑j) A₀).arrow

Tactic:
simp only [Subobject.mk_arrow]

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) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ transfiniteIterate (largerSubobject hG) m A₀ = ⨆ j, transfiniteIterate (largerSubobject hG) (↑j) A₀
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 κ
f : Arrow C
⊢ objMap I κ (𝟙 f) = 𝟙 (obj I κ f.hom)

Tactic:
by
  simp only [objMap, Functor.map_id]
  rfl

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

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

Tactic:
induction k

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.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty f (πObj I κ f)
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts f

Tactic:
refine ⟨_, _, _, ?_, transfiniteCompositionsOfShape_ιObj I κ f⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty f (πObj I κ f)
⊢ RetractArrow f (ιObj I κ f)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
      simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)

Tactic:
rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ←
        emultiplicity_le_emultiplicity_iff, mul_left_comm,
        emultiplicity_mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)

Tactic:
exact hF d (lt_add_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:
norm_cast at h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
hz : ‖z‖ = 1
⊢ z.inv * z = 1

Tactic:
rw [mul_comm, mul_inv hz]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ r * ↑r.den = ↑r.num

Tactic:
@Rat.mul_den_eq_num r

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ ↑r.num = ↑r.num
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)
T : C
hT : Limits.IsTerminal T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ (ConcreteCategory.hom (f.hom.app (op T))) ((equiv₀ F hT) x) = (equiv₀ G hT) ((map f 0) x)

Tactic:
by
  simp only [equiv₀, AddEquiv.trans_apply, addEquiv₀_map f x]
  rfl

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

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

Tactic:
apply stationaryPoint_spec hf
  · apply le_max_left
  · exact le_rfl

Goal state after:
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
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
⊢ x ≠ 0

Tactic:
intro h0

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
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
h0 : x = 0
⊢ False
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ IsPullback (𝟙 X) (𝟙 X) f f

Tactic:
by
  constructor
  · intro
    exact IsPullback.of_isLimit (PullbackCone.isLimitMkIdId f)
  · intro hf
    exact (mono_iff_fst_eq_snd hf.isLimit).2 rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ padicNorm p (↑f i) ≠ padicNorm p (-↑g i)

Tactic:
← padicNorm.neg (g i)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
h : padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠ padicNorm p (-↑g i)
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x

Tactic:
let b : X.residueField x →ₐ[S.residueField (f x)] Ω :=
    IsSepClosed.lift

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
algInst✝¹ : Algebra ↑(S.residueField (f x)) ↑(X.residueField x) := m.toAlgebra
algInst✝ : Algebra ↑(S.residueField (f x)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑(X.residueField x) →ₐ[↑(S.residueField (f x))] Ω := IsSepClosed.lift
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
⊢ ⋃ i,
      Set.range
        ⇑((SpecToEquivOfField (SeparableClosure ↑(S.residueField i)) S).invFun
            ⟨i, CommRingCat.ofHom (algebraMap (↑(S.residueField i)) (SeparableClosure ↑(S.residueField i)))⟩) =
    Set.univ

Tactic:
ext s

Goal state after:
S : Scheme
s : ↥S
⊢ s ∈
      ⋃ i,
        Set.range
          ⇑((SpecToEquivOfField (SeparableClosure ↑(S.residueField i)) S).invFun
              ⟨i, CommRingCat.ofHom (algebraMap (↑(S.residueField i)) (SeparableClosure ↑(S.residueField i)))⟩) ↔
    s ∈ Set.univ
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
h✝ : n < q
⊢ f.app (op ⦋n⦌) ≫ 0 = 0 ≫ f.app (op ⦋n + 1⦌)

pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
h✝ : ¬n < q
⊢ f.app (op ⦋n⦌) ≫ ((-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) = ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)

Tactic:
· rw [zero_comp, comp_zero]

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
h✝ : ¬n < q
⊢ f.app (op ⦋n⦌) ≫ ((-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) = ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑↑p)⁻¹

Tactic:
rw [← @Rat.cast_natCast ℚ_[p] _ p]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q φ

Tactic:
← hφ

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ (P q).f (n + 1))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
by simpa using norm_int_le_one _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
h : ∃ i, ∀ j ≥ i, ‖↑f j - ↑f i‖ < ↑ε
⊢ ∃ i, ∀ j ≥ i, padicNormE (↑f j - ↑f i) < ε

Tactic:
dsimp [norm] at h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
h : ∃ i, ∀ j ≥ i, ↑(padicNormE (↑f j - ↑f i)) < ↑ε
⊢ ∃ i, ∀ j ≥ i, padicNormE (↑f j - ↑f i) < ε
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ QInfty = 0

Tactic:
ext n
  apply PInfty_f_comp_QInfty_f

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

Goal state before:
pp: case neg.inl.H
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
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ ⟨a + 1, ⋯⟩ ≤ j.castSucc

pp: case neg.inl
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
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ (⟨a + 1, ⋯⟩.castLT ⋯) ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

Tactic:
· rw [Fin.le_iff_val_le_val]
      dsimp
      lia

Goal state after:
case neg.inl
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
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ (⟨a + 1, ⋯⟩.castLT ⋯) ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ f.f Δ.len = f.f Δ'.len ≫ 0

Tactic:
· rw [zero_comp, comp_zero]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
by_cases h₃ : Isδ₀ i

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : ¬Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0