mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    ((relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
        (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
          πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv) ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))

Tactic:
assoc,

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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      ((relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
          πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv) ≫
        (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))
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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      ((relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
          πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv) ≫
        (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))

Tactic:
assoc,

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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        (πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv) ≫
          (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))
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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        (πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv) ≫
          (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))

Tactic:
assoc,

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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫
          (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv ≫
            (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫
              Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f))
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).incl.app (Order.succ j) ≫ πObj I κ f) ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv =
    (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
        (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
          πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
assoc,

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).incl.app (Order.succ j) ≫
      πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv =
    (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
        (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
          πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv
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
l : (↑⟨Arrow.mk i, hi⟩).right ⟶ (relativeCellComplexιObj I κ f).F.obj (Order.succ j)
hl₁ : i ≫ l = t ≫ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯)
hl₂ : l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f = b
⊢ (l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j)) ≫ πObj I κ f = b

Tactic:
assoc,

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
l : (↑⟨Arrow.mk i, hi⟩).right ⟶ (relativeCellComplexιObj I κ f).F.obj (Order.succ j)
hl₁ : i ≫ l = t ≫ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯)
hl₂ : l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f = b
⊢ l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f = b
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 : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ ((transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
        (Subobject.underlyingIso f).hom) ≫
      f =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow

Tactic:
assoc,

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 : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
      (Subobject.underlyingIso f).hom ≫ f =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
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
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp

Tactic:
· exact antitone_rlp (generatingMonomorphisms_le_monomorphisms _)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Tactic:
conv =>

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case singleton
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
k : ℕ
hF : ∀ i ∈ {k}, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ {k}, F i)

Tactic:
rw [Finset.sum_singleton]

Goal state after:
case singleton
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
k : ℕ
hF : ∀ i ∈ {k}, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (F k)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
⊢ ⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1

Tactic:
have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ * if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1

Tactic:
rw [dif_pos h]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩ = 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * n)! = padicValNat p n ! + n

Tactic:
by
  apply Nat.cast_injective (R := ℕ∞)
  rw [padicValNat_eq_emultiplicity <| factorial_ne_zero (p * n), Nat.cast_add,
      padicValNat_eq_emultiplicity <| factorial_ne_zero n]
  exact Prime.emultiplicity_factorial_mul hp.out

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf✝ : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
h : IsLimit (Fork.ofι (F.map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
h' : IsLimit Types.equalizerLimit.cone := Types.equalizerLimit.isLimit
⊢ ⟨equalizer.ι f g, ⋯⟩ ≫ ⟨f, hf✝⟩ = ⟨equalizer.ι f g, ⋯⟩ ≫ ⟨g, hg⟩

Tactic:
by ext; exact equalizer.condition f g

Goal state after:
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
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ (c.fst ≫ φ) ≫ c.fst = 𝟙 c.pt ≫ c.fst

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ ≫ c.fst = 𝟙 c.pt ≫ c.fst
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
Z : C
p₁ : Z ⟶ Y₁
p₂ : Z ⟶ Y₂
z : Φ.fiber.obj Z
fac : p₁ ≫ f₁ = p₂ ≫ f₂
hz₁ : (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁
hz₂ : (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂
φ₁ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₁ hf₁ := ObjectProperty.homMk (Over.homMk p₁ ⋯)
φ₂ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₂ hf₂ := ObjectProperty.homMk (Over.homMk p₂ ⋯)
⊢ s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫ Pi.π (fun t ↦ M) y₂ =
    s.π.app (op (R.arrows.categoryMk f₁ hf₁)) ≫ Pi.π (fun t ↦ M) y₁

Tactic:
simpa [hz₁, hz₂, φ₁, φ₂] using!
    (Cone.w s φ₂.op =≫ Pi.π _ z).trans (Cone.w s φ₁.op =≫ Pi.π _ z).symm

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
⊢ (f + g).norm = max f.norm g.norm

Tactic:
classical
  have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne
  exact if hf : f ≈ 0 then by
    have : LimZero (f - 0) := hf
    have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
    have h1 : (f + g).norm = g.norm := norm_equiv this
    have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
    rw [h1, h2, max_eq_right (norm_nonneg _)]
  else
    if hg : g ≈ 0 then by
      have : LimZero (g - 0) := hg
      have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
      have h1 : (f + g).norm = f.norm := norm_equiv this
      have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
      rw [h1, h2, max_eq_left (norm_nonneg _)]
    else by
      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.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ ↑m = ↑n → m = n

Tactic:
by
    rw [← Rat.cast_natCast]
    norm_cast
    exact id

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

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op (X i)))) (toGlued hf i) = yonedaEquiv (f i)

Tactic:
rw [← yoneda_toGlued_yonedaGluedToSheaf hf i, yonedaEquiv_comp,
    yonedaEquiv_yoneda_map]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (lim f - ↑f i) < ε

Tactic:
← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (lim f - ↑(↑(lim' f) i) + (↑(↑(lim' f) i) - ↑f i)) < ε
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ (f ≫ φ) ≫ X.δ j.succ = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ f ≫ φ ≫ X.δ j.succ = 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
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

Tactic:
assoc,

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.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg
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⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ = (φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩) ≫ X.δ j.succ

Tactic:
assoc,

Goal state after:
case neg
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⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ = φ ≫ (X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩) ≫ X.δ j.succ