mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case exists_of_eq
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
⊢ ∃ a_1 ∈ Submonoid.powers f,
    a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))

Tactic:
refine ⟨_, ⟨k, rfl⟩, ?_⟩

Goal state after:
case exists_of_eq
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r = (X.isoOfEq ⋯).hom ≫ toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr

Tactic:
← Iso.inv_comp_eq,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ (X.isoOfEq ⋯).inv ≫ fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r = toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))
        ↑x)

Tactic:
Subtype.forall

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop f)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := ⋯
⊢ ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
        ↑x)

Tactic:
Subtype.forall

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop f)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop r))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑x)

Tactic:
Subtype.forall

Goal state after:
case map_unit
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
                    (modulesSpecToSheaf.obj ((𝟭 (Spec (CommRingCat.of ↑R)).Modules).obj N)).obj).obj
                r)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (x : ↥(Submonoid.powers (unop r))),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑x)

Tactic:
Subtype.forall

Goal state after:
case map_unit
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ∀ (a : ↑R) (b : a ∈ Submonoid.powers (unop r)),
    IsUnit
      ((algebraMap (↑R)
          (Module.End ↑R
            ↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r)))
        ↑⟨a, b⟩)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case exists_of_eq
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) := ⋯
⊢ ∀ {x_1 y : A⁰_ f},
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) x_1 =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y →
      ∃ c, ↑c * x_1 = ↑c * y

Tactic:
intro y

Goal state after:
case exists_of_eq
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 : A⁰_ f
⊢ ∀ {y_1 : A⁰_ f},
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y =
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y_1 →
      ∃ c, ↑c * y = ↑c * y_1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
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 ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)

Tactic:
by
      apply_fun HomogeneousLocalization.val at e
      simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mk, mk_eq_mk',
        IsLocalization.mk'_eq_iff_eq] at e
      obtain ⟨⟨c, hcx⟩, hc⟩ := IsLocalization.exists_of_eq (M := x.1.1.toIdeal.primeCompl) e
      obtain ⟨i, hi⟩ := not_forall.mp ((x.1.1.isHomogeneous.mem_iff _).not.mp hcx)
      refine ⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩
      apply_fun fun x ↦ (decompose 𝒜 x (i + z.deg + y.deg)).1 at hc
      conv_rhs at hc => rw [add_right_comm]
      rwa [← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        ← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        mul_assoc, mul_assoc] at hc
      exacts [y.den.2, z.num.2, z.den.2, y.num.2]

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
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
⊢ ∀ ⦃X : Q.Over ⊤ S⦄ (S_1 : Presieve X) (Ti : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → S_1 f → Presieve Y),
    S_1 ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h} →
      (∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : S_1 f),
          Ti f H ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}) →
        S_1.bind Ti ∈ {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}

Tactic:
rintro X _ T ⟨𝒰, h, p, rfl⟩ H
    choose V h pV hV using H
    let 𝒱j (j : 𝒰.I₀) : (Cover (precoverage P) ((𝒰.X j).asOverProp S (p j)).left) :=
      V ((𝒰.f j).asOverProp S) ⟨j⟩
    refine ⟨𝒰.bind (fun j ↦ 𝒱j j), inferInstance, fun j ↦ pV _ _ _, ?_⟩
    convert!
      Presieve.ofArrows_bind _ (fun j ↦ ((𝒰.f j).asOverProp S)) _
        (fun Y f H j ↦ ((V f H).X j).asOverProp S (pV _ _ _))
        (fun Y f H j ↦ ((V f H).f j).asOverProp S)
    apply hV

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
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
| g ≫ l₂

Tactic:
← pullback.lift_snd 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)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
| g ≫ pullback.lift l₁ l₂ h ≫ pullback.snd f f
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
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ res data G₀ h₁ ≫ G₀.obj.map { Y := Z₀, f := a, hf := ⋯ }.f.op =
    res data G₀ h₂ ≫ G₀.obj.map { Y := Z₀, f := a, hf := ⋯ }.f.op

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, (data X).mem₁₀ h₁.i₀ h₂.i₀ b₁ b₂ (by rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.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
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨(data X).sieve₁₀ b₁ b₂, ⋯⟩),
    (res data G₀ h₁ ≫ G₀.obj.map { Y := Z₀, f := a, hf := ⋯ }.f.op) ≫ G₀.obj.map I.f.op =
      (res data G₀ h₂ ≫ G₀.obj.map { Y := Z₀, f := a, hf := ⋯ }.f.op) ≫ G₀.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

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

Tactic:
change F.map g₁' ≫ _ = F.map g₂' ≫ _

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

Goal state before:
pp: X : Scheme
⊢ Presieve.IsSheaf fpqcTopology (yoneda.obj X)

Tactic:
fpqcTopology_eq_propQCTopology,

Goal state after:
X : Scheme
⊢ Presieve.IsSheaf (propQCTopology @Flat) (yoneda.obj X)
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.zariskiTopology
    (Scheme.forgetToTop.op ⋙ TopCat.uliftFunctor.op ⋙ yoneda.obj (TopCat.of (ULift.{u_1, v} T)))

Tactic:
apply Scheme.forgetToTop.op_comp_isSheaf_of_isSheaf _ TopCat.grothendieckTopology

Goal state after:
T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf TopCat.grothendieckTopology (TopCat.uliftFunctor.op ⋙ yoneda.obj (TopCat.of (ULift.{u_1, v} T)))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
⊢ ∀ (y : (fun X ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
    (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = this.lift x ⋯

Tactic:
intro y

Goal state after:
case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
⊢ (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = this.lift x ⋯
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
this : RepresentablyFlat (Over.forget P ⊤ S)
⊢ CoverPreserving (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck
    (K.toGrothendieck.over S) (Over.forget P ⊤ S)

Tactic:
exact coverPreserving_comap_forget _ H

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

Goal state before:
pp: case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a

Tactic:
first | intro a; exact elim0 a

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

Goal state before:
pp: case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

Tactic:
first | intro a; exact elim0 a

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

Goal state before:
pp: case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b

Tactic:
first | intro a; exact elim0 a

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

Goal state before:
pp: case pred
⊢ Fin 0 → Fin 0

Tactic:
first | intro a; exact elim0 a

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

Goal state before:
pp: case he
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
⊢ ∀ ⦃X Y_1 : C⦄ (f : X ⟶ Y_1) (x : (CategoryTheory.yoneda.obj Y).obj (op Y_1)),
    Equiv.ulift.symm ((ConcreteCategory.hom ((CategoryTheory.yoneda.obj Y).map f.op)) x) =
      (ConcreteCategory.hom ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).map f.op)) (Equiv.ulift.symm x)

Tactic:
intros
      rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
refine ⟨_, _, _, _, _, ?_, c.isPushout⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
⊢ coproducts.{w, v, u} (ofHoms g) c.m
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X

Tactic:
constructor
  · rintro ⟨_⟩
    rfl
  · intro h
    rw [← Φ.prop.arrow_mk_mem_toSet_iff, h]
    apply prop_toSucc

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 X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
⊢ ιFunctorObj f πX ≫ πFunctorObj f πX = πX

Tactic:
simp [ιFunctorObj, πFunctorObj]

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✝ X✝ : C
πX✝ : X✝ ⟶ S✝
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX✝)) C
inst✝² : HasPushout (functorObjTop f πX✝) (functorObjLeft f πX✝)
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
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
b' : B i ⟶ T
hb' : b ≫ Arrow.Hom.right τ = b'
t' : A i ⟶ Y
ht' : t ≫ Arrow.Hom.left τ = t'
⊢ t' ≫ πY = f i ≫ b'

Tactic:
have := τ.w

Goal state after:
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✝)
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
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
b' : B i ⟶ T
hb' : b ≫ Arrow.Hom.right τ = b'
t' : A i ⟶ Y
ht' : t ≫ Arrow.Hom.left τ = t'
this : Arrow.Hom.left τ ≫ (Arrow.mk πY).hom = (Arrow.mk πX).hom ≫ Arrow.Hom.right τ
⊢ t' ≫ πY = f i ≫ b'
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inr
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
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₁₂ : i₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃

Tactic:
· rw [map_id, comp_id]

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
i : J
hi : i < j
⊢ (ofCocone c).map (homOfLE ⋯) = (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv

Tactic:
by
  dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]
  rw [dif_neg (by simp), dif_pos hi, comp_id]

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

Goal state before:
pp: case neg.inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ : J
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h

Tactic:
· rw [map_id, comp_id]

Goal state after:
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 : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hki).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩

Tactic:
rw [← comp_apply, ← map_comp, ← op_comp, homOfLE_comp,
      e.map_limit k hk (hki.trans hij)]
    congr
    ext ⟨l, hl⟩
    dsimp
    rw [← comp_apply, ← map_comp]
    rfl

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

Goal state before:
pp: case e_x
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
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ : e₁.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩
h₂ : e₂.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
l : J
hl : l ∈ Set.Iio i
this : Subsingleton (d.Extension val₀ l)
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val

Tactic:
exact congr_arg val (Subsingleton.elim (e₁.ofLE hl.le) (e₂.ofLE hl.le))

Goal state after: