mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { coeff := f.coeff + g.coeff }.sum h = f.sum h + g.sum h

Tactic:
exact Finsupp.sum_add_index h_zero h_add

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S₁ k
inst✝¹ : SMulZeroClass S₂ k
inst✝ : SMulCommClass S₁ S₂ k
x✝² : S₁
x✝¹ : S₂
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ x✝² • x✝¹ • { coeff := coeff✝ } = x✝¹ • x✝² • { coeff := coeff✝ }

Tactic:
simp_rw [← ofCoeff_smul, smul_comm]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ trop (∑ i ∈ s, f i) = ∏ i ∈ s, trop (f i)

Tactic:
by
  convert! Multiset.trop_sum (s.val.map f)
  simp only [Multiset.map_map, Function.comp_apply]
  rfl

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a : G
⊢ (of k G) a = single a 1

Tactic:
by
  simp [of, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
Module: Mathlib.Topology.Sheaves.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{v_1, w} J
inst✝ : HasLimitsOfShape J C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
⊢ c.pt.IsSheaf

Tactic:
by
  let F' : J ⥤ Sheaf C X :=
    { obj := fun j => ⟨F.obj j, H j⟩
      map := fun f => ⟨F.map f⟩ }
  let e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents fun _ => Iso.refl _
  exact Presheaf.isSheaf_of_iso
    ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
    (limit F').2

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X).c.app U = X.presheaf.map (𝟙 U)

Tactic:
by
  rw [id_c, map_id]
  rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafOfFunctions

Goal state before:
pp: case refine_2
X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
index : ↥(iSup U) → ι
index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)
s : (x : ↥(iSup U)) → T ↑x := fun x ↦ sf (index x) ⟨↑x, ⋯⟩
⊢ ∀ (y : ToType ((X.presheafToTypes T).obj (Opposite.op (iSup U)))),
    (fun s ↦ (X.presheafToTypes T).IsGluing U sf s) y → y = s

Tactic:
· -- Now we just need to check that the lift we picked was the only possible one.
      -- So we suppose we had some other gluing `t` of our sections
      intro t ht
      -- and observe that we need to check that it agrees with our choice
      -- for each `x ∈ ↑(iSup U)`.
      funext x
      exact congr_fun (ht (index x)) ⟨x.1, index_spec x⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus (↑I * ↑J)

Tactic:
← X.zeroLocus_span (U := U) (↑I * ↑J),

Goal state after:
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus ↑(Ideal.span (↑I * ↑J))
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ precoverage P ≤ precoverage Q

Tactic:
by
  grw [precoverage, precoverage, MorphismProperty.precoverage_monotone h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
right✝ : R ∈ P.precoverage.coverings X
⊢ ∃ Y g, R g ∧ x ∈ Set.range ⇑g

Tactic:
jointlySurjectivePrecoverage,

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : R ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings X
right✝ : R ∈ P.precoverage.coverings X
⊢ ∃ Y g, R g ∧ x ∈ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv = Scheme.Hom.app f U

Tactic:
simp [Scheme.Hom.appLE_eq_app]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := LocallyRingedSpace.forgetToSheafedSpace)
  apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := SheafedSpace.forgetToPresheafedSpace)
  erw [← PreservesPullback.iso_hom_snd
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]
  -- Porting note: was `inferInstance`
  exact IsIso.comp_isIso' inferInstance <|
    PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha✝ : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
W : Opens ↑(PrimeSpectrum.Top R)
hxW : ↑x ∈ W
hWU : W ⟶ U
ax : M
as : R
ha : ∀ (x : ↥W), ∃ (hs : as ∉ (↑x).asIdeal), (fun x ↦ a (hWU x)) x = LocalizedModule.mk ax ⟨as, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
refine ⟨V ⊓ W, ⟨hxV, hxW⟩, homOfLE (inf_le_left.trans hVU.le), rx • ax, as * rs, fun y ↦ ?_⟩

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha✝ : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
W : Opens ↑(PrimeSpectrum.Top R)
hxW : ↑x ∈ W
hWU : W ⟶ U
ax : M
as : R
ha : ∀ (x : ↥W), ∃ (hs : as ∉ (↑x).asIdeal), (fun x ↦ a (hWU x)) x = LocalizedModule.mk ax ⟨as, hs⟩
y : ↥(V ⊓ W)
⊢ ∃ (hs : as * rs ∉ (↑y).asIdeal), (fun x ↦ (r • a) ((homOfLE ⋯) x)) y = LocalizedModule.mk (rx • ax) ⟨as * rs, hs⟩
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
⊢ r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((ConcreteCategory.hom (X.presheaf.Γgerm x)) r)

Tactic:
simp [toΓSpecFun, IsLocalRing.closedPoint]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = Set.range ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i)))

Tactic:
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_I₀, Equiv.refl_apply, PreZeroHypercover.pullback₁_X]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = Set.range ⇑(pullback.snd U.ι (𝒰.f i))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    x ∈ p.asIdeal

Tactic:
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff ((structureSheaf R).presheaf.stalk p)
        p.asIdeal x]

Goal state after:
case w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    (algebraMap ↑R ↑((structureSheaf ↑R).presheaf.stalk p)) x ∈
      IsLocalRing.maximalIdeal ↑((structureSheaf ↑R).presheaf.stalk p)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ IsLocalizedModule x.asIdeal.primeCompl (toStalkₗ R M x)

Tactic:
by
  convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ' R M x).hom
      (modulePresheafStalkIso R M x).symm
  ext m
  let α : TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
    (forget₂ _ _).obj ((structurePresheafInModuleCat R M).stalk x) :=
    Limits.colimit.isoColimitCocone ⟨_, Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
    (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
      structurePresheafInModuleCat R M))⟩
  refine α.addCommGroupIsoToAddEquiv.eq_symm_apply.mpr ?_
  change α.hom _ = _
  have : TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf ⊤ x (by simp) ≫ α.hom =
      (forget₂ _ _).map ((structurePresheafInModuleCat R M).germ ⊤ x (by simp)) :=
    Limits.colimit.isoColimitCocone_ι_hom (C := Ab) ..
  exact congr($this _)

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
clear_value z

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k))
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ?m.92 ∈ ↑(U i)
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X

Tactic:
dsimp [coprodZeroIso, binaryCofanZeroRight]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫
      (colimit.isoColimitCocone
          { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X }).hom =
    𝟙 X
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) ''
      ↑((↑(TopCat.Hom.frameHom (pullback.fst (D.f i j) (D.f i k)).base)).toFunctor.1 U) =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹'
      ↑{ carrier := ⇑(ConcreteCategory.hom (D.f i j).base) '' ↑U, is_open' := ⋯ }

Tactic:
apply pullback_base

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
gluedLiftPullbackMap_fst_assoc,

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec

Tactic:
have : IsEmpty (Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ)) :=
    @Function.isEmpty _ _ spec_punit_isEmpty (Scheme.Spec.mapIso
      (initialIsoIsInitial (initialOpOfTerminal CommRingCat.punitIsTerminal))).hom
  have := preservesInitial_of_iso Scheme.Spec (asIso (initial.to _))
  exact preservesColimitsOfShape_pempty_of_preservesInitial _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ Arrow.mk (pullback.diagonal f ∣_ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩)) ≅
    Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))

Tactic:
refine (morphismRestrictOpensRange _ _).trans ?_

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩)) ≅
    Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x✝ :
  (MultispanShape.prod
      (Cover.ulift
              (Opens.iSupOpenCover fun i_1 ↦
                Hom.opensRange (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk : k ∈ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← CategoryTheory.GlueData.ι, reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        ← cancel_epi (Hom.isoOpensRange (F.map _)).hom.toLRSHom]

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x✝ :
  (MultispanShape.prod
      (Cover.ulift
              (Opens.iSupOpenCover fun i_1 ↦
                Hom.opensRange (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk : k ∈ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
⊢ 1 ∈ Ideal.span (Set.range fun a ↦ ↑a)

Tactic:
simp [hsfone]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
⊢ P
    ((algebraMap T
          ((fun x ↦
              match x with
              | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
            (a, b))).comp
      (g.comp f))

Tactic:
let a' := (algebraMap T (Localization.Away b.val)) (g a.val)

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
⊢ P
    ((algebraMap T
          ((fun x ↦
              match x with
              | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
            (a, b))).comp
      (g.comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case restrict
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥↑U
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U.ι ≫ f) x))

Tactic:
Scheme.Hom.stalkMap_comp,

Goal state after:
case restrict
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥↑U
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (U.ι x) ≫ Scheme.Hom.stalkMap U.ι x))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : SurjectiveOnStalks (Spec.map ψ)
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ IsEmbedding (L ∘ ⇑(pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂))

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks)] at H

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ IsEmbedding (L ∘ ⇑(pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂))