mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Over.Hom.left
        ((bialgSpec R).map
            (CommBialgCat.ofHom
                ((Bialgebra.TensorProduct.comm ↑R ↑A ↑A).toBialgHom.comp (Bialgebra.comulBialgHom ↑R ↑A))).op).hom =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Over.Hom.left ((bialgSpec R).map (CommBialgCat.ofHom (Bialgebra.comulBialgHom ↑R ↑A)).op).hom
⊢ Over.Hom.left ((β_ ((Spec A).asOver (Spec R)) ((Spec A).asOver (Spec R))).hom ≫ μ) = Over.Hom.left μ

Tactic:
dsimp [commBialgCatEquivComonCommAlgCat] at this ⊢

Goal state after:
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
⊢ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom ≫ Over.Hom.left μ = Over.Hom.left μ
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h i : c ⟶ d
η : h ⟶ i
η₁ : g ≫ h ⟶ g ≫ i
η₂ : f ≫ g ≫ h ⟶ f ≫ g ≫ i
η₃ : f ≫ g ≫ h ⟶ (f ≫ g) ≫ i
η₄ : (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ≫ g) ◁ η = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e_a
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
      map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
      (pullbackSpecIso R S S).hom

Tactic:
rw [← Iso.comp_inv_eq]

Goal state after:
case e_a
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ (map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
        map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
      (pullbackSpecIso R S S).inv =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
g : b ⟶ c
h : c ⟶ d
η : f ⟶ f'
η₁ : f ≫ g ⟶ f' ≫ g
η₂ : (f ≫ g) ≫ h ⟶ (f' ≫ g) ≫ h
η₃ : (f ≫ g) ≫ h ⟶ f' ≫ g ≫ h
η₄ : f ≫ g ≫ h ⟶ f' ≫ g ≫ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ≫ h) = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ V ⊆ ⋃ i ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t), (basicOpen i).carrier

Tactic:
by simpa using ht

Goal state after:
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
⊢ (carrier x).IsPrime

Tactic:
by
  refine Ideal.IsPrime.comap _ (hK := ?_)
  exact IsLocalization.isPrime_of_isPrime_disjoint
    (Submonoid.powers f) _ _ inferInstance
    ((disjoint_powers_iff_notMem_of_isPrime _).mpr x.2)

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

Goal state before:
pp: case refine_1.refine_1
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : TopologicalSpace.Opens ↥↑V
⊢ ((Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).obj W).left =
    (((Opens.overEquivalence V).symm.functor ⋙ Over.map f).obj W).left

Tactic:
suffices U.ι ''ᵁ ((X.homOfLE (leOfHom f)) ''ᵁ W) = V.ι ''ᵁ W by simpa
      simp [← Scheme.Hom.comp_image]

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

Goal state before:
pp: case pos
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ =
    (m + m).choose j •
      (HomogeneousLocalization.mk
            { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
          HomogeneousLocalization.mk
            { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }).val

Tactic:
simp only [HomogeneousLocalization.val_mul,
    HomogeneousLocalization.val_mk, Localization.mk_mul, ← smul_mk]

Goal state after:
case pos
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (m + m).choose j • Localization.mk ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j)) ⟨f ^ (i + i), ⋯⟩ =
    (m + m).choose j •
      Localization.mk ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j) * (proj 𝒜 i) b ^ m) (⟨f ^ i, ⋯⟩ * ⟨f ^ i, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case neg
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ =
    (m + m).choose j •
      (HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
          HomogeneousLocalization.mk
            { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
              den_mem := ⋯ }).val

Tactic:
simp only [HomogeneousLocalization.val_mul,
    HomogeneousLocalization.val_mk, Localization.mk_mul, ← smul_mk]

Goal state after:
case neg
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (m + m).choose j • Localization.mk ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j)) ⟨f ^ (i + i), ⋯⟩ =
    (m + m).choose j •
      Localization.mk ((proj 𝒜 i) a ^ m * ((proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j)))
        (⟨f ^ i, ⋯⟩ * ⟨f ^ i, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
X✝ Y✝ : (Opens ↥(Spec R))ᵒᵖ
i : X✝ ⟶ Y✝
⊢ M.val.map i ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map i))).map
        (ModuleCat.ofHom { toAddHom := (ModuleCat.Hom.hom (f.hom.app Y✝)).toAddHom, map_smul' := ⋯ }) =
    ModuleCat.ofHom { toAddHom := (ModuleCat.Hom.hom (f.hom.app X✝)).toAddHom, map_smul' := ⋯ } ≫ N.val.map i

Tactic:
by ext x; exact congr($(f.1.naturality i).hom x)

Goal state after:
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 : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ (CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv))
      z

Tactic:
apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ («Proj».stalkIso' 𝒜 x) ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z) =
    (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯)).hom' z
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
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
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0

Tactic:
have hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i) := by
            rw [← mul_assoc]
            exact basicOpen_mul_le_left _ _
          have hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j) := by
            rw [mul_comm (g i) (g j), ← mul_assoc]
            exact basicOpen_mul_le_left _ _
          rw [map_sub, ← M.presheaf.map_comp_apply, ← op_comp, ← M.presheaf.map_comp_apply,
            ← op_comp, homOfLE_comp, homOfLE_comp, ← homOfLE_comp hfgigi (hfgi i),
            ← homOfLE_comp hfgigj (hfgi j), op_comp, M.presheaf.map_comp_apply, ← ht i,
            M.map_smul_Spec, ← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp, op_comp,
            M.presheaf.map_comp_apply, ← ht j, M.map_smul_Spec, ← M.presheaf.map_comp_apply,
            ← op_comp, homOfLE_comp]
          simp

Goal state after:
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 𝒜
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    classical
    obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 := by
      by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop
    exact ⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩

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

Goal state before:
pp: case refine_2
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
Y : ↥X.left → Q.Over ⊤ S
f : (x : ↥X.left) → Y x ⟶ X
y : (x : ↥X.left) → ↥(Y x).left
hf : ∀ (x : ↥X.left), R.arrows (f x)
hP : ∀ (x : ↥X.left), P (f x).left
hy : ∀ (x : ↥X.left), (f x).left (y x) = x
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
let 𝒰 : X.left.Cover (precoverage P) :=
      { I₀ := X.left,
        X := fun i ↦ (Y i).left
        f := fun i ↦ (f i).left
        mem₀ := by
          rw [presieve₀_mem_precoverage_iff]
          refine ⟨fun x ↦ ⟨x, y x, hy x⟩, hP⟩ }

Goal state after:
case refine_2
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
Y : ↥X.left → Q.Over ⊤ S
f : (x : ↥X.left) → Y x ⟶ X
y : (x : ↥X.left) → ↥(Y x).left
hf : ∀ (x : ↥X.left), R.arrows (f x)
hP : ∀ (x : ↥X.left), P (f x).left
hy : ∀ (x : ↥X.left), (f x).left (y x) = x
𝒰 : Cover (precoverage P) X.left := { I₀ := ↥X.left, X := fun i ↦ (Y i).left, f := fun i ↦ (f i).left, mem₀ := ⋯ }
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1
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
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t) = 0

Tactic:
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]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
⊢ Over.Hom.left q ≫ ⋯.choose ≫ π ⋯.choose = ⋯.choose ≫ π ⋯.choose

Tactic:
generalize_proofs h1 h2 h3 h4

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
h1 : ∃ a g, g ≫ π a = B.hom
h2 : ∃ g, g ≫ π h1.choose = B.hom
h3 : ∃ a g, g ≫ π a = A.hom
h4 : ∃ g, g ≫ π h3.choose = A.hom
⊢ Over.Hom.left q ≫ h2.choose ≫ π h1.choose = h4.choose ≫ π h3.choose
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

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

Tactic:
rw [← Φ.prop.arrow_mk_mem_toSet_iff, h]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.toSuccArrow X ∈ Φ.prop.toSet
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

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

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:
· dsimp [map]
      obtain hi₃' | rfl := hi₃.lt_or_eq
      · rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
      · rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
          Cocone.w_assoc]

Goal state after:
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₃
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
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'
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapTgt f τ =
    Sigma.ι (functorObjTgtFamily f πY) { i := i, t := t', b := b', w := ⋯ }

Tactic:
subst hb' ht'
  simp [functorMapTgt]

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
⊢ ∀ {X Y : ↑(Set.Iio j)} (f : X ⟶ Y),
    (restrictionLT (ofCocone c) ⋯).map f ≫
        (match Y with
          | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom =
      (match X with
          | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom ≫
        F.map f

Tactic:
by intros; apply ofCoconeObjIso_hom_naturality

Goal state after:
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
hc : IsColimit c
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
h : ⊥ < j
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f

Tactic:
rw [liftHom_fac hj s ⊥ h]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
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
h : ⊥ < j
⊢ (↑s (Opposite.op ⟨⊥, h⟩)).f' = f
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
simpa using transfiniteCompositions_le_llp_rlp.{w} (coproducts.{w} W).pushouts

Goal state after: