mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M}, U ∈ {U | ∃ i, U = ↑(B i)} → ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ -x) ⁻¹' U

Tactic:
rintro _ ⟨i, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ -x) ⁻¹' ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ -x) ⁻¹' ↑(B i)

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ -x) ⁻¹' ↑(B i)

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ -x) ⁻¹' ↑(B i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' ↑(B i)

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' ↑(B i)

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M}, U ∈ {U | ∃ i, U = ↑(B i)} → ∃ V ∈ 𝓝 0, ∃ W ∈ {U | ∃ i, U = ↑(B i)}, V • W ⊆ U

Tactic:
rintro _ ⟨i, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ {U | ∃ i, U = ↑(B i)}, V • W ⊆ ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ ∈ 𝓝 0

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ W ∈ {U | ∃ i, U = ↑(B i)}, univ • W ⊆ ↑(B i)

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ ∈ 𝓝 0
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ W ∈ {U | ∃ i, U = ↑(B i)}, univ • W ⊆ ↑(B i)

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ W ∈ {U | ∃ i, U = ↑(B i)}, univ • W ⊆ ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ • ↑(B i) ⊆ ↑(B i)

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ • ↑(B i) ⊆ ↑(B i)

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ • ↑(B i) ⊆ ↑(B i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧

pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ • x) ⁻¹' ↑(B i)

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ • x) ⁻¹' ↑(B i)

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ • x) ⁻¹' ↑(B i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ addZ P Q = -(Q x * P z) * P z

Tactic:
rw [addZ, hQz]

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * 0 ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ ↑(B i) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ (B i).toAddSubgroup.carrier

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ ↑(B i) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ (B i).toAddSubgroup.carrier

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ (B i).toAddSubgroup.carrier
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz,

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
·

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q