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

Goal state before:

Tactic:
(single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [h]

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

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (x.sum fun a b ↦ y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)) =
    ((mapDomain ⇑f) x).sum fun a₁ b₁ ↦ ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
sum_mapDomain_index (by simp) (by simp [add_mul, single_add, sum_add])

Goal state after:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (x.sum fun a b ↦ y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)) =
    x.sum fun a m ↦ ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (f a * a₂) (m * f a • b₂)
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
g : X ⟶ Y
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h : { hom := { base := f, c := fc } }.hom.base = g.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g.hom x
⊢ { hom := { base := f, c := fc } } = g

Tactic:
obtain ⟨g, gc⟩ := g

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
g : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
gc : Y.presheaf ⟶ (pushforward C g).obj X.presheaf
h : { hom := { base := f, c := fc } }.hom.base = { hom := { base := g, c := gc } }.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x
⊢ { hom := { base := f, c := fc } } = { hom := { base := g, c := gc } }
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : (g₁ ≫ X.ofRestrict hf).base = (g₂ ≫ X.ofRestrict hf).base
⊢ g₁.base = g₂.base

Tactic:
simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base ≫ f = g₂.base ≫ f
⊢ g₁.base = g₂.base
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.snd f g) = ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
rw [← show _ = (pullback.snd f g).base from
    PreservesPullback.iso_hom_snd Scheme.forgetToTop f g, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.fst f.base g.base)]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
  · erw [TopCat.pullback_snd_image_fst_preimage]
    rw [Set.image_univ]
    rfl
  rw [← TopCat.epi_iff_surjective]
  infer_instance

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

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
H : ∃ i, s i ∉ x.asIdeal
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose))))))

Tactic:
let i := H.choose

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
H : ∃ i, s i ∉ x.asIdeal
i : ι := H.choose
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose))))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd =
    {
        toHom :=
          PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
        prop := ⋯ } ≫
      (pullbackConeOfLeft f g).snd

Tactic:
exact h₂.trans <| LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 <|
          PullbackCone.mk s.fst.1 s.snd.1 <| congr_arg
            LocallyRingedSpace.Hom.toHom s.condition).symm

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)

Goal state after:
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 (forgetToSheafedSpace.map (pullback.snd f g))
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯) =
    CommRingCat.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)

Tactic:
delta CommRingCat.ofHom CommRingCat.of Bundled.of

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯) =
    ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
delta pullbackRestrictIsoRestrict; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
delta pullbackRestrictIsoRestrict; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
← comp_preimage,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = (V.ι ≫ f) ⁻¹ᵁ U.ι ''ᵁ O
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯ ≫
      pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ =
    𝟙 (pullback (equalizer.ι f g) (pullback.fst s v))

Tactic:
ext <;> simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) =
    (equalizerPullbackMapIso hf hg (𝒰.f i)).inv ≫
      equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
        (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)

Tactic:
ext <;> simp [pullback.condition]

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
a : M
b : R
hb : U ≤ basicOpen b
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f U V hUV) (const a b U hb)) x✝ = ↑(const (f a) (σ b) V ⋯) x✝

Tactic:
by simp [comapₗ, comapFun]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ ↑((comap f U V hUV) (const a b U hb)) p = ↑(const (f a) (f b) V ⋯) p

Tactic:
rw [comap_apply, const_apply, const_apply]
    convert_to! Localization.localRingHom _ _ _ _ (Localization.mk _ _) = Localization.mk _ _
    simp [Localization.mk_eq_mk']

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
      (imageBasicOpen f g U s).carrier)

Tactic:
← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom
    g.toShHom)).isOpen_preimage,

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(TopCat.homeoOfIso
          (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g))) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_2
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
⊢ (∃ I, s = X.zeroLocus ↑I) → IsClosed s

Tactic:
· rintro ⟨I, rfl⟩
    exact zeroLocus_isClosed X I.carrier

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
⊢ U ≤ Scheme.Hom.opensRange (Sigma.ι g j) → U ≤ ⊥

Tactic:
hU'

Goal state after:
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
⊢ U ≤ ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inr_inr_coprodMap f g).flip.isoPullback.hom]
    convert! hg
    simp [Scheme.Cover.pullbackHom, coprodOpenCover]

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

Goal state before:
pp: P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q

Tactic:
delta AffineTargetMorphismProperty

Goal state after:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P f'

Tactic:
by
  rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
  exact (P.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)).mp (hf ⟨_, isAffineOpen_opensRange iY⟩)

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.toPreZeroHypercover.1
e : pullback (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)

Tactic:
have : e.hom ≫ pullback.fst _ _ = X.affineCover.pullbackHom (pullback.fst _ _) i := by
    simp [e, Scheme.Cover.pullbackHom]

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.toPreZeroHypercover.1
e : pullback (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
this : e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x✝

Tactic:
exact surjective_iff _

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

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
· intro ⟨s, hsone, hs⟩
    obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone
    exact ⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) =
    Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv

Tactic:
ext1 <;> simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]
  · congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1); simp
  · congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x); simp

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
⊢ Q.diagonal f ↔ P.diagonal f

Tactic:
let := isLocal_affineProperty P
  refine ⟨fun hf ↦ ?_, diagonal_of_diagonal_of_isPullback P .of_id_fst⟩
  rw [← Q.diagonal.cancel_left_of_respectsIso
    (pullback.fst (f := f) (g := 𝟙 Y)), pullback.condition, Category.comp_id] at hf
  let 𝒰 := X.affineCover.pushforwardIso (inv (pullback.fst (f := f) (g := 𝟙 Y)))
  have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
  exact HasAffineProperty.diagonal_of_openCover.{u, u, u} P f (Scheme.coverOfIsIso (𝟙 _))
    (fun _ ↦ 𝒰) (fun _ _ _ ↦ hf _ _)

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
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)
⊢ P ((Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f))

Tactic:
apply hPc _ _ (hsf a.val a.property)

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 := ⋯
a' : Localization.Away ↑b := ⋯
this :
  (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)
⊢ P (Localization.awayMap g' ↑a)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top.a.refine_2
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((X'.isoOfEq ⋯).hom ≫ i₁ ∣_ f ⁻¹ᵁ U i) (i₂ ∣_ U i) (f ∣_ U i)

Tactic:
← (isPullback_morphismRestrict f _).paste_vert_iff

Goal state after:
case of_sSup_eq_top.a.refine_2
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) (((X'.isoOfEq ⋯).hom ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ (f ⁻¹ᵁ U i).ι) (i₂ ∣_ U i ≫ (U i).ι) f

case of_sSup_eq_top.a.refine_2
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i = ((X'.isoOfEq ⋯).hom ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
by
  refine topologically_isZariskiLocalAtTarget P ?_ (fun f _ U hU hU' ↦ (hP f U hU hU').mpr)
  introv hf hs H
  refine (hP f (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ?_ hf).mp H ⟨1⟩
  rw [IsOpenCover, ← top_le_iff]
  exact le_iSup (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ⟨0⟩

Goal state after: