ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : E<VAR>hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source<GOAL>((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range ↑I] x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : E<VAR>hx : x ∈ ↑I '' (f.symm ≫ₕ f').source<GOAL>↑I '' (f.symm ≫ₕ f').source ∈ 𝓝[range ↑I] x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : H<VAR>hx : x ∈ (f.symm ≫ₕ f').source<GOAL>↑I '' (f.symm ≫ₕ f').source ∈ 𝓝[range ↑I] ↑I x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : H<VAR>hx : x ∈ (f.symm ≫ₕ f').source<GOAL>(f.symm ≫ₕ f').source ∈ 𝓝 x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b c a : α<GOAL>a ≤ ⊤ᶜ ↔ a ≤ ⊥
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r✝ : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>r : β → β → Prop<VAR>inst✝ : IsTrans β r<VAR>f : ℤ → β<VAR>h : ∀ (n : ℤ), r (f n) (f (n + 1))<VAR>a b : ℤ<VAR>hab : a < b<GOAL>r (f a) (f b)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r✝ : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>r : β → β → Prop<VAR>inst✝ : IsTrans β r<VAR>f : ℤ → β<VAR>h : ∀ (n : ℤ), r (f n) (f (n + 1))<VAR>a : ℤ<VAR>n : ℕ<VAR>hab : a < a + ↑n.succ<GOAL>r (f a) (f (a + ↑n.succ))
<VAR>a✝ b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n a : ℕ<VAR>ha : 0 < a<GOAL>(∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n
<VAR>a✝ b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n a : ℕ<VAR>ha : 0 < a<VAR>han : ¬a ∣ n<GOAL>a * (n / a) ≠ n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>∡ p₁ s.center p₂ = ↑π - 2 • ∡ s.center p₂ p₁
<VAR>q : ℚ<VAR>q_pos : 0 < q<GOAL>(fract q⁻¹).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<GOAL>(fract q⁻¹).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<GOAL>(fract q⁻¹).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<GOAL>(fract q⁻¹).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<VAR>q_inv_eq : q⁻¹ = q_inv<GOAL>(fract q⁻¹).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<VAR>q_inv_eq : q⁻¹ = q_inv<GOAL>(q_inv - ↑⌊q_inv⌋).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<VAR>q_inv_eq : q⁻¹ = q_inv<GOAL>((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<VAR>q_inv_eq : q⁻¹ = q_inv<GOAL>↑q.den - q.num * ⌊q_inv⌋ < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<VAR>q_inv_eq : q⁻¹ = q_inv<VAR>q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den<GOAL>↑q.den - q.num * ⌊q_inv⌋ < q.num
<VAR>q : ℚ<VAR>q_pos : 0 < q<VAR>q_num_pos : 0 < q.num<VAR>q_num_abs_eq_q_num : ↑q.num.natAbs = q.num<VAR>q_inv : ℚ := ↑q.den / ↑q.num<VAR>q_inv_def : q_inv = ↑q.den / ↑q.num<VAR>q_inv_eq : q⁻¹ = q_inv<VAR>q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den<VAR>this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs<GOAL>↑q.den - q.num * ⌊q_inv⌋ < q.num
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>hb2 : 2 ∣ b<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = m * (r * s)<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = m * (r * s)<VAR>hrsz : r * s ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = m * (r * s)<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = m * (r * s)<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi : m = i ^ 2 ∨ m = -i ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = m * (r * s)<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi : m = i ^ 2 ∨ m = -i ^ 2<VAR>hi' : ¬m = -i ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = m * (r * s)<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : m.gcd (r * s) = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd : r * s = d ^ 2 ∨ r * s = -d ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd : r * s = d ^ 2 ∨ r * s = -d ^ 2<VAR>hd' : ¬r * s = -d ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : r * s = d ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : r * s = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : r * s = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<VAR>ht : PythagoreanTriple (a ^ 2) (b ^ 2) c<VAR>h2 : (a ^ 2).gcd (b ^ 2) = 1<VAR>ha22 : a ^ 2 % 2 = 1<VAR>m n : ℤ<VAR>ht1 : a ^ 2 = m ^ 2 - n ^ 2<VAR>ht2 : b ^ 2 = 2 * m * n<VAR>ht3 : c = m ^ 2 + n ^ 2<VAR>ht4 : m.gcd n = 1<VAR>ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>ht6 : 0 ≤ m<VAR>htt : PythagoreanTriple a n m<VAR>h3 : a.gcd n = 1<VAR>hb20 : b ^ 2 ≠ 0<VAR>h4 : 0 < m<VAR>r s : ℤ<VAR>left✝ : a = r ^ 2 - s ^ 2<VAR>htt2 : n = 2 * r * s<VAR>htt3 : m = r ^ 2 + s ^ 2<VAR>htt4 : r.gcd s = 1<VAR>htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0<VAR>htt6 : 0 ≤ r<VAR>hcp : (r * s).gcd m = 1<VAR>b' : ℤ<VAR>hb2' : b = 2 * b'<VAR>hs : b' ^ 2 = r * s * m<VAR>hrsz : r * s ≠ 0<VAR>h2b0 : b' ≠ 0<VAR>i : ℤ<VAR>hi' : ¬m = -i ^ 2<VAR>hi : m = i ^ 2<VAR>d : ℤ<VAR>hd' : ¬r * s = -d ^ 2<VAR>hd : s * r = d ^ 2<VAR>j : ℤ<VAR>hj : r = j ^ 2 ∨ r = -j ^ 2<VAR>hj0 : j ≠ 0<GOAL>False