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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generateSingleton f).arrows g → (generate (Presieve.singleton f)).arrows g

Tactic:
rintro ⟨g, h⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g✝ : Z ⟶ X
g : Z ⟶ Y
h : g ≫ f = g✝
⊢ (generate (Presieve.singleton f)).arrows g✝
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (yoneda.obj (F ⋙ uliftFunctor.{v, w}).reprX ⋙ uliftFunctor.{w, v}) R

Tactic:
rw [isSheafFor_comp_uliftFunctor_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (yoneda.obj (F ⋙ uliftFunctor.{v, w}).reprX) R
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
T : Over X
g : T.left ⟶ Y
hT : g ≫ f = T.hom
h₁ : (Sieve.generateSingleton f).arrows (Over.mk f).hom
h₂ :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
    g₁ ≫ f = g₂ ≫ f →
      g₁ ≫ S.ι.app { obj := Over.mk f, property := h₁ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := h₁ }
h₃ : (Sieve.generateSingleton f).arrows T.hom
y : D := { obj := Over.mk f, property := ⋯ }
x : D := { obj := Over.mk T.hom, property := ⋯ }
g' : x ⟶ y := ObjectProperty.homMk (Over.homMk g ⋯)
⊢ F.map g' ≫ S.ι.app { obj := Over.mk f, property := h₁ } = S.ι.app { obj := T, property := h₃ }

Tactic:
S.w

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
T : Over X
g : T.left ⟶ Y
hT : g ≫ f = T.hom
h₁ : (Sieve.generateSingleton f).arrows (Over.mk f).hom
h₂ :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
    g₁ ≫ f = g₂ ≫ f →
      g₁ ≫ S.ι.app { obj := Over.mk f, property := h₁ } = g₂ ≫ S.ι.app { obj := Over.mk f, property := h₁ }
h₃ : (Sieve.generateSingleton f).arrows T.hom
y : D := { obj := Over.mk f, property := ⋯ }
x : D := { obj := Over.mk T.hom, property := ⋯ }
g' : x ⟶ y := ObjectProperty.homMk (Over.homMk g ⋯)
⊢ S.ι.app x = S.ι.app { obj := T, property := h₃ }
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
T : Over B✝
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {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 := ⋯ }
h₃ : (Sieve.generateFamily X π).arrows T.hom
A : D := { obj := Over.mk (π a), property := ⋯ }
B : D := { obj := Over.mk T.hom, property := ⋯ }
i : B ⟶ A := ObjectProperty.homMk (Over.homMk g ⋯)
⊢ F.map i ≫ S.ι.app { obj := Over.mk (π a), property := ⋯ } = S.ι.app { obj := T, property := h₃ }

Tactic:
S.w

Goal state after:
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
T : Over B✝
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {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 := ⋯ }
h₃ : (Sieve.generateFamily X π).arrows T.hom
A : D := { obj := Over.mk (π a), property := ⋯ }
B : D := { obj := Over.mk T.hom, property := ⋯ }
i : B ⟶ A := ObjectProperty.homMk (Over.homMk g ⋯)
⊢ S.ι.app B = S.ι.app { obj := T, property := h₃ }
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ (F.map p₁ ≫ Sieve.ofArrows.h ha) ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map (p₁ ≫ a)

Tactic:
rw [assoc, ha', map_comp]

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

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

Tactic:
have := isContinuous_comap_forget (S := S) _ H
  refine (Functor.restrictedTopology_eq_inducedTopology_of_isContinuous ?_).symm
  rw [toGrothendieck_comap_forget_eq_restrictedTopology _ H]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ c₂.ι.app j ≫ g = c₁.ι.app j ≫ 0

Tactic:
hg j,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = c₁.ι.app j ≫ 0
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✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ f j₁

Tactic:
dsimp only [f]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
⊢ ∃ j₁, ⟨j', hj'✝⟩ ≤ ⟨↑j₁.1, ⋯⟩
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
⊢ W.transfiniteCompositionsOfShape J ≤ transfiniteCompositions.{w, v, u} W

Tactic:
intro A

Goal state after:
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
A : C
⊢ ∀ ⦃Y : C⦄ (f : A ⟶ Y), W.transfiniteCompositionsOfShape J f → transfiniteCompositions.{w, v, u} W f
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ 𝟙 Φ.X₀ ≫ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    ((Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯)) ≫ (Φ.iterationFunctor J).map f

Tactic:
rw [id_comp, assoc, ← Functor.map_comp]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯ ≫ f)
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 ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val))

Tactic:
by
    rw [← comp_apply, ← map_comp, ← comp_apply, ← map_comp, ← op_comp, ← op_comp,
      homOfLE_comp, homOfLE_comp, e.map_succ k (lt_of_lt_of_le hk hij)]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Additive

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.Additive
X Y : C
f g : X ⟶ Y
⊢ (adj.homEquiv X (F.obj Y)) (F.map (f + g)) = (adj.homEquiv X (F.obj Y)) (F.map f + F.map g)

Tactic:
simp [homEquiv_unit]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ Mono (pushout.desc p f ⋯)

Tactic:
· exact (IsPushout.of_hasPushout _ _).mono_of_isPullback_of_mono
      (IsPullback.of_hasPullback p f) _ (by simp) (by simp)

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
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)
h : Function.Injective fun j ↦ transfiniteIterate (largerSubobject hG) j A₀
⊢ False

Tactic:
by simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0

Tactic:
apply zpow_ne_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ¬↑p ^ (-padicValRat p q) = 0

Tactic:
apply zpow_ne_zero

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ ↑p ^ (-padicValRat p ↑z) ≤ 1

Tactic:
exact zpow_le_one_of_nonpos₀ (mod_cast hp.1.one_le) (by simp)

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

Goal state before:
pp: case cons
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ Finset.cons s S' Hnot, F i)

Tactic:
rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]

Goal state after:
case cons
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (F s + ∑ x ∈ S', F x)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p b - padicValNat p m = padicValNat p b

Tactic:
eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p b - 0 = padicValNat p b
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ i ∈ Finset.Ico (0 + 1) (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum

Tactic:
rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1,
    Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]

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
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
g : Φ.presheafFiber.obj P₂ ⟶ M
⊢ (⇑Φ.skyscraperPresheafHomEquiv ∘ fun x ↦ Φ.presheafFiber.map f ≫ x) g =
    ((fun g ↦ f ≫ g) ∘ ⇑Φ.skyscraperPresheafHomEquiv) g

Tactic:
simp [skyscraperPresheafHomEquiv_naturality_left]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
⊢ f.norm = g.norm

Tactic:
classical
  exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
    simp only [hf, hg, norm, dif_pos]
  else by
    have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
    simp only [hg, hf, norm, dif_neg, not_false_iff]
    let i := max (stationaryPoint hf) (stationaryPoint hg)
    have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
    have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
    rw [hpf, hpg, h]

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

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

Tactic:
intro V

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this : Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U
V : C
⊢ ∀ (s : ToType ((shrinkYoneda.{w, v, u}.obj U).obj (op V))), Presheaf.imageSieve f s ∈ J V
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
hf : F.relativelyRepresentable (F.map f)
g : Y ⟶ Z
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf.fst' (F.map g) ≫ f) = F.map (hf.snd (F.map g) ≫ g)

Tactic:
simp [(hf.w (F.map g))]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf.lift i h hi ≫ hf.snd g) = F.map h

Tactic:
by simpa [lift] using! PullbackCone.IsLimit.lift_snd _ _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
⊢ ⋃ i,
      Set.range
        ⇑((SpecToEquivOfField (SeparableClosure ↑(S.residueField i)) S).invFun
            ⟨i, CommRingCat.ofHom (algebraMap (↑(S.residueField i)) (SeparableClosure ↑(S.residueField i)))⟩) =
    Set.univ

Tactic:
ext s
    simp only [Equiv.invFun_as_coe, Set.mem_iUnion, Set.mem_range, Set.mem_univ, iff_true]
    exact ⟨s, default, by simp [SpecToEquivOfField]⟩

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

Goal state before:
pp: case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε

Tactic:
have := (stationaryPoint_spec hne' le_rfl hle).symm
          simp only [const_apply, CauSeq.sub_apply, padicNorm.zero, sub_self] at this
          simpa only [this]

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

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

Tactic:
rw [← Functor.map_comp, lift_snd]
      exact h

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ padicNormE (↑f i - ↑(limSeq f i)) < ε

Tactic:
refine lt_of_lt_of_le h ((div_le_iff₀' <| mod_cast succ_pos _).mpr ?_)

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ (↑i + 1) * ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ (↑i + 1) * ε

Tactic:
right_distrib

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε + 1 * ε
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
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ nullHomotopicMap' (hσ' q) =
    nullHomotopicMap' fun i j hij ↦ hσ' q i j hij ≫ ((alternatingFaceMapComplex C).map f).f j

Tactic:
comp_nullHomotopicMap'

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (nullHomotopicMap' fun i j hij ↦ ((alternatingFaceMapComplex C).map f).f i ≫ hσ' q i j hij) =
    nullHomotopicMap' fun i j hij ↦ hσ' q i j hij ≫ ((alternatingFaceMapComplex C).map f).f j
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
⊢ φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
have hnaq_shift (d : ℕ) : n + d = a + d + q := by lia

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
⊢ φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ n + 1 ≤ ↑⟨a, ⋯⟩ + (q + 1)

Tactic:
by
        simp only [hnaq, add_assoc]
        rfl

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
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ (↑p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num)⁻¹ ≤ 1

Tactic:
apply inv_le_one_of_one_le₀

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