awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
simp :
  HMul.hMul (α := A) (β := A) (2 : A) ((f : (a : R) → A) W.a₄ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) W.a₁ : A) ((f : (a : R) → A) W.a₃ : A) =
    (f : (a : R) → A) (2 * W.a₄ + W.a₁ * W.a₃)
⊢ (W.map f).b₄ = (f : (a : R) → A) W.b₄

Tactic:
simp only [b₄, map_a₁, map_a₃, map_a₄]

Premises used: WeierstrassCurve.map_a₄, WeierstrassCurve.b₄, WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ HMul.hMul (α := A) (β := A) (2 : A) ((f : (a : R) → A) W.a₄ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) W.a₁ : A) ((f : (a : R) → A) W.a₃ : A) =
    (f : (a : R) → A) (2 * W.a₄ + W.a₁ * W.a₃)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
simp :
  HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₃ : A) 2 +
      HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₆ : A) =
    (f : (a : R) → A) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆)
⊢ (W.map f).b₆ = (f : (a : R) → A) W.b₆

Tactic:
simp only [b₆, map_a₃, map_a₆]

Premises used: WeierstrassCurve.map_a₆, WeierstrassCurve.map_a₃, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₃ : A) 2 +
      HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₆ : A) =
    (f : (a : R) → A) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
simp :
  HMul.hMul (β := A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₁ : A) 2) ((f : (a : R) → A) W.a₆ : A) +
            HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₂ : A))
              ((f : (a : R) → A) W.a₆ : A) -
          HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) ((f : (a : R) → A) W.a₁ : A) ((f : (a : R) → A) W.a₃ : A))
            ((f : (a : R) → A) W.a₄ : A) +
        HMul.hMul (α := A) ((f : (a : R) → A) W.a₂ : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₃ : A) 2) -
      HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₄ : A) 2 =
    (f : (a : R) → A)
      (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
        HPow.hPow (β := ℕ) W.a₄ 2)
⊢ (W.map f).b₈ = (f : (a : R) → A) W.b₈

Tactic:
simp only [b₈, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]

Premises used: WeierstrassCurve.map_a₂, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, WeierstrassCurve.b₈, WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ HMul.hMul (β := A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₁ : A) 2) ((f : (a : R) → A) W.a₆ : A) +
            HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (4 : A) ((f : (a : R) → A) W.a₂ : A))
              ((f : (a : R) → A) W.a₆ : A) -
          HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) ((f : (a : R) → A) W.a₁ : A) ((f : (a : R) → A) W.a₃ : A))
            ((f : (a : R) → A) W.a₄ : A) +
        HMul.hMul (α := A) ((f : (a : R) → A) W.a₂ : A) (HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₃ : A) 2) -
      HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.a₄ : A) 2 =
    (f : (a : R) → A)
      (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
        HPow.hPow (β := ℕ) W.a₄ 2)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
simp :
  HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 2 -
      HMul.hMul (α := A) (β := A) (24 : A) ((f : (a : R) → A) W.b₄ : A) =
    (f : (a : R) → A) (HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄)
⊢ (W.map f).c₄ = (f : (a : R) → A) W.c₄

Tactic:
simp only [c₄, map_b₂, map_b₄]

Premises used: WeierstrassCurve.c₄, WeierstrassCurve.map_b₄, WeierstrassCurve.map_b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 2 -
      HMul.hMul (α := A) (β := A) (24 : A) ((f : (a : R) → A) W.b₄ : A) =
    (f : (a : R) → A) (HPow.hPow (β := ℕ) W.b₂ 2 - 24 * W.b₄)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
simp :
  -HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 3 +
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (36 : A) ((f : (a : R) → A) W.b₂ : A))
          ((f : (a : R) → A) W.b₄ : A) -
      HMul.hMul (α := A) (β := A) (216 : A) ((f : (a : R) → A) W.b₆ : A) =
    (f : (a : R) → A) (-HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
⊢ (W.map f).c₆ = (f : (a : R) → A) W.c₆

Tactic:
simp only [c₆, map_b₂, map_b₄, map_b₆]

Premises used: WeierstrassCurve.map_b₆, WeierstrassCurve.map_b₄, WeierstrassCurve.c₆, WeierstrassCurve.map_b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ -HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 3 +
        HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (36 : A) ((f : (a : R) → A) W.b₂ : A))
          ((f : (a : R) → A) W.b₄ : A) -
      HMul.hMul (α := A) (β := A) (216 : A) ((f : (a : R) → A) W.b₆ : A) =
    (f : (a : R) → A) (-HPow.hPow (β := ℕ) W.b₂ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
simp :
  HMul.hMul (β := A) (-HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 2) ((f : (a : R) → A) W.b₈ : A) -
          8 * HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₄ : A) 3 -
        27 * HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₆ : A) 2 +
      HMul.hMul (β := A)
        (HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (9 : A) ((f : (a : R) → A) W.b₂ : A))
          ((f : (a : R) → A) W.b₄ : A))
        ((f : (a : R) → A) W.b₆ : A) =
    (f : (a : R) → A)
      (-HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
        9 * W.b₂ * W.b₄ * W.b₆)
⊢ (W.map f).Δ = (f : (a : R) → A) W.Δ

Tactic:
simp only [Δ, map_b₂, map_b₄, map_b₆, map_b₈]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.map_b₈, WeierstrassCurve.map_b₆, WeierstrassCurve.map_b₄, WeierstrassCurve.map_b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
⊢ HMul.hMul (β := A) (-HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₂ : A) 2) ((f : (a : R) → A) W.b₈ : A) -
          8 * HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₄ : A) 3 -
        27 * HPow.hPow (α := A) (β := ℕ) ((f : (a : R) → A) W.b₆ : A) 2 +
      HMul.hMul (β := A)
        (HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (9 : A) ((f : (a : R) → A) W.b₂ : A))
          ((f : (a : R) → A) W.b₄ : A))
        ((f : (a : R) → A) W.b₆ : A) =
    (f : (a : R) → A)
      (-HPow.hPow (β := ℕ) W.b₂ 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) W.b₄ 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
        9 * W.b₂ * W.b₄ * W.b₆)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
⊢ W.map (RingHom.id R) = W

Tactic:
rfl

Premises used: WeierstrassCurve.map, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
A : Type v
inst_1 : CommRing A
f : R →+* A
B : Type w
inst_2 : CommRing B
g : A →+* B
⊢ (W.map f).map g = W.map (g.comp f)

Tactic:
rfl

Premises used: WeierstrassCurve.map, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
S : Type s
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type v
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type w
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
g : A →ₐ[S] B
⊢ (W⁄A).map (↑g : A →+* B) = W⁄B

Tactic:
congrArg W.map <| g.comp_algebraMap_of_tower R

Premises used: congrArg, AlgHom.comp_algebraMap_of_tower, WeierstrassCurve.baseChange, WeierstrassCurve.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)

Tactic:
rcases mk.inj h with ⟨_, _, _, _, _⟩

Premises used: WeierstrassCurve.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)

Tactic:
rcases mk.inj h with ⟨_, _, _, _, _⟩

Premises used: WeierstrassCurve.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)

Tactic:
rcases mk.inj h with ⟨_, _, _, _, _⟩

Premises used: WeierstrassCurve.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)

Tactic:
rcases mk.inj h with ⟨_, _, _, _, _⟩

Premises used: WeierstrassCurve.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left₃ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)

Tactic:
rcases mk.inj h with ⟨_, _, _, _, _⟩

Premises used: WeierstrassCurve.mk.inj
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
a₁ : x.a₁ = x_1.a₁
a₂ : x.a₂ = x_1.a₂
a₃ : x.a₃ = x_1.a₃
a₄ : x.a₄ = x_1.a₄
a₆ : x.a₆ = x_1.a₆
⊢ x = x_1

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)

Tactic:
hf
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
a₁ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
⊢ x.a₁ = x_1.a₁

Tactic:
apply_fun _ using hf
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
a₂ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
⊢ x.a₂ = x_1.a₂

Tactic:
apply_fun _ using hf
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
a₃ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
⊢ x.a₃ = x_1.a₃

Tactic:
apply_fun _ using hf
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
a₄ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
⊢ x.a₄ = x_1.a₄

Tactic:
apply_fun _ using hf
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right a₆ : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ x.a₆ = x_1.a₆

Tactic:
apply_fun _ using hf
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑f : (a : R) → A)
x x_1 : WeierstrassCurve R
h :
  Eq.{v + 1} (α := WeierstrassCurve A) ((fun (W : WeierstrassCurve R) ↦ W.map f) x)
    ((fun (W : WeierstrassCurve R) ↦ W.map f) x_1)
left : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₁ : A) ((f : (a : R) → A) x_1.a₁ : A)
left_1 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₂ : A) ((f : (a : R) → A) x_1.a₂ : A)
left_2 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₃ : A) ((f : (a : R) → A) x_1.a₃ : A)
left_3 : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₄ : A) ((f : (a : R) → A) x_1.a₄ : A)
right : Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)
⊢ Eq.{v + 1} (α := A) ((f : (a : R) → A) x.a₆ : A) ((f : (a : R) → A) x_1.a₆ : A)

Tactic:
assumption