mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫
      (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫
        (Proj.restrict ⋯).presheaf.germ ⊤ x True.intro ≫ (Proj.restrictStalkIso ⋯ x).hom =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv

Tactic:
rw [LocallyRingedSpace.restrictStalkIso_hom_eq_germ]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫
      (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫
        Proj.presheaf.germ (⋯.functor.obj ⊤) ((ConcreteCategory.hom (pbo f).inclusion') x) ⋯ =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ m * i = m • i

Tactic:
smul_eq_mul

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ m * i = m * i
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ Existence.universally f✝

Tactic:
· rwa [MorphismProperty.IsStableUnderBaseChange.universally_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
⊢ IsClosedImmersion (pullback.diagonal f)

Tactic:
suffices h : ValuativeCriterion.Existence (pullback.diagonal f) by
      have := UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h
      exact .of_isPreimmersion _ (pullback.diagonal f).isClosedMap.isClosed_range

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
⊢ ValuativeCriterion.Existence (pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case h
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
p : Q (𝒰.X i ↘ S)
⊢ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).arrows
    (Hom.asOver (𝒰.f i) S)

Tactic:
use (𝒰.X i).asOverProp S p, MorphismProperty.Over.homMk (𝒰.f i) (comp_over (𝒰.f i) S), 𝟙 _

Goal state after:
case h
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.I₀
p : Q (𝒰.X i ↘ S)
⊢ (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩).arrows
      (MorphismProperty.Over.homMk (𝒰.f i) ⋯ True.intro) ∧
    Hom.asOver (𝒰.f i) S =
      𝟙 ((𝒰.X i).asOver S) ≫ (MorphismProperty.Over.forget Q ⊤ S).map (MorphismProperty.Over.homMk (𝒰.f i) ⋯ True.intro)
Module: Mathlib.CategoryTheory.Sites.Point.Basic

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✝⁶ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁵ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory A FC
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
⊢ J.W.IsInvertedBy Φ.presheafFiber

Tactic:
intro P Q f hf
  obtain ⟨_, _⟩ := (J.W_iff_isLocallyBijective f).1 hf
  rw [← isIso_iff_of_reflects_iso _ (forget A), isIso_iff_bijective]
  exact Φ.toPresheafFiber_map_bijective f

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }

Tactic:
let Y' : D := ⟨Over.mk f, 𝟙 _, by simp⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
S : Cocone (Sieve.generateSingleton f).arrows.diagram
Z : C
g₁ g₂ : Z ⟶ Y
h : g₁ ≫ f = g₂ ≫ f
Y' : D := { obj := Over.mk f, property := ⋯ }
⊢ g₁ ≫ S.ι.app { obj := Over.mk f, property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := ⋯ }
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 : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
⊢ T.hom ≫ m = (aux e ⋯).ι.app { obj := T, property := ⋯ }

Tactic:
simp only [← ha, Category.assoc, hm]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
T : Over B
a : α
g : T.left ⟶ X a
ha : g ≫ π a = T.hom
⊢ g ≫ e a = (aux e ⋯).ι.app { obj := T, property := ⋯ }
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: ⊢ etalePrecoverage ≤ proetalePrecoverage

Tactic:
by
  rw [proetalePrecoverage, propQCPrecoverage, etalePrecoverage, le_inf_iff]
  refine ⟨precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f hf ↦ f.isOpenMap, ?_⟩
  apply precoverage_mono
  intro X Y f hf
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: case refine_1
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 : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₁ :
  A₁ ⟶
    { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
        zero := ⋯ }.X₁
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.f
⊢ x₁ ≫ t = 0

pp: case refine_2
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 : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₁ :
  A₁ ⟶
    { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
        zero := ⋯ }.X₁
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.f
⊢ π₁ ≫ z = (-kernel.lift t x₁ ?refine_1) ≫ kernel.map t b l r ⋯

Tactic:
· simpa using hx₁.symm =≫ biprod.fst

Goal state after:
case refine_2
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 : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₁ :
  A₁ ⟶
    { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
        zero := ⋯ }.X₁
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.f
⊢ π₁ ≫ z = (-kernel.lift t x₁ ⋯) ≫ kernel.map t b l r ⋯
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 : ¬IsMax i
⊢ W ((h.iic j).F.map (homOfLE ⋯))

Tactic:
have := h.map_mem i.1 (by
      rw [not_isMax_iff] at hi ⊢
      obtain ⟨i', hi'⟩ := hi
      exact ⟨j, lt_of_lt_of_le hi' i'.2⟩)
    rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
    have eq : Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
      Arrow.mk (homOfLE (Order.le_succ i.1)) :=
        Arrow.ext rfl (Set.Iic.coe_succ_of_not_isMax hi) rfl
    replace eq := congr_arg h.F.mapArrow.obj eq
    convert! this using 1

Goal state after:
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
h : IsMin ⊥
iter₁ iter₂ : Φ.Iteration ⊥
h₂ h₁₂ : ⊥ ≤ ⊥
⊢ iter₁.F.obj ⟨⊥, h₂⟩ = iter₂.F.obj ⟨⊥, h₂⟩

Tactic:
by simp only [obj_bot]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
⊢ F.map (homOfLE ⋯) ≫ sq'.f' ≫ p = c.ι.app ⊥ ≫ g

Tactic:
sq'.w₂,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
⊢ F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g = c.ι.app ⊥ ≫ g
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ RelativeCellComplex (fun x ↦ I.homFamily) (ιObj I κ f)

Tactic:
have := hasIterationOfShape I κ
  let h := transfiniteCompositionOfShapeSuccStructPropιIteration I κ
  exact
  { toTransfiniteCompositionOfShape :=
      h.toTransfiniteCompositionOfShape.map ((evaluation _ _).obj f ⋙ Arrow.leftFunc)
    attachCells j hj :=
      attachCellsOfSuccStructProp I κ (h.map_mem j hj) f }

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

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicValInt p ↑p = 1

Tactic:
simp [padicValNat.self hp]

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ (generatingMonomorphisms G).pushouts (⊤.ofLE (largerSubobject hG ⊤) ⋯)

Tactic:
have := (Subobject.isIso_arrow_iff_eq_top (largerSubobject hG (⊤ : Subobject X))).2 (by simp)

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
this : IsIso (largerSubobject hG ⊤).arrow
⊢ (generatingMonomorphisms G).pushouts (⊤.ofLE (largerSubobject hG ⊤) ⋯)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) (n₁ * d₂) ≤ multiplicity (↑p) n₂ + multiplicity (↑p) d₁

Tactic:
← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| multiplicity (↑p) (n₁ * d₂) ≤ multiplicity (↑p) (n₂ * d₁)
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
⊢ (generatingMonomorphisms G).HasSmallObjectArgument

Tactic:
exact ⟨κ, inferInstance, inferInstance,
    { preservesColimit {A B X Y} i hi f hf := by
        let hf' : (monomorphisms C).TransfiniteCompositionOfShape κ.ord.ToType f :=
          { toTransfiniteCompositionOfShape := hf.toTransfiniteCompositionOfShape
            map_mem j hj := by
              have := (hf.attachCells j hj).pushouts_coproducts
              simp only [ofHoms_homFamily] at this
              refine (?_ : _ ≤ monomorphisms C) _ this
              simp only [pushouts_le_iff, coproducts_le_iff]
              exact generatingMonomorphisms_le_monomorphisms G }
        have (j j' : κ.ord.ToType) (φ : j ⟶ j') : Mono (hf'.F.map φ) := hf'.mem_map φ
        apply preservesColimit_coyoneda_obj_of_mono (Y := hf'.F) (κ := κ)
        obtain ⟨S⟩ := hi
        exact Subobject.hasCardinalLT_of_mono hκ S.arrow }⟩

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

Goal state before:
pp: p : ℕ
⊢ padicNorm p 0 = 0

Tactic:
by simp [padicNorm]

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

Goal state before:
pp: p : ℕ
⊢ padicNorm p 1 = 1

Tactic:
by simp [padicNorm]

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

Goal state before:
pp: p : ℕ
hp : p ≠ 1
a n : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a

Tactic:
rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity_of_ne_one hp ha, Nat.cast_le]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b

Tactic:
by
  simp_rw [padicValInt]
  rw [Int.natAbs_mul, padicValNat.mul] <;> rwa [Int.natAbs_ne_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
⊢ ∀ (X Y : F.Elements), ∃ W x x, True

Tactic:
rintro ⟨X, x⟩ ⟨Y, y⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
⊢ ∃ W x x, True
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
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
⊢ ∃ Z p₁ p₂ z,
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧ (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁ ∧ (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂

Tactic:
let α₁ : Φ.fiber.elementsMk _ y₁ ⟶ Φ.fiber.elementsMk _ x := ⟨f₁, hy₁⟩
    let α₂ : Φ.fiber.elementsMk _ y₂ ⟶ Φ.fiber.elementsMk _ x := ⟨f₂, hy₂⟩
    obtain ⟨z, q₁, q₂, fac⟩ := IsCofiltered.cospan α₁ α₂
    rw [Subtype.ext_iff] at fac
    refine ⟨z.1, q₁.1, q₂.1, z.2, fac, ?_, ?_⟩
    all_goals rw [CategoryOfElements.map_snd]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ m = n → m = n

Tactic:
exact id

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
X : SimplicialObject C
⊢ QInfty ≫ PInfty = 0

Tactic:
ext n
  apply QInfty_f_comp_PInfty_f

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (b : Splitting.IndexSet Δ),
    Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) b ≫
        (Iso.refl (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))).pt).hom =
      (Splitting.cofan' (fun n ↦ K.X n) (obj K)
            (fun n ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ).inj
        b

Tactic:
intro A
      dsimp [Splitting.cofan']
      rw [comp_id, Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
        (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl), Γ₀.Obj.Termwise.mapMono_id]
      dsimp
      rw [id_comp]
      rfl

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

Goal state before:
pp: case pos
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⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
A : IndexSet (op ⦋n⦌)
hA : A.EqId
⊢ f ≫ (s.πSummand A ≫ (s.cofan (op ⦋n⦌)).inj A) ≫ PInfty.f n = 0

Tactic:
dsimp at hA
      subst hA
      rw [assoc, reassoc_of% h, zero_comp]

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
n : ℕ
⊢ PInfty.f n - PInfty.f n ≫ PInfty.f n = 0

Tactic:
PInfty_f_idem,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ PInfty.f n - PInfty.f n = 0
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

Tactic:
· have ht : (t : ℝ) = 1 / 2 := by linarith
    norm_num [ht]

Goal state after:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ piToPiTop X ≫ CategoryTheory.Functor.pi' (proj X) = 𝟙 (CategoryTheory.Grpd.of ((i : I) → ↑(π.obj (X i))))

Tactic:
by
    change piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 _
    apply CategoryTheory.Functor.ext ?_ ?_
    · intros; rfl
    · intros; ext; simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : f.Nullhomotopic
g : C(Y, Z)
⊢ (g.comp f).Nullhomotopic

Tactic:
by
  obtain ⟨y, hy⟩ := hf
  use g y
  exact .comp (.refl g) hy

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 Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ L.map (homMk P.p₀) = L.map (homMk P.p₁)

Tactic:
have := Localization.inverts L (weakEquivalences _) (homMk P.ι) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)

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
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
this : IsIso (L.map (homMk P.ι))
⊢ L.map (homMk P.p₀) = L.map (homMk P.p₁)