mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i j : V.affineOneHypercover.I₀
k : V.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.pullback (V.affineOneHypercover.p₁ k ≫ V.affineOneHypercover.f i)
        (Sieve.generate
          (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).X
            (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f))).arrows

Tactic:
← Sieve.pullbackArrows_comm,

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i j : V.affineOneHypercover.I₀
k : V.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.generate
        (Presieve.pullbackArrows (V.affineOneHypercover.p₁ k ≫ V.affineOneHypercover.f i)
          (Presieve.ofArrows (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).X
            (Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f))).arrows
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
this :
  ∀ (R : CommRingCat) (𝒰 : Cover (propQCPrecoverage P) (Spec R)),
    (∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ → Presieve.IsSheafFor F 𝒰.presieve₀
h𝒰 : ¬((∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀)
𝒱 : AffineCover P (Spec R)
f✝ : 𝒱.cover ⟶ 𝒰.forgetQc
hfin : Finite 𝒱.I₀
ho : ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f✝.h₀ j)
V : Scheme
f : V ⟶ Spec R
i j : V.affineOneHypercover.I₀
k : V.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Presieve.ofArrows
      (fun i_1 ↦
        pullback ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f i_1)
          (V.affineOneHypercover.p₁ k ≫ V.affineOneHypercover.f i))
      fun x ↦
      pullback.snd ((Precoverage.ZeroHypercover.pullback₂ f 𝒱.cover).f x)
        (V.affineOneHypercover.p₁ k ≫ V.affineOneHypercover.f i))

Tactic:
exact (this _ (.ofQuasiCompactCover ((𝒱.cover.pullback₂ f).pullback₂ _)
              (qc := by dsimp; infer_instance))
            ⟨fun l ↦ .of_isIso (pullbackLeftPullbackSndIso (𝒱.f l) f _).hom, hfin⟩).isSeparatedFor

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
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) = J.yonedaEquiv (J.yoneda.map g ≫ f)

Tactic:
by
  simp [yonedaEquiv, CategoryTheory.yonedaEquiv_naturality]
  rfl

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
I : Type u_2
x✝ : Category.{u_1, u_2} I
⊢ PreservesLimitsOfShape I J.yoneda

Tactic:
have : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J _) :=
    inferInstanceAs <| PreservesLimitsOfShape I CategoryTheory.yoneda

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
I : Type u_2
x✝ : Category.{u_1, u_2} I
this : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J (Type v))
⊢ PreservesLimitsOfShape I J.yoneda
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj ⟨k₂, h₂⟩ = F.obj ⟨k₂, h₂⟩

Tactic:
by rw [h.tgt]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ (objIso F X ⟨i, ⋯⟩).hom ≫ (objIso F X ⟨i, h₁⟩).inv = 𝟙 (obj F X ⟨i, ⋯⟩)

Tactic:
Iso.hom_inv_id

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ 𝟙 (obj F X ⟨i, ⋯⟩) = 𝟙 (obj F X ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (∃ ι A B f, W = ofHoms f) → IsSmall.{w, v, u} W

Tactic:
rintro ⟨_, _, _, _, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
w✝³ : Type w
w✝² w✝¹ : w✝³ → C
w✝ : (i : w✝³) → w✝² i ⟶ w✝¹ i
⊢ IsSmall.{w, v, u} (ofHoms w✝)
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

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

Tactic:
exact coproducts_of_small _ _ (colimitsOfShape_colimMap _ (by rintro ⟨j⟩; constructor))

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
⊢ Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
      Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right

Tactic:
have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)
  dsimp at this ⊢
  rw [← cancel_epi (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right,
    ← reassoc_of% this, comp_id]

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

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

Tactic:
unfold padicNorm at h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖0‖ ≤ ↑p ^ (-↑n) ↔ 0 ∈ Ideal.span {↑p ^ n}

Tactic:
simp only [norm_zero, zpow_neg, zpow_natCast, inv_nonneg, iff_true, Submodule.zero_mem]

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case coe
p : ℕ
hp : Fact (Nat.Prime p)
x : Multiplicative ℤ
⊢ ∃ a, (padicValuation p) a = ↑x

Tactic:
| coe x =>

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
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : F✝.relativelyRepresentable f
hg : F✝.relativelyRepresentable g
X : C
h : F✝.obj X ⟶ H
⊢ IsPullback (hf.fst (hg.fst h)) (F✝.map (hf.snd (hg.fst h) ≫ hg.snd h)) (f ≫ g) h

Tactic:
simpa using IsPullback.paste_vert (hf.isPullback (hg.fst h)) (hg.isPullback h)

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✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ = φ'

Tactic:
apply pullback.hom_ext <;> ext <;> simpa

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 = 𝟙 (K[X].X 0)

Tactic:
by
  induction q with
  | zero => rfl
  | succ q hq =>
    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p

Tactic:
exact mod_cast hp.1.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
this : { num := n, den := d, den_nz := hn, reduced := hd } = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
norm_num [this]

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

Goal state before:
pp: case zero
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
n : ℕ
⊢ G.map ((𝟙 K[X]).f n) = (𝟙 K[((whiskering C D).obj G).obj X]).f n

Tactic:
apply G.map_id

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
⊢ ∃ b, f ≈ const norm b

Tactic:
exists q

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
⊢ f ≈ const norm q
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = 𝟙 (((whiskering C D).obj G).obj X _⦋n⦌)

Tactic:
apply G.map_id

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

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

Tactic:
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.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  (𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) ≫ PInfty.f n) ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌) ≫ PInfty.f n) ≫
          𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
rw [id_comp, id_comp, comp_id, comp_id] at h₁₄

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef 1 = 0

Tactic:
rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]

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

Goal state before:
pp: case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ⟨b + 1, ⋯⟩ < j.succ

Tactic:
rw [Fin.lt_def, Fin.val_succ]

Goal state after:
case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ↑⟨b + 1, ⋯⟩ < ↑j + 1
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✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq : K[X].d i j ≫ (∑ A, s.πSummand A ≫ (s.cofan (op ⦋j⦌)).inj A) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

Tactic:
rw [Fintype.sum_eq_add_sum_compl (IndexSet.id (op ⦋j⦌)), add_comp, comp_add, assoc,
      Preadditive.sum_comp, Preadditive.comp_sum, Finset.sum_eq_zero, add_zero] at eq

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
      s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
        (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ ∀ x ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
    K[X].d i j ≫ (s.πSummand x ≫ (s.cofan (op ⦋j⦌)).inj x) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 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✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq : K[X].d i j ≫ (∑ A, s.πSummand A ≫ (s.cofan (op ⦋j⦌)).inj A) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

Tactic:
rw [Fintype.sum_eq_add_sum_compl (IndexSet.id (op ⦋j⦌)), add_comp, comp_add, assoc,
      Preadditive.sum_comp, Preadditive.comp_sum, Finset.sum_eq_zero, add_zero] at eq
    swap
    · intro A hA
      simp only [Finset.mem_compl, Finset.mem_singleton] at hA
      simp only [assoc, ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ _ hA, comp_zero]
    rw [eq, comp_zero]

Goal state after:
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✝ : Preadditive C
⊢ (s.toKaroubiNondegComplexIsoN₁.hom ≫ s.toKaroubiNondegComplexIsoN₁.inv).f = 𝟙 s.nondegComplex

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f = 𝟙 s.nondegComplex
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_map
I : Type u
X : I → TopCat
⊢ autoParam
    (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯)
    CategoryTheory.Functor.ext._auto_1

Tactic:
intro _ _ f

Goal state after:
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ Limits.PreservesLimit (Discrete.functor X) π

Tactic:
by
  apply Limits.preservesLimit_of_preserves_limit_cone (TopCat.piFanIsLimit X)
  apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun
  simp only [coneDiscreteComp_obj_mapCone]
  apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm
  exact Grpd.piLimitFanIsLimit _

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I
⊢ (if ↑(0, x).2 ≤ 1 / 2 then (F.eval (0, x).1).extend (2 * ↑(0, x).2)
    else (G.eval (0, x).1).extend (2 * ↑(0, x).2 - 1)) =
    (p₀.trans p₁).toContinuousMap x

Tactic:
simp [Path.trans]

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I
⊢ (if ↑(1, x).2 ≤ 1 / 2 then (F.eval (1, x).1).extend (2 * ↑(1, x).2)
    else (G.eval (1, x).1).extend (2 * ↑(1, x).2 - 1)) =
    (q₀.trans q₁).toContinuousMap x

Tactic:
simp [Path.trans]

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → (ContinuousMap.id Y).Nullhomotopic

pp: case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic → ContractibleSpace Y

Tactic:
· intro
    apply id_nullhomotopic

Goal state after:
case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic → ContractibleSpace Y
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
⊢ Nonempty (X ≃ₕ Y)

Tactic:
rcases ContractibleSpace.hequiv_unit' (X := X) with ⟨h⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
h : X ≃ₕ Unit
⊢ Nonempty (X ≃ₕ Y)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ weakEquivalences (CofibrantObject C) f ↔ weakEquivalences (CofibrantObject C) g

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (cofibrations Cᵒᵖ).HasFactorization (trivialFibrations Cᵒᵖ)

Tactic:
by
  rw [cofibrations_op, trivialFibrations_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✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations (Over S)).IsStableUnderRetracts

Tactic:
cofibrations_over_def,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations C).over.IsStableUnderRetracts