mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU : ∃ V, IsCompact V.carrier ∧ (fun p ↦ g p.fst p.snd) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
⊢ (fun x ↦ f x.fst x.snd) ∘ p = fun x ↦ g x.fst x.snd

Tactic:
ext

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU : ∃ V, IsCompact V.carrier ∧ (fun p ↦ g p.fst p.snd) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
x✝ : (i : σ) × Y i
⊢ ((fun x ↦ f x.fst x.snd) ∘ p) x✝ = g x✝.fst x✝.snd
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case h
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ (⋯.isoSpec.hom ≫ ⋯.fromSpec ≫ 𝒰.f (f { down := idx s }.down)) ⟨x s, ⋯⟩ = s

Tactic:
← IsAffineOpen.isoSpec_inv_ι,

Goal state after:
case h
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ (⋯.isoSpec.hom ≫ (⋯.isoSpec.inv ≫ (V { down := idx s }.down).ι) ≫ 𝒰.f (f { down := idx s }.down)) ⟨x s, ⋯⟩ = s
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
⊢ D.map f ≫
      {
        toCommaMorphism :=
          (𝒱 b).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    {
        toCommaMorphism :=
          (𝒱 a).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } ≫
      ((Functor.const J).obj d.glued).map f

Tactic:
ext

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := ⋯
a b : J
f : a ⟶ b
⊢ (D.map f ≫
        {
          toCommaMorphism :=
            (𝒱 b).glueMorphismsOverOfLocallyDirected
              (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
          prop_hom_left := trivial, prop_hom_right := trivial }).left =
    ({
          toCommaMorphism :=
            (𝒱 a).glueMorphismsOverOfLocallyDirected
              (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
          prop_hom_left := trivial, prop_hom_right := trivial } ≫
        ((Functor.const J).obj d.glued).map f).left
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
ext

Goal state after:
B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
x✝ : ↑(of ↑X)
⊢ (ConcreteCategory.hom (ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π)) x✝ =
    (ConcreteCategory.hom (ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π)) x✝
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
ext; exact hab

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
ext

Goal state after:
B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
x✝ : ↑(of ↑X)
⊢ (ConcreteCategory.hom (ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π)) x✝ =
    (ConcreteCategory.hom (ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π)) x✝
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
ext; exact hab

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ hπ.liftEquiv.symm (Hom.hom g) = ⟨Hom.hom e, ⋯⟩

Tactic:
ext

Goal state after:
B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a✝ : ↑X
⊢ ↑(hπ.liftEquiv.symm (Hom.hom g)) a✝ = ↑⟨Hom.hom e, ⋯⟩ a✝
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
j✝ : J
⊢ ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
      d.transitionMap hij ≫ (d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s) =
    ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
      (MorphismProperty.Over.map ⊤ ⋯).map
          ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
        (Over.pullbackMapHomPullback (Cover.trans 𝒰 hij) ⋯ trivial (𝒰.f j) (𝒰.f i) ⋯).app s.pt

Tactic:
ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := ⋯
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
j✝ : J
⊢ (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
        d.transitionMap hij ≫ (d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left =
    (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
        (MorphismProperty.Over.map ⊤ ⋯).map
            ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
          (Over.pullbackMapHomPullback (Cover.trans 𝒰 hij) ⋯ trivial (𝒰.f j) (𝒰.f i) ⋯).app s.pt).left
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
⊢ Set.range (⇑(TopCat.Hom.hom (π.base ≫ b)) ∘ ⇑(TopCat.Hom.hom (fst π (𝒰.f i)).base)) ⊆ Set.range ⇑(Opens.ι ↑(↑i).2)

Tactic:
← TopCat.coe_comp,

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
⊢ Set.range ⇑(ConcreteCategory.hom ((fst π (𝒰.f i)).base ≫ π.base ≫ b)) ⊆ Set.range ⇑(Opens.ι ↑(↑i).2)
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.397} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.397} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
a : J
𝒲 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
⊢ d.gluedCocone.ι.app a ≫
      {
        toCommaMorphism :=
          𝒱.glueMorphismsOverOfLocallyDirected
            (fun i ↦
              ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                pullback.fst s.pt.hom (𝒰.f i))
            ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    s.ι.app a

Tactic:
ext

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.397} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.397} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := ⋯
s : Cocone D
a : J
𝒲 : (a : J) → (D.obj a).left.OpenCover := ⋯
⊢ (d.gluedCocone.ι.app a ≫
        {
          toCommaMorphism :=
            𝒱.glueMorphismsOverOfLocallyDirected
              (fun i ↦
                ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                  pullback.fst s.pt.hom (𝒰.f i))
              ⋯ ⋯,
          prop_hom_left := trivial, prop_hom_right := trivial }).left =
    (s.ι.app a).left
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
⊢ Set.range ⇑(TopCat.Hom.hom (𝒰.f i).base) ⊆ ⇑(TopCat.Hom.hom b) ⁻¹' ↑↑(↑i).2

Tactic:
exact trans (by simp [𝒰]) i.2.2

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.442} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.442} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
⊢ m =
    {
      toCommaMorphism :=
        𝒱.glueMorphismsOverOfLocallyDirected
          (fun i ↦
            ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
              pullback.fst s.pt.hom (𝒰.f i))
          ⋯ ⋯,
      prop_hom_left := trivial, prop_hom_right := trivial }

Tactic:
ext

Goal state after:
case refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.442} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.442} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := ⋯
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
⊢ m.left =
    {
        toCommaMorphism :=
          𝒱.glueMorphismsOverOfLocallyDirected
            (fun i ↦
              ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                pullback.fst s.pt.hom (𝒰.f i))
            ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial }.left
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ (d.cocone i).ι.app a ≫ (d.pullbackGluedIso i).inv ≫ (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map m =
    ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s).ι.app a

Tactic:
ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := ⋯
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ ((d.cocone i).ι.app a ≫ (d.pullbackGluedIso i).inv ≫ (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map m).left =
    (((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s).ι.app a).left
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹ = x✝

Tactic:
ext

Goal state after:
case a₁
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₁ = x✝.a₁

case a₂
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₂ = x✝.a₂

case a₃
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₃ = x✝.a₃

case a₄
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₄ = x✝.a₄

case a₆
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₆ = x✝.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Tactic:
ext

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a

case b
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b

case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.c = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.c

case d
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.d = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }

Tactic:
ext

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a

case b
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b

case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.c = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.c

case d
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.d = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext

Goal state after:
case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑(x✝² * x✝¹ * x✝).u = ↑(x✝² * (x✝¹ * x✝)).u

case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).r = (x✝² * (x✝¹ * x✝)).r

case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).s = (x✝² * (x✝¹ * x✝)).s

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).t = (x✝² * (x✝¹ * x✝)).t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext <;> simp only [mul_def, Units.val_mul]

Goal state after:
case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝².u * ↑x✝¹.u * ↑x✝.u = ↑x✝².u * (↑x✝¹.u * ↑x✝.u)

case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * ↑x✝.u ^ 2 + x✝.r = x✝².r * (↑x✝¹.u * ↑x✝.u) ^ 2 + (x✝¹.r * ↑x✝.u ^ 2 + x✝.r)

case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝.u * (↑x✝¹.u * x✝².s + x✝¹.s) + x✝.s = ↑x✝¹.u * ↑x✝.u * x✝².s + (↑x✝.u * x✝¹.s + x✝.s)

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².t * ↑x✝¹.u ^ 3 + x✝².r * x✝¹.s * ↑x✝¹.u ^ 2 + x✝¹.t) * ↑x✝.u ^ 3 +
        (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * x✝.s * ↑x✝.u ^ 2 +
      x✝.t =
    x✝².t * (↑x✝¹.u * ↑x✝.u) ^ 3 + x✝².r * (↑x✝.u * x✝¹.s + x✝.s) * (↑x✝¹.u * ↑x✝.u) ^ 2 +
      (x✝¹.t * ↑x✝.u ^ 3 + x✝¹.r * x✝.s * ↑x✝.u ^ 2 + x✝.t)