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

Goal state before:
pp: 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 := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
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) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
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) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
⊢ (⋃ C ∈ S₁, C.toSet) ∪ ⋃ C ∈ S₂, C.toSet = ⋃ C ∈ S₁ ∪ S₂, C.toSet

Tactic:
by
        simpa using (Set.biUnion_union (SetLike.coe S₁) S₂ _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ Set.univ = closure (⇑f '' Set.univ)

Tactic:
symm

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ closure (⇑f '' Set.univ) = Set.univ
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 : 𝒰.I₀
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.f i) xi = (𝒰.f j) xj
⊢ ∃ k fi fj xk, (𝒰.trans fi) xk = xi ∧ (𝒰.trans fj) xk = xj

Tactic:
by
  obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj h
  obtain ⟨k, fi, fj, xk, rfl⟩ := 𝒰.exists_lift_trans_eq z
  use k, fi, fj, xk
  simp [← Scheme.Hom.comp_apply]

Goal state after:
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
z : ↥(pullback.diagonalObj f)
φ : Spec ((pullback f f).residueField z) ⟶ pullback f f := (pullback f f).fromSpecResidueField z
hφ₁ : φ ≫ pullback.fst f f = φ ≫ pullback.snd f f
hφ₂ : φ = (φ ≫ pullback.fst f f) ≫ pullback.diagonal f
⊢ (pullback.diagonal f) ((φ ≫ pullback.fst f f) (IsLocalRing.closedPoint ↑((pullback f f).residueField z))) = z

Tactic:
rw [← Scheme.Hom.comp_apply, ← hφ₂, Scheme.fromSpecResidueField_apply]

Goal state after:
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
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this : Module.Free R M
⊢ ∃ T,
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T, C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀✝ g ^ g.powBound

Tactic:
have : Module.Finite R M := .of_basis (AdjoinRoot.powerBasis' hi).basis

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
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
⊢ ∃ T,
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T, C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀✝ g ^ g.powBound
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: 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)
⊢ { 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 }.presieve₀ ∈
    (precoverage P).coverings W

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩
    · obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₁ f) x
      use i
      exact (mem_range_iff_of_surjective ((𝒰.pullback₁ f).f i) _
        ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
          (f.asOverProp S) ((𝒰.f _).asOverProp S)).inv)
        (PreservesPullback.iso_inv_fst _ _ _) x).mp hy
    · simp only [← CategoryTheory.Over.forget_map]
      rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
        ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
      rw [← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
      exact P.pullback_fst _ _ (𝒰.map_prop j)

Goal state after:
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✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := fun i' hii' ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W)ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f = A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯

Tactic:
ext <;> simp [hab]

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

Goal state before:
pp: 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 : (Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).I₀
⊢ (Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).f j ≫ W ↘ S = (Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).X j ↘ S

Tactic:
by exact (pullback.snd ((𝒰.f j).asOverProp S) (f.asOverProp S)).w

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
x✝ : ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)
i : ι
hi : i ∈ s
h : X i
hmem : h ∈ ↑(sSup (Us ⟨i, hi⟩))
heq : f i h = x
⊢ ∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd

Tactic:
coe_sSup,

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
x✝ : ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)
i : ι
hi : i ∈ s
h : X i
hmem : h ∈ ⋃ i_1 ∈ Us ⟨i, hi⟩, ↑i_1
heq : f i h = x
⊢ ∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.266} 𝒰.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.266} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
this : (𝒱 a).f i ≫ (D.map f).left = ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).left ≫ (𝒱 b).f i
⊢ Over.Hom.left (Comma.Hom.hom ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f ≫ (d.cocone i).ι.app b)) ≫
      colimit.ι d.relativeGluingData.functor i =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
Cocone.w

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.266} 𝒰.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.266} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
this : (𝒱 a).f i ≫ (D.map f).left = ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).left ≫ (𝒱 b).f i
⊢ Over.Hom.left (Comma.Hom.hom ((d.cocone i).ι.app a)) ≫ colimit.ι d.relativeGluingData.functor i =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ ↑(W.map f).Δ' = f ↑W.Δ'

Tactic:
by
  rw [coe_Δ', map_Δ, coe_Δ']

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

Goal state before:
pp: case inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ 1 < 3

Tactic:
decide

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

Goal state before:
pp: case inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ 0 < 3

Tactic:
decide

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

Goal state before:
pp: case inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: case inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < 3

Tactic:
decide

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

Goal state before:
pp: case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 0 < 3

Tactic:
decide

Goal state after:
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
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appLE (c.π.app (i x)) (U x) (c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯))
      (t x) =
    (ConcreteCategory.hom
        (Scheme.Hom.appLE (c.π.app (i y)) (U y) (c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯))
      (t y)

Tactic:
simp_rw [Scheme.Hom.appLE, ConcreteCategory.comp_apply, ht, TopCat.Presheaf.restrictOpen,
        TopCat.Presheaf.restrict, ← ConcreteCategory.comp_apply, ← Functor.map_comp]

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
⊢ (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) s =
    (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) s
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: 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
q : MvPolynomial (Fin m) R
⊢ (commAlgEquiv R (Fin n) (Fin m)) (MvPolynomial.C q) =
    (commAlgEquiv R (Fin n) (Fin m)) ((commAlgEquiv R (Fin n) (Fin m)).symm (0 + σ q))

Tactic:
by simp [commAlgEquiv_C, σ]

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

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (t ^ 2 - C 4 * s * u).IsHomogeneous 2

Tactic:
exact isHomogeneous_X_pow .. |>.sub CXY

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 0 = 0

Tactic:
by
  simp [preNormEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 1 = 1

Tactic:
by
  simp [preNormEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ preNormEDS b c d (-n) = -preNormEDS b c d n

Tactic:
by
  simp [preNormEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ ¬Even 3

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ Even 4

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ ¬Odd 4

Tactic:
decide

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p • 1 + q • if 1 = 0 then 1 else 0) *
        (((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • if 0 = 1 then 1 else 0) +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • 1) -
      ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1 +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • if 1 = 0 then 1 else 0) *
        ((p • if 0 = 1 then 1 else 0) + q • 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
one_ne_zero,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p • 1 + q • if False then 1 else 0) *
        (((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • if 0 = 1 then 1 else 0) +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • 1) -
      ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1 +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • if False then 1 else 0) *
        ((p • if 0 = 1 then 1 else 0) + q • 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
n : ℕ
⊢ f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n

Tactic:
induction n using normEDSRec' with

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
n : ℤ
⊢ f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n

Tactic:
by
  simp [preNormEDS]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Even 3

Tactic:
decide

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Odd 4

Tactic:
decide

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ Even 2

Tactic:
decide

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialX = C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z ^ 2 + C W'.a₄ * Z ^ 4)

Tactic:
rw [polynomialX, polynomial]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv x)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)) =
    C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z ^ 2 + C W'.a₄ * Z ^ 4)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : E.IsElliptic
inst✝¹ : E'.IsElliptic
p : ℕ
inst✝ : CharP F p
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝ : NeZero 2
this : 2 ^ 2 ≠ 0
⊢ 4 ≠ 0

Tactic:
norm_num1 at this

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : E.IsElliptic
inst✝¹ : E'.IsElliptic
p : ℕ
inst✝ : CharP F p
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝ : NeZero 2
this : 4 ≠ 0
⊢ 4 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : E.IsElliptic
inst✝¹ : E'.IsElliptic
p : ℕ
inst✝ : CharP F p
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝¹ : NeZero 2
this✝ : NeZero 4
this : 2 * 3 ≠ 0
⊢ 6 ≠ 0

Tactic:
norm_num1 at this

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : E.IsElliptic
inst✝¹ : E'.IsElliptic
p : ℕ
inst✝ : CharP F p
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝¹ : NeZero 2
this✝ : NeZero 4
this : 6 ≠ 0
⊢ 6 ≠ 0