ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>is : List ι<VAR>hl : (i :: is).Nodup<VAR>v w : TProd α (i :: is)<VAR>hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi<GOAL>v = w
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>is : List ι<VAR>hl : (i :: is).Nodup<VAR>v w : TProd α (i :: is)<VAR>hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi<GOAL>v.1 = w.1
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>is : List ι<VAR>hl : (i :: is).Nodup<VAR>v w : TProd α (i :: is)<VAR>hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi<GOAL>v.2 = w.2
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j✝ : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>is : List ι<VAR>hl : (i :: is).Nodup<VAR>v w : TProd α (i :: is)<VAR>hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi<VAR>j : ι<VAR>hj : j ∈ is<GOAL>TProd.elim v.2 hj = TProd.elim w.2 hj
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : (i : ι) → C₁.X i ≅ C₂.X i<VAR>hf : autoParam (∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) _auto✝<VAR>i : ι<GOAL>({ f := fun i => (f i).hom, comm' := hf } ≫ { f := fun i => (f i).inv, comm' := ⋯ }).f i = (𝟙 C₁).f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : (i : ι) → C₁.X i ≅ C₂.X i<VAR>hf : autoParam (∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) _auto✝<VAR>i : ι<GOAL>({ f := fun i => (f i).inv, comm' := ⋯ } ≫ { f := fun i => (f i).hom, comm' := hf }).f i = (𝟙 C₂).f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>n : ℕ<VAR>f : α → 𝕜<VAR>g : α → R<VAR>h : IsBigOWith c l (f ^ n) (g ^ n)<VAR>hn : n ≠ 0<VAR>hc : c ≤ c' ^ n<VAR>hc' : 0 ≤ c'<VAR>x : α<VAR>hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖<GOAL>‖g x ^ n‖ ≤ ‖g x‖ ^ n
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<VAR>r : ℝ<GOAL>re (z / ↑r) = re z / r
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → ε' → ε<VAR>g' : β → γ → ε'<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)<VAR>x✝ : Set ε<GOAL>image2 f (image2 g s t) u ⊆ x✝ ↔ image2 f' s (image2 g' t u) ⊆ x✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : CanonicallyOrderedCommSemiring α<VAR>a✝ b✝ c : α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a * (b - 1) = a * b - a
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>s t : Set V<VAR>sconn : (H.induce s).Connected<VAR>tconn : (H.induce t).Connected<VAR>sintert : (s ⊓ t).Nonempty<GOAL>(H.induce (s ∪ t)).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>s t : Set V<VAR>sconn : (H.induce s).Connected<VAR>tconn : (H.induce t).Connected<VAR>sintert : (s ⊓ t).Nonempty<GOAL>H.induce s ⊔ H.induce t ≤ H.induce (s ∪ t)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>s t : Set V<VAR>sconn : (H.induce s).Connected<VAR>tconn : (H.induce t).Connected<VAR>sintert : (s ⊓ t).Nonempty<GOAL>(H.induce s ⊔ H.induce t).verts = (H.induce (s ∪ t)).verts
<VAR>y z : ℝ<VAR>n : ℕ<VAR>hy : 0 < y<VAR>hx : 0 ≤ 0<VAR>h : log 0 < z * log y<GOAL>0 < y ^ z
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : C<VAR>hA : IsSubterminal A<VAR>inst✝ : HasBinaryProduct A A<GOAL>prod.fst ≫ diag A = 𝟙 (A ⨯ A)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : C<VAR>hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g<VAR>inst✝ : HasBinaryProduct A A<GOAL>prod.fst ≫ diag A = 𝟙 (A ⨯ A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>0 < (f.cycleOf x).support.card ↔ f x ≠ x
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>simple : ∀ (i : B), p (cs.simple i)<VAR>one : p 1<VAR>mul : ∀ (w w' : W), p w → p w' → p (w * w')<GOAL>p w
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>simple : ∀ (i : B), p (cs.simple i)<VAR>one : p 1<VAR>mul : ∀ (w w' : W), p w → p w' → p (w * w')<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>p w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : ¬G.Reachable u v<GOAL>G.edist u v = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>e.symm ≈ e'.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>RightInvOn (↑e'.symm) (↑e) e'.target
<VAR>ι : Type u_1<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : succFn i ≤ i<GOAL>IsMax i
<VAR>ι : Type u_1<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : succFn i ≤ i<VAR>j : ι<VAR>x✝ : i ≤ j<VAR>hij_lt : i < j<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : succFn i ≤ i<VAR>j : ι<VAR>x✝ : i ≤ j<VAR>hij_lt : i < j<VAR>h_succFn_eq : succFn i = i<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : succFn i ≤ i<VAR>j : ι<VAR>x✝ : i ≤ j<VAR>hij_lt : i < j<VAR>h_succFn_eq : succFn i = i<VAR>h_glb : IsGLB (↑(Finset.Ioc i j)) i<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : succFn i ≤ i<VAR>j : ι<VAR>x✝ : i ≤ j<VAR>hij_lt : i < j<VAR>h_succFn_eq : succFn i = i<VAR>h_glb : IsGLB (↑(Finset.Ioc i j)) i<VAR>hi_mem : i ∈ Finset.Ioc i j<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : LocallyFiniteOrder ι<VAR>i : ι<VAR>hi : succFn i ≤ i<VAR>j : ι<VAR>x✝ : i ≤ j<VAR>hij_lt : i < j<VAR>h_succFn_eq : succFn i = i<VAR>h_glb : IsGLB (↑(Finset.Ioc i j)) i<VAR>hi_mem : i < i ∧ i ≤ j<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<GOAL>HasSum (fun n => (p.changeOrigin y n) fun x => z) (f (x + y + z))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<VAR>this : f (x + y + z) = (p.changeOrigin y).sum z<GOAL>HasSum (fun n => (p.changeOrigin y n) fun x => z) (f (x + y + z))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<VAR>this : f (x + y + z) = (p.changeOrigin y).sum z<GOAL>HasSum (fun n => (p.changeOrigin y n) fun x => z) ((p.changeOrigin y).sum z)
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>g : M<VAR>r : R<GOAL>r ∈ (span R {g}).annihilator ↔ r • g = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : Group G<VAR>a : G<VAR>l : List G<VAR>hl : (a :: l).prod = 1<VAR>n : ℕ<GOAL>((a :: l).rotate n).prod = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : Group G<VAR>a : G<VAR>l : List G<VAR>hl : (a :: l).prod = 1<VAR>n : ℕ<VAR>this : n % (a :: l).length ≤ (a :: l).length<GOAL>((a :: l).rotate n).prod = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : Group G<VAR>a : G<VAR>l : List G<VAR>n : ℕ<VAR>hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1<VAR>this : n % (a :: l).length ≤ (a :: l).length<GOAL>((a :: l).rotate n).prod = 1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<GOAL>IsClosed {x | ClusterPt x f}
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<GOAL>IsClosed (⋂ i, {x | (¬∀ᶠ (x : X) in 𝓝 x, i x) ∨ ∃ᶠ (x : X) in f, i x})
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<VAR>p : X → Prop<GOAL>IsOpen fun x => (𝓝 x).sets {x | (fun x => p x) x}
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<VAR>p : X → Prop<GOAL>IsOpen fun x => f.sets {x | (fun x => ¬(fun x => p x) x) x}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : AEMeasurable φ μ<VAR>f : β → G<VAR>hfm : AEStronglyMeasurable f (Measure.map φ μ)<VAR>g : β → G := AEStronglyMeasurable.mk f hfm<GOAL>Measure.map φ μ = Measure.map (AEMeasurable.mk φ hφ) μ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m i : ℤ<VAR>z : Cochain F G 0<VAR>hz : z ∈ cocycle F G 0<GOAL>z.v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m i : ℤ<VAR>z : Cochain F G 0<VAR>hz : δ 0 1 z = 0<GOAL>z.v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) ⋯
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hnmcp : n.gcd m = 1<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hnmcp : n.gcd m = 1<VAR>hmncp : m.gcd n = 1<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hnmcp : n.gcd m = 1<VAR>hmncp : m.gcd n = 1<VAR>hm2 : m % 2 = 0<VAR>hn2 : n % 2 = 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hnmcp : n.gcd m = 1<VAR>hmncp : m.gcd n = 1<VAR>hm2 : m % 2 = 0<VAR>hn2 : n % 2 = 1<GOAL>h.IsPrimitiveClassified