ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<VAR>x ζ : (𝓞 K)ˣ<VAR>f : Fin (rank K) → ℤ<VAR>hζ : ζ ∈ torsion K<VAR>h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i<GOAL>f = ⇑((basisModTorsion K).repr (Additive.ofMul ↑x))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<VAR>x ζ : (𝓞 K)ˣ<VAR>f : Fin (rank K) → ℤ<VAR>hζ : ζ ∈ torsion K<VAR>h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i<GOAL>Additive.ofMul ↑x = ∑ i : Fin (rank K), f i • (basisModTorsion K) i
<VAR>X₀ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁴ : TopologicalSpace X₀<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : LocallyCompactSpace Y<VAR>f : X₀ → X<VAR>hf : QuotientMap f<VAR>g : Y × X → Z<VAR>hg : Continuous fun p => g (p.1, f p.2)<GOAL>Continuous g
<VAR>X₀ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁴ : TopologicalSpace X₀<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : LocallyCompactSpace Y<VAR>f : X₀ → X<VAR>hf : QuotientMap f<VAR>g : Y × X → Z<VAR>hg : Continuous fun p => g (p.1, f p.2)<VAR>this : Continuous fun p => g (p.swap.1, f p.swap.2)<GOAL>Continuous g
<VAR>X₀ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁴ : TopologicalSpace X₀<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : LocallyCompactSpace Y<VAR>f : X₀ → X<VAR>hf : QuotientMap f<VAR>g : Y × X → Z<VAR>hg : Continuous fun p => g (p.1, f p.2)<VAR>this✝ : Continuous fun p => g (p.swap.1, f p.swap.2)<VAR>this : Continuous fun p => (g ∘ Prod.swap) (f p.1, p.2)<GOAL>Continuous g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F G F' G' : C ⥤ D<VAR>α : F ⟶ G<VAR>β : F' ⟶ G'<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(F.map f ⊗ F'.map f) ≫ (α.app Y ⊗ β.app Y) = (α.app X ⊗ β.app X) ≫ (G.map f ⊗ G'.map f)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a✝ b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>n : ℕ<VAR>r : R<VAR>nN : n ≤ N<GOAL>i (r * a ^ n * b ^ (N - n)) = i b ^ N * eval (i a * bi) (Polynomial.map i (C r * X ^ n))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a✝ b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>n : ℕ<VAR>r : R<VAR>nN : n ≤ N<GOAL>i (r * a ^ n * b ^ (N - n)) = i b ^ N * (i r * eval (i a * bi) X ^ n)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a✝ b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>n : ℕ<VAR>r : R<VAR>nN : n ≤ N<GOAL>i b ^ (N - n) * (i r * i a ^ n) = i b ^ N * (i r * (i a * bi) ^ n)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a✝ b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>n : ℕ<VAR>r : R<VAR>nN : n ≤ N<GOAL>i b ^ (N - n + n - n) * (i r * i a ^ n) = i b ^ (N - n + n) * (i r * (i a * bi) ^ n)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a✝ b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<VAR>n : ℕ<VAR>r : R<VAR>nN : n ≤ N<GOAL>i b ^ (N - n + n - n) * (i r * (i a * (bi * i b)) ^ n) = i b ^ (N - n + n) * (i r * (i a * bi) ^ n)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>a : Γ<VAR>l : ListBlank Γ<VAR>f : Γ → List Γ'<VAR>hf : ∃ n, f default = List.replicate n default<GOAL>(cons a l).bind f hf = append (f a) (l.bind f hf)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>a : Γ<VAR>l✝ : ListBlank Γ<VAR>f : Γ → List Γ'<VAR>hf : ∃ n, f default = List.replicate n default<VAR>l : List Γ<GOAL>(cons a ⟦l⟧).bind f hf = append (f a) (bind ⟦l⟧ f hf)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>a : Γ<VAR>l✝ : ListBlank Γ<VAR>f : Γ → List Γ'<VAR>hf : ∃ n, f default = List.replicate n default<VAR>l : List Γ<GOAL>(cons a (mk l)).bind f hf = append (f a) ((mk l).bind f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<GOAL>s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<GOAL>↑s.encard.toNat = 3 ↔ s.encard = 3
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R Q<VAR>inst✝ : Module R S<VAR>f g : N →ₗ[R] P<GOAL>lTensor M (f - g) = lTensor M f - lTensor M g
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R Q<VAR>inst✝ : Module R S<VAR>f g : N →ₗ[R] P<GOAL>(lTensorHom M) (f - g) = (lTensorHom M) f - (lTensorHom M) g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v f : E<VAR>is_lax_milgram : ∀ (w : E), ⟪f, w⟫_𝕜 = (B v) w<GOAL>f = B♯ v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v f : E<VAR>is_lax_milgram : ∀ (w : E), ⟪f, w⟫_𝕜 = (B v) w<GOAL>∀ (v_1 : E), ⟪f, v_1⟫_𝕜 = ⟪B♯ v, v_1⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v f : E<VAR>is_lax_milgram : ∀ (w : E), ⟪f, w⟫_𝕜 = (B v) w<VAR>w : E<GOAL>⟪f, w⟫_𝕜 = ⟪B♯ v, w⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v f : E<VAR>is_lax_milgram : ∀ (w : E), ⟪f, w⟫_𝕜 = (B v) w<VAR>w : E<GOAL>⟪f, w⟫_𝕜 = (B v) w
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>x : F<VAR>hx : x ≠ 0<GOAL>(C x * f).natSepDegree = f.natSepDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom (range Iic)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>MeasurableSpace.generateFrom (range Ioi) = MeasurableSpace.generateFrom (range Iic)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>MeasurableSpace.generateFrom (range Ioi) ≤ MeasurableSpace.generateFrom (range Iic)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>((taylor r) f).coeff 1 = eval r (derivative f)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s✝ t : Set E<VAR>x✝ y x : E<VAR>s : Set E<GOAL>infEdist x⁻¹ s⁻¹ = infEdist x s
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c₁ * f x ≤ f u
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : DecidableEq ι<VAR>C : (⨁ (i : ι), β i) → Prop<VAR>x : ⨁ (i : ι), β i<VAR>H_zero : C 0<VAR>H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)<VAR>H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)<GOAL>C x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : DecidableEq ι<VAR>C : (⨁ (i : ι), β i) → Prop<VAR>x : ⨁ (i : ι), β i<VAR>H_zero : C 0<VAR>H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)<VAR>H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)<GOAL>∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → C f → C (DFinsupp.single i b + f)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : DecidableEq ι<VAR>C : (⨁ (i : ι), β i) → Prop<VAR>x : ⨁ (i : ι), β i<VAR>H_zero : C 0<VAR>H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)<VAR>H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)<VAR>i : ι<VAR>b : β i<VAR>f : Π₀ (i : ι), β i<VAR>h1 : f i = 0<VAR>h2 : b ≠ 0<VAR>ih : C f<GOAL>C (DFinsupp.single i b + f)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s₁ s₂ : Set P<VAR>h : affineSpan k s₁ ∥ affineSpan k s₂<GOAL>vectorSpan k s₁ = vectorSpan k s₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s₁ s₂ : Set P<VAR>h : affineSpan k s₁ ∥ affineSpan k s₂<GOAL>(affineSpan k s₁).direction = (affineSpan k s₂).direction
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.432420, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>X : HomologicalComplex C (ComplexShape.up ℤ)<GOAL>contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.432420, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>X : HomologicalComplex C (ComplexShape.up ℤ)<VAR>h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))<GOAL>contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<GOAL>MeromorphicAt (-f) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<GOAL>-f = (fun x => -1) • f
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>z : 𝕜<GOAL>(-f) z = ((fun x => -1) • f) z
<VAR>x : ℂ<GOAL>sin x = -1 ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x
<VAR>x : ℂ<GOAL>(∃ k, ↑k * (2 * ↑π) = x + ↑π / 2) ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x y : 𝕜<GOAL>{ toFun := fun x => ↑(RCLike.re x) + ↑(RCLike.im x) * I, invFun := fun x => ↑x.re + ↑x.im * RCLike.I, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := fun x => ↑(RCLike.re x) + ↑(RCLike.im x) * I, invFun := fun x => ↑x.re + ↑x.im * RCLike.I, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun x => ↑(RCLike.re x) + ↑(RCLike.im x) * I, invFun := fun x => ↑x.re + ↑x.im * RCLike.I, left_inv := ⋯, right_inv := ⋯ }.toFun y
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x y : 𝕜<GOAL>↑(RCLike.re x) + ↑(RCLike.re y) + (↑(RCLike.im x) + ↑(RCLike.im y)) * I = ↑(RCLike.re x) + ↑(RCLike.im x) * I + (↑(RCLike.re y) + ↑(RCLike.im y) * I)
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x y : 𝕜<GOAL>{ toFun := fun x => ↑(RCLike.re x) + ↑(RCLike.im x) * I, invFun := fun x => ↑x.re + ↑x.im * RCLike.I, left_inv := ⋯, right_inv := ⋯ }.toFun (x * y) = { toFun := fun x => ↑(RCLike.re x) + ↑(RCLike.im x) * I, invFun := fun x => ↑x.re + ↑x.im * RCLike.I, left_inv := ⋯, right_inv := ⋯ }.toFun x * { toFun := fun x => ↑(RCLike.re x) + ↑(RCLike.im x) * I, invFun := fun x => ↑x.re + ↑x.im * RCLike.I, left_inv := ⋯, right_inv := ⋯ }.toFun y
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x y : 𝕜<GOAL>↑(RCLike.re x) * ↑(RCLike.re y) - ↑(RCLike.im x) * ↑(RCLike.im y) + (↑(RCLike.re x) * ↑(RCLike.im y) + ↑(RCLike.im x) * ↑(RCLike.re y)) * I = (↑(RCLike.re x) + ↑(RCLike.im x) * I) * (↑(RCLike.re y) + ↑(RCLike.im y) * I)
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x y : 𝕜<GOAL>↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + (↑(RCLike.re y) * ↑(RCLike.im x) * I - ↑(RCLike.im x) * ↑(RCLike.im y)) = ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I + ↑(RCLike.im x) * ↑(RCLike.im y) * I ^ 2
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x y : 𝕜<GOAL>↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + (↑(RCLike.re y) * ↑(RCLike.im x) * I - ↑(RCLike.im x) * ↑(RCLike.im y)) = ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I + ↑(RCLike.im x) * ↑(RCLike.im y) * -1
<VAR>m n : Nat<GOAL>∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n
<VAR>n N : ℕ<GOAL>(List.filter (fun x => decide (x < N)) n.primeFactorsList).prod ∈ N.smoothNumbers
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : Fork f g<GOAL>s.π.app one = s.ι ≫ f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hyz : s.WOppSide y z<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hyz : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ z)<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)<GOAL>p₂ -ᵥ y = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)<VAR>h : p₂ -ᵥ y = 0<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)<VAR>h : p₂ = y<GOAL>False
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsColimit (CokernelCofork.ofπ 0 ⋯)<VAR>Z✝ : C<VAR>u v : Y ⟶ Z✝<VAR>huv : f ≫ u = f ≫ v<VAR>W : C<VAR>w : Y ⟶ W<VAR>hw : equalizer.ι u v ≫ w = 0<VAR>hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)<VAR>m : X ⟶ equalizer u v<VAR>hm : m ≫ equalizer.ι u v = f<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsColimit (CokernelCofork.ofπ 0 ⋯)<VAR>Z✝ : C<VAR>u v : Y ⟶ Z✝<VAR>huv : f ≫ u = f ≫ v<VAR>W : C<VAR>w : Y ⟶ W<VAR>hw : equalizer.ι u v ≫ w = 0<VAR>hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)<VAR>m : X ⟶ equalizer u v<VAR>hm : m ≫ equalizer.ι u v = f<VAR>hwf : f ≫ w = 0<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsColimit (CokernelCofork.ofπ 0 ⋯)<VAR>Z✝ : C<VAR>u v : Y ⟶ Z✝<VAR>huv : f ≫ u = f ≫ v<VAR>W : C<VAR>w : Y ⟶ W<VAR>hw : equalizer.ι u v ≫ w = 0<VAR>hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)<VAR>m : X ⟶ equalizer u v<VAR>hm : m ≫ equalizer.ι u v = f<VAR>hwf : f ≫ w = 0<VAR>n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W<VAR>hn : Cofork.π (CokernelCofork.ofπ 0 ⋯) ≫ n = w<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsColimit (CokernelCofork.ofπ 0 ⋯)<VAR>Z✝ : C<VAR>u v : Y ⟶ Z✝<VAR>huv : f ≫ u = f ≫ v<VAR>W : C<VAR>w : Y ⟶ W<VAR>hw : equalizer.ι u v ≫ w = 0<VAR>hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)<VAR>m : X ⟶ equalizer u v<VAR>hm : m ≫ equalizer.ι u v = f<VAR>hwf : f ≫ w = 0<VAR>n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W<VAR>hn : 0 = w<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsColimit (CokernelCofork.ofπ 0 ⋯)<VAR>Z✝ : C<VAR>u v : Y ⟶ Z✝<VAR>huv : f ≫ u = f ≫ v<VAR>W : C<VAR>w : Y ⟶ W<VAR>hw : equalizer.ι u v ≫ w = 0<VAR>hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)<VAR>m : X ⟶ equalizer u v<VAR>hm : m ≫ equalizer.ι u v = f<VAR>hwf : f ≫ w = 0<VAR>n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W<VAR>hn : 0 = w<VAR>this : IsIso (equalizer.ι u v)<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : NormalMonoCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsColimit (CokernelCofork.ofπ 0 ⋯)<VAR>Z✝ : C<VAR>u v : Y ⟶ Z✝<VAR>huv : f ≫ u = f ≫ v<VAR>W : C<VAR>w : Y ⟶ W<VAR>hw : equalizer.ι u v ≫ w = 0<VAR>hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)<VAR>m : X ⟶ equalizer u v<VAR>hm : m ≫ equalizer.ι u v = f<VAR>hwf : f ≫ w = 0<VAR>n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W<VAR>hn : 0 = w<VAR>this : IsIso (equalizer.ι u v)<GOAL>equalizer.ι u v ≫ u = equalizer.ι u v ≫ v
<VAR>x✝ y✝ z✝ : ℤ<VAR>h✝ : PythagoreanTriple x✝ y✝ z✝<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h_coprime : x.gcd y = 1<VAR>h_parity : x % 2 = 1<VAR>h_pos : 0 < z<GOAL>∃ m n, x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
<VAR>x✝ y✝ z✝ : ℤ<VAR>h✝ : PythagoreanTriple x✝ y✝ z✝<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h_coprime : x.gcd y = 1<VAR>h_parity : x % 2 = 1<VAR>h_pos : 0 < z<VAR>m n : ℤ<VAR>ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2<VAR>ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)<VAR>ht3 : m.gcd n = 1<VAR>ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<GOAL>∃ m n, x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
<VAR>x✝ y✝ z✝ : ℤ<VAR>h✝ : PythagoreanTriple x✝ y✝ z✝<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h_coprime : x.gcd y = 1<VAR>h_parity : x % 2 = 1<VAR>h_pos : 0 < z<VAR>m n : ℤ<VAR>ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2<VAR>ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)<VAR>ht3 : m.gcd n = 1<VAR>ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hm : 0 ≤ m<GOAL>∃ m n, x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m