mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
⊢ FamilyOfElements.Compatible fun ⦃Y⦄ f a ↦ ⋯.elim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
t : F.obj (op I)
h :
  (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : F.obj (op I)), (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj (op I)
x✝ : Y
⊢ (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) ((ConcreteCategory.hom a).toFun x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
t : F.obj (op I)
h :
  (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : F.obj (op I)), (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj (op I)
⊢ a = default

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
⊢ IsTerminal (F.obj (op I))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
⊢ (Pi.lift fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift fun i ↦ (c.inj i).op) ≫ piComparison F fun i ↦ op (X i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP : W'.Nonsingular (u • P)
⊢ W'.Nonsingular P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift fun i ↦ (c.inj i).op) ≫ piComparison F fun i ↦ op (X i)
⊢ (Pi.lift fun i ↦ (c.inj i).op) = (productIsProduct fun x ↦ op (X x)).lift c.op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (↑hu.unit⁻¹ • u • P)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ P y ^ 2 + W'.a₁ * P x * P y - W'.a₂ * P x ^ 2 ≠ 0)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
h : 3 * 0 ^ 2 = 0 ∧ 1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2 = 0
⊢ 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![0, 1, 0]

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
⊢ have this := ⋯;
  (piComparison F fun x ↦ op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]⟧

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
hP : W.NonsingularLift P
hQ : W.NonsingularLift Q
⊢ W.NonsingularLift (W.addMap P Q)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : ¬W.Nonsingular P
⊢ toAffine W P = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z = 0
⊢ toAffine W P = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
⊢ toAffine W P = Affine.Point.some (P x / P z) (P y / P z) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
X Y : F
h : W.Nonsingular ![X, Y, 1]
⊢ toAffine W ![X, Y, 1] = Affine.Point.some X Y ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
t : F.obj (∏ᶜ fun x ↦ op (X x))
ht₁ :
  (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      t =
    b
ht₂ :
  ∀ (y : (fun X ↦ X) (F.obj (∏ᶜ fun x ↦ op (X x)))),
    (fun a ↦
          (ConcreteCategory.hom
                (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
                  Equalizer.Presieve.Arrows.forkMap F X c.inj))
              a =
            b)
        y →
      y = t
y : F.obj (op c.pt)
hy : (fun x ↦ (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b) y
⊢ (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      ((ConcreteCategory.hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).hom)) y) =
    b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
⊢ IsSheafFor F (ofArrows X c.inj)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
h : P ≈ Q
⊢ toAffine W P = toAffine W Q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0 ∧ P z ^ 2 ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
and_iff_left <| pow_ne_zero 2 hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Nonsingular P ↔ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ P ≈ Q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
⊢ Equalizer.Presieve.Arrows.firstMap F X c.inj = Equalizer.Presieve.Arrows.secondMap F X c.inj

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    toAffine W P + toAffine W Q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomial = (MvPolynomial.map f) W'.polynomial

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (W'.map f).Equation (⇑f ∘ P)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (W'.map f).Equation (⇑f ∘ P) ↔ W'.Equation P

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialX = (MvPolynomial.map f) W'.polynomialX

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialY = (MvPolynomial.map f) W'.polynomialY

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
⊢ PreservesLimit (Discrete.functor fun x ↦ op (X x)) F

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialZ = (MvPolynomial.map f) W'.polynomialZ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (W'.map f).Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomial = (MvPolynomial.map ↑f) (W'⁄A).polynomial

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ Continuous (ULift.map ⇑(ConcreteCategory.hom f))

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : TopCat
f : uliftFunctor.obj X✝ ⟶ uliftFunctor.obj Y✝
⊢ Continuous (ULift.down ∘ ⇑(ConcreteCategory.hom f) ∘ ULift.up)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ (W'⁄B).Equation (⇑f ∘ P)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Equation (⇑f ∘ P) ↔ (W'⁄A).Equation P

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialX = (MvPolynomial.map ↑f) (W'⁄A).polynomialX

Tactic:
by

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

Goal state before:
pp: ⊢ PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialY = (MvPolynomial.map ↑f) (W'⁄A).polynomialY

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialZ = (MvPolynomial.map ↑f) (W'⁄A).polynomialZ

Tactic:
by

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

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
⊢ s ⊆ Set.range ⇑Homeomorph.ulift.symm

Tactic:
by

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

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ ⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s ⊆ Set.range ⇑Homeomorph.ulift

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
by

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

Goal state before:
pp: ⊢ PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
by

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

Goal state before:
pp: X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (x : ↑X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (E.f i))

Tactic:
by

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

Goal state before:
pp: X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (i : E.I₀), Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (E.f i))

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
i : 𝒰.I₀
y : ↑(𝒰.X i)
⊢ (ConcreteCategory.hom (𝒰.f i)) y ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f i))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
⊢ ∀ (x_1 y : 𝓤.I₀), pullback.fst (𝓤.f x_1) (𝓤.f y) ≫ x (𝓤.f x_1) ⋯ = pullback.snd (𝓤.f x_1) (𝓤.f y) ≫ x (𝓤.f y) ⋯

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i : 𝒰.I₀
⊢ Continuous (⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: ⊢ zariskiTopology.Subcanonical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: ⊢ (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: ⊢ forgetToTop.IsContinuous zariskiTopology TopCat.grothendieckTopology

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: X : Scheme
i j :
  (X.affineCover.refineOneHypercover fun i j ↦
      (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover.toPreZeroHypercover).I₀
⊢ (X.affineCover.refineOneHypercover fun i j ↦
          (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover.toPreZeroHypercover).sieve₁'
      i j ∈
    zariskiTopology
      (pullback
        ((X.affineCover.refineOneHypercover fun i j ↦
              (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover.toPreZeroHypercover).f
          i)
        ((X.affineCover.refineOneHypercover fun i j ↦
              (pullback (X.affineCover.f i) (X.affineCover.f j)).affineCover.toPreZeroHypercover).f
          j))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
⊢ PreservesLimitsOfShape (Discrete ι) F

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
Y : Scheme
i : J
⊢ 𝟙 (F.obj i) ≫ c.ι.app i = colimit.ι F i ≫ iso.inv

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
⊢ Sieve.ofArrows F.obj c.ι.app ∈ Scheme.zariskiTopology c.pt

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)

Tactic:
by

Goal state after: