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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f + g) * h = f * h + g * h

Tactic:
simp only [mul_def]
    refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
      simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

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

Goal state before:
pp: R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rcases le_total x y with h | h

Goal state after:
case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ (x + y) ^ n = x ^ n + y ^ n

case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : ↥U) → T ↑x
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
x : ↥V
⊢ ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)

Tactic:
by
    specialize w (i x)
    rcases w with ⟨V', m', i', p⟩
    exact ⟨V ⊓ V', ⟨x.2, m'⟩, V.infLELeft _, P.res (V.infLERight V') _ p⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c

Tactic:
· ext
    -- Porting note: was one liner
    -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
    rw [NatTrans.comp_app, sheafedSpaceMap_hom_c_app, Functor.whiskerRight_app, eqToHom_refl]
    erw [(sheafedSpaceObj T).presheaf.map_id]
    dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
    rw [comap_comp]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          U p hp))
      s =
    y
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
change PrimeSpectrum.basicOpen r ≤ U at hrU

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          U p hp))
      s =
    y
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ x ∈ basicOpen g' ⊓ basicOpen g

pp: case refine_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ basicOpen g' ⊓ basicOpen g ≤ U

pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩

Tactic:
· exact ⟨hxg', (hfg ⟨x, hxV⟩).1⟩

Goal state after:
case refine_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ basicOpen g' ⊓ basicOpen g ≤ U

case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝¹ x✝ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
⊢ (x✝¹ * x✝) ≫ (forget₂ TopCommRingCat TopCat).map φ =
    x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ * x✝ ≫ (forget₂ TopCommRingCat TopCat).map φ

Tactic:
ext; exact φ.1.map_mul _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ ↑(const (g i • f j) (g i * g j) (basicOpen (g i * g j)) ⋯) a =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ⋯).op))
          (const (f j) (g j) (basicOpen (g j)) ⋯))
      a

Tactic:
exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]; ring_nf⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsUnit ((ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r)

Tactic:
convert!
    (X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
      (X.toRingedSpace.isUnit_res_basicOpen r)

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (X.toRingedSpace.presheaf.map (homOfLE ⋯).op)) r)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)

Tactic:
refine .paste_horiz (v₁₂ := iY.resLE _ _
    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_

Goal state after:
case refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (Y.homOfLE ⋯) (resLE iY UT UY ⋯) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (T.homOfLE hUST)

case refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)
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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
have := IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
        (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ x, x.2⟩

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : IsUnit ((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
⊢ s ∈ I

Tactic:
refine Submodule.mem_of_localization_maximal
      (fun P hP ↦ X.presheaf.stalk (hU.fromSpec ⟨P, hP.isPrime⟩))
      (fun P hP ↦ Algebra.linearMap _ _) _ _ ?_

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
⊢ ∀ (P : Ideal ↑Γ(X, U)) [inst : P.IsMaximal],
    (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
      Submodule.localized₀ P.primeCompl
        (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.ι i))

Tactic:
intro x y h

Goal state after:
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
⊢ x = y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = U.ι ⁻¹ᵁ X.basicOpen r

Tactic:
by
  dsimp [toSpecΓ]
  simp only [Scheme.toSpecΓ_preimage_basicOpen, preimage_basicOpen, ι_app, homOfLE_leOfHom]
  rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.ι_preimage_self.symm).op,
    ← ConcreteCategory.comp_apply]
  congr 3
  simp [← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ Function.Injective ⇑(fromGlued 𝒰)

Tactic:
intro x y h

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y : ↥(gluedCover 𝒰).glued
h : (fromGlued 𝒰) x = (fromGlued 𝒰) y
⊢ x = y
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) = snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)

Tactic:
← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ map (fst f (𝒰.f i) ≫ f)
      (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd _ _) (𝟙 _) (𝟙 _) (by simp) (by simp))

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))).hom ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯) ≫
      fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) =
    ((pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))).hom ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯) ≫
      snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ ∃ (eq :
    op
        ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
          (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U)))))) =
      (Opens.map (D.f j k).base).op.obj (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U)))),
    D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
      (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
        invApp (pullback.snd (D.f j i) (D.f j k))
            (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U))))) ≫
          (D.V (j, k)).presheaf.map (eqToHom eq)

Tactic:
constructor
  · delta opensImagePreimageMap
    simp_rw [Category.assoc]
    rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]
    · erw [← (D.V (j, k)).presheaf.map_comp]
      · simp_rw [← Category.assoc]
        erw [← comp_c_app, ← comp_c_app]
        · simp_rw [Category.assoc]
          dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
          rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
          congr

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
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f j ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f j ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, PreZeroHypercover.pullback₁_f]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ coprod.inl ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inl ≫ coprodSpec ↑R ↑S

Tactic:
rw [coprodComparison_inl_assoc, coprodSpec, coprod.inl_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inl,
        limit.isoLimitCone_inv_π]

Goal state after:
case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.left }) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ (i : (Scheme.Cover.ulift 𝒰).I₀), P (f ∣_ Scheme.Hom.opensRange ((Scheme.Cover.ulift 𝒰).f i))

Tactic:
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Injective)

Tactic:
refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s)
    fun f ι U H _ hf x₁ x₂ e ↦ ?_

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
α✝ β✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β✝
f : α✝ → β✝
ι : Type u_1
U : ι → Opens β✝
H : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hf : ∀ (i : ι), Function.Injective ((U i).carrier.restrictPreimage f)
x₁ x₂ : α✝
e : f x₁ = f x₂
⊢ x₁ = x₂
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X : Scheme
U : X.Opens
hU : Dense ↑U
⊢ DenseRange ⇑U.ι

Tactic:
by simpa [DenseRange] using hU

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
hf : Q.diagonal (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso X.affineCover (inv (pullback.fst f (𝟙 Y)))
⊢ P.diagonal f

Tactic:
have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this✝ : Q.IsLocal := isLocal_affineProperty P
hf : Q.diagonal (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso X.affineCover (inv (pullback.fst f (𝟙 Y)))
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ P.diagonal f
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
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)
⊢ ⊤ ≤
    Ideal.span
      (Set.range fun x ↦
        match x with
        | (a, b) => g ↑a * ↑b)

Tactic:
← hsgone,

Goal state after:
case refine_1
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)
⊢ Ideal.span ↑sg ≤
    Ideal.span
      (Set.range fun x ↦
        match x with
        | (a, b) => g ↑a * ↑b)
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)
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)
this :
  (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)
⊢ IsLocalization (Submonoid.map g' (Submonoid.powers ↑a))
    (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))

Tactic:
exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val

Goal state after: