mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)), this⟩),
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
          IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
        G₀.obj.map I.f.op =
      (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
        G₀.obj.map I.f.op

Tactic:
rintro ⟨V₀, a, ⟨x₁, fac₁⟩, ⟨x₂, fac₂⟩⟩

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
        IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
      G₀.obj.map { Y := V₀, f := a, hf := ⋯ }.f.op =
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj.map { Y := V₀, f := a, hf := ⋯ }.f.op
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁸ : P.IsStableUnderComposition
K : Precoverage C
inst✝⁷ : K.HasIsos
inst✝⁶ : K.IsStableUnderBaseChange
inst✝⁵ : K.IsStableUnderComposition
inst✝⁴ : K.HasPullbacks
inst✝³ : HasFiniteWidePullbacks C
inst✝² : P.HasOfPostcompProperty P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.ContainsIdentities
H : K ≤ P.precoverage
⊢ (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck =
    (Over.forget P ⊤ S).inducedTopology (K.toGrothendieck.over S)

Tactic:
have := isContinuous_comap_forget (S := S) _ H

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁸ : P.IsStableUnderComposition
K : Precoverage C
inst✝⁷ : K.HasIsos
inst✝⁶ : K.IsStableUnderBaseChange
inst✝⁵ : K.IsStableUnderComposition
inst✝⁴ : K.HasPullbacks
inst✝³ : HasFiniteWidePullbacks C
inst✝² : P.HasOfPostcompProperty P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.ContainsIdentities
H : K ≤ P.precoverage
this :
  (Over.forget P ⊤ S).IsContinuous
    (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck (K.toGrothendieck.over S)
⊢ (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck =
    (Over.forget P ⊤ S).inducedTopology (K.toGrothendieck.over S)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ presheafObjObjIso.hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i) =
    presheafObjπ data G₀ (unop (op (F.obj X₀))) i

Tactic:
presheafObjObjIso.hom_mapPreimage data G₀ _ (𝟙 _) (fac := by simp),

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ (𝟙 (F.obj ((data (F.obj X₀)).X i))) =
    presheafObjπ data G₀ (unop (op (F.obj X₀))) i
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ Y₀ : C₀
a : Y₀ ⟶ X₀
Y : C
i : (data (F.obj X₀)).I₀
b : F.obj Y₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : b ≫ (data (F.obj X₀)).f i = F.map a
⊢ (presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀) ≫ G₀.obj.map a.op =
    𝟙 (G₀.obj.obj (op X₀)) ≫ G₀.obj.map a.op

Tactic:
simp [presheafObjObjIso.hom_map data G₀ _ b fac, ← IsDenseSubsite.mapPreimage_comp, fac]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : J.Subcanonical
ι : Type u_1
inst✝² : CoproductsOfShapeDisjoint C ι
inst✝¹ : HasPullbacks C
inst✝ : HasStrictInitialObjects C
hcov : ∀ {X : ι → C} {c : Cofan X} (x : IsColimit c), Sieve.ofArrows X c.inj ∈ J c.pt
htriv : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
⊢ PreservesColimitsOfShape (Discrete ι) J.yoneda

Tactic:
by
  apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_of_discrete
  refine fun X ↦ ⟨fun {c : Cofan X} hc ↦ ⟨(Limits.Cofan.isColimitMapCoconeEquiv _ _ _).symm ?_⟩⟩
  have (i : ι) : Mono (c.inj i) := .of_coproductDisjoint hc _
  refine isColimitCofanMkYoneda _ _ (hcov hc) htriv fun hij Y a b hab ↦ ⟨?_⟩
  exact .ofCoproductDisjointOfCommSq hij hc _ _ hab

Goal state after:
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✝¹ : LinearOrder α
h : α ≤i J
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Tactic:
have := hj.nonempty_Iio.to_subtype
    exact hasColimitsOfShape_of_initialSeg _
      (InitialSeg.trans (Set.principalSegIio j) h)

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

Goal state before:
pp: 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₁ ≤ i₂
hi₂ : i₂ < j
⊢ (ofCocone c).map (homOfLE hi) = (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv

Tactic:
dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]

Goal state after:
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₁ ≤ i₂
hi₂ : i₂ < j
⊢ (if h₂ : i₂ < j then (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then (ofCocone.objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (ofCocone.objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯) =
    (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
simp [hp.1.ne_zero]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ padicValNat 2 (n + 1) ≠ 0 ∨ 1 < 2 ∧ n ≠ 0

Tactic:
simp [hn]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
⊢ (if x✝ * y✝ = 0 then 0 else exp (-padicValRat p (x✝ * y✝))) =
    (if x✝ = 0 then 0 else exp (-padicValRat p x✝)) * if y✝ = 0 then 0 else exp (-padicValRat p y✝)

Tactic:
split_ifs <;>
    simp_all [padicValRat.mul, exp_add, mul_comm]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n = 0
⊢ padicValNat p n ! ≤ n

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ : J.Point
⊢ presheafFiber (𝟙 Φ) = 𝟙 Φ.presheafFiber

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ₁ Φ₂ Φ₃ : J.Point
f : Φ₁ ⟶ Φ₂
g : Φ₂ ⟶ Φ₃
⊢ presheafFiber (f ≫ g) = presheafFiber g ≫ presheafFiber f

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ : J.Point
⊢ sheafFiber (𝟙 Φ) = 𝟙 Φ.sheafFiber

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ₁ Φ₂ Φ₃ : J.Point
f : Φ₁ ⟶ Φ₂
g : Φ₂ ⟶ Φ₃
⊢ sheafFiber (f ≫ g) = sheafFiber g ≫ sheafFiber f

Tactic:
by
  cat_disch

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

Goal state before:
pp: case neg
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_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
have ha_norm : ‖a‖ = 1 := by
        have hx : x ≠ 0 := by
          intro h0
          rw [h0, norm_zero] at hx
          exact hx zero_le_one
        rw [ha, padicNormE.mul, Padic.norm_p_pow, Padic.norm_eq_zpow_neg_valuation hx,
          ← zpow_add', hn_coe, neg_neg, neg_add_cancel, zpow_zero]
        exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))

Goal state after:
case neg
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
ha_norm : ‖a‖ = 1
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1
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
P Q : Cᵒᵖ ⥤ A
M : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : P ⟶ Q
g : Q ⟶ Φ.skyscraperPresheaf M
⊢ Φ.skyscraperPresheafHomEquiv.symm (f ≫ g) = Φ.presheafFiber.map f ≫ Φ.skyscraperPresheafHomEquiv.symm g

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y)

Tactic:
refine Eq.trans (congr_arg _ ht)
        (Φ.obj.toPresheafFiber_naturality_apply f _ v y).symm

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
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ P snd

Tactic:
rw [← hg.1.lift_snd (fst ≫ f) snd (by simpa using h.w)]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) ≤ ?b

Tactic:
apply padicNormE.add_le

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

Goal state before:
pp: case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) ≤ ?hbc.h₁.b

Tactic:
apply padicNormE.add_le

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
⊢ (if x✝¹ * x✝ = 0 then 0 else exp (-(x✝¹ * x✝).valuation)) =
    (if x✝¹ = 0 then 0 else exp (-x✝¹.valuation)) * if x✝ = 0 then 0 else exp (-x✝.valuation)

Tactic:
by split_ifs <;> simp_all [add_comm]

Goal state after:
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
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝.Hom Y✝
Φ₂₃ : Y✝.Hom Z✝
n : ℕ
⊢ X✝.s.ι n ≫ Φ₁₂.F.app (op ⦋n⦌) ≫ Φ₂₃.F.app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z✝.s.ι n

Tactic:
simp only [assoc, Split.Hom.comm_assoc, Split.Hom.comm]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X Y : SimplicialObject A
f : X ⟶ Y
⊢ AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
    PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ K.d (n + 1) n =
    ∑ j,
      ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        ((-1) ^ ↑j • (Γ₀.obj K).δ j) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
Fintype.sum_eq_single (0 : Fin (n + 2))

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ K.d (n + 1) n =
    ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      ((-1) ^ ↑0 • (Γ₀.obj K).δ 0) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌))

C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ∀ (x : Fin (n + 2)),
    x ≠ 0 →
      ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
          ((-1) ^ ↑x • (Γ₀.obj K).δ x) ≫ (Γ₀.splitting K).πSummand (Splitting.IndexSet.id (op ⦋n⦌)) =
        0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 (summand s.N Δ A)

Tactic:
simp [πSummand]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = Γ₂N₁.hom

Tactic:
← cancel_epi Γ₂N₁.inv,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = Γ₂N₁.inv ≫ Γ₂N₁.hom
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ (P (m + k + 1 + 1)).f (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₂.succ).op ≫ X.map (SimplexCategory.δ (Fin.castLT 0 ⋯)).op ≫ X.map i.op =
    0

Tactic:
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ j₂.succ_ne_zero, zero_comp]

Goal state after:
case pos.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ m + k + 1 + 2 ≤ ↑j₂.succ + (m + k + 1 + 1)
Module: Mathlib.Topology.Homotopy.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : ↑X
⊢ (ConcreteCategory.hom (ι₀ ≫ F.h)) x = (ConcreteCategory.hom f₀) x

Tactic:
exact F.map_zero_left x

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x

Tactic:
rw [comp_as_mul, inv_mul_cancel, id_as_one]

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ F.symm.symm = F

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝² x✝¹ : CofibrantObject C
x✝ : x✝² ⟶ x✝¹
h : WeakEquivalence x✝
⊢ (weakEquivalences (HoCat C)).inverseImage toHoCat x✝

Tactic:
simpa only [MorphismProperty.inverseImage_iff, ← weakEquivalence_iff,
      weakEquivalence_toHoCat_map_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences Cᵒᵖ).HasTwoOutOfThreeProperty

Tactic:
by
  rw [weakEquivalences_op]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences Cᵒᵖ).IsStableUnderRetracts

Tactic:
by
  rw [weakEquivalences_op]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
inst✝ : CategoryWithWeakEquivalences C
X Y : Over S
f : X ⟶ Y
⊢ WeakEquivalence f ↔ WeakEquivalence (Over.Hom.left f)

Tactic:
simp only [weakEquivalence_iff, weakEquivalences_over_def, MorphismProperty.over_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
h₁ : (hom (Sigma.ι X₁ i₁ ≫ Limits.Sigma.map f)) x₁ = (hom (f i₁ ≫ Sigma.ι X₂ i₁)) x₁
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)

Tactic:
have h₂ := congr_hom (Sigma.ι_map f i₂) x₂

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
h₁ : (hom (Sigma.ι X₁ i₁ ≫ Limits.Sigma.map f)) x₁ = (hom (f i₁ ≫ Sigma.ι X₂ i₁)) x₁
h₂ : (hom (Sigma.ι X₁ i₂ ≫ Limits.Sigma.map f)) x₂ = (hom (f i₂ ≫ Sigma.ι X₂ i₂)) x₂
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hs : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr ((ConcreteCategory.hom g) y₀✝))

Tactic:
rw [← h]

Goal state after:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hs : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr ((ConcreteCategory.hom g) x₀✝))