theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t_iff_ϕ_preimages {F : Type u_1} [Field F] [Fintype F] (t 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 ϕ_of_t := ↑(ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); have ϕ_of_neg_t := ↑(ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); ϕ_of_t = ϕ_of_neg_t ↔ ¬∃ (p : { n : F // n ≠ t ∧ n ≠ -t }), ↑(ϕ (↑p) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3) = ϕ_of_t

theorem Elligator.Elligator1.point_props_iff_point_in_ϕ_over_F_of_point {F : Type u_1} [Field F] [Fintype F] (t 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; ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ↔ ↑point ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3

theorem Elligator.Elligator1.ϕ_of_t2_eq_x_y {F : Type u_1} [Field F] [Fintype F] (t 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 x_of_t := point.1; have y_of_t := point.2; have t' := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point; have ϕ_of_t' := ↑(ϕ t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); ϕ_of_t' = (x_of_t, y_of_t)

theorem Elligator.Elligator1.X2_defined {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have y := (↑point).2; 2 * (y + 1) ≠ 0

theorem Elligator.Elligator1.z_defined {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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ^ 2 ≠ 0

theorem Elligator.Elligator1.t2_defined {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have u2_of_point := u2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; 1 + u2_of_point ≠ 0