mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ?refine_1⟩
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)

pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ IsCauSeq norm x

Tactic:
swap

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ IsCauSeq norm x

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ?refine_1⟩
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)
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 : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
g : M ⟶ N
⊢ Φ.skyscraperPresheafHomEquiv (f ≫ g) = Φ.skyscraperPresheafHomEquiv f ≫ Φ.skyscraperPresheafFunctor.map g

Tactic:
ext
  dsimp
  ext
  dsimp
  rw [skyscraperPresheafHomEquiv_app_π]
  dsimp
  rw [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]

Goal state after:
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 : Φ.presheafFiber.obj Q ⟶ M
⊢ Φ.skyscraperPresheafHomEquiv.symm (Φ.skyscraperPresheafHomEquiv (Φ.presheafFiber.map f ≫ g)) =
    Φ.skyscraperPresheafHomEquiv.symm (f ≫ Φ.skyscraperPresheafHomEquiv g)

Tactic:
by simp [Φ.skyscraperPresheafHomEquiv_naturality_left_symm]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
⊢ Sieve.ofArrows U f ∈ J X

Tactic:
rw [J.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map]
    refine hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)
    obtain ⟨x, rfl⟩ := (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm.surjective x
    obtain ⟨i, y, rfl⟩ := hf Φ x
    refine ⟨Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w}.obj (U i)) i)
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app _ y), ?_⟩
    have := ConcreteCategory.congr_hom
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality (f i)) y
    dsimp at this ⊢
    rw [this, ← Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i, Functor.map_comp]
    rfl

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
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
⊢ Sieve.ofArrows U f ∈ J X ↔
    ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x

Tactic:
by
  refine ⟨fun hf Φ x ↦ ?_, fun hf ↦ ?_⟩
  · obtain ⟨Z, _, ⟨_, p, _, ⟨i⟩, rfl⟩, z, rfl⟩ := Φ.obj.jointly_surjective _ hf x
    exact ⟨i, Φ.obj.fiber.map p z, by simp⟩
  · rw [J.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map]
    refine hP.jointly_reflect_isLocallySurjective _ (fun Φ x ↦ ?_)
    obtain ⟨x, rfl⟩ := (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm.surjective x
    obtain ⟨i, y, rfl⟩ := hf Φ x
    refine ⟨Φ.obj.presheafFiber.map (Sigma.ι (fun i ↦ shrinkYoneda.{w}.obj (U i)) i)
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app _ y), ?_⟩
    have := ConcreteCategory.congr_hom
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality (f i)) y
    dsimp at this ⊢
    rw [this, ← Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i, Functor.map_comp]
    rfl

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

Goal state before:
pp: case inr
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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this✝ :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
hf' : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
this : Presheaf.IsLocallySurjective J f'
V : C
g : V ⟶ U
v : ToType ((pullback f (shrinkYonedaEquiv.symm s)).obj (op V))
hv :
  (ConcreteCategory.hom (f'.app (op V))) v =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))
⊢ (ConcreteCategory.hom (f.app (op V)))
      ((ConcreteCategory.hom ((pullback.fst f (shrinkYonedaEquiv.symm s)).app (op V))) v) =
    (ConcreteCategory.hom (F₂.map g.op)) s

Tactic:
refine (ConcreteCategory.congr_hom (NatTrans.congr_app
      (pullback.condition (f := f)) (op V)) _).trans ?_

Goal state after:
case inr
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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this✝ :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
hf' : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
this : Presheaf.IsLocallySurjective J f'
V : C
g : V ⟶ U
v : ToType ((pullback f (shrinkYonedaEquiv.symm s)).obj (op V))
hv :
  (ConcreteCategory.hom (f'.app (op V))) v =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))
⊢ (ConcreteCategory.hom ((pullback.snd f (shrinkYonedaEquiv.symm s) ≫ shrinkYonedaEquiv.symm s).app (op V))) v =
    (ConcreteCategory.hom (F₂.map g.op)) s
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✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) α =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) β
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)

Tactic:
simp [h]

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
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x, ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

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

Tactic:
swap

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
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) j))) •
        (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) j))) ≫ X.σ ⟨a, ⋯⟩ =
      0

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
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x, ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
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
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ i,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i)) * (-1) ^ (a + 1)) •
          (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i)) =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

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

Tactic:
swap

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
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 3) j)) * (-1) ^ (a + 1)) •
        (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) j)) =
      0

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
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ i,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i)) * (-1) ^ (a + 1)) •
          (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i)) =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
h : q = 0
⊢ ‖q‖ = ↑0

Tactic:
simp [h]

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

Tactic:
add_comm a,

Goal state after:
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
⊢ b + a + c = f
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
⊢ b + (a + c) = f

Tactic:
add_comm a,

Goal state after:
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
⊢ b + (c + a) = f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
⊢ ‖z1‖ = ‖z2‖

Tactic:
← norm_neg z2

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
⊢ ‖z1‖ = ‖-z2‖
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ CompleteSpace ℚ_[p]

Tactic:
by
  apply complete_of_cauchySeq_tendsto
  intro u hu
  let c : CauSeq ℚ_[p] norm := ⟨u, Metric.cauchySeq_iff'.mp hu⟩
  refine ⟨c.lim, fun s h ↦ ?_⟩
  rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
  have := c.equiv_lim ε ε0
  simp only [mem_map, mem_atTop_sets]
  exact this.imp fun N hN n hn ↦ hε (hN n hn)

Goal state after:
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
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
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

pp: case neg
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
⊢ ⟨a, ⋯⟩.succ < j.succ

Tactic:
swap

Goal state after:
case neg
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
⊢ ⟨a, ⋯⟩.succ < j.succ

case neg
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
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
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 ⋯)

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

Tactic:
swap

Goal state after:
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

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

Goal state before:
pp: case neg.inr
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
ham'' : a = m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

pp: case neg.inr.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
ham'' : a = m
⊢ ⟨a + 1, ⋯⟩ = j.castSucc

Tactic:
swap

Goal state after:
case neg.inr.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
ham'' : a = m
⊢ ⟨a + 1, ⋯⟩ = j.castSucc

case neg.inr
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
ham'' : a = m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
A : IndexSet (op Δ)
⊢ (s.cofan (op Δ)).inj A ≫ f.app (op Δ) = (s.cofan (op Δ)).inj A ≫ g.app (op Δ)

Tactic:
induction Δ using SimplexCategory.rec with | _ n
   =>  _ 

Goal state after:
case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ f.app (op ⦋n⦌) = (s.cofan (op ⦋n⦌)).inj A ≫ g.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (NormalizedMooreComplex.objX X 0).Factors (PInfty.f 0)

pp: case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).Factors (PInfty.f (n + 1))

Tactic:
· apply top_factors

Goal state after:
case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).Factors (PInfty.f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ b ∈ Finset.univ, b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0

Tactic:
intro B

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
⊢ B ∈ Finset.univ → B ≠ A → (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mp.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
f : Z ⟶ X _⦋0⦌
h : f ≫ PInfty.f 0 = 0
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋0⦌)) = 0

Tactic:
dsimp at h
      rw [comp_id] at h
      rw [h, zero_comp]

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

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ (PInfty.f (n + 1) + QInfty.f (n + 1)) = f ≫ 𝟙 (K[X].X (n + 1))
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
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✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso (F.map f)

Tactic:
simp only [F, F₁]

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)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ F₂ ⋙ F₃ ⋙ F₄).map f)