ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>s : Set Y<VAR>hs : IsOpen s<GOAL>(e.trans (ofSet s hs)).source = (e.restr (↑e ⁻¹' s)).source
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<GOAL>U ∈ p.basisSets ↔ ∃ i r, 0 < r ∧ U = (i.sup p).ball 0 r
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>s : Set ℝ≥0∞<VAR>hs : ∀ r ∈ s, r ≠ ⊤<VAR>hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤<GOAL>(sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>firstDiff x y ≤ longestPrefix x s
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>firstDiff x y + 1 ≤ shortestPrefixDiff x s
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x y : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>1 ≤ shortestPrefixDiff x s
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s t : Set L<VAR>h : s ⊆ t<GOAL>lieSpan R L s ≤ lieSpan R L t
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s t : Set L<VAR>h : s ⊆ t<GOAL>s ⊆ ↑(lieSpan R L t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∈ s<VAR>x : α<GOAL>x ∈ insert a (s.erase a) ↔ x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∈ s<VAR>x : α<GOAL>x = a ∨ x ∈ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∈ s<VAR>x : α<GOAL>x = a → x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<GOAL>Integrable (fun x => RCLike.re (f x)) μ ∧ Integrable (fun x => RCLike.im (f x)) μ ↔ Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<GOAL>Memℒp (fun x => RCLike.re (f x)) 1 μ ∧ Memℒp (fun x => RCLike.im (f x)) 1 μ ↔ Memℒp f 1 μ
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y<GOAL>∀ (x y : α), dist (f x) (f y) ≤ ↑1 * dist x y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 x).HasBasis p s<GOAL>(∀ ⦃i : ι⦄, p i → ∀ ⦃j : Unit⦄, True → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E 𝕜<VAR>z : G<GOAL>‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E 𝕜<VAR>z : G<GOAL>‖f.smulRight z‖₊ ≤ ‖f‖₊ * ‖z‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E 𝕜<VAR>z : G<GOAL>‖f‖₊ * ‖z‖₊ ≤ ‖f.smulRight z‖₊
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p✝ : ℝ<VAR>s : Set ℝ<VAR>p : ℝ<GOAL>(deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<GOAL>(deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p✝ : ℝ<VAR>s : Set ℝ<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>n D : ℤ<VAR>f : LaurentSeries K<VAR>H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))<VAR>hnd : n < D<VAR>h_n_ord : ¬n < HahnSeries.order f<GOAL>f.coeff n = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>n D : ℤ<VAR>f : LaurentSeries K<VAR>H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))<VAR>hnd : n < D<VAR>h_n_ord : HahnSeries.order f ≤ n<GOAL>f.coeff n = 0
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<GOAL>levyProkhorovEDist μ ν ≤ max (μ univ) (ν univ)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y \ x = y \ z<GOAL>y ⊓ x ⊓ y \ x = y ⊓ z ⊓ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y \ x = y \ z<GOAL>y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y ⊓ x = y ⊓ z<GOAL>y \ x = y \ z
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f : R[X]<VAR>N : ℕ<GOAL>reflect N (-f) = -reflect N f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : s.max = ⊥<VAR>H : s.Nonempty<GOAL>s = ∅
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : s.max = ⊥<VAR>H : s.Nonempty<VAR>a : α<VAR>ha : s.max = ↑a<GOAL>s = ∅
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>(a :: l).erase b <+~ a :: l.erase b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>f : G ≃g turanGraph n r<VAR>hr : 0 < r<GOAL>G.IsTuranMaximal r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>f : G ≃g turanGraph n r<VAR>hr : 0 < r<VAR>J : SimpleGraph V<VAR>w✝ : DecidableRel J.Adj<VAR>j : J.IsTuranMaximal r<GOAL>G.IsTuranMaximal r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>f : G ≃g turanGraph n r<VAR>hr : 0 < r<VAR>J : SimpleGraph V<VAR>w✝ : DecidableRel J.Adj<VAR>j : J.IsTuranMaximal r<VAR>g : J ≃g turanGraph (Fintype.card V) r<GOAL>G.IsTuranMaximal r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>f : G ≃g turanGraph n r<VAR>hr : 0 < r<VAR>J : SimpleGraph V<VAR>w✝ : DecidableRel J.Adj<VAR>j : J.IsTuranMaximal r<VAR>g : J ≃g turanGraph n r<GOAL>G.IsTuranMaximal r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = ⟪y, ↑v⟫_𝕜<GOAL>x - y ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = ⟪y, ↑v⟫_𝕜<GOAL>∀ u ∈ K, ⟪x - y, u⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = ⟪y, ↑v⟫_𝕜<VAR>u : E<VAR>hu : u ∈ K<GOAL>⟪x - y, u⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = ⟪y, ↑v⟫_𝕜<VAR>u : E<VAR>hu : u ∈ K<GOAL>⟪x, u⟫_𝕜 = ⟪y, u⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s t : Multiset α<GOAL>countP p (s + t) = countP p s + countP p t
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h0 : n ≠ 0<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>f : ℕ → α<GOAL>∑ i ∈ filter Squarefree n.divisors, f i = ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h0 : n ≠ 0<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>f : ℕ → α<GOAL>(Multiset.map (f ∘ fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum = (Multiset.map (fun i => f i.val.prod) (normalizedFactors n).toFinset.powerset.val).sum
<VAR>d✝ : ℤ<VAR>c d x y n : ℕ<VAR>xy : SqLe x c y d<GOAL>SqLe (n * x) c (n * y) d
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I<GOAL>I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I<GOAL>I.cotangentEquivIdeal (I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩) = I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩)
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I<GOAL>⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<VAR>h : Disjoint b c<GOAL>a ≤ a ∆ b ⊔ a ∆ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<VAR>h : Disjoint b c<GOAL>a ≤ b ∆ a ⊔ c ∆ a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : Mul G<VAR>inst✝ : IsRightCancelMul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), y * r = 0 ↔ y = 0<VAR>x : G<GOAL>(f * single x r).support = map (mulRightEmbedding x) f.support
<VAR>α : Type u<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : Invertible 2<GOAL>⅟2 + ⅟2 = 1
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h₁ : IsZero T.obj₁<VAR>h₃ : IsZero T.obj₃<GOAL>IsZero T.obj₂
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h₁ : IsZero T.obj₁<VAR>h₃ : IsZero T.obj₃<GOAL>T.mor₁ = 0 ∧ T.mor₂ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>p : PMF α<VAR>b : β<VAR>s : Set β<GOAL>(map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R✝ : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>a✝ a' a₁ a₂ a₃ b✝ b' b₁ b₂ b₃ c c₁ c₂ : R✝<VAR>R : Type u_2<VAR>inst✝ : DivisionRing R<VAR>a b : R<GOAL>a / b = a * b⁻¹
<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>hb : 0 < b<GOAL>0 < a / b ↔ 0 < a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>(((foldr Q (foldr'Aux Q f) ⋯) (1, n)) ((ι Q) m * x)).2 = (f m) (x, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>((ι Q) m * (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1, (f m) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x)).2 = (f m) (x, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>((((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2) = (x, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>(((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1 = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : LazyList α<VAR>ys : Thunk (LazyList α)<VAR>f : α → LazyList β<GOAL>(xs.append ys).bind f = (xs.bind f).append { fn := fun x => ys.get.bind f }
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s✝ s : Set G<GOAL>closure s ≤ normalClosure s
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l : List α✝<GOAL>(l₁ ++ l₂).Disjoint l ↔ l₁.Disjoint l ∧ l₂.Disjoint l
<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>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>s : Set β<VAR>hf : Injective f<VAR>hf' : Measurable f<VAR>h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ<VAR>hs : MeasurableSet s<GOAL>(comap f μ) (f ⁻¹' s) = μ (s ∩ range f)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>hs1 : 1 ∈ S<VAR>ht1 : 1 ∈ T<GOAL>hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>hs1 : 1 ∈ S<VAR>ht1 : 1 ∈ T<GOAL>1 = hST.equiv.symm (⟨1, hs1⟩, ⟨1, ht1⟩)
<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>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (↑(extChartAt I x) x)
<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>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContinuousWithinAt f s x ∧ ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (↑(extChartAt I x) x)
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f : M →ₗ[R] M<GOAL>((toMatrix b b) f).trace = ((toMatrix b b) ((id ∘ₗ f) ∘ₗ id)).trace
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f : M →ₗ[R] M<GOAL>((toMatrix b b) ((id ∘ₗ f) ∘ₗ id)).trace = ((toMatrix c b) id * (toMatrix c c) f * (toMatrix b c) id).trace
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f : M →ₗ[R] M<GOAL>((toMatrix c b) id * (toMatrix c c) f * (toMatrix b c) id).trace = ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace