theorem Elligator.Elligator1.Y_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y_of_t ≠ 0

theorem Elligator.Elligator1.X_mul_Y_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X_of_t * Y_of_t ≠ 0

theorem Elligator.Elligator1.one_add_X_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; 1 + X_of_t ≠ 0

theorem Elligator.Elligator1.Y_comparison {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) : let t1 := ↑t; let t2 := -t1; have h2_2 := ⋯; have X1 := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2 := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y1 := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y2 := Y ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y2 = Y1 / X1 ^ 3