mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ : HVertexOperator Γ R V W
⊢ ∀ ⦃a₂ : HVertexOperator Γ R V W⦄, coeff a₁✝ = coeff a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ a₂✝ : HVertexOperator Γ R V W
⊢ coeff a₁✝ = coeff a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
g : Lex (Γ' × Γ)
⊢ ((of R).symm ((of R) (A.compHahnSeries B (u + v)).ofIterate)).coeff g =
    ((of R).symm ((of R) (A.compHahnSeries B u).ofIterate + (of R) (A.compHahnSeries B v).ofIterate)).coeff g

Tactic:
simp [HahnSeries.ofIterate]

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
x : U
g : Lex (Γ' × Γ)
⊢ ((of R).symm ((of R) (A.compHahnSeries B (r • x)).ofIterate)).coeff g =
    ((of R).symm ((RingHom.id R) r • (of R) (A.compHahnSeries B x).ofIterate)).coeff g

Tactic:
simp [HahnSeries.ofIterate]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
⊢ i ∈ s → IsClosed (↑(X.basicOpen i))ᶜ

Tactic:
_

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsClosed (↑(X.basicOpen i))ᶜ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
⊢ b ≤ x → x ≤ b

Tactic:
_

Goal state after:
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
⊢ x ≤ b
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
i : ι
j : σ i
z : Y i j
⊢ ∃ i_1,
    (ConcreteCategory.hom (f i)) ((ConcreteCategory.hom (g i j)) z) ∈
      Set.range ⇑(ConcreteCategory.hom (g i_1.fst i_1.snd ≫ f i_1.fst))

Tactic:
use ⟨i, j⟩, z

Goal state after:
case h
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
i : ι
j : σ i
z : Y i j
⊢ (ConcreteCategory.hom (g ⟨i, j⟩.fst ⟨i, j⟩.snd ≫ f ⟨i, j⟩.fst)) z =
    (ConcreteCategory.hom (f i)) ((ConcreteCategory.hom (g i j)) z)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  (Presieve.ofArrows (fun i ↦ F.obj (X i)) fun i ↦ F.map (f i)) ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj S)
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ (Presieve.ofArrows (fun i ↦ F.obj (P i)) fun i ↦ F.map (p₁ i)) ∈
    Types.jointlySurjectivePrecoverage.coverings (F.obj Y)

Tactic:
Types.ofArrows_mem_jointlySurjectivePrecoverage_iff

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ∀ (x : (fun X ↦ X) (F.obj Y)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
⊢ ∀ [inst : HasPullback f g], Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))

Tactic:
_

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
⊢ Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
⊢ m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s

Tactic:
_

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
⊢ m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X✝ ⟶ Y), MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Scheme
⊢ ∀ (f : X✝ ⟶ Y✝), MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ [inst : HasPullback f g], IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι F i).hom.base)

Tactic:
rw [← show _ = (colimit.ι F i).hom.base from
    ι_preservesColimitIso_inv (SheafedSpace.forget C) F i]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv))
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
⊢ m ≫ (pullbackConeOfLeft f g).fst = s.fst →
    m ≫ (pullbackConeOfLeft f g).snd = s.snd →
      m =
        {
          toHom :=
            PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
              (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
          prop := ⋯ }

Tactic:
_

Goal state after:
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
⊢ m ≫ (pullbackConeOfLeft f g).snd = s.snd →
    m =
      {
        toHom :=
          PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
        prop := ⋯ }
Module: Mathlib.Topology.Sheaves.CommRingCat

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

Tactic:
ext; exact φ.1.map_one

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W = V.ι ''ᵁ W ⊓ U

Tactic:
by
  ext x
  constructor
  · rintro ⟨⟨y, hyU⟩, hyW, rfl⟩
    exact ⟨⟨⟨y, e hyU⟩, by simpa [homOfLE_apply'] using hyW, rfl⟩, hyU⟩
  · rintro ⟨⟨y, hyW, rfl⟩, hyU⟩
    exact ⟨⟨y.1, hyU⟩, by simpa [homOfLE_apply'] using hyW, rfl⟩

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
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u : ↥(↑⟨p, hfp⟩).asIdeal.primeCompl
hu : u • ⟨↑d, ⋯⟩ • a = u • ⟨↑b, ⋯⟩ • c
⊢ ↑u ∈ ↑(⊥.colon {d • a - b • c})

Tactic:
simpa [sub_eq_zero, smul_sub]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ Hom.appTop (X.homOfLE ⋯) ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i

Tactic:
X.homOfLE_appTop,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι) = Set.range ⇑U.ι

Tactic:
by
    have : V.ι ''ᵁ (V.ι ⁻¹ᵁ U) = U := by simpa [Scheme.Hom.image_preimage_eq_opensRange_inf]
    rw [Scheme.Hom.comp_base, TopCat.coe_comp, Scheme.Opens.range_ι, Set.range_comp, ← this]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ (TopCat.Hom.hom (Spec.locallyRingedSpaceMap (f.c.app (op ⊤))).base) ((TopCat.Hom.hom X.toΓSpec.base) x) =
    (TopCat.Hom.hom Y.toΓSpec.base) ((TopCat.Hom.hom f.base) x)

Tactic:
change PrimeSpectrum.comap (f.c.app (op ⊤)).hom (X.toΓSpecFun x) = Y.toΓSpecFun (f.base x)

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤))) (X.toΓSpecFun x) =
    Y.toΓSpecFun ((ConcreteCategory.hom f.base) x)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (localizationtoStalkₗ R M x)) (LocalizedModule.mk f s) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯)) (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
apply ((Module.End.isUnit_iff _).mp (isUnit_toStalkₗ' _ s.1 s.2)).1 ?_

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) ↑s)
      ((ConcreteCategory.hom (localizationtoStalkₗ R M x)) (LocalizedModule.mk f s)) =
    ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) ↑s)
      ((ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2
  rw [IsAffineOpen.fromSpec, Scheme.Hom.comp_app, Scheme.Opens.ι_app, Scheme.Hom.app_eq _ this,
    ← Scheme.Hom.appTop, IsAffineOpen.isoSpec_inv_appTop]
  simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom,
    Category.assoc, ← X.presheaf.map_comp_assoc]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U = ⇑hU.fromSpec '' Set.univ

Tactic:
convert! hU.range_fromSpec.symm

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ⇑hU.fromSpec '' Set.univ = Set.range ⇑hU.fromSpec
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basicOpen_le ⟨x, hf₂⟩ hx.2

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
⊢ ⇑(hom s.π) ∘ ⇑(hom f) = ⇑(hom s.π) ∘ ⇑(hom g)

Tactic:
ext x; exact ConcreteCategory.congr_hom s.condition x

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
x : ↑Γ(X, U)
⊢ x ∈ s → ↑(X.basicOpen x) ⊆ ↑U

Tactic:
_

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ ↑(X.basicOpen x) ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier

Tactic:
refine ⟨fun h => by rw [h], ?_⟩
      intro h
      apply_fun Set.image hU.fromSpec at h
      rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
        at h
      simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
      ext1
      refine Set.Subset.antisymm ?_ h
      simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
      intro x _
      exact X.basicOpen_le x

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
x : ↑Γ(X, U)
⊢ x ∈ s → X.basicOpen x ≤ U

Tactic:
_

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ X.basicOpen x ≤ U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_1
D : GlueData
h : MkCore
i j k : h.J
x : { p // (ConcreteCategory.hom (h.V i j).inclusion') p.1 = (ConcreteCategory.hom (h.V i k).inclusion') p.2 }
⊢ { p // (ConcreteCategory.hom (h.V j k).inclusion') p.1 = (ConcreteCategory.hom (h.V j i).inclusion') p.2 }

Tactic:
refine ⟨⟨⟨(h.t i j x.1.1).1, ?_⟩, h.t i j x.1.1⟩, rfl⟩

Goal state after:
case refine_1
D : GlueData
h : MkCore
i j k : h.J
x : { p // (ConcreteCategory.hom (h.V i j).inclusion') p.1 = (ConcreteCategory.hom (h.V i k).inclusion') p.2 }
⊢ ↑((ConcreteCategory.hom (h.t i j)) (↑x).1) ∈ h.V j k
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))
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (pullback.fst (D.f i j) (D.f i k) ≫ D.f i j).c.app U =
      (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k).c.app U ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)
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
i j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
simp_rw [Category.assoc, cocycle_fst_snd 𝒰 f g i j k]

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
⊢ (gluing 𝒰 f g).glued ⟶ Y

Tactic:
apply Multicoequalizer.desc _ _ fun i ↦ pullback.snd _ _
  simp [t_fst_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Topology.IsOpenEmbedding ⇑(Sigma.desc α)

pp: case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
· suffices Topology.IsOpenEmbedding (Sigma.desc α ∘ sigmaMk f) by
      convert! this.comp (sigmaMk f).symm.isOpenEmbedding; ext; simp
    refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
    · fun_prop
    · rintro ⟨ix, x⟩ ⟨iy, y⟩ e
      have : α ix x = α iy y := by
        simpa [← Scheme.Hom.comp_apply] using e
      obtain rfl : ix = iy := by
        by_contra h
        exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl
      rw [(α ix).isOpenEmbedding.injective this]
    · rw [isOpenMap_sigma]
      intro i
      simpa [← Scheme.Hom.comp_apply] using (α i).isOpenEmbedding.isOpenMap

Goal state after:
case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
⊢ IsOpenImmersion (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)

Tactic:
have : pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp) =
        (pullbackSymmetry _ _).hom ≫ (pullbackLeftPullbackSndIso _ _ _).inv ≫
          pullback.fst _ _ ≫ (pullbackSymmetry _ _).hom := by aesop

Goal state after:
case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
this :
  pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry (𝒰.f i ≫ f) g).hom ≫
      (pullbackLeftPullbackSndIso g f (𝒰.f i)).inv ≫
        pullback.fst (pullback.snd g f) (𝒰.f i) ≫ (pullbackSymmetry g f).hom
⊢ IsOpenImmersion (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ : Scheme
⊢ ∀ {Y Z : Scheme} (e : X✝ ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ : Scheme
⊢ ∀ {Z : Scheme} (e : X✝ ≅ Y✝) (f : Y✝ ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ : Scheme
⊢ ∀ {Z : Scheme} (e : X✝ ≅ Y✝) (f : Y✝ ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
_

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
⊢ ∀ (e : X✝ ≅ Y✝) (f : Y✝ ⟶ Z✝) [inst : IsAffine Z✝], of P f → of P (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
⊢ ∀ (e : X✝ ≅ Y✝) (f : Y✝ ⟶ Z✝) [inst : IsAffine Z✝], of P f → of P (e.hom ≫ f)

Tactic:
_

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
⊢ ∀ (f : Y✝ ⟶ Z✝) [inst : IsAffine Z✝], of P f → of P (e✝.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
⊢ ∀ (f : Y✝ ⟶ Z✝) [inst : IsAffine Z✝], of P f → of P (e✝.hom ≫ f)

Tactic:
_

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
⊢ ∀ [inst : IsAffine Z✝], of P f✝ → of P (e✝.hom ≫ f✝)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
⊢ ∀ [inst : IsAffine Z✝], of P f✝ → of P (e✝.hom ≫ f✝)

Tactic:
_

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
inst✝ : IsAffine Z✝
⊢ of P f✝ → of P (e✝.hom ≫ f✝)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ : Scheme
⊢ ∀ {Y Z : Scheme} (e : Y ≅ Z) (f : X✝ ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
_

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ : Scheme
⊢ ∀ {Z : Scheme} (e : Y✝ ≅ Z) (f : X✝ ⟶ Y✝) [inst : IsAffine Y✝], of P f → of P (f ≫ e.hom)