ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>l : List ℕ<VAR>k : ℕ<GOAL>l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>s t : Set ι<VAR>f✝ g✝ : ι → M₀<VAR>i✝ : ι<VAR>f g : ι → M₀<VAR>i : ι<GOAL>(s ∩ t).indicator (fun j => f j * g j) i = s.indicator f i * t.indicator g i
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>s t : Set ι<VAR>f✝ g✝ : ι → M₀<VAR>i✝ : ι<VAR>f g : ι → M₀<VAR>i : ι<GOAL>s.indicator (t.indicator fun j => f j * g j) i = s.indicator f i * t.indicator g i
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N₁ N₂ : L.Substructure M<VAR>hN₁ : N₁.CG<VAR>hN₂ : N₂.CG<VAR>t₁ : Set M<VAR>ht₁ : t₁.Countable ∧ (closure L).toFun t₁ = N₁<VAR>t₂ : Set M<VAR>ht₂ : t₂.Countable ∧ (closure L).toFun t₂ = N₂<GOAL>(closure L).toFun (t₁ ∪ t₂) = N₁ ⊔ N₂
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<VAR>σ : ↥H<VAR>hσ : orderOf σ = Fintype.card α<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<VAR>σ : ↥H<VAR>hσ : orderOf σ = Fintype.card α<VAR>hσ1 : orderOf ↑σ = Fintype.card α<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<VAR>σ : ↥H<VAR>hσ : orderOf σ = Fintype.card α<VAR>hσ1 : orderOf ↑σ = Fintype.card α<VAR>hσ2 : (↑σ).IsCycle<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<VAR>σ : ↥H<VAR>hσ : orderOf σ = Fintype.card α<VAR>hσ1 : orderOf ↑σ = Fintype.card α<VAR>hσ2 : (↑σ).IsCycle<VAR>hσ3 : (↑σ).support = ⊤<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<VAR>σ : ↥H<VAR>hσ : orderOf σ = Fintype.card α<VAR>hσ1 : orderOf ↑σ = Fintype.card α<VAR>hσ2 : (↑σ).IsCycle<VAR>hσ3 : (↑σ).support = ⊤<VAR>hσ4 : Subgroup.closure {↑σ, τ} = ⊤<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>H : Subgroup (Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<VAR>this : Fact (Nat.Prime (Fintype.card α))<VAR>σ : ↥H<VAR>hσ : orderOf σ = Fintype.card α<VAR>hσ1 : orderOf ↑σ = Fintype.card α<VAR>hσ2 : (↑σ).IsCycle<VAR>hσ3 : (↑σ).support = ⊤<VAR>hσ4 : Subgroup.closure {↑σ, τ} = ⊤<GOAL>↑σ ∈ ↑H ∧ τ ∈ ↑H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (μ + ν) t ≠ ⊤<GOAL>ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (ν + μ) t ≠ ⊤<GOAL>ν (toMeasurable (ν + μ) t ∩ s) = ν (t ∩ s)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁵ : AddCommGroup V<VAR>inst✝¹⁴ : Module 𝕜 V<VAR>inst✝¹³ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹² : AddCommGroup W<VAR>inst✝¹¹ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<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>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>w : W<GOAL>Integrable (fun v => e (-(L v) w) • f v) μ ↔ Integrable f μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁵ : AddCommGroup V<VAR>inst✝¹⁴ : Module 𝕜 V<VAR>inst✝¹³ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹² : AddCommGroup W<VAR>inst✝¹¹ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<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>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>w : W<VAR>aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v => e (-(L v) x) • g v) μ<GOAL>Integrable (fun v => e (-(L v) w) • f v) μ ↔ Integrable f μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁵ : AddCommGroup V<VAR>inst✝¹⁴ : Module 𝕜 V<VAR>inst✝¹³ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹² : AddCommGroup W<VAR>inst✝¹¹ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<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>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>w : W<VAR>aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v => e (-(L v) x) • g v) μ<VAR>hf : Integrable (fun v => e (-(L v) w) • f v) μ<VAR>this : Integrable (fun v => e (-(L v) (-w)) • e (-(L v) w) • f v) μ<GOAL>Integrable f μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁵ : AddCommGroup V<VAR>inst✝¹⁴ : Module 𝕜 V<VAR>inst✝¹³ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹² : AddCommGroup W<VAR>inst✝¹¹ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<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>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>w : W<VAR>aux : ∀ {g : V → E}, Integrable g μ → ∀ (x : W), Integrable (fun v => e (-(L v) x) • g v) μ<VAR>hf : Integrable (fun v => e (-(L v) w) • f v) μ<VAR>this : Integrable (fun v => f v) μ<GOAL>Integrable f μ
<VAR>m n k : ℕ<GOAL>m.gcd (k * m + n) = m.gcd n
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>hx : IsFixedPt f x<VAR>hy : IsFixedPt f y<GOAL>x = y ∨ edist x y = ⊤
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>hx : IsFixedPt f x<VAR>hy : IsFixedPt f y<VAR>h : ¬edist x y = ⊤<GOAL>edist x y ≤ 0
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>f : F<GOAL>HasDerivAt (fun y => c y • f) (c' • f) x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' univ x<VAR>f : F<GOAL>HasDerivWithinAt (fun y => c y • f) (c' • f) univ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>q.lift (x * y) = q.lift x * q.lift y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re • 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + ((x.imI * y.re) • q.i + (x.imI * y.imI) • (q.i * q.i) + (x.imI * y.imJ) • (q.i * q.j) + (x.imI * y.imK) • (q.i * q.k)) + ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (q.j * q.i) + (x.imJ * y.imJ) • (q.j * q.j) + (x.imJ * y.imK) • (q.j * q.k)) + ((x.imK * y.re) • q.k + (x.imK * y.imI) • (q.k * q.i) + (x.imK * y.imJ) • (q.k * q.j) + (x.imK * y.imK) • (q.k * q.k))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + ((x.imI * y.re) • q.i + (x.imI * y.imI) • c₁ • 1 + (x.imI * y.imJ) • q.k + (x.imI * y.imK) • c₁ • q.j) + ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • -q.k + (x.imJ * y.imJ) • c₂ • 1 + (x.imJ * y.imK) • -c₂ • q.i) + ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₂ • q.i + (x.imK * y.imK) • -((c₁ * c₂) • 1))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i + (x.imI * y.imI * c₁) • 1 + (x.imI * y.imJ) • q.k + (x.imI * y.imK * c₁) • q.j + (x.imJ * y.re) • q.j + -((x.imJ * y.imI) • q.k) + (x.imJ * y.imJ * c₂) • 1 + -((x.imJ * y.imK * c₂) • q.i) + (x.imK * y.re) • q.k + -((x.imK * y.imI * c₁) • q.j) + (x.imK * y.imJ * c₂) • q.i + -((x.imK * y.imK * (c₁ * c₂)) • 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i + (x.imI * y.imI * c₁) • 1 + (x.imI * y.imJ) • q.k + (x.imI * y.imK * c₁) • q.j + (x.imJ * y.re) • q.j + -((x.imJ * y.imI) • q.k) + (x.imJ * y.imJ * c₂) • 1 + -((x.imJ * y.imK * c₂) • q.i) + (x.imK * y.re) • q.k + -((x.imK * y.imI * c₁) • q.j) + (x.imK * y.imJ * c₂) • q.i + -((c₁ * c₂ * x.imK * y.imK) • 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i + (c₁ * (x.imI * y.imI)) • 1 + (x.imI * y.imJ) • q.k + (c₁ * (x.imI * y.imK)) • q.j + (x.imJ * y.re) • q.j + -((x.imJ * y.imI) • q.k) + (x.imJ * y.imJ * c₂) • 1 + -((x.imJ * y.imK * c₂) • q.i) + (x.imK * y.re) • q.k + -((c₁ * (x.imK * y.imI)) • q.j) + (x.imK * y.imJ * c₂) • q.i + -((c₁ * c₂ * x.imK * y.imK) • 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i + (c₁ * (x.imI * y.imI)) • 1 + (x.imI * y.imJ) • q.k + (c₁ * (x.imI * y.imK)) • q.j + (x.imJ * y.re) • q.j + -((x.imJ * y.imI) • q.k) + (c₂ * (x.imJ * y.imJ)) • 1 + -((c₂ * (x.imJ * y.imK)) • q.i) + (x.imK * y.re) • q.k + -((c₁ * (x.imK * y.imI)) • q.j) + (c₂ * (x.imK * y.imJ)) • q.i + -((c₂ * c₁ * x.imK * y.imK) • 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i + (c₁ * x.imI * y.imI) • 1 + (x.imI * y.imJ) • q.k + (c₁ * x.imI * y.imK) • q.j + (x.imJ * y.re) • q.j + -((x.imJ * y.imI) • q.k) + (c₂ * x.imJ * y.imJ) • 1 + -((c₂ * x.imJ * y.imK) • q.i) + (x.imK * y.re) • q.k + -((c₁ * x.imK * y.imI) • q.j) + (c₂ * x.imK * y.imJ) • q.i + -((c₁ * c₂ * x.imK * y.imK) • 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>(x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₂ * x.imJ * y.imJ) • 1 + -((c₁ * c₂ * x.imK * y.imK) • 1) + (x.re * y.imI) • q.i + (x.imI * y.re) • q.i + -((c₂ * x.imJ * y.imK) • q.i) + (c₂ * x.imK * y.imJ) • q.i + (x.re * y.imJ) • q.j + (c₁ * x.imI * y.imK) • q.j + (x.imJ * y.re) • q.j + -((c₁ * x.imK * y.imI) • q.j) + (x.re * y.imK) • q.k + (x.imI * y.imJ) • q.k + -((x.imJ * y.imI) • q.k) + (x.imK * y.re) • q.k = (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i + (c₁ * x.imI * y.imI) • 1 + (x.imI * y.imJ) • q.k + (c₁ * x.imI * y.imK) • q.j + (x.imJ * y.re) • q.j + -((x.imJ * y.imI) • q.k) + (c₂ * x.imJ * y.imJ) • 1 + -((c₂ * x.imJ * y.imK) • q.i) + (x.imK * y.re) • q.k + -((c₁ * x.imK * y.imI) • q.j) + (c₂ * x.imK * y.imJ) • q.i + -((c₁ * c₂ * x.imK * y.imK) • 1)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Iio a = Ioo ⊥ ↑a
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>addZ P Q = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>Disjoint (a ⊓ b) (a ⊓ b)ᶜ
<VAR>a b c d m n i : ℤ<VAR>h : 0 < i<GOAL>↑(i.toNat - 1) = i - 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝[(fun t => x + t • v) ⁻¹' s] 0] fun t => f (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<VAR>A : Continuous fun t => x + t • v<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝[(fun t => x + t • v) ⁻¹' s] 0] fun t => f (x + t • v)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>¬(x ~ᵢ y) ↔ ∃ s, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>𝕜 : Type u_3<VAR>inst✝ : NormedField 𝕜<VAR>v : 𝕜<GOAL>(ContinuousLinearMap.smulRight 1 v).det = v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>𝕜 : Type u_3<VAR>inst✝ : NormedField 𝕜<VAR>v : 𝕜<VAR>this : ContinuousLinearMap.smulRight 1 v = v • 1<GOAL>(ContinuousLinearMap.smulRight 1 v).det = v
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>testAgainstNN 0 f = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : ↑S<GOAL>EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S ↑x₀
<VAR>z : ℤ<VAR>hz : 0 ≤ z<GOAL>Irrational √↑z ↔ ¬IsSquare z
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 1<VAR>hb : b % 2 = 1<VAR>hr : jacobiSymNat b a = r<GOAL>jacobiSymNat a b = r
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>x : A<GOAL>↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>x : A<GOAL>⇑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>l₁ l₂ : List α<VAR>k : ℕ<GOAL>(l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n < (permutations'Aux x s).length<GOAL>(permutations'Aux x s).get ⟨n, hn⟩ = insertNth n x s
<VAR>R : Type u_2<VAR>K : Type ?u.6272<VAR>L : Type ?u.6275<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>i : ℕ<GOAL>(minpolyDiv R x).coeff i = (algebraMap R S) ((minpoly R x).coeff (i + 1)) + (minpolyDiv R x).coeff (i + 1) * x
<VAR>R : Type u_2<VAR>K : Type ?u.6272<VAR>L : Type ?u.6275<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>i : ℕ<GOAL>(minpolyDiv R x).coeff i = (minpolyDiv R x * (X - C x)).coeff (i + 1) + (minpolyDiv R x).coeff (i + 1) * x
<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>r : ℝ<VAR>v : V<VAR>p₁ p₂ : P<GOAL>dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = ⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ
<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>r : ℝ<VAR>v : V<VAR>p₁ p₂ : P<GOAL>r * (r * ⟪v, v⟫_ℝ) + 2 * (r * ⟪v, p₁ -ᵥ p₂⟫_ℝ) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ = ⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B✝ A B : Matrix n n α<VAR>h : A * B = 1<VAR>this✝ : Invertible B.det := B.detInvertibleOfLeftInverse A h<VAR>this : Invertible B := B.invertibleOfDetInvertible<GOAL>B * A = 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>s : Finset α<VAR>hc : (↑s).Pairwise fun i j => Commute (x i) (x j)<GOAL>∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>hc : (↑∅).Pairwise fun i j => Commute (x i) (x j)<GOAL>∀ (n : ℕ), ∅.sum x ^ n = ∑ k : { x // x ∈ ∅.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯