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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
⊢ IsClosed Z

Tactic:
simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
⊢ IsOpen (⋃ i, ⇑fT ⁻¹' ↑(Ti i) ∩ ⇑p ⁻¹' ↑(U i))
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝³ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝² : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝¹ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this✝ : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
⊢ ((t ^ m) ^ (p.natDegree - 1) * t ^ m) • eval₂ (algebraMap R S) (t ^ n • r) p = 0

Tactic:
mul_smul,

Goal state after:
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝³ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝² : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝¹ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this✝ : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
⊢ (t ^ m) ^ (p.natDegree - 1) • t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg.inl
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
he0 : ¬e = { val := 0 }
h✝ : Subsingleton R
⊢ P R e

Tactic:
convert! hP₁ R; ext; exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [Adjunction.homEquiv_symm_apply, Adjunction.homEquiv_symm_apply]

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))

Tactic:
have := isIso_of_isTerminal specULiftZIsTerminal.{u} terminalIsTerminal (terminal.from _)
  rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]
  convert! (inferInstance : Algebra.FinitePresentation (ULift ℤ) ℤ[n])
  exact Algebra.algebra_ext _ _ fun _ ↦ rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (Spec.map (CommRingCat.ofHom C))

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := isomorphisms _), ← isomorphisms,
      ← arrow_mk_iso_iff (isomorphisms _) (arrowIsoΓSpecOfIsAffine _)]
    exact ⟨inferInstance, (ConcreteCategory.isIso_iff_bijective _).mpr
      ⟨C_injective n _, C_surjective _⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: case refine_2.refine_1
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) ≫ i = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp only [Category.assoc, ← SpecMap_residueFieldIsoBase_inv (f ≫ i) x hx, ← Spec.map_comp,
        Iso.inv_hom_id, Spec.map_id, ← H']

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: case refine_2.refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) ≫ i = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp only [Category.assoc, ← SpecMap_residueFieldIsoBase_inv (f ≫ i) x hx, ← Spec.map_comp,
        Iso.inv_hom_id, Spec.map_id, ← H']

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
by
  have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_
  · simpa only [Scheme.Spec_stalkClosedPointTo_fromSpecStalk] using this
  · rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]
  · apply Spec.map_injective
    rw [← cancel_mono (S.fromSpecStalk _)]
    simpa only [Spec.map_comp, Category.assoc, Scheme.SpecMap_stalkMap_fromSpecStalk,
      Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc,
      Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : { f // f.compHom sY = Hom.toRationalMap sX }
⊢ (↑f).fromFunctionField ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX

Tactic:
obtain ⟨f, hf⟩ := f
    obtain ⟨f, rfl⟩ := f.exists_rep
    simpa [fromFunctionField_toRationalMap] using! congr(RationalMap.fromFunctionField $hf)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
this : Finite ↑I
⊢ ⨆ x, ↑↑x = UX

Tactic:
by rwa [iSup_subtype, eq_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUX : IsCompact ↑UX
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
this : Finite ↑I
⊢ ⨆ i, ↑↑i = UX

Tactic:
by rwa [iSup_subtype, eq_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
hIUT : ∀ (i : ↑I), ↑↑i ≤ UT
this : Finite ↑I
⊢ ⨆ i, ↑↑i = UT

Tactic:
by rwa [iSup_subtype, eq_comm]

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

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
⊢ f.toRationalMap.comp g.toRationalMap = (f.comp g).toRationalMap

Tactic:
rw [RationalMap.comp_def, PartialMap.toRationalMap_eq_iff]
  exact PartialMap.comp_equiv_of_equiv_left f.representative_toRationalMap_equiv _

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

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)

Tactic:
by
  rw [← f₃.toRationalMap_representative]
  simp_rw [comp_def, ← PartialMap.comp_assoc, PartialMap.toRationalMap_eq_iff]
  apply PartialMap.comp_equiv_of_equiv_left
  rw [← f₂.toRationalMap_representative, comp_def]
  apply (f₁.representative.comp f₂.representative).representative_toRationalMap_equiv.trans
  apply PartialMap.comp_equiv_of_equiv_right
  rw [toRationalMap_representative]

Goal state after:
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.71} 𝒰.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.71} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
⊢ P d.relativeGluingData.toBase

Tactic:
by
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) 𝒰]
    intro i
    rw [Scheme.Cover.pullbackHom,
      ← (d.relativeGluingData.isPullback_natTrans_ι_toBase i).flip.isoPullback_inv_snd,
      P.cancel_left_of_respectsIso]
    exact (d.cocone i).pt.prop

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
inst✝¹ : F.ReflectsEffectiveEpiFamilies
α✝ : Type
inst✝ : Finite α✝
B✝ : C
x✝¹ : α✝ → C
x✝ : (a : α✝) → x✝¹ a ⟶ B✝
h : EffectiveEpiFamily (fun a ↦ F.obj (x✝¹ a)) fun a ↦ F.map (x✝ a)
⊢ EffectiveEpiFamily x✝¹ x✝

Tactic:
have := F.effectiveEpiFamily_of_map _ _ h
    infer_instance

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

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
⊢ degBound k D 0 = 1

Tactic:
rw [degBound]

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

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k D (n + 1) = numBound k D (n + 1) ^ numBound k D (n + 1) * degBound k D n

Tactic:
rw [degBound]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (∑ x, if x = i then (smithCoeffs b (span {f}) ⋯ i * 1) • b' x else 0) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))

Tactic:
Finset.sum_ite_eq',

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (if i ∈ Finset.univ then (smithCoeffs b (span {f}) ⋯ i * 1) • b' i else 0) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (↑(Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))) (b' i) =
    (↑(Algebra.lmul R S).toRingHom f ∘ₗ
        ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ∘ₗ
          ↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)))
      (b' i)

Tactic:
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
    Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul,
    zero_smul, Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ((selfBasis b (span {f}) hI) ((Equiv.refl ι) i)))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a : ℤ
⊢ atom W a a = W a * W 0

Tactic:
by
  rw [atom, ← two_mul, Int.mul_tdiv_cancel_left _ two_ne_zero, sub_self, Int.zero_tdiv]

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:
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:
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:
simp [preNormEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑m + 1) =
    (preNormEDS b c d (-↑m + 2) * preNormEDS b c d (-↑m) ^ 3 * if Even (-↑m) then b else 1) -
      preNormEDS b c d (-↑m - 1) * preNormEDS b c d (-↑m + 1) ^ 3 * if Even (-↑m) then 1 else b

Tactic:
rcases m with _ | m
    · simp
    simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, ih]
    ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ preNormEDS b c d (2 * m + 1) =
    (preNormEDS b c d (m + 2) * preNormEDS b c d m ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (m - 1) * preNormEDS b c d (m + 1) ^ 3 * if Even m then 1 else b

Tactic:
by
  induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _ | _
    iterate 2 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_odd ..
  | neg ih m =>
    rcases m with _ | m
    · simp
    simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, ih]
    ring1

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:
simp [preNormEDS]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ W.Ψ (2 * m) * W.ψ₂ = W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2

Tactic:
by
  simp_rw [Ψ, preΨ_even, if_pos <| even_two_mul m, Int.even_add, Int.even_sub, even_two, iff_true,
    Int.not_even_one, iff_false]
  split_ifs <;> C_simp <;> ring1

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

Goal state before:
pp: case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₁) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)

Tactic:
simp only [hxy.left, hxy.right, add_of_Y_eq rfl rfl]

Goal state after:
case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ 0 =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' ⋯) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
rw [show 2 = ((1 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_two, if_neg Nat.not_even_one, Ψ₂Sq,
    preΨ'_three, preΨ'_one, if_neg Nat.not_even_one, Ψ₃]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ((X * W.preΨ₄ ^ 2 * if Even 3 then 1 else W.Ψ₂Sq) - W.preΨ' (3 + 2) * W.preΨ' 3 * if Even 3 then W.Ψ₂Sq else 1) =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
if_neg <| by decide,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.preΨ' (3 + 2) * W.preΨ' 3 * if Even 3 then W.Ψ₂Sq else 1) =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.coeff 3 ≠ 0

Tactic:
rwa [coeff_Ψ₂Sq]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₃.natDegree ≤ 4

Tactic:
rw [Ψ₃]
  compute_degree

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₃.natDegree ≤ 4

Tactic:
by
  rw [Ψ₃]
  compute_degree

Goal state after: