mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : (f₁.restrict W hW hWl).hom = (f₂.restrict W hW hWr).hom
⊢ f₁.compHom g ≈ f₂.compHom g

Tactic:
refine ⟨W, hW, hWl, hWr, ?_⟩

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : (f₁.restrict W hW hWl).hom = (f₂.restrict W hW hWr).hom
⊢ ((f₁.compHom g).restrict W hW hWl).hom = ((f₂.compHom g).restrict W hW hWr).hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
by
  dsimp [RationalMap.toPartialMap]
  refine (f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_
  generalize_proofs _ _ H _
  have : H.choose = f := (equiv_iff_of_domain_eq_of_isSeparated (S := ⊤_ _) H.choose_spec.2).mp
    (toRationalMap_eq_iff.mp H.choose_spec.1)
  exact ((ext_iff _ _).mp this.symm).choose_spec.symm

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
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch

Goal state after:
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
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)
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
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch

Goal state after:
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
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)
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₂.representative.toRationalMap).representative.equiv
    (f₁.representative.comp f₂.representative.toRationalMap.representative)

Tactic:
comp_def

Goal state after:
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₁.representative.comp f₂.representative).toRationalMap.representative.equiv
    (f₁.representative.comp f₂.representative.toRationalMap.representative)
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_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
⊢ (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    d.transitionMap hij

Tactic:
apply (isColimitOfPreserves (Over.map _ (d.prop_trans hij)) (d.isColimit i)).hom_ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt := ⋯
⊢ ∀ (j_1 : J),
    ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j_1 ≫
        (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
          (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
      ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j_1 ≫ d.transitionMap hij
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
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : D
ε : (a : α) → e.functor.obj (X a) ⟶ W✝
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W✝
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
⊢ m =
    (e.toAdjunction.homEquiv B W✝).symm (EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯)

Tactic:
simp only [Adjunction.homEquiv_counit,
      Equivalence.toAdjunction_counit]
    have := EffectiveEpiFamily.uniq X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h)
    specialize this (e.unit.app _ ≫ e.inverse.map m) fun a ↦ ?_
    · rw [← congrArg e.inverse.map (hm a)]
      simp
    · simp [← this]

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 := ⋯
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
⊢ m.left =
    {
        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 }.left

Tactic:
refine 𝒱.hom_ext _ _ fun i ↦ ?_

Goal state after:
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.458} 𝒰.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.458} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
⊢ 𝒱.f i ≫ m.left =
    𝒱.f i ≫
      {
          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 }.left
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.a₁ ^ 2 + 4 * f W.a₂ = f (W.a₁ ^ 2 + 4 * W.a₂)

Tactic:
map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ 2 * f W.a₄ + f W.a₁ * f W.a₃ = f (2 * W.a₄ + W.a₁ * W.a₃)

Tactic:
map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.a₃ ^ 2 + 4 * f W.a₆ = f (W.a₃ ^ 2 + 4 * W.a₆)

Tactic:
map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.a₁ ^ 2 * f W.a₆ + 4 * f W.a₂ * f W.a₆ - f W.a₁ * f W.a₃ * f W.a₄ + f W.a₂ * f W.a₃ ^ 2 - f W.a₄ ^ 2 =
    f (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2)

Tactic:
map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ f W.b₂ ^ 2 - 24 * f W.b₄ = f (W.b₂ ^ 2 - 24 * W.b₄)

Tactic:
map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ -f W.b₂ ^ 3 + 36 * f W.b₂ * f W.b₄ - 216 * f W.b₆ = f (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)

Tactic:
map_simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ -f W.b₂ ^ 2 * f W.b₈ - 8 * f W.b₄ ^ 3 - 27 * f W.b₆ ^ 2 + 9 * f W.b₂ * f W.b₄ * f W.b₆ =
    f (-W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) =
    C 0 * Y ^ 3 + C 1 * Y ^ 2 + C (C 0 * X ^ 3 + C 0 * X ^ 2 + C W.a₁ * X + C W.a₃) * Y +
      C (C (-1) * X ^ 3 + C (-W.a₂) * X ^ 2 + C (-W.a₄) * X + C (-W.a₆))

Tactic:
map_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
⊢ Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)) =
    C 0 * Y ^ 3 + C 1 * Y ^ 2 + (C (C 0) * C X ^ 3 + C (C 0) * C X ^ 2 + C (C W.a₁) * C X + C (C W.a₃)) * Y +
      (-C (C 1) * C X ^ 3 + -C (C W.a₂) * C X ^ 2 + -C (C W.a₄) * C X + -C (C W.a₆))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ Y ^ 2 + C (C (W.map f).a₁ * X + C (W.map f).a₃) * Y -
      C (X ^ 3 + C (W.map f).a₂ * X ^ 2 + C (W.map f).a₄ * X + C (W.map f).a₆) =
    Polynomial.map (mapRingHom f)
      (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ C (C (W.map f).a₁) * Y - C (C 3 * X ^ 2 + C (2 * (W.map f).a₂) * X + C (W.map f).a₄) =
    Polynomial.map (mapRingHom f) (C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄))

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ C (C 2) * Y + C (C (W.map f).a₁ * X + C (W.map f).a₃) =
    Polynomial.map (mapRingHom f) (C (C 2) * Y + C (C W.a₁ * X + C W.a₃))

Tactic:
map_simp

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

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ ↑{ u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
          t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.u =
    ↑{ u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
          s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
          t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.u

Tactic:
map_simp

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

Goal state before:
pp: case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.r =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.r

Tactic:
map_simp

Goal state after:
case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ C.r * φ ↑C'.u ^ 2 + φ C'.r = φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.s =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.s

Tactic:
map_simp

Goal state after:
case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ ↑C'.u * φ C.s + φ C'.s = ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.t =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.t

Tactic:
map_simp

Goal state after:
case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ C.t * φ ↑C'.u ^ 3 + φ C.r * φ C'.s * φ ↑C'.u ^ 2 + φ C'.t =
    φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₁
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
        a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
        a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
        a₄ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
            (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
              2 * φ C.s * φ C.t),
        a₆ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
            (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
              φ C.r * φ C.t * φ W.a₁) }.a₁ =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
        a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
        a₄ :=
          φ
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
        a₆ :=
          φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }.a₁

Tactic:
map_simp

Goal state after:
case a₁
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s) = φ ↑C.u⁻¹ * (φ W.a₁ + 2 * φ C.s)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₂
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
        a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
        a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
        a₄ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
            (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
              2 * φ C.s * φ C.t),
        a₆ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
            (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
              φ C.r * φ C.t * φ W.a₁) }.a₂ =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
        a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
        a₄ :=
          φ
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
        a₆ :=
          φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }.a₂

Tactic:
map_simp

Goal state after:
case a₂
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2) =
    φ ↑C.u⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₃
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
        a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
        a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
        a₄ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
            (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
              2 * φ C.s * φ C.t),
        a₆ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
            (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
              φ C.r * φ C.t * φ W.a₁) }.a₃ =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
        a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
        a₄ :=
          φ
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
        a₆ :=
          φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }.a₃

Tactic:
map_simp

Goal state after:
case a₃
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t) =
    φ ↑C.u⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₄
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
        a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
        a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
        a₄ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
            (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
              2 * φ C.s * φ C.t),
        a₆ :=
          ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
            (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
              φ C.r * φ C.t * φ W.a₁) }.a₄ =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
        a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
        a₄ :=
          φ
            (↑C.u⁻¹ ^ 4 *
              (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
        a₆ :=
          φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }.a₄

Tactic:
map_simp

Goal state after:
case a₄
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
      (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
        2 * φ C.s * φ C.t) =
    φ ↑C.u⁻¹ ^ 4 *
      (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
        2 * φ C.s * φ C.t)