ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₁ : Function.LeftInverse φ' φ<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (x : X), ((f.inverse' g k₂ h₁ h₂).comp f) x = (MulActionHom.id M) x
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₁ : Function.LeftInverse φ' φ<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>x : X<GOAL>((f.inverse' g k₂ h₁ h₂).comp f) x = (MulActionHom.id M) x
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₁ : Function.LeftInverse φ' φ<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>x : X<GOAL>(f.inverse' g k₂ h₁ h₂) (f x) = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>h : IsGLB s a<GOAL>b ≤ a ↔ b ∈ lowerBounds s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>h : IsGLB s a<GOAL>b ≤ a ↔ b ∈ Iic a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys : List α<GOAL>(xs ++ ys).enum = xs.enum ++ enumFrom xs.length ys
<VAR>x : ℝ<GOAL>WithBot.some ∘ WithTop.some ⁻¹' Ici ↑↑x = Ici x
<VAR>x : ℝ<GOAL>WithTop.some ⁻¹' (WithBot.some ⁻¹' Ici ↑↑x) = Ici x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y) ⋯<GOAL>(s.erase a).noncommProd comm' * a = s.noncommProd comm
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y) ⋯<GOAL>∀ b ∈ s.erase a, Commute a b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y) ⋯<VAR>b : α<VAR>hb : b ∈ s.erase a<GOAL>Commute a b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y) ⋯<VAR>hb : a ∈ s.erase a<GOAL>Commute a a
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ y ∈ {x | x ∈ s.erase a}, x ≠ y → Commute x y) ⋯<VAR>b : α<VAR>hb : b ∈ s.erase a<VAR>hab : a ≠ b<GOAL>Commute a b
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.i = 0 ↔ l = []
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<GOAL>(dickson 1 1 m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ : Subgroup α<VAR>a b : α<VAR>s : Subgroup α<VAR>g z : α<GOAL>z ∈ {x | ↑x = ↑g} ↔ z ∈ g • ↑s
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<GOAL>∀ (v : G), ‖↑G v‖ ≤ 1 * ‖v‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>0 < a / b ↔ 0 < b
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<GOAL>H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<GOAL>H.normalizer = H ↔ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>h : H.normalizer = H<GOAL>∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0<GOAL>H.normalizer ≤ H
<VAR>y z : ℝ<VAR>hy : 0 ≤ y<VAR>hz : 0 ≤ z<VAR>x✝ : ℝ≥0<GOAL>↑x✝ ^ (y + z) = ↑x✝ ^ y * ↑x✝ ^ z
<VAR>n m : ℕ<VAR>p i : Fin n<VAR>h : i ≤ p<GOAL>p.predAbove i.castSucc = i
<GOAL>max (lsub fun i => (star.moveLeft i).birthday) (lsub fun i => (star.moveRight i).birthday) = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a : α<VAR>z : ℤ<GOAL>⌈a + ↑z⌉ = ⌈a⌉ + z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x₁ x₂ : E<VAR>y : F<GOAL>(fun x => (x, y)) '' [x₁-[𝕜]x₂] = [(x₁, y)-[𝕜](x₂, y)]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x₁ x₂ : E<VAR>y : F<GOAL>(fun x => (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = (fun p => p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x₁ x₂ : E<VAR>y : F<VAR>a : 𝕜 × 𝕜<VAR>ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}<GOAL>(a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedGroup E<VAR>inst✝ : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : E → F<VAR>hi : Isometry f<VAR>h₁ : f 1 = 1<VAR>x : E<GOAL>‖f x‖ = ‖x‖
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<GOAL>(↑(iso S f).symm ∘ₗ f) m = (LocalizedModule.mkLinearMap S M) m
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<GOAL>1 • f m = f m
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>comm : h ≫ f = k ≫ g<VAR>inst✝² : PreservesLimit (cospan f g) G<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback (G.map f) (G.map g)<GOAL>(iso G f g).inv ≫ G.map (pullback.fst f g) = pullback.fst (G.map f) (G.map g)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R (-n) = T R n
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<VAR>x : X.V<GOAL>(((linearization k G).obj X).ρ g) (Finsupp.single x 1) = Finsupp.single (X.ρ g x) 1
<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 : Set α<VAR>f : α → β<VAR>ι : Type u_8<VAR>μ ν : ι → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum μ + sum ν) s = (sum fun n => μ n + ν n) s
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Multiset ℕ<VAR>n : ℕ<GOAL>s.sum % n = (map (fun x => x % n) s).sum % n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R<VAR>x : υ → R<GOAL>comap (g.comp f) x = comap f (comap g x)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R<VAR>x : υ → R<VAR>i : σ<GOAL>comap (g.comp f) x i = comap f (comap g x) i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a✝ b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u : Set α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<VAR>x : α<GOAL>x ∈ insert a s \ {a} ↔ x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Multiset α<GOAL>{x | x ∈ s}.Finite
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>E' : Type u_3<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>fst✝ : E<VAR>snd✝ : E'<VAR>hf : ContDiffAt 𝕜 n f (fst✝, snd✝).1<VAR>hg : ContDiffAt 𝕜 n g (fst✝, snd✝).2<GOAL>ContDiffAt 𝕜 n (Prod.map f g) (fst✝, snd✝)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>ker f ≤ ker (g.comp f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>ker f ≤ comap f (ker g)
<VAR>𝕜 : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : Fintype ι₁<VAR>inst✝ : Fintype ι₂<VAR>v : OrthonormalBasis ι₁ 𝕜 E<VAR>w : OrthonormalBasis ι₂ 𝕜 F<GOAL>∀ (i : ι₁ ⊕ ι₂), (v.prod w) i = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) i
<VAR>𝕜 : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : Fintype ι₁<VAR>inst✝ : Fintype ι₂<VAR>v : OrthonormalBasis ι₁ 𝕜 E<VAR>w : OrthonormalBasis ι₂ 𝕜 F<GOAL>(∀ (a : ι₁), (v.prod w) (Sum.inl a) = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inl a)) ∧ ∀ (b : ι₂), (v.prod w) (Sum.inr b) = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)
<VAR>A B : TopCat<GOAL>prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 (↑(π.obj A) × ↑(π.obj B))
<VAR>A B : TopCat<GOAL>∀ (X : ↑(π.obj A) × ↑(π.obj B)), (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X
<VAR>A B : TopCat<GOAL>∀ (X Y : ↑(π.obj A) × ↑(π.obj B)) (f : X ⟶ Y), HEq ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map f) ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map f)
<VAR>A B : TopCat<VAR>x₀ : ↑(π.obj A)<VAR>x₁ : ↑(π.obj B)<VAR>y₀ : ↑(π.obj A)<VAR>y₁ : ↑(π.obj B)<VAR>f₀ : (x₀, x₁).1 ⟶ (y₀, y₁).1<VAR>f₁ : (x₀, x₁).2 ⟶ (y₀, y₁).2<GOAL>HEq ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map (f₀, f₁)) ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁))
<VAR>A B : TopCat<VAR>x₀ : ↑(π.obj A)<VAR>x₁ : ↑(π.obj B)<VAR>y₀ : ↑(π.obj A)<VAR>y₁ : ↑(π.obj B)<VAR>f₀ : (x₀, x₁).1 ⟶ (y₀, y₁).1<VAR>f₁ : (x₀, x₁).2 ⟶ (y₀, y₁).2<VAR>this : Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧ Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁<GOAL>HEq ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map (f₀, f₁)) ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁))
<VAR>A B : TopCat<GOAL>(projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))
<VAR>A B : TopCat<GOAL>∀ (X : ↑(π.obj (TopCat.of (↑A × ↑B)))), ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X
<VAR>A B : TopCat<GOAL>∀ (X Y : ↑(π.obj (TopCat.of (↑A × ↑B)))) (f : X ⟶ Y), HEq (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f) ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
<VAR>A B : TopCat<VAR>x₀ : ↑A<VAR>x₁ : ↑B<VAR>y₀ : ↑A<VAR>y₁ : ↑B<VAR>f : { as := (x₀, x₁) } ⟶ { as := (y₀, y₁) }<GOAL>HEq (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f) ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
<VAR>A B : TopCat<VAR>x₀ : ↑A<VAR>x₁ : ↑B<VAR>y₀ : ↑A<VAR>y₁ : ↑B<VAR>f : { as := (x₀, x₁) } ⟶ { as := (y₀, y₁) }<VAR>this : Path.Homotopic.prod (Path.Homotopic.projLeft f) (Path.Homotopic.projRight f) = f<GOAL>HEq (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f) ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
<VAR>A B : TopCat<VAR>x₀ : ↑A<VAR>x₁ : ↑B<VAR>y₀ : ↑A<VAR>y₁ : ↑B<VAR>f : { as := (x₀, x₁) } ⟶ { as := (y₀, y₁) }<VAR>this : Path.Homotopic.prod (Path.Homotopic.projLeft f) (Path.Homotopic.projRight f) = f<GOAL>(prodToProdTop A B).map (Path.Homotopic.projLeft f, Path.Homotopic.projRight f) = f
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>hg : ContDiffOn 𝕜 (↑n) g s<GOAL>iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>a / b < 1 ↔ b < a
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : l.Nodup<VAR>h' : a ∈ l<GOAL>(List.insert a l).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : l.Nodup<VAR>h' : a ∈ l<GOAL>l.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : l.Nodup<VAR>h' : a ∉ l<GOAL>(List.insert a l).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : l.Nodup<VAR>h' : a ∉ l<GOAL>a ∉ l ∧ l.Nodup
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : IsScalarTower R A A<VAR>a b x✝ : A<GOAL>(mulLeft R (a * b)) x✝ = (mulLeft R a ∘ₗ mulLeft R b) x✝
<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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : Subsingleton ι<GOAL>iIndepFun m f κ μ
<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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : Subsingleton ι<VAR>s : Finset ι<VAR>f' : (i : ι) → Set (β i)<VAR>hf' : ∀ i ∈ s, MeasurableSet (f' i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)
<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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : Subsingleton ι<VAR>f' : (i : ι) → Set (β i)<VAR>hf' : ∀ i ∈ ∅, MeasurableSet (f' i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ ∅, f i ⁻¹' f' i) = ∏ i ∈ ∅, (κ a) (f i ⁻¹' f' i)
<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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : Subsingleton ι<VAR>s : Finset ι<VAR>f' : (i : ι) → Set (β i)<VAR>hf' : ∀ i ∈ s, MeasurableSet (f' i)<VAR>x : ι<VAR>hx : x ∈ s<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i ⁻¹' f' i) = ∏ i ∈ s, (κ a) (f i ⁻¹' f' i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Mul M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<GOAL>𝓝 a * 𝓝 b ≤ 𝓝 (a * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Mul M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<GOAL>map (Function.uncurry fun x x_1 => x * x_1) (𝓝 (a, b)) ≤ 𝓝 (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>map reverse l.tails = l.reverse.inits.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>f' g' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>c : ℂ<VAR>hf : HasFDerivAt f f' x<VAR>hg : HasFDerivAt g g' x<VAR>h0 : f x ∈ slitPlane<GOAL>HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>h : IsRatStieltjesPoint f a<VAR>q : ℚ<GOAL>toRatCDF f a q = f a q
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{?u.1506, u_1} C₁<VAR>inst✝⁷ : Category.{?u.1510, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{?u.2123, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>R R' : Φ.RightResolution X₂<VAR>φ : R ⟶ R'<GOAL>L.map (Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = (isoOfHom L W₂ R.w ⋯).inv ≫ y