mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)).IsIntegral ↔ (CommRingCat.Hom.hom φ).IsIntegral

R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ IsAffine (Spec S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X

Goal state after:
case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Z S : Scheme
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
hX : ∃ S, X = Spec S
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_2
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
· apply RingHom.Flat.generalizingMap_comap
    rwa [← HasRingHomProperty.Spec_iff (P := @Flat)]

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

Goal state before:
pp: n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [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 → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
⊢ ∃ i, e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree

Tactic:
have : ∃ n : ℕ, ∃ i, (e.1 i).degree = n ∧ (e.1 i) ≠ 0 := by
        obtain ⟨i, hi⟩ := he0; exact ⟨(e.1 i).natDegree, i, degree_eq_natDegree hi, hi⟩
      let m := Nat.find this
      obtain ⟨i, hi, hi'⟩ : ∃ i, (e.1 i).degree = m ∧ (e.1 i) ≠ 0 := Nat.find_spec this
      refine ⟨i, hi', fun j hj ↦ ?_⟩
      refine hi.le.trans ?_
      rw [degree_eq_natDegree hj, Nat.cast_le]
      exact Nat.find_min' _ ⟨j, degree_eq_natDegree hj, hj⟩

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

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ (∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd) →
    Relation.EqvGen F.ColimitTypeRel x y

Tactic:
rintro ⟨k, f, f', h⟩
    apply Relation.EqvGen.trans (y := ⟨k, F.map f' y.2⟩)
    · exact .rel _ _ ⟨f, by rw [← h]⟩
    · exact .symm _ _ (.rel _ _ ⟨f', rfl⟩)

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
⊢ IsClosed[inst✝²] D.support

Tactic:
convert!
    isClosed_sdiff_of_codiscreteWithin
      ((supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
        D.supportLocallyFiniteWithinDomain)
      hU

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
⊢ D.support = U \ {x | (fun x ↦ D x = 0 x) x}
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
⊢ ∃ U, ∃ (hx : x ∈ U), IsAffineOpen U ∧ U ≤ V ∧ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
obtain ⟨U, hx, hU, H⟩ := Scheme.IsGermInjectiveAt.cond (x := x)
  obtain ⟨f, hf, hxf⟩ := hU.exists_basicOpen_le ⟨x, hxV⟩ hx
  exact ⟨X.basicOpen f, hxf, hU.basicOpen f, hf, injective_germ_basicOpen U hU x hx f hxf H⟩

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
⊢ IsGenericPoint (f (genericPoint ↥X)) Set.univ

Tactic:
convert! (genericPoint_spec X).image f.continuous

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ Set.univ = closure (⇑f '' Set.univ)
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
this✝ : Nonempty ↥↑A
gA : ↑Γ(X, A) := (ConcreteCategory.hom (X.presheaf.map (homOfLE hAU).op)) g
h_germ_gA : (ConcreteCategory.hom (X.presheaf.germ A (genericPoint ↥X) hxA)) gA = f
hxV : genericPoint ↥X ∈ X.basicOpen gA
this : Nonempty ↥↑(X.basicOpen gA)
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
refine ⟨X.basicOpen gA, hA.basicOpen gA,
    X.presheaf.map (X.basicOpen_le gA).hom.op gA, ‹_›, ?_,
    X.toRingedSpace.isUnit_res_basicOpen gA⟩

Goal state after:
X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
this✝ : Nonempty ↥↑A
gA : ↑Γ(X, A) := (ConcreteCategory.hom (X.presheaf.map (homOfLE hAU).op)) g
h_germ_gA : (ConcreteCategory.hom (X.presheaf.germ A (genericPoint ↥X) hxA)) gA = f
hxV : genericPoint ↥X ∈ X.basicOpen gA
this : Nonempty ↥↑(X.basicOpen gA)
⊢ (ConcreteCategory.hom (X.germToFunctionField (X.basicOpen gA)))
      ((ConcreteCategory.hom (X.presheaf.map ⋯.hom.op)) gA) =
    f
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X

Goal state after:
case inr
I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
this :
  ∀ {X : Scheme} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X),
    c.π.app i ≫ a = c.π.app j ≫ b →
      ∀ (f : X ⟶ Spec R) [LocallyOfFiniteType f],
        t.app i = a ≫ f → t.app j = b ≫ f → (∃ S, X = Spec S) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hX : ¬∃ S, X = Spec S
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
X : Scheme
inst✝¹ : IsAffine X
a : D.obj i ⟶ X
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hX : ∃ S, X = Spec S
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
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✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i✝ j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i✝ ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i✝ ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i✝ = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i✝ ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i✝ ≫ a = c.π.app j ≫ b →
      t.app i✝ = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (e.app i)

Tactic:
dsimp [e]

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i✝ j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i✝ ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i✝ ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i✝ = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i✝ ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i✝ ≫ a = c.π.app j ≫ b →
      t.app i✝ = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (D.obj i).toSpecΓ
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
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound * c.degBound ^ c'.degBound = c.degBound ^ (c'.degBound + 1)

Tactic:
pow_succ'

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
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound * c.degBound ^ c'.degBound = c.degBound * c.degBound ^ c'.degBound
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
suffices g = ofHom (hπ.liftEquiv ⟨e.hom,
      fun a b hab ↦ CategoryTheory.congr_fun (h
          (ofHom ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption

Goal state after:
B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ g = ofHom (hπ.liftEquiv ⟨Hom.hom e, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit W.twoTorsionPolynomial.discr ↔ IsUnit W.Δ

Tactic:
rw [twoTorsionPolynomial_discr, IsUnit.mul_iff, show (16 : R) = 2 ^ 4 by norm_num1]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit (2 ^ 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case ht
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : ¬S.degBound = 0
⊢ 1 ≤ S.degBound

Tactic:
rwa [Nat.one_le_iff_ne_zero]

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
⊢ -(y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)) = 0 ↔
    1 ^ 6 *
        (W.a₆ + { u := 1, r := x, s := 0, t := y }.r * W.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W.a₂ +
                { u := 1, r := x, s := 0, t := y }.r ^ 3 -
              { u := 1, r := x, s := 0, t := y }.t * W.a₃ -
            { u := 1, r := x, s := 0, t := y }.t ^ 2 -
          { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W.a₁) =
      0

Tactic:
congr! 1

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

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

Tactic:
congr! 1

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (-y - W'.a₁ * x - W'.a₃) ^ 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) + W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (C • W).IsElliptic

Tactic:
rw [isElliptic_iff, variableChange_Δ]
  exact (C.u⁻¹.isUnit.pow 12).mul W.isUnit_Δ

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]
⊢ (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:
by rw [polynomial]; ring1

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

Goal state before:
pp: case refine_3
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))
hs : zeroLocus s₀ = Set.range (comap g)
t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))
⊢ t = comap g ⁻¹' comap σ ⁻¹' t ∩ Set.univ

Tactic:
Set.inter_univ,

Goal state after:
case refine_3
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))
hs : zeroLocus s₀ = Set.range (comap g)
t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))
⊢ t = comap g ⁻¹' comap σ ⁻¹' t
Module: Mathlib.Data.Nat.EvenOddRec

Goal state before:
pp: P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → false = true)

Tactic:
simp [H]

Goal state after:
Module: Mathlib.Data.Nat.EvenOddRec

Goal state before:
pp: P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → true = true)

Tactic:
simp [H]

Goal state after: