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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ ny →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) y ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
intro n hn

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ nx →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) x ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
intro n hn

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ HomogeneousLocalization.mk { deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
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 ⋯).toTopCat
⊢ (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))).inv ≫
      (Spec A⁰_ f).presheaf.germ ⊤ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) ⋯ ≫
        LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
by
  dsimp
  erw [LocallyRingedSpace.stalkMap_germ (toSpec 𝒜 f) ⊤ x (by simp)]
  erw [toOpen_toSpec_val_c_app_assoc]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case exists_of_eq.e_6.e_a
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
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ c ^ m * (↑z.den * ↑y.num) = ↑y.den * (c ^ m * ↑z.num)

Tactic:
mul_left_comm y.den.1,

Goal state after:
case exists_of_eq.e_6.e_a
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
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e✝ :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ c ^ m * (↑z.den * ↑y.num) = c ^ m * (↑y.den * ↑z.num)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
⊢ (commSq.i₁ ≫ X'_to_X) ≫ f = Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ ≫ Y'_to_Y

Tactic:
by simp only [Category.assoc, hP.w, reassoc_of% commSq.commSq.w]

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

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver f) → Cover.Over S (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver f), T f H = (V f H).toPresieveOver
⊢ 𝒰.toPresieveOver.bind T = Cover.toPresieveOver (Precoverage.ZeroHypercover.bind 𝒰 fun j ↦ V (Hom.asOver (𝒰.f j) S) ⋯)

Tactic:
convert!
      Presieve.ofArrows_bind _ (fun j ↦ (𝒰.f j).asOver S) _ (fun Y f H j ↦ ((V f H).X j).asOver S)
        (fun Y f H j ↦ ((V f H).f j).asOver S)

Goal state after:
case e'_2.e'_5
P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver f → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver f) → Cover.Over S (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver f), T f H = (V f H).toPresieveOver
e_1✝ : Presieve X = Presieve (OverClass.asOver X.left S)
e_3✝ : X = OverClass.asOver X.left S
e_4✝ : 𝒰.toPresieveOver ≍ Presieve.ofArrows (fun j ↦ OverClass.asOver (𝒰.X j) S) fun j ↦ Hom.asOver (𝒰.f j) S
x✝² : Over S
x✝¹ : x✝² ⟶ X
x✝ : 𝒰.toPresieveOver x✝¹
⊢ T x✝¹ x✝ = Presieve.ofArrows (fun j ↦ ((V x✝¹ x✝).X j).asOver S) fun j ↦ Hom.asOver ((V x✝¹ x✝).f j) S
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝

Tactic:
apply of_specializingMap

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
⊢ l₁ = l₂

Tactic:
let Z := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
⊢ l₁ = l₂
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallGrothendieckTopology P S) X ↔ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
rw [smallGrothendieckTopology_eq_toGrothendieck_smallPretopology _ le_rfl]

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallPretopology P P).toGrothendieck X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
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
⊢ ∃ n, f ^ n • t = 0

Tactic:
use ⨆ i, n i

Goal state after:
case h
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
⊢ (f ^ ⨆ i, n i) • t = 0
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
B : Type u''
inst✝² : Category.{v'', u''} B
inst✝¹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v'', u''} B
X : C
x : Φ.fiber.obj X
x✝¹ x✝ : Cᵒᵖ ⥤ A
f : x✝¹ ⟶ x✝
⊢ ((evaluation Cᵒᵖ A).obj (op X)).map f ≫ Φ.toPresheafFiber X x x✝ = Φ.toPresheafFiber X x x✝¹ ≫ Φ.presheafFiber.map f

Tactic:
simp [presheafFiber, toPresheafFiber]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_2
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W := ⋯
W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
U : C
π : U ⟶ W
hπ : (Sieve.coverByImage F W).arrows π
⊢ Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)) ∈ J (F.obj (Nonempty.some hπ).obj)

Tactic:
apply functorPushforward_imageSieve_mem

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
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)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i

Tactic:
refine Presheaf.IsSheaf.hom_ext hG₀
      ⟨_, cover_lift F J₀ _ (J.pullback_stable ((data X).f i) S.2)⟩ _ _ ?_

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
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)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback F (Sieve.pullback ((data X).f i) ↑S), ⋯⟩),
    (f₁ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op =
      (f₂ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsConstant J F

Tactic:
have : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) := by
    rw [← constantSheafAdj_counit_w]
    infer_instance
  rw [F.isConstant_iff_isIso_counit_app (hT := hT)]
  exact isIso_of_reflects_iso _ (sheafCompose J U)

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : ¬IsMin i
j : Fin (n + 1)
⊢ j < i ↔ j ≤ cases 0 castSucc i

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (by simpa using! hi)
        simp [le_castSucc_iff]

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

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

Tactic:
obtain rfl : i = 0 := by simpa using! hi

Goal state after:
n : ℕ
hi : IsMin 0
⊢ cases 0 castSucc 0 = 0
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
⊢ IsColimit (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i))

Tactic:
have heq (s : Cofan fun i ↦ J.yoneda.obj (X i))
      {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j) (hab : a ≫ c.inj i = b ≫ c.inj j) :
      (s.inj i).hom.app (op Y) a = (s.inj j).hom.app (op Y) b := by
    by_cases h : i = j
    · subst h
      rw [(cancel_mono _).mp hab]
    · obtain ⟨h⟩ := hdisj h a b hab
      have := Types.isTerminalEquivUnique _ (Sheaf.isTerminalOfBotCover s.pt _ (hempty Y h))
      exact Subsingleton.elim _ _
  refine Cofan.IsColimit.mk _ (fun s ↦ ⟨?_⟩) (fun s j ↦ ?_) fun s m hm ↦ ?_
  · refine (s.pt.2.isSheafFor _ H).extend ?_
    refine ⟨fun Y ↦ ↾fun g ↦ ((s.inj (Sieve.ofArrows.i g.2)).hom.app Y)
      (Sieve.ofArrows.h g.2), ?_⟩
    intro ⟨Y⟩ ⟨Z⟩ ⟨(g : Z ⟶ Y)⟩
    ext u
    simp only [Sieve.functor_obj, Sieve.generate_apply, Sieve.functor_map, Quiver.Hom.unop_op',
      TypeCat.Fun.toFun_apply, comp_apply, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
      ← heq s (g ≫ Sieve.ofArrows.h u.2)
      (Sieve.ofArrows.h <| Sieve.downward_closed _ u.2 g) (by simp)]
    exact ConcreteCategory.congr_hom ((s.inj _).hom.naturality g.op) _
  · ext : 1
    let u (j : ι) : CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows _ c.inj).functor :=
      (Sieve.ofArrows _ c.inj).toFunctor (c.inj j) (Sieve.ofArrows_mk _ _ j)
    have (j : ι) : u j ≫ (Sieve.ofArrows _ c.inj).functorInclusion =
      CategoryTheory.yoneda.map (c.inj j) := rfl
    dsimp
    simp only [← this, Category.assoc, Presieve.IsSheafFor.functorInclusion_comp_extend]
    ext Z (g : Z.unop ⟶ X j)
    have h : Sieve.ofArrows X c.inj (g ≫ c.inj j) :=
      Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ j) _
    exact heq s (Sieve.ofArrows.h h) g (by simp)
  · ext : 1
    dsimp
    apply Presieve.IsSheafFor.unique_extend
    ext Y ⟨g, hg⟩
    simp [← hm (Sieve.ofArrows.i hg)]

Goal state after:
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
by_cases hb' : j ≤ b

Goal state after:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : ¬j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
k₁ k₂ : ↑(Set.Iio i)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
simpa using leOfHom φ

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
k₁ k₂ : ↑(Set.Iic i)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
simpa using leOfHom φ

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
⊢ functorMapSrc f τ ≫ functorObjTop f πY = functorObjTop f πX ≫ Arrow.Hom.left τ

Tactic:
by
  ext ⟨i, t, b, w⟩
  simp [ι_functorMapSrc_assoc f τ i t b w _ rfl]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
hc : IsColimit c
x✝ : ↑(Set.Iio j)
i : J
hi : i ∈ Set.Iio j
⊢ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv = (ofCoconeObjIso c i ⋯).inv ≫ (ofCocone c).map (homOfLE ⋯)

Tactic:
ofCocone_map_to_top _ _ hi,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
hc : IsColimit c
x✝ : ↑(Set.Iio j)
i : J
hi : i ∈ Set.Iio j
⊢ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv =
    (ofCoconeObjIso c i ⋯).inv ≫ (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv
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
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts (hf.F.map (homOfLE ⋯))
⊢ (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤ monomorphisms C

Tactic:
simp only [pushouts_le_iff, coproducts_le_iff]

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
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts (hf.F.map (homOfLE ⋯))
⊢ generatingMonomorphisms G ≤ monomorphisms C
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 κ
⊢ I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
rw [llp_rlp_of_isCardinalForSmallObjectArgument' I κ]

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 κ
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y✝ : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
y : ℚ_[p]
hy : ‖y‖ ≤ 1
⊢ dist ⟨x, hx⟩ ⟨y, hy⟩ = ‖-⟨x, hx⟩ + ⟨y, hy⟩‖

Tactic:
exact dist_eq_norm_neg_add x y

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

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

Tactic:
by
  rw [norm_def, coe_intCast, Padic.norm_intCast_lt_one_iff]

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

Goal state before:
pp: X : Scheme
⊢ IsGrothendieckAbelian.{u + 1, u + 1, u + 2} (Sheaf (ProEt.topology X) Ab)

Tactic:
by
  -- Without this, lean starts searching for `EssentiallySmall.{max (u + 1) ?v}` and fails.
  have : EssentiallySmall.{u + 1} X.ProEt := inferInstance
  exact Sheaf.isGrothendieckAbelian_of_essentiallySmall (ProEt.topology X) Ab.{u + 1}

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

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑f j) < ε

Tactic:
intro n hn

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f n) < ε
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
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
X : C
ι : Type u_1
inst✝ : Small.{w, 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
Φ : P.FullSubcategory
x : Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)
⊢ ∃ a, (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)))) a = x

Tactic:
obtain ⟨x, rfl⟩ := (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm.surjective x

Goal state after:
case refine_2
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
X : C
ι : Type u_1
inst✝ : Small.{w, 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
Φ : P.FullSubcategory
x : Φ.obj.fiber.obj X
⊢ ∃ a,
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)))) a =
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm x