mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).IsElliptic

pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).IsElliptic

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).IsElliptic

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).j = j

pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).j = j

Tactic:
·

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).j = j

pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).j = j

Tactic:
·

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).j = j

Tactic:
·

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).j = j

Tactic:
·

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).j = j

pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j

Tactic:
·

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j

Tactic:
·

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j

Tactic:
have := Fact.mk (Ne.isUnit h0)
      have := Fact.mk (sub_ne_zero.2 h1728).isUnit
      simp_rw [ofJ_ne_0_ne_1728 j h0 h1728, ofJNe0Or1728_j]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case id
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
j✝ : WalkingMulticospan J
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.id j✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        j✝) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      j✝

pp: case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)

pp: case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)

Tactic:
·

Goal state after:
case id
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
j✝ : WalkingMulticospan J
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.id j✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        j✝) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      j✝
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)

pp: case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)

Tactic:
·

Goal state after:
case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)

Tactic:
·

Goal state after:
case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case left
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
a✝ : J.L
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.left a✝) =
    ↑s (WalkingMulticospan.left a✝)

pp: case right
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
r : J.R
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.right r) =
    ↑s (WalkingMulticospan.right r)

Tactic:
·

Goal state after:
case left
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
a✝ : J.L
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.left a✝) =
    ↑s (WalkingMulticospan.left a✝)
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case right
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
r : J.R
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.right r) =
    ↑s (WalkingMulticospan.right r)

Tactic:
·

Goal state after:
case right
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
r : J.R
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.right r) =
    ↑s (WalkingMulticospan.right r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

pp: case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

pp: case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows

Tactic:
·

Goal state after:
case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

pp: case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows

Tactic:
·

Goal state after:
case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows

Tactic:
·

Goal state after:
case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s t : (E.multifork F).pt
hst : (E.multifork F).toSections s = (E.multifork F).toSections t
⊢ s = t

pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
⊢ ∃ a, (E.multifork F).toSections a = s

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s t : (E.multifork F).pt
hst : (E.multifork F).toSections s = (E.multifork F).toSections t
⊢ s = t
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
⊢ ∃ a, (E.multifork F).toSections a = s

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
⊢ ∃ a, (E.multifork F).toSections a = s
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
⊢ (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map gi.op)) (s i)) =
    (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map gj.op)) (s j))

Tactic:
simp only [← comp_apply, ← Functor.map_comp, ← op_comp, hf₁, hf₂]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
⊢ (ConcreteCategory.hom (F.map (h ≫ E.p₁ k).op)) (s i) = (ConcreteCategory.hom (F.map (h ≫ E.p₂ k).op)) (s j)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

pp: case neg
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
·

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
·

Goal state after:
case neg
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q