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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }

Tactic:
by
      intro Z a₁ a₂ g₁ g₂ h
      let A₁ : D := ⟨Over.mk (π a₁), a₁, 𝟙 _, by simp⟩
      let A₂ : D := ⟨Over.mk (π a₂), a₂, 𝟙 _, by simp⟩
      let Z' : D := ⟨Over.mk (g₁ ≫ π a₁), a₁, g₁, rfl⟩
      let i₁ : Z' ⟶ A₁ := ObjectProperty.homMk (Over.homMk g₁)
      let i₂ : Z' ⟶ A₂ := ObjectProperty.homMk (Over.homMk g₂)
      change F.map i₁ ≫ _ = F.map i₂ ≫ _
      simp only [F, A₁, A₂, S.w]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π → (Presieve.ofArrows X π).EffectiveEpimorphic

Tactic:
rintro ⟨h⟩
    change Nonempty _
    rw [Sieve.generateFamily_eq]
    apply Nonempty.map (isColimitOfEffectiveEpiFamilyStruct _ _) h

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
i : 𝒰.I₀
⊢ P (𝒰.X i).hom

Tactic:
← CategoryTheory.Over.w (𝒰.f i)

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
i : 𝒰.I₀
⊢ P (Over.Hom.left (𝒰.f i) ≫ ((Over.forget P ⊤ S).obj X).hom)
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝¹ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.Exact
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
x₃ : A₂ ⟶ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.X₁
hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.f
⊢ (π₂ ≫ x₂) ≫ r = x₃ ≫ b

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
  have := hc.mono_ι_app_of_isFiltered
  have := NatTrans.mono_of_mono_app c.ι
  obtain ⟨j, _⟩ := exists_isIso_of_functor_from_monoOver (F z) hXκ _
    (colimit.isColimit _) (f z) (hf z) (epi_f hc z)
  refine ⟨j, inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι _).app j, ?_⟩
  dsimp
  rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : PartialOrder J
F : J ⥤ C
J' : Type w'
inst✝¹ : PartialOrder J'
f : J' ≤i J
inst✝ : F.IsWellOrderContinuous
m' : J'
hm' : Order.IsSuccLimit m'
⊢ Order.IsSuccLimit ((Set.principalSegIio m').transInitial f).top

Tactic:
by simpa

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

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ∃ b, i < b
⊢ ∃ b, ↑i < b

Tactic:
obtain ⟨i', hi'⟩ := hi

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i i' : ↑(Set.Iic j)
hi' : i < i'
⊢ ∃ b, ↑i < b
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
e : J ≃o J'
⊢ W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'

Tactic:
by
  ext _ _ f
  exact ⟨fun ⟨h⟩ ↦ ⟨h.ofOrderIso e.symm⟩, fun ⟨h⟩ ↦ ⟨h.ofOrderIso e⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ Arrow.mk ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) = Φ.toSuccArrow ((functor hj iter).obj ⟨i, ⋯⟩)

Tactic:
arrow_mk_mapObj,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ arrowMap (iter (Order.succ i) ⋯).F i (Order.succ i) ⋯ ⋯ = Φ.toSuccArrow ((functor hj iter).obj ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ Arrow.mk ((iter k ⋯).mapObj (iter i hij) ⋯ ⋯ ⋯ ⋯) = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk

Tactic:
arrow_mk_mapObj,

Goal state after:
case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ arrowMap (iter i hij).F k i ⋯ ⋯ = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ Arrow.mk ((iter l₁ pf✝⁹).mapObj (iter l₂ pf✝⁷) pf✝⁵ pf✝⁴ pf✝³ pf✝⁵) =
    arrowMap (functor hj iter) (↑⟨l₁, pf✝²⟩) (↑⟨l₂, pf✝¹⟩) pf✝ pf✝¹

Tactic:
arrow_mk_mapObj,

Goal state after:
case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter l₂ pf✝⁷).F l₁ l₂ pf✝⁵ pf✝³ = arrowMap (functor hj iter) (↑⟨l₁, pf✝²⟩) (↑⟨l₂, pf✝¹⟩) pf✝ pf✝¹
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
⊢ φ₁ = φ₂

Tactic:
by
  refine c.isColimit.hom_ext (fun j ↦ ?_)
  dsimp
  induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa [← cancel_epi c.isoBot.inv] using h₀
  | succ j hj hj' =>
    apply (c.attachCells j hj).hom_ext
    · simpa using hj'
    · intro i
      simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })
  | isSuccLimit j hj hj' =>
    exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
      (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)

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

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ i < Order.succ i

Tactic:
by
          simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
          exact ⟨_, hi⟩

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
this✝ : HasIterationOfShape κ.ord.ToType C
this : NoMaxOrder κ.ord.ToType
⊢ (Iso.refl (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).left).hom ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f))).hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).hom ≫
      (((evaluation (Arrow C) (Arrow C)).obj f).mapIso ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)).hom

Tactic:
have := NatTrans.congr_app ((succStruct I κ).iterationFunctor_map_succ j (not_isMax j)) f
    dsimp at this
    dsimp [iterationFunctor]
    rw [id_comp, this, assoc, Iso.inv_hom_id_app, comp_id]
    dsimp [succStruct]

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 g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f.hom)))
⊢ objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ Arrow.Hom.right φ

Tactic:
let e₂ := asIso ((ιIteration I κ).app (Arrow.mk g.hom)).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 κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f.hom)))
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk g.hom)))
⊢ objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ Arrow.Hom.right φ
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 G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
J : Type w
w✝³ : LinearOrder J
w✝² : OrderBot J
w✝¹ : SuccOrder J
w✝ : WellFoundedLT J
h : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J i
⊢ (generatingMonomorphisms G).pushouts.rlp p

Tactic:
by simpa

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
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
hf' : (monomorphisms C).TransfiniteCompositionOfShape κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape := hf.toTransfiniteCompositionOfShape;
  { toTransfiniteCompositionOfShape := __TransfiniteCompositionOfShape, map_mem := ⋯ }
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.F.map φ)
⊢ PreservesColimit hf.F (coyoneda.obj (Opposite.op A))

Tactic:
apply preservesColimit_coyoneda_obj_of_mono (Y := hf'.F) (κ := κ)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
hf' : (monomorphisms C).TransfiniteCompositionOfShape κ.ord.ToType f := ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.F.map φ)
⊢ HasCardinalLT (Subobject A) κ
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Tactic:
simp [padicNorm, hq]

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

Goal state before:
pp: p : ℕ
q : ℚ
hq : ¬q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
simp [padicNorm, hq]

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

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

Tactic:
intro hq

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
hq : ¬q = 0
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x).valuation = ↑x.valuation

Tactic:
simp [valuation, valuation_coe_nonneg]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ x = ↑(unitCoeff hx) * ↑p ^ x.valuation

Tactic:
apply Subtype.coe_injective

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (fun a ↦ ↑a) x = (fun a ↦ ↑a) (↑(unitCoeff hx) * ↑p ^ x.valuation)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: 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
hx : x ≠ 0
⊢ ‖a‖ = 1

Tactic:
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]

Goal state after:
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
hx : x ≠ 0
⊢ ↑p ≠ 0 ∨ -x.valuation + -↑n ≠ 0 ∨ -x.valuation = 0 ∧ -↑n = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
have hf : f * g ≈ 0 := mul_equiv_zero _ hg
      simp only [hf, hg, norm, dif_pos, mul_zero]

Goal state after:
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
    exact IsPullback.of_isLimit (PullbackCone.isLimitMkIdId f)

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 : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → Epi f

Tactic:
intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h
    rw [hf]

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

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

Tactic:
have hfg' : f + g ≈ f := by
          change LimZero (g - 0) at hg
          change LimZero (f + g - f); · simpa only [add_sub_cancel_left, sub_zero] using hg

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
⊢ (f + g).norm ≤ max f.norm g.norm
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : S.Etale
t : ↥S
a : S.residueField t ⟶ CommRingCat.of Ω
y : ↥(Hom.fiber X.hom t)
hs₀ : ((SpecToEquivOfField Ω S).symm ⟨t, a⟩) default = t
⊢ (Hom.fiberToSpecResidueField X.hom t) y = (Spec.map a) default

Tactic:
subsingleton

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
⊢ False

Tactic:
obtain ⟨N, hN⟩ := cauchy₂ f hε

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
this : X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0
⊢ (((-1) ^ 0 • X.σ ⟨0, ⋯⟩) ≫ eqToHom ⋯) ≫ K[X].d 1 0 = 0

Tactic:
by simpa

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

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 m : ℕ
hnm : c.Rel m n
⊢ hσ' q n m hnm = G.map (hσ' q n m hnm)

Tactic:
unfold hσ' hσ
  split_ifs
  · simp only [Functor.map_zero, zero_comp]
  · simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
    rfl

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

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 : ℕ
⊢ (Hσ q).f n = G.map ((Hσ q).f n)

Tactic:
unfold Hσ
  have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
  simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq
  rw [eq]
  let h := (Functor.congr_obj (map_alternatingFaceMapComplex G) X).symm
  congr

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
this : ‖↑↑z‖ ≤ 1
⊢ ‖↑z‖ ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNormE (↑f j - ↑f i) < ε

Tactic:
have h := isCauSeq f ε (mod_cast hε)
      dsimp [norm] at h
      exact mod_cast h

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
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Tactic:
let Y₄ := (karoubiFunctorCategoryEmbedding _ _).obj ((toKaroubi _).obj Y.X)

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)
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ {i | ↑i < q + 1}.erase q' = {i | ↑i < q}

Tactic:
ext ⟨i, hi⟩
        simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
        lia

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ False

Tactic:
apply hθ

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ A.pull θ = Splitting.IndexSet.mk e

Tactic:
· dsimp only [SimplicialObject.Splitting.IndexSet.pull]
    congr
    exact SimplexCategory.factorThruImage_eq fac

Goal state after: