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 =
    ((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

Tactic:
← cancel_mono ((ιIteration I κ).app f).right,

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.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Small.{w, max u v} (Subobject G)
⊢ MorphismProperty.IsSmall.{w, v, u} (MorphismProperty.ofHoms fun X ↦ X.arrow)

Tactic:
infer_instance

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)

Tactic:
simp only [hc1, hc2]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) =
    ↑(multiplicity (↑p) (c * q.num)) - ↑(multiplicity (↑p) (c * ↑q.den))
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)
⊢ Mono (transfiniteIterate (largerSubobject hG) m A₀).arrow

Tactic:
infer_instance

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
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator (separator C)
⊢ (generatingMonomorphisms (separator C)).rlp.llp.HasFunctorialFactorization (generatingMonomorphisms (separator C)).rlp

Tactic:
infer_instance

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

Goal state before:
pp: case neg
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 (∑ x ∈ Finset.range d, F x + F d)

Tactic:
refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
      refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
      exact hF _ (lt_trans hi (lt_add_one _))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
| padicValNat p n !

Tactic:
rw [← one_mul (padicValNat p n !)]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
| 1 * padicValNat p n !
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) ≤ 1

Tactic:
· rw [← le_log_iff_exp_le] <;>
    simp_all

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
have h : k ≤ n + k := by exact Nat.le_add_left k n
  simp only [Nat.choose_eq_factorial_div_factorial h]
  rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
      padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]
  simp only [sub_one_mul_padicValNat_factorial]
  rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]

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

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

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g : Z ⟶ X
⊢ ∀ (h : Z ⟶ X), g ≫ f = h ≫ f → g = h

Tactic:
g'

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
⊢ g ≫ f = g' ≫ f → g = g'
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ IsIso c.fst → c.fst = c.snd

Tactic:
intro

Goal state after:
case mpr
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
⊢ c.fst = c.snd
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
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:
intro

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
a✝ : Mono f
⊢ IsPullback (𝟙 X) (𝟙 X) f f
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g : Y ⟶ Z
⊢ ∀ (h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

Tactic:
g'

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
⊢ f ≫ g = f ≫ g' → g = g'
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ IsIso c.inl → c.inl = c.inr

Tactic:
intro

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
⊢ c.inl = c.inr
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
intro

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
a✝ : Epi f
⊢ IsPushout f f (𝟙 Y) (𝟙 Y)
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : S.Etale
R : Sieve X
hR : R ∈ S.smallEtaleTopology X
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj X
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f)) y = φ

Tactic:
by
    cases X with | _ X f
    obtain ⟨φ : Spec (.of Ω) ⟶ X, rfl : φ ≫ f = s, rfl⟩ := Over.homMk_surjective φ
    obtain ⟨𝒰, h, _, le⟩ := (mem_smallGrothendieckTopology _ _).1 hR
    obtain ⟨i, y, hy⟩ := 𝒰.exists_eq (φ default)
    obtain ⟨l, hl₁, hl₂⟩ := exists_fac_of_etale_of_isSepClosed (𝒰.f i) φ _ hy
    have : 𝒰.f i ≫ f = 𝒰.X i ↘ S := HomIsOver.comp_over (f := 𝒰.f i) (S := S)
    exact ⟨(𝒰.X i).asOverProp S inferInstance,
      MorphismProperty.Over.homMk (𝒰.f i), le _ _ ⟨i⟩, Over.homMk l, by cat_disch⟩

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

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝² : Field Ω
inst✝¹ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
s₀ : ↥S
hs₀ : s default = s₀
Y X : Scheme
f : Y ⟶ X
inst✝ : Etale f
x : ↥X
⊢ Etale (Limits.pullback.snd f (X.fromSpecResidueField x))

Tactic:
infer_instance

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

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

Tactic:
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.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y' : B
⊢ (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'

Tactic:
simp [equivalence₂, equivalence₁CounitIso_eq]

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

Goal state before:
pp: case left
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ Sheaf.IsLocallyInjective (yonedaGluedToSheaf hf)

Tactic:
infer_instance

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

Goal state before:
pp: case right
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ Sheaf.IsLocallySurjective (yonedaGluedToSheaf hf)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
⊢ ∀ (g_1 : F.obj a' ⟶ X), ∃ b snd fst, IsPullback fst (F.map snd) g g_1

Tactic:
g'

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
⊢ ∃ b snd fst, IsPullback fst (F.map snd) g g'
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
w✝² : C
w✝¹ : w✝² ⟶ a
w✝ : F.obj w✝² ⟶ F.obj a
pbRepr :
  IsPullback w✝ (F.map w✝¹) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
    (g ≫ pullback.snd (terminal.from X) (terminal.from X))
⊢ ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        pullback.fst (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (⊤_ D)) ⋯ ⋯)) ≫
      pullback.diagonal (terminal.from X) =
    ((pbRepr.isoPullback ≪≫
            (pullbackDiagonalMapIdIso (g ≫ pullback.fst (terminal.from X) (terminal.from X))
                (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (terminal.from X)).symm).hom ≫
        pullback.snd (pullback.diagonal (terminal.from X))
          (pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
            ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X)
            (terminal.from X) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
            (g ≫ pullback.snd (terminal.from X) (terminal.from X)) (𝟙 (⊤_ D)) ⋯ ⋯)) ≫
      pullback.map ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
        ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) (terminal.from X) (terminal.from X)
        (g ≫ pullback.fst (terminal.from X) (terminal.from X)) (g ≫ pullback.snd (terminal.from X) (terminal.from X))
        (𝟙 (⊤_ D)) ⋯ ⋯

Tactic:
by rw [assoc]; simp [pullback.condition]

Goal state after:
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 : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ a + b + (c + d + e) = f

Tactic:
rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)

Tactic:
change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _)

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ↑(PadicSeq.norm f) = ↑p ^ (-PadicSeq.valuation f)
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.h
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 φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫ X.σ 0 ≫ ((-1) ^ ↑j.succ.succ • X.δ j.succ.succ) = 0

Tactic:
comp_zsmul,

Goal state after:
case neg.h
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 φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫ ((-1) ^ ↑j.succ.succ • X.σ 0 ≫ X.δ j.succ.succ) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.h
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 φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫ ((-1) ^ ↑j.succ.succ • X.σ 0 ≫ X.δ j.succ.succ) = 0

Tactic:
comp_zsmul,

Goal state after:
case neg.h
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 φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ (-1) ^ ↑j.succ.succ • φ ≫ X.σ 0 ≫ X.δ j.succ.succ = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
by_cases hx : x = 0
  · simpa only [hx, zero_add] using min_le_right _ _
  by_cases hy : y = 0
  · simpa only [hy, add_zero] using min_le_left _ _
  have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := nonarchimedean x y
  simpa only [norm_eq_zpow_neg_valuation hxy, norm_eq_zpow_neg_valuation hx,
    norm_eq_zpow_neg_valuation hy, le_max_iff,
    zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt : 1 < (p : ℝ)), neg_le_neg_iff, ← min_le_iff]

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

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ X.σ i ≫ (P (q + 1)).f (n + 1 + 1) = 0

Tactic:
← id_comp (X.σ i),

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
⊢ (𝟙 (X _⦋n + 1⦌) ≫ X.σ i) ≫ (P (q + 1)).f (n + 1 + 1) = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Epi (𝟙 (unop Δ))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 (unop Δ))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono A.e → A.EqId

Tactic:
intro

Goal state after:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
a✝ : Mono A.e
⊢ A.EqId
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
⊢ x✝¹ = x✝

Tactic:
by
    ext n
    dsimp
    ext
    exact HomologicalComplex.congr_hom hf n

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (Karoubi (HomologicalComplex C c))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ∀ [IsIso (N₁.map f)], IsIso f

Tactic:
intro

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
⊢ ∀ [IsIso (N₂.map f)], IsIso f

Tactic:
intro

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (Γ₂N₂.natTrans.app P) = inv (N₂Γ₂.inv.app (N₂.obj P))
⊢ IsIso (inv (N₂Γ₂.inv.app (N₂.obj P)))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Path.cast ⋯ ⋯ p = p'

Tactic:
Path.cast_eq_iff_heq

Goal state after:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ p ≍ p'
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Path.cast ⋯ ⋯ p = p'

Tactic:
rw [Path.cast_eq_iff_heq]
  exact heq_of_cons_eq_cons h

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
⊢ ∀ (X : C), f X * (f X)⁻¹ = 𝟙 ()

Tactic:
intro

Goal state after:
M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ : C
⊢ f X✝ * (f X✝)⁻¹ = 𝟙 ()