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

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Tactic:
rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩
    intro x
    obtain ⟨y, hy⟩ := 𝒰.covers x
    refine ⟨(𝒰.X (𝒰.idx x)).asOverProp S (p _), (𝒰.f (𝒰.idx x)).asOverProp S, y, hle _ _ ?_,
      𝒰.map_prop _, hy⟩
    use 𝒰.idx x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ basicOpen (g i) ≤ V

Tactic:
by rw [hg]; exact le_iSup_of_le _ le_rfl

Goal state after:
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
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
this :
  ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
⊢ Function.Injective ⇑(ConcreteCategory.hom (Φ.presheafFiber.map f))

Tactic:
rintro q₁ q₂ h

Goal state after:
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
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
this :
  ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
q₁ q₂ : CC (Φ.presheafFiber.obj P)
h : (ConcreteCategory.hom (Φ.presheafFiber.map f)) q₁ = (ConcreteCategory.hom (Φ.presheafFiber.map f)) q₂
⊢ q₁ = q₂
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.functorPullback F (Sieve.pullback ((data a.Y).f i ≫ a.f) (data X).toPreOneHypercover.sieve₀), ⋯⟩),
    ((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op =
      (s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op

Tactic:
by
        rintro ⟨X₀, b, ⟨_, c, _, h, fac₁⟩⟩
        obtain ⟨j⟩ := h
        refine Presheaf.IsSheaf.hom_ext hG₀
          ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F c⟩ _ _ ?_
        rintro ⟨Y₀, d, e, fac₂⟩
        dsimp at i j c fac₁ ⊢
        have he : S (F.map e ≫ (data X).f j) := by
          rw [fac₂, assoc, fac₁]
          simpa only [assoc] using S.1.downward_closed a.hf (F.map d ≫ F.map b ≫ (data a.Y).f i)
        simp only [assoc, ← Functor.map_comp, ← op_comp, ← fac₁]
        conv_lhs => simp only [op_comp, Functor.map_comp, assoc, lift_map_assoc]
        rw [← Functor.map_comp, ← op_comp, ← fac₂, liftAux_fac _ _ _ he]
        simpa using s.condition
          { fst := { hf := he, .. }
            snd := a
            r := ⟨_, 𝟙 _, F.map d ≫ F.map b ≫ (data a.Y).f i, by
              simp only [fac₁, fac₂, assoc, id_comp]⟩ }

Goal state after:
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 : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
⊢ (presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op =
    (presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, (data X).mem₁₀ i₁ i₂ b₁ b₂ (by simp only [h₁, h₂, assoc, fac])⟩ _ _ ?_

Goal state after:
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 : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩),
    ((presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫
          G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫
        G₀.obj.map I.f.op =
      ((presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫
          G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫
        G₀.obj.map I.f.op
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: case h
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)
𝒱 : PreZeroHypercover X := ⋯
⊢ Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [Presieve.map_ofArrows]

Goal state after:
case h
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)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun i ↦ Over.mk ⊤ (𝒰.X i).hom ⋯, f := fun i ↦ Over.homMk (Over.Hom.left (𝒰.f i)) ⋯ trivial }
⊢ (Presieve.ofArrows (fun i ↦ (Over.forget P ⊤ S).obj (𝒱.X i)) fun i ↦ (Over.forget P ⊤ S).map (𝒱.f i)) =
    Presieve.ofArrows 𝒰.X 𝒰.f
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✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ (colimit.cocone X₁).ι.app j ≫ colimMap φ = c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom

Tactic:
colimit.cocone_ι,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ colimit.ι X₁ j ≫ colimMap φ = c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom
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
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂

Tactic:
by
    rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]

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

Goal state before:
pp: case refine_1
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
⊢ (colimit.cocone S.X₁).ι.app j ≫ colimMap S.f =
    c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom

Tactic:
colimit.cocone_ι,

Goal state after:
case refine_1
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
⊢ colimit.ι S.X₁ j ≫ colimMap S.f = c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
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
⊢ (colimit.cocone S.X₂).ι.app j ≫ colimMap S.g =
    c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom

Tactic:
colimit.cocone_ι,

Goal state after:
case refine_2
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
⊢ colimit.ι S.X₂ j ≫ colimMap S.g = c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom
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 (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) = (ConcreteCategory.hom (f.hom.app Y)) g.unop

Tactic:
rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : ¬IsMax i
j : Fin (n + 1)
⊢ ?m.68 ≠ last ?m.67

Tactic:
by simpa using! hi

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : IsMax i
⊢ i = last n

Tactic:
by simpa using! hi

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : ¬IsMin i
j : Fin (n + 1)
⊢ ?m.70 ≠ 0

Tactic:
by simpa using! hi

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : IsMin i
⊢ i = 0

Tactic:
by simpa using! hi

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

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ b ≤ a

Tactic:
rw [← s.le_iff_le]

Goal state after:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ s.toRelEmbedding b ≤ s.toRelEmbedding a
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝² : Small.{u, u_1} α
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : Shrink.{u, u_1} α
⊢ ⊥ ≤ a

Tactic:
simp [← (orderIsoShrink.{u} α).symm.le_iff_le]

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow C
⊢ Arrow.Hom.left (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (πFunctorObj f g.hom)))

pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow C
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (πFunctorObj f g.hom)))

Tactic:
· apply functorMap_id

Goal state after:
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow C
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (πFunctorObj f g.hom)))
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
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    val₀

Tactic:
d.map_lift _ _ _ _ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)

Goal state after:
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
⊢ ↑⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩
      (op ⟨⊥, ⋯⟩) =
    val₀
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

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

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1
      (exists_larger_subobject hG A hA).choose_spec.choose_spec
    exact Arrow.isoMk (Iso.refl _)
      (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA])))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (q.num * ↑r.den * ↑q.den)

Tactic:
emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den) + emultiplicity ↑p ↑q.den
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation

Tactic:
rw [valuation_p_pow_mul _ _ this]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ n + c.valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ x ∈ Ideal.span {↑p ^ n} ↔ n ≤ x.valuation

Tactic:
by
  rw [Ideal.mem_span_singleton]
  constructor
  · rintro ⟨c, rfl⟩
    suffices c ≠ 0 by
      rw [valuation_p_pow_mul _ _ this]
      exact le_self_add
    contrapose hx
    rw [hx, mul_zero]
  · nth_rewrite 2 [unitCoeff_spec hx]
    simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _

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

Tactic:
intro hf
    simpa only [← cancel_epi f] using c.condition

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Presieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ≤ (Sieve.ofArrows U f).arrows

Tactic:
Presieve.ofArrows_le_iff

Goal state after:
case refine_2.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ ∀ (i_1 : ι'), (Sieve.ofArrows U f).arrows (f (i i_1))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε

Tactic:
dsimp [padicNormE]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Padic.mk f - ↑(↑f i)) < ε
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
inst✝ : F.Faithful
c : C
a b : c ⟶ hf.pullback g
h₁ : F.map a ≫ hf.fst g = F.map b ≫ hf.fst g
h₂ : a ≫ hf.snd g = b ≫ hf.snd g
⊢ F.map a ≫ ⋯.cone.snd = F.map b ≫ ⋯.cone.snd

Tactic:
by simpa using! F.congr_map h₂

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

Goal state before:
pp: 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) < ε
⊢ padicNormE (⟦q'⟧ - ↑(↑q' N)) < ε

Tactic:
dsimp [padicNormE]

Goal state after:
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) < ε
⊢ { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Completion.mk q' - ↑(↑q' N)) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ ‖↑p‖ ^ n = ↑p ^ (-n)

Tactic:
norm_p,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑p)⁻¹ ^ n = ↑p ^ (-n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
norm_p,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < (↑p)⁻¹⁻¹