theorem
Elligator.Elligator1.u2_eq_u
{F : Type u_1}
[Field F]
[Fintype F]
(t : { t : F // t ≠ 1 ∧ t ≠ -1 })
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(X_h :
have point := ↑(ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3);
have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point;
X2_of_t = X_of_t)
:
theorem
Elligator.Elligator1.u2_eq_u'
{F : Type u_1}
[Field F]
[Fintype F]
(t : { t : F // t ≠ 1 ∧ t ≠ -1 })
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(X_h :
have point := ↑(ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3);
have h2_2 := ⋯;
have X'_of_t := X ⟨-↑t, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point;
X2_of_t = X'_of_t)
:
have h2_2 := ⋯;
have point := ↑(ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3);
have u'_of_t := u ⟨-↑t, h2_2⟩ q field_cardinality q_prime_power q_mod_4_congruent_3;
have u2_of_t := u2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point;
u2_of_t = u'_of_t
theorem
Elligator.Elligator1.u2_h1
{F : Type u_1}
[Field F]
[Fintype F]
(t : { t : F // t ≠ 1 ∧ t ≠ -1 })
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
:
have point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3;
have h2_2 := ⋯;
have u'_of_t := u ⟨-↑t, h2_2⟩ q field_cardinality q_prime_power q_mod_4_congruent_3;
have u2_of_t := u2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
u2_of_t = u_of_t ∨ u2_of_t = u'_of_t
noncomputable def
Elligator.Elligator1.u'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
:
F
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Elligator.Elligator1.u'_pow_two_eq_X_pow_two
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
theorem
Elligator.Elligator1.u'_eq_X2_or_u'_eq_neg_X2
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
theorem
Elligator.Elligator1.u'_ne_neg_one
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
theorem
Elligator.Elligator1.one_add_u'_ne_zero
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
theorem
Elligator.Elligator1.u'_ne_zero
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
noncomputable def
Elligator.Elligator1.v'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
:
F
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Elligator.Elligator1.v'_eq_z'_mul_Y'_pow_two
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have z := z' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
X ≠ 1 → v = z * Y ^ 2
theorem
Elligator.Elligator1.v'_ne_zero
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
theorem
Elligator.Elligator1.χ_of_v'_eq_χ_of_z'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have z := z' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
have χ_of_z := LegendreSymbol.χ z q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → χ_of_v = χ_of_z
theorem
Elligator.Elligator1.χ_of_z'_eq_z'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have z := z' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_z := LegendreSymbol.χ z q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → χ_of_z = z
theorem
Elligator.Elligator1.χ_of_v'_eq_z'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have z := z' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → χ_of_v = z
theorem
Elligator.Elligator1.X'_eq_χ_of_v'_mul_u'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have u := u' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → X = χ_of_v * u
theorem
Elligator.Elligator1.Y'_pow_two_eq_χ_of_v'_mul_v'
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → Y ^ 2 = χ_of_v * v
theorem
Elligator.Elligator1.χ_of_v'_eq_z'_unfold_of_X'_ne_1
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
have c := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have term := Y * (X ^ 2 + 1 / c ^ 2);
have χ_of_term := LegendreSymbol.χ term q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → χ_of_v = χ_of_term
theorem
Elligator.Elligator1.χ_of_v'_eq_χ_Y'_mul_u'_pow_two_add_one_over_c_pow_two
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have u := u' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
have c := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have term := Y * (u ^ 2 + 1 / c ^ 2);
have χ_of_term := LegendreSymbol.χ term q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → χ_of_v = χ_of_term
theorem
Elligator.Elligator1.u'_pow_two_add_one_over_c_pow_two_ne_zero
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
:
theorem
Elligator.Elligator1.Y'_observation1
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have u := u' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_Y := LegendreSymbol.χ Y q field_cardinality q_prime_power q_mod_4_congruent_3;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
have c := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have χ_of_u'_pow_two_add_one_over_c_pow_two :=
LegendreSymbol.χ (u ^ 2 + 1 / c ^ 2) q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → χ_of_Y = χ_of_v * χ_of_u'_pow_two_add_one_over_c_pow_two
theorem
Elligator.Elligator1.Y'_observation2
{F : Type u_1}
[Field F]
[Fintype F]
(s : F)
(s_h1 : s ≠ 0)
(s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0)
(q : ℕ)
(field_cardinality : Fintype.card F = q)
(q_prime_power : IsPrimePow q)
(q_mod_4_congruent_3 : q % 4 = 3)
(point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 })
(point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point)
(x_ne_zero : (↑point).1 ≠ 0)
(y_ne_one : (↑point).2 ≠ 1)
:
have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point;
have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have v := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have u := u' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props;
have χ_of_Y := LegendreSymbol.χ Y q field_cardinality q_prime_power q_mod_4_congruent_3;
have χ_of_v := LegendreSymbol.χ v q field_cardinality q_prime_power q_mod_4_congruent_3;
have c := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have χ_of_u'_pow_two_add_one_over_c_pow_two :=
LegendreSymbol.χ (u ^ 2 + 1 / c ^ 2) q field_cardinality q_prime_power q_mod_4_congruent_3;
X ≠ 1 → Y = (χ_of_v * v) ^ ((q + 1) / 4) * χ_of_v * χ_of_u'_pow_two_add_one_over_c_pow_two