mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case h_option
R : Type u_1
inst✝² : CommRing R
σ : Type u_3
inst✝¹ : Finite σ
α✝ : Type u_3
inst✝ : Fintype α✝
IH : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim R + ↑(Nat.card (Option α✝)) ≤ ringKrullDim (MvPolynomial (Option α✝) R)

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]
    exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ ord R (x ^ (n + 1)) = (n + 1) • ord R x

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ ord R (x ^ n * x) = (n + 1) • ord R x
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (conjugateEquiv adj ((Adjunction.id a).comp adj')) ((λ_ l').hom ≫ φ) = (conjugateEquiv adj adj') φ ≫ (ρ_ r').inv

Tactic:
simp only [conjugateEquiv_apply, mateEquiv_id_comp_right,
    id_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc]
  bicategory

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩

Tactic:
num_smul

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk (n • ↑x✝.num) ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (Quotient.mk'' y1 + Quotient.mk'' y2).val = val (Quotient.mk'' y1) + val (Quotient.mk'' y2)

Tactic:
rw [← mk_add, val_mk, val_mk, val_mk, Localization.add_mk]; 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 - 1 + 1) * (↑z.den * ↑y.num) = c ^ (m - 1 + 1) * (↑y.den * ↑z.num)

Tactic:
pow_succ,

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 - 1) * c * (↑z.den * ↑y.num) = c ^ (m - 1) * c * (↑y.den * ↑z.num)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ (pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯).inv ≫ fst ((affineOpenCover 𝒜).openCover.f i) ((affineOpenCover 𝒜).openCover.f j) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)

Tactic:
erw [pullbackAwayιIso_inv_fst]

Goal state after:
case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯)) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)
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, f ^ n • t = 0

Tactic:
have (i : ι) : ∃ (n : ℕ), M.presheaf.map (homOfLE (hgle i)).op (f ^ n • t) = 0 := by
      have := (h₁ i).uniqueness (f * g i) (basicOpen_mul_le_right f (g i))
        (M.presheaf.map (homOfLE (hgle i)).op t) ?_
      · obtain ⟨n, hn⟩ := this
        use n
        rw [mul_pow, mul_comm, mul_smul, ← Scheme.Modules.map_smul_Spec] at hn
        exact ((M.isSMulRegular_of_le_basicOpen le_rfl).pow n).right_eq_zero_of_smul hn
      · rw [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp,
          ← homOfLE_comp ((basicOpen_mul_le_left f (g i))) hf, op_comp, M.presheaf.map_comp_apply]
        simp [hs]
    choose n hn using this
    use ⨆ i, n i
    apply TopCat.Sheaf.eq_of_locally_eq' ⟨_, M.isSheaf⟩ (fun i ↦ basicOpen (g i)) _
      (fun i ↦ homOfLE (by rw [hg]; exact le_iSup_of_le _ le_rfl))
    · simp [hg]
    · intro i
      have : n i ≤ ⨆ i, n i := le_ciSup (Finite.bddAbove_range _) _
      have : ⨆ i, n i = ((⨆ i, n i) - n i) + n i := by lia
      rw [this, pow_add, mul_smul, Scheme.Modules.map_smul_Spec, hn i]
      simp

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.IsLocallySurjective J f
X : C
x : Φ.fiber.obj X
z : ToType (Q.obj (op X))
⊢ ∃ a, (ConcreteCategory.hom (Φ.presheafFiber.map f)) a = (ConcreteCategory.hom (Φ.toPresheafFiber X x Q)) z

Tactic:
obtain ⟨Y, g, ⟨t, ht⟩, y, rfl⟩ := Φ.jointly_surjective _ (Presheaf.imageSieve_mem J f z) x

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.IsLocallySurjective J f
X : C
z : ToType (Q.obj (op X))
Y : C
g : Y ⟶ unop (op X)
t : ToType (P.obj (op Y))
ht : (ConcreteCategory.hom (f.app (op Y))) t = (ConcreteCategory.hom (Q.map g.op)) z
y : Φ.fiber.obj Y
⊢ ∃ a,
    (ConcreteCategory.hom (Φ.presheafFiber.map f)) a =
      (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) Q)) z
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).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ liftAux hG₀ s j ≫ G.map (F.map e).op = s.ι a ≫ G.map (F.map d ≫ F.map b ≫ (data a.Y).f i).op

Tactic:
liftAux_fac _ _ _ he

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)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ s.ι { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he } = s.ι a ≫ G.map (F.map d ≫ F.map b ≫ (data a.Y).f i).op
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
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
⊢ res data G₀ h₁ = res data G₀ h₂

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F h₁.q)
      (IsDenseSubsite.imageSieve_mem J₀ J F h₂.q)⟩ _ _ ?_

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
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve h₁.q ⊓ F.imageSieve h₂.q, ⋯⟩),
    res data G₀ h₁ ≫ G₀.obj.map I.f.op = res data G₀ h₂ ≫ G₀.obj.map I.f.op
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
⊢ (presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha)) ≫
      G₀.obj.map p₁.op =
    (presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hb)) ≫
      G₀.obj.map p₂.op

Tactic:
rw [assoc, assoc, IsDenseSubsite.mapPreimage_comp_map,
          IsDenseSubsite.mapPreimage_comp_map,
          ← restriction_eq_of_fac data G₀ (F.map (p₁ ≫ a))
            (F.map p₁ ≫ Sieve.ofArrows.h ha) (by rw [assoc, ha', map_comp]),
          restriction_eq_of_fac data G₀ (F.map (p₁ ≫ a))
            (F.map p₂ ≫ Sieve.ofArrows.h hb) (by rw [assoc, hb', fac, map_comp])]

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

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)

Tactic:
rw [isSheaf_iff_isSheaf_of_type, Scheme.fpqcTopology_eq_propQCTopology,
    isSheaf_type_propQCTopology_iff]

Goal state after:
T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.zariskiTopology (continuousMapPresheaf T) ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (continuousMapPresheaf T) (Presieve.singleton (Spec.map f))
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: case refine_2
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 }
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
use 𝒱.presieve₀

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 := ⋯
⊢ Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
s : Subobject X
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ s
⊢ Subobject.mk f ≤ s

Tactic:
induction s using Subobject.ind with | _ g
     =>  _ 

Goal state after:
case a.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
⊢ Subobject.mk f ≤ Subobject.mk g
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
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
i : J
hij : i < j
⊢ (SqStruct.map (lift hj s) (homOfLE ⋯)).f' = (↑s (Opposite.op ⟨i, hij⟩)).f'

Tactic:
apply liftHom_fac

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✝ : F.Additive
Y : D
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
⊢ ((G ⋙ preadditiveYoneda ⋙ (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj Y).map
        g ≫
      (AddEquiv.ulift.trans ((adj.homAddEquiv (unop Y✝) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso.hom =
    (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X✝) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso.hom ≫
      ((preadditiveYoneda ⋙
                (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                  (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
            Y).map
        g

Tactic:
ext ⟨y⟩

Goal state after:
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✝ : F.Additive
Y : D
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
y : ↑((preadditiveYoneda.obj (G.obj Y)).obj X✝)
⊢ (AddCommGrpCat.Hom.hom
        (((G ⋙ preadditiveYoneda ⋙ (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                Y).map
            g ≫
          (AddEquiv.ulift.trans ((adj.homAddEquiv (unop Y✝) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso.hom))
      { down := y } =
    (AddCommGrpCat.Hom.hom
        ((AddEquiv.ulift.trans ((adj.homAddEquiv (unop X✝) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso.hom ≫
          ((preadditiveYoneda ⋙
                    (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                      (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                Y).map
            g))
      { down := y }
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
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom ≫ Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f)) =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
iterationFunctorObjObjRightIso_ιIteration_app_right,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f)).incl.app j =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom
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:
simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h

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
m : J
hm : Order.IsSuccLimit m
this✝ : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ transfiniteIterate (largerSubobject hG) m A₀ = ⨆ j, transfiniteIterate (largerSubobject hG) (↑j) A₀

Tactic:
exact transfiniteIterate_limit (largerSubobject hG) A₀ m hm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
l : (↑⟨Arrow.mk i, hi⟩).right ⟶ (relativeCellComplexιObj I κ f).F.obj (Order.succ j)
hl₁ : i ≫ l = t ≫ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯)
hl₂ : l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f = b
⊢ (l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j)) ≫ πObj I κ f = b

Tactic:
by rw [assoc, hl₂]

Goal state after: