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

Goal state before:
pp: case e'_3.f.a
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := ⋯
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (Localization.Away c)
hxT₁ : x ∈ ↑T₁
⊢ comap q₁.toRingHom '' x.toSet ∈ 𝒫 Set.range (comap q₁.toRingHom)

Tactic:
exact Set.image_subset_range ..

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X S : Scheme
U : X.Opens
sX : X ⟶ S
hU : Dense ↑U
inst✝ : IsRationalOver sX
n : Type u
hn : BirationalOver sX (𝔸(n; S) ↘ S)
⊢ IsRationalOver (U.ι ≫ sX)

Tactic:
exact ⟨n, (U.birationalOver_of_dense sX hU).trans hn⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
xk : ↥(𝒰.X k)
h :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk))
⊢ ∃ k_1 fi_1 fj_1 xk_1,
    (𝒰.trans fi_1) xk_1 = (pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk) ∧
      (𝒰.trans fj_1) xk_1 = (pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk)

Tactic:
use k, fi, fj, xk

Goal state after:
case h
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
xk : ↥(𝒰.X k)
h :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk))
⊢ (𝒰.trans fi) xk = (pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk) ∧
    (𝒰.trans fj) xk = (pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans fi) (𝒰.trans fj) ⋯) xk)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : f x₁ = f x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : f x₁ = f x₂
t : ↥(pullback f f)
ht₁ : (pullback.fst f f) t = x₁
ht₂ : (pullback.snd f f) t = x₂
⊢ x₁ = x₂
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
⊢ Function.Surjective ⇑(pullback.diagonal f)

Tactic:
intro z

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
z : ↥(pullback.diagonalObj f)
⊢ ∃ a, (pullback.diagonal f) a = z
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ d.toBase ((colimit.ι d.functor j) xj) = (𝒰.f j) ((trans 𝒰 fj) uk)

Tactic:
← h

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (𝒰.f i) ((trans 𝒰 fi) uk) = (𝒰.f j) ((trans 𝒰 fj) uk)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₁.refine_1
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ comap Polynomial.C '' (zeroLocus (Set.range { val := 0 }.val) \ zeroLocus {f}) =
    ConstructibleSetData.toSet
      (Finset.image (fun j ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2)))

pp: case hP₁.refine_2
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ ∀ C ∈ Finset.image (fun j ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2)),
    C.n ≤ { val := 0 }.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ { val := 0 } ^ { val := 0 }.powBound

Tactic:
· convert! image_comap_C_basicOpen f
      · simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_sdiff]
        congr 1
        rw [← Set.univ_subset_iff]
        rintro x _ _ ⟨_, rfl⟩
        exact zero_mem x.asIdeal
      · suffices Set.range f.coeff = ⋃ i < f.natDegree + 2, {f.coeff i} by
          simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_sdiff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]
        trans f.coeff '' (Set.Iio (f.natDegree + 2))
        · refine ((Set.image_subset_range _ _).antisymm ?_).symm
          rintro _ ⟨i, rfl⟩
          by_cases! hi : i ≤ f.natDegree
          · exact ⟨i, hi.trans_lt (by simp), rfl⟩
          · exact ⟨f.natDegree + 1, by simp, by simp [f.coeff_eq_zero_of_natDegree_lt hi]⟩
        · ext; simp [eq_comm]

Goal state after:
case hP₁.refine_2
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ ∀ C ∈ Finset.image (fun j ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2)),
    C.n ≤ { val := 0 }.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ { val := 0 } ^ { val := 0 }.powBound
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝¹ : IsAffine (A.𝒰D.X j)
this✝ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
⊢ ∃ k hki',
    (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.b

Tactic:
have : LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ A.𝒰S.pullbackHom f j.fst.fst) := by
    dsimp [Scheme.Cover.pullbackHom]; infer_instance

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝² : IsAffine (A.𝒰D.X j)
this✝¹ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this✝ : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
this : LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ Scheme.Cover.pullbackHom A.𝒰S f j.fst.fst)
⊢ ∃ k hki',
    (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.b
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃.inr.refine_2
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
⊢ C ∈ S → C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ c ^ c.powBound

Tactic:
hC

Goal state after:
case hP₃.inr.refine_2
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.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ c ^ c.powBound
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case pos
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) }
k : Fin n
a✝ : k ∈ Finset.univ
hkj : k = j
⊢ (c.val j %ₘ c.val i).degree ≤ (c.val k).degree

Tactic:
subst hkj; exact (degree_modByMonic_le _ hi).trans hle

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case ht
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
⊢ 0 < ∑ i, (c.val i).degree.succ

Tactic:
refine Fintype.sum_pos (Pi.lt_def.mpr ⟨by positivity, i, by simp [hi']⟩)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₆ = W.a₃ ^ 2

Tactic:
rw [b₆]
  linear_combination 2 * W.a₆ * CharP.cast_eq_zero R 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),
    (∀ (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:
intro s m hm
    ext
    refine 𝒱.hom_ext _ _ fun i ↦ ?_
    have : (d.pullbackGluedIso i).inv ≫ (Over.pullback P ⊤ (𝒰.f i)).map m =
        (d.isColimit i).desc ((Over.pullback P ⊤ (𝒰.f i)).mapCocone s) := by
      refine (d.isColimit i).hom_ext fun a ↦ ?_
      rw [IsColimit.fac]
      ext
      apply pullback.hom_ext
      · dsimp
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          pullbackGluedIso_inv_fst_assoc]
        rw [← congr($(hm a).left)]
        simp [fst_gluedCocone_ι_assoc]
      · simp
    rw [Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left]
    simp [𝒱, ← this]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

Tactic:
rw [nonsingular_iff', equation_iff_variableChange, equation_zero, ← neg_ne_zero, or_comm,
    nonsingular_zero, variableChange_a₃, variableChange_a₄, inv_one, Units.val_one]

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (1 ^ 3 * (W.a₃ + { u := 1, r := x, s := 0, t := y }.r * W.a₁ + 2 * { u := 1, r := x, s := 0, t := y }.t) ≠ 0 ∨
        1 ^ 4 *
            (W.a₄ - { u := 1, r := x, s := 0, t := y }.s * W.a₃ + 2 * { u := 1, r := x, s := 0, t := y }.r * W.a₂ -
                  ({ u := 1, r := x, s := 0, t := y }.t +
                      { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.s) *
                    W.a₁ +
                3 * { u := 1, r := x, s := 0, t := y }.r ^ 2 -
              2 * { u := 1, r := x, s := 0, t := y }.s * { u := 1, r := x, s := 0, t := y }.t) ≠
          0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
h : y = W'.negY x y
⊢ W'.a₁ * W'.negY x y = 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ↔ W'.a₁ * y = 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄

Tactic:
← h

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
h : y = W'.negY x y
⊢ W'.a₁ * y = 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ↔ W'.a₁ * y = 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

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

Tactic:
(simp [field]; ring1)

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree

Tactic:
natDegree_eq_of_degree_eq
      (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)

Goal state after:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ finrank F (S ⧸ span {f}) = (∏ i, smithCoeffs b (span {f}) ⋯ i).natDegree
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case mul_X.refine_1
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
H : Ideal.span s₀ ≤ RingHom.ker g
i : Fin n
q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₂ : MvPolynomial (Fin m) R
hq₁ : q₁ ∈ Ideal.span s₀
⊢ q₁ * MvPolynomial.C (MvPolynomial.X i) + σ q₂ * (MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) ∈
    Ideal.span s₀

Tactic:
exact add_mem (Ideal.mul_mem_right _ _ hq₁)
            (Ideal.mul_mem_left _ _ (Ideal.subset_span (Set.mem_range_self _)))

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ atomRel W a b c d = rel W ((a - d) / 2) ((b - d) / 2) ((c - d) / 2) d

Tactic:
by
  simp only [rel_eq, Int.mul_ediv_cancel', Int.ModEq.dvd parity.1, Int.ModEq.dvd parity.2.1,
    Int.ModEq.dvd parity.2.2, sub_add_cancel]

Goal state after: