ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : Algebra R A<VAR>h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)<VAR>x : R<VAR>y : S<VAR>z : A<GOAL>(x • y) • z = x • y • z
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>ascPochhammer S (n + 1) = ascPochhammer S n * (X + ↑n)
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : GroupWithZero K<VAR>inst✝ : Fintype K<VAR>a : K<VAR>ha : a ≠ 0<GOAL>a ^ (q - 1) = 1
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v w : V<VAR>hvw : G.Adj v w<VAR>hv : u ≠ v<VAR>hw : u ≠ w<VAR>x✝ : V<GOAL>x✝ ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ x✝ ∈ ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β<VAR>ha₀ : 0 ≤ a₀<VAR>ha₁ : 0 ≤ a₁<VAR>hb₀ : 0 ≤ b₀<VAR>hb₁ : 0 ≤ b₁<VAR>hc₀ : 0 ≤ c₀<VAR>hc₁ : 0 ≤ c₁<VAR>hd₀ : 0 ≤ d₀<VAR>hd₁ : 0 ≤ d₁<VAR>h₀₀ : a₀ * b₀ ≤ c₀ * d₀<VAR>h₁₀ : a₁ * b₀ ≤ c₀ * d₁<VAR>h₀₁ : a₀ * b₁ ≤ c₀ * d₁<VAR>h₁₁ : a₁ * b₁ ≤ c₁ * d₁<GOAL>(a₀ + a₁) * (b₀ + b₁) ≤ (c₀ + c₁) * (d₀ + d₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β<VAR>ha₀ : 0 ≤ a₀<VAR>ha₁ : 0 ≤ a₁<VAR>hb₀ : 0 ≤ b₀<VAR>hb₁ : 0 ≤ b₁<VAR>hc₀ : 0 ≤ c₀<VAR>hc₁ : 0 ≤ c₁<VAR>hd₀ : 0 ≤ d₀<VAR>hd₁ : 0 ≤ d₁<VAR>h₀₀ : a₀ * b₀ ≤ c₀ * d₀<VAR>h₁₀ : a₁ * b₀ ≤ c₀ * d₁<VAR>h₀₁ : a₀ * b₁ ≤ c₀ * d₁<VAR>h₁₁ : a₁ * b₁ ≤ c₁ * d₁<GOAL>a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β<VAR>ha₀ : 0 ≤ a₀<VAR>ha₁ : 0 ≤ a₁<VAR>hb₀ : 0 ≤ b₀<VAR>hb₁ : 0 ≤ b₁<VAR>hc₀ : 0 ≤ c₀<VAR>hc₁ : 0 ≤ c₁<VAR>hd₀ : 0 ≤ d₀<VAR>hd₁ : 0 ≤ d₁<VAR>h₀₀ : a₀ * b₀ ≤ c₀ * d₀<VAR>h₁₀ : a₁ * b₀ ≤ c₀ * d₁<VAR>h₀₁ : a₀ * b₁ ≤ c₀ * d₁<VAR>h₁₁ : a₁ * b₁ ≤ c₁ * d₁<VAR>hcd : 0 < c₀ * d₁<GOAL>a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β<VAR>ha₀ : 0 ≤ a₀<VAR>ha₁ : 0 ≤ a₁<VAR>hb₀ : 0 ≤ b₀<VAR>hb₁ : 0 ≤ b₁<VAR>hc₀ : 0 ≤ c₀<VAR>hc₁ : 0 ≤ c₁<VAR>hd₀ : 0 ≤ d₀<VAR>hd₁ : 0 ≤ d₁<VAR>h₀₀ : a₀ * b₀ ≤ c₀ * d₀<VAR>h₁₀ : a₁ * b₀ ≤ c₀ * d₁<VAR>h₀₁ : a₀ * b₁ ≤ c₀ * d₁<VAR>h₁₁ : a₁ * b₁ ≤ c₁ * d₁<VAR>hcd : 0 < c₀ * d₁<GOAL>(a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : a ≤ b * c<VAR>b0 : b = 0<GOAL>a / b ≤ c
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>F : C ⥤ D<VAR>hF : CoverPreserving J K F<VAR>G : D ⥤ A<VAR>hG : CoverPreserving K L G<VAR>U✝ : C<VAR>S✝ : Sieve U✝<VAR>hS : S✝ ∈ J.sieves U✝<GOAL>Sieve.functorPushforward (F ⋙ G) S✝ ∈ L.sieves ((F ⋙ G).obj U✝)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>F : C ⥤ D<VAR>hF : CoverPreserving J K F<VAR>G : D ⥤ A<VAR>hG : CoverPreserving K L G<VAR>U✝ : C<VAR>S✝ : Sieve U✝<VAR>hS : S✝ ∈ J.sieves U✝<GOAL>Sieve.functorPushforward G (Sieve.functorPushforward F S✝) ∈ L.sieves ((F ⋙ G).obj U✝)
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).inf = s₁.inf ⊓ s₂.inf
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>{v | Odd (G.degree v)}.toFinset.card = 0 ∨ {v | Odd (G.degree v)}.toFinset.card = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>{v | Odd (G.degree v)}.toFinset = Finset.filter (fun v => Odd (G.degree v)) Finset.univ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hI : I.IsPrimary<VAR>hJ : J.IsPrime<VAR>x : R ⧸ I<VAR>e : J = (Submodule.span R {x}).annihilator<GOAL>J = I.radical
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hI : I.IsPrimary<VAR>hJ : J.IsPrime<VAR>x : R ⧸ I<VAR>e : J = (Submodule.span R {x}).annihilator<VAR>this : x ≠ 0<GOAL>J = I.radical
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hI : I.IsPrimary<VAR>hJ : J.IsPrime<VAR>x : R<VAR>e : J = (Submodule.span R {(Ideal.Quotient.mkₐ R I) x}).annihilator<VAR>this : (Ideal.Quotient.mkₐ R I) x ≠ 0<GOAL>J = I.radical
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hI : I.IsPrimary<VAR>hJ : J.IsPrime<VAR>x : R<VAR>this : (Ideal.Quotient.mkₐ R I) x ≠ 0<VAR>e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I<GOAL>J = I.radical
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hI : I.IsPrimary<VAR>hJ : J.IsPrime<VAR>x : R<VAR>this : (Ideal.Quotient.mkₐ R I) x ≠ 0<VAR>e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I<GOAL>J ≤ I.radical
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hI : I.IsPrimary<VAR>hJ : J.IsPrime<VAR>x : R<VAR>this : (Ideal.Quotient.mkₐ R I) x ≠ 0<VAR>e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I<GOAL>I.radical ≤ J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖x + y - z‖ * ‖x + y - z‖ = (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 - ‖x + z‖ * ‖x + z‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<VAR>h₀ : ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)<GOAL>‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a * b < b⁻¹ * b ↔ a * b < 1
<VAR>K : Type ?u.590273<VAR>L : Type ?u.590276<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hpq : q ∣ p<GOAL>(aeval (root q)) p = 0
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f : ι → E<GOAL>‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f : ι → E<GOAL>Multiplicative.ofAdd ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, Multiplicative.ofAdd ‖f i‖
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f : ι → E<GOAL>(⇑Multiplicative.ofAdd ∘ norm) 1 = 1
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f : ι → E<VAR>x y : E<GOAL>(⇑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (⇑Multiplicative.ofAdd ∘ norm) x * (⇑Multiplicative.ofAdd ∘ norm) y
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.edist u v = G.edist v u
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>sInf (Set.range fun x => ↑x.reverse.length) = G.edist v u
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>x : G<GOAL>x ∈ ⋃ q, quotToDoset H K q ↔ x ∈ Set.univ
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>x : G<GOAL>∃ i, ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out' i * y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>x : G<GOAL>∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out' (mk H K x) * y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>x h k : G<VAR>h3 : h ∈ H<VAR>h4 : k ∈ K<VAR>h5 : Quotient.out' (mk H K x) = h * x * k<GOAL>∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out' (mk H K x) * y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>x h k : G<VAR>h3 : h ∈ H<VAR>h4 : k ∈ K<VAR>h5 : Quotient.out' (mk H K x) = h * x * k<GOAL>x = h⁻¹ * Quotient.out' (mk H K x) * k⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h0 : q ≠ 0<VAR>hl : q.degree < p.degree<VAR>hcontra : p ∣ q<GOAL>False
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>h : m ≤ n<GOAL>(contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>h : m ≤ n<GOAL>∀ (f : H → H) (s : Set H), (contDiffPregroupoid n I).property f s → (contDiffPregroupoid m I).property f s
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>h : m ≤ n<VAR>f : H → H<VAR>s : Set H<VAR>hfs : (contDiffPregroupoid n I).property f s<GOAL>(contDiffPregroupoid m I).property f s
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>z : ℤ<VAR>A : Matrix m m 𝔸<GOAL>exp 𝕂 (z • A) = exp 𝕂 A ^ z
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n✝ : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n✝<VAR>inst✝⁵ : DecidableEq n✝<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<VAR>n : ℕ<GOAL>exp 𝕂 (↑n • A) = exp 𝕂 A ^ ↑n
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n✝ : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n✝<VAR>inst✝⁵ : DecidableEq n✝<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<VAR>n : ℕ<GOAL>exp 𝕂 (-↑n • A) = exp 𝕂 A ^ (-↑n)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝ : CommSemiring S'<VAR>f : R →+* S<VAR>s : Set R<VAR>x : PrimeSpectrum S<GOAL>x ∈ (fun y => { asIdeal := Ideal.comap f y.asIdeal, isPrime := ⋯ }) ⁻¹' zeroLocus s ↔ x ∈ zeroLocus (⇑f '' s)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>A₀ A₁ B₀ B₁ : R<VAR>A₀_inv : A₀ ^ 2 = 1<VAR>A₁_inv : A₁ ^ 2 = 1<VAR>B₀_inv : B₀ ^ 2 = 1<VAR>B₁_inv : B₁ ^ 2 = 1<GOAL>(2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>ι' : ι → Sort u_6<VAR>f : (i : ι) → ι' i → α → ℝ≥0∞<GOAL>∫⁻ (a : α), ⨅ i, ⨅ h, f i h a ∂μ ≤ ⨅ i, ⨅ h, ∫⁻ (a : α), f i h a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>ι' : ι → Sort u_6<VAR>f : (i : ι) → ι' i → α → ℝ≥0∞<VAR>a : α<GOAL>⨅ i, ⨅ h, f i h a = (⨅ i, ⨅ j, f i j) a
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : i ≠ p.castSucc<GOAL>p.castSucc.succAbove (p.predAbove i) = i
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h✝ : i ≠ p.castSucc<VAR>h : i < p.castSucc<GOAL>p.castSucc.succAbove (p.predAbove i) = i
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h✝ : i ≠ p.castSucc<VAR>h : p.castSucc < i<GOAL>p.castSucc.succAbove (p.predAbove i) = i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>hf : IsMulOneCocycle f<GOAL>IsMulOneCoboundary f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>hf : IsMulOneCocycle f<VAR>z : L<VAR>hz : aux f z ≠ 0<GOAL>IsMulOneCoboundary f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>hf : IsMulOneCocycle f<VAR>z : L<VAR>hz : aux f z ≠ 0<VAR>this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z<GOAL>IsMulOneCoboundary f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>hf : IsMulOneCocycle f<VAR>z : L<VAR>hz : aux f z ≠ 0<VAR>this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z<GOAL>∀ (g : L ≃ₐ[K] L), g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>hf : IsMulOneCocycle f<VAR>z : L<VAR>hz : aux f z ≠ 0<VAR>this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z<VAR>g : L ≃ₐ[K] L<GOAL>g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>z : L<VAR>hz : aux f z ≠ 0<VAR>this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z<VAR>g : L ≃ₐ[K] L<VAR>hf : ∀ (g h : L ≃ₐ[K] L), ↑(f (g * h)) = g ↑(f h) * ↑(f g)<GOAL>∑ h : L ≃ₐ[K] L, ↑(f h) * h z = g (∑ h : L ≃ₐ[K] L, ↑(f h) * h z) * ↑(f g)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>z : L<VAR>hz : aux f z ≠ 0<VAR>this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z<VAR>g : L ≃ₐ[K] L<VAR>hf : ∀ (g h : L ≃ₐ[K] L), ↑(f (g * h)) = g ↑(f h) * ↑(f g)<GOAL>∑ h : L ≃ₐ[K] L, ↑(f h) * h z = ∑ x : L ≃ₐ[K] L, ↑(f (g * x)) * g (x z)
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<GOAL>a / b ≤ a / c ↔ c ≤ b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (cocompact X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>hy : ¬ClusterPt y l<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (cocompact X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>hy : ∃ x, ∃ (_ : x ∈ 𝓝 y), ∃ x_1, ∃ (_ : x_1 ∈ l), Disjoint x x_1<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (cocompact X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (cocompact X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<VAR>K : Set X<VAR>hKc : IsCompact K<VAR>hKs : Kᶜ ⊆ f ⁻¹' s<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (cocompact X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<VAR>K : Set X<VAR>hKc : IsCompact K<VAR>hKs : Kᶜ ⊆ f ⁻¹' s<VAR>this : f '' K ∈ l<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y✝ : Y<VAR>hf : Tendsto f (cocompact X) (𝓝 y✝)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>hle : l ≤ 𝓟 (insert y✝ (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y✝<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<VAR>K : Set X<VAR>hKc : IsCompact K<VAR>hKs : Kᶜ ⊆ f ⁻¹' s<VAR>this : f '' K ∈ l<VAR>y : Y<VAR>hy : y ∈ f '' K<VAR>hyl : ClusterPt y l<GOAL>∃ x ∈ insert y✝ (range f), ClusterPt x l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>f : β → Option α<VAR>l : List β<VAR>_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'<GOAL>Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>f : β → Option α<VAR>l : List β<VAR>_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'<GOAL>Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>f : β → Option α<VAR>_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'<VAR>a : β<VAR>l : List β<VAR>IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l<GOAL>Pairwise R (filterMap f (a :: l)) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>s : Set E<VAR>hs : Orthonormal 𝕜 Subtype.val<GOAL>∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w