mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
⊢ ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n g

Tactic:
_

Goal state after:
case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
⊢ ∀ [inst : CommRing R₀✝] [inst_1 : Algebra R₀✝ R], Statement R₀✝ R n g
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
⊢ ∀ [inst : Algebra R₀✝ R], Statement R₀✝ R n g

Tactic:
_

Goal state after:
case hP₂
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
⊢ Statement R₀✝ R n g
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
      f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.I₀
⊢ P
    ((MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S).map
      (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f j) S)))

Tactic:
← PreservesPullback.iso_hom_fst,

Goal state after:
case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
      f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.I₀
⊢ P
    ((PreservesPullback.iso (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
          (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f j) S)).hom ≫
      pullback.fst
        ((MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S).map
          (Hom.asOverProp f S))
        ((MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S).map
          (Hom.asOverProp (𝒰.f j) S)))
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n { val := Function.update e.val j (e.val j %ₘ e.val i) }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_

Goal state after:
case hP₃
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
              Statement R₀ R n { val := Function.update e.val j (e.val j %ₘ e.val i) }) →
            ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
⊢ ∀ [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n c

Tactic:
_

Goal state after:
case hP₃
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝ : CommRing R₀
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n c
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝ : CommRing R₀
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n c

Tactic:
_

Goal state after:
case hP₃
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
⊢ Statement R₀ R n c
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝¹ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
k : Fin n
h✝ : ¬k = j
⊢ coeff(c.val k) ⊆ ↑(coeffSubmodule R₀ c)

Tactic:
exact (Set.subset_iUnion (fun i ↦ coeff(c.val i)) k).trans
                  (Set.subset_union_right.trans Submodule.subset_span)

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

Goal state before:
pp: S : Scheme
𝒰 : PreZeroHypercover S
𝒱 : PreZeroHypercover S
f : 𝒱.Hom 𝒰
inst✝ : QuasiCompactCover 𝒱
⊢ QuasiCompactCover 𝒰

Tactic:
refine ⟨fun {U} hU ↦ ?_⟩

Goal state after:
S : Scheme
𝒰 : PreZeroHypercover S
𝒱 : PreZeroHypercover S
f : 𝒱.Hom 𝒰
inst✝ : QuasiCompactCover 𝒱
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (fun x ↦ ⇑(𝒰.f x)) ↑U
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
⊢ k ∈ Finset.univ → (Function.update c.val j (c.val j %ₘ c.val i) k).degree.succ ≤ (c.val k).degree.succ

Tactic:
_

Goal state after:
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
a✝ : k ∈ Finset.univ
⊢ (Function.update c.val j (c.val j %ₘ c.val i) k).degree.succ ≤ (c.val k).degree.succ
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₄
R✝ : Type u_2
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
⊢ ∀ [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ (Away c)],
            Statement R₀ (Away c) n
              { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ (R ⧸ Ideal.span {c})],
              Statement R₀ (R ⧸ Ideal.span {c}) n
                { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_

Goal state after:
case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
            Statement R₀ (Away c) n
              { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
          (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
              Statement R₀ (R ⧸ Ideal.span {c}) n
                { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
            ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
    Statement R₀ (Away c) n
      { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }
R₀ : Type u_1
⊢ ∀ [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_

Goal state after:
case hP₄
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
    Statement R₀ (Away c) n
      { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }
R₀ : Type u_1
inst✝ : CommRing R₀
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₄
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
    Statement R₀ (Away c) n
      { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }
R₀ : Type u_1
inst✝ : CommRing R₀
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n e

Tactic:
_

Goal state after:
case hP₄
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
    Statement R₀ (Away c) n
      { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
⊢ Statement R₀ R n e
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 =
    (d.cocone i).ι.app a ≫ (d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)

Tactic:
rw [IsColimit.fac]

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 := 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
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
h : W.c₄ = 0
⊢ 0 ^ 3 = 0

Tactic:
zero_pow three_ne_zero

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
h : W.c₄ = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ -{ a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
          c :=
            2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
          d :=
            -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
              (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) }.toPoly =
    -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
neg_inj,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
        c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
        d :=
          -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
            (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) }.toPoly =
    (X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
k : I
fkj : k ⟶ j
hk :
  (ConcreteCategory.hom (Scheme.Hom.app (D.map fkj) (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
      (((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ -
        ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))
          ⋯) =
    0
⊢ ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fkj ≫ fjx)) (U x))) (t x) |_
        (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))
      ⋯ =
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fkj ≫ fjy)) (U y))) (t y) |_
        (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))
      ⋯

Tactic:
have H : (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y) ≤
        D.map fkj ⁻¹ᵁ ((D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) := by simp; rfl

Goal state after:
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
k : I
fkj : k ⟶ j
hk :
  (ConcreteCategory.hom (Scheme.Hom.app (D.map fkj) (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
      (((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ -
        ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))
          ⋯) =
    0
H : D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y ≤ D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)
⊢ ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fkj ≫ fjx)) (U x))) (t x) |_
        (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))
      ⋯ =
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fkj ≫ fjy)) (U y))) (t y) |_
        (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))
      ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (fun x ↦ x ^ 2) Y - (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y) =
    W'.polynomial * 1

Tactic:
rw [polynomial]; ring1

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂)) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))

Tactic:
XYIdeal_add_eq,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂)) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticSequence W
x : R
p q r : ℤ
⊢ IsEllipticNet.rel (x • W) p q r 0 = 0

Tactic:
by linear_combination (norm := (simp [IsEllipticNet.rel]; ring1)) x ^ 4 * h p q r

Goal state after: