mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
k : Type u_2
inst✝ : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := ↑u
hu : u₀ = ↑u
h₀ : IsUnit u₀
⊢ u₀.divXPowOrder = u₀

Tactic:
]

Goal state after:
R : Type u_1
k : Type u_2
inst✝ : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := ↑u
hu : u₀ = ↑u
h₀ : IsUnit u₀
⊢ u₀.divXPowOrder = u₀
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) ≤ 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) ≤ 1
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ emultiplicity X ↑P ↔ ↑c ≤ emultiplicity Polynomial.X P

pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ↑P ≠ 0

Tactic:
]

Goal state after:
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ emultiplicity X ↑P ↔ ↑c ≤ emultiplicity Polynomial.X P

k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ↑P ≠ 0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) = 1 ↔ x ∉ v.asIdeal

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) = 1 ↔ x ∉ v.asIdeal
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
x✝ : k⟦X⟧
⊢ constantCoeff x✝ = 0 ↔ constantCoeff x✝ = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) < 1 ↔ x ∈ v.asIdeal

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) < 1 ↔ x ∈ v.asIdeal
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ↑(↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (unzero ⋯)) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ↑(↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (unzero ⋯)) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^
      (Multiplicative.toAdd (unzero ⋯) + ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors)) =
    1

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^
      (Multiplicative.toAdd (unzero ⋯) + ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors)) =
    1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) =
    0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) =
    0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ Multiplicative.toAdd (unzero ⋯) + ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors) = 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ Multiplicative.toAdd (unzero ⋯) + ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₃) =
    -48

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₃) =
    -48
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
a : v₁ = v₂
⊢ mk v₂ = mk v₂

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ((algebraMap (𝓞 K) K) x)‖ < 1
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Tactic:
]

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ((algebraMap (𝓞 K) K) x)‖ < 1
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ((algebraMap (𝓞 K) K) x)‖ < 1
hx2 : ‖(embedding v₂) ((algebraMap (𝓞 K) K) x)‖ = 1
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Tactic:
]

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ((algebraMap (𝓞 K) K) x)‖ < 1
hx2 : ‖(embedding v₂) ((algebraMap (𝓞 K) K) x)‖ = 1
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
⊢ mk v = mk v

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x✝ y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (embedding w) = ↑v
x : K
⊢ ↑v x = (HeightOneSpectrum.adicAbv K w) x

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x✝ y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (embedding w) = ↑v
x : K
⊢ ↑v x = (HeightOneSpectrum.adicAbv K w) x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 3)
⊢ IsUnit (-27)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 3)
⊢ IsUnit (-27)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ ↑(ofJ0 R).Δ'⁻¹ * 0 ^ 3 = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ ↑(ofJ0 R).Δ'⁻¹ * 0 ^ 3 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ IsUnit (-64)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ IsUnit (-64)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = -64 * 1728

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 2)
⊢ (-48) ^ 3 = -64 * 1728
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (j ^ 2 * (j - 1728) ^ 9)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (j ^ 2 * (j - 1728) ^ 9)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = j ^ 2 * (j - 1728) ^ 9 * j

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = j ^ 2 * (j - 1728) ^ 9 * j
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ ‖(embedding v.maximalIdeal) ↑x‖ * ↑(absNorm (v.maximalIdeal.maxPowDividing (span {x}))) = 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ ‖(embedding v.maximalIdeal) ↑x‖ * ↑(absNorm (v.maximalIdeal.maxPowDividing (span {x}))) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 ≠ 0
⊢ ofJ0 F = ofJ0 F

Tactic:
]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ ofJ1728 F = ofJ1728 F

Tactic:
]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ ofJ0 F = ofJ0 F

Tactic:
]

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

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ1728 F = ofJ1728 F

Tactic:
]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ ofJNe0Or1728 j = ofJNe0Or1728 j

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ1728 F).IsElliptic

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ1728 F).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ0 F).IsElliptic

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ0 F).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : 2 ≠ 0
this : Fact (IsUnit 2)
⊢ (ofJ1728 F).IsElliptic

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : 2 ≠ 0
this : Fact (IsUnit 2)
⊢ (ofJ1728 F).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this✝ : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).IsElliptic

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
this✝ : Fact (IsUnit j)
this : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).IsElliptic
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
h_dense : DenseRange ⇑Φ
⊢ closure ↑Φ.range = Set.univ

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
h_dense : DenseRange ⇑Φ
⊢ closure ↑Φ.range = Set.univ
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyConnected f
x : ↥S
⊢ _root_.IsConnected (⇑(fiberι f x) '' Set.univ)

Tactic:
]

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyConnected f
x : ↥S
⊢ _root_.IsConnected (⇑(fiberι f x) '' Set.univ)
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyConnected f
inst✝² : GeometricallyConnected g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ ConnectedSpace ↥(pullback f (pullback.fst g x))

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyConnected f
inst✝² : GeometricallyConnected g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ ConnectedSpace ↥(pullback f (pullback.fst g x))
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ Sieve.generate ⊥ ∈ (grothendieckTopology P) X

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ Sieve.generate ⊥ ∈ (grothendieckTopology P) X
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
x✝ : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ (precoverage P).coverings X
hle : R ≤ S.arrows
⊢ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
Precoverage.mem_iff_exists_zeroHypercover

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
x✝ : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
x✝ : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
x✝ : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
⊢ (Precoverage.toPretopology Scheme (precoverage P)).toGrothendieck =
    (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
⊢ (Precoverage.toPretopology Scheme (precoverage P)).toGrothendieck =
    (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
⊢ Function.Bijective (Types.sectionOfCone c) ↔ Function.Bijective (Types.sectionOfCone c)

Tactic:
]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]

Tactic:
smul_fin3,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = ![P x, W.negY P, P z]

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 -
                      (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 -
                      (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0