ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>↑‖⟪x, y⟫_𝕜‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 - ↑(normSq x) * ↑‖⟪x, y⟫_𝕜‖ ^ 2 + ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) = ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫_𝕜‖ ^ 2)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : centroid k fs₁ s.points = centroid k fs₂ s.points<GOAL>fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) = (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)<GOAL>fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) = (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)<VAR>ha : (↑univ).indicator (centroidWeightsIndicator k fs₁) = (↑univ).indicator (centroidWeightsIndicator k fs₂)<GOAL>fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) = (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)<VAR>ha : ∀ (a : Fin (n + 1)), (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) a = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) a<GOAL>fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) = (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)<VAR>i : Fin (n + 1)<VAR>ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i<VAR>key : ∀ (n : ℕ), ↑n + 1 ≠ 0<GOAL>i ∈ fs₁ ↔ i ∈ fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) = (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)<VAR>i : Fin (n + 1)<VAR>ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i<VAR>key : ∀ (n : ℕ), ↑n + 1 ≠ 0<VAR>hi : i ∈ fs₁<VAR>hni : i ∉ fs₂<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<VAR>h : (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) = (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)<VAR>i : Fin (n + 1)<VAR>ha : (↑fs₁).indicator (const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i = (↑fs₂).indicator (const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i<VAR>key : ∀ (n : ℕ), ↑n + 1 ≠ 0<VAR>hi : i ∈ fs₂<VAR>hni : i ∉ fs₁<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cocycle F G 0<GOAL>Cochain.ofHom z.homOf = ↑z
<VAR>f g : ℕ → ℂ<VAR>s a : ℂ<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = g n<GOAL>LSeriesHasSum f s a ↔ LSeriesHasSum g s a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>eLpNorm (s.indicator f) ⊤ μ = eLpNorm f ⊤ (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hp : p ≠ ⊤<GOAL>eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<GOAL>IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun x => x + dt) v
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v<GOAL>IsIntegralCurve γ v
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v<GOAL>γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v<VAR>t : ℝ<GOAL>γ t = ((γ ∘ fun x => x + dt) ∘ fun x => x + -dt) t
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : Path.Homotopy (toLoop i p) (toLoop i q)<GOAL>∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (0, x_1) = ↑p x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : Path.Homotopy (toLoop i p) (toLoop i q)<GOAL>∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (1, x_1) = ↑q x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : Path.Homotopy (toLoop i p) (toLoop i q)<GOAL>∀ (t : ↑I), ∀ x_1 ∈ Cube.boundary N, { toFun := fun x_2 => { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun (t, x_2), continuous_toFun := ⋯ } x_1 = ↑p x_1
<VAR>α : Type u_1<VAR>m : Num<VAR>n : ℕ<GOAL>↑(m <<< n) = ↑m <<< n
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>↑0 = ↑zero <<< n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a✝ : PosNum<GOAL>↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a✝ : PosNum<GOAL>↑(a✝ <<< n) = ↑a✝ <<< n
<VAR>α : Type u_1<VAR>a✝ : PosNum<VAR>n : ℕ<VAR>IH : ↑(a✝ <<< n) = ↑a✝ <<< n<GOAL>↑(a✝ <<< (n + 1)) = ↑a✝ <<< (n + 1)
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>w : List T<VAR>hgw : w ∈ g.reverse.language<GOAL>w.reverse ∈ g.language
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>w : List T<VAR>hgw : w ∈ g.reverse.language<GOAL>w.reverse ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w).reverse
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra ℂ A<VAR>hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0<VAR>a : A<VAR>z : ℂ<VAR>h : z ∈ σ a<GOAL>(algebraMap ℂ A) z = a
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>map f (comap f J) = f.idealRange ⊓ J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>map f (comap f J) ≤ f.idealRange ⊓ J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>f.idealRange ⊓ J ≤ map f (comap f J)
<VAR>n : ℕ<GOAL>(2 ^ n).testBit n = true
<VAR>n : ℕ<GOAL>(1 &&& 1 != 0) = true
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i j : ι<VAR>inst✝³ : K.HasHomology i<VAR>inst✝² : K.HasHomology j<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : L.HasHomology j<GOAL>K.opcyclesToCycles i j ≫ K.homologyπ j = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α✝<VAR>π : β → Type u_3<VAR>inst✝² : Fintype β<VAR>inst✝¹ : (b : β) → PseudoMetricSpace (π b)<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_4<VAR>inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>f g : (j : Fin n) → α (i.succAbove j)<GOAL>dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) (Metric.ball (t₀ / a) ε)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)<GOAL>IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) (Metric.ball (t₀ / a) (ε / |a|))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)<GOAL>Metric.ball (t₀ / a) (ε / |a|) = {t | t * a ∈ Metric.ball t₀ ε}
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)<VAR>t : ℝ<GOAL>t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ t ∈ {t | t * a ∈ Metric.ball t₀ ε}
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ g₃ g : G<GOAL>⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝⁷ : Fact (1 ≤ p)<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Semiring 𝕜<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (β✝ i)<VAR>inst✝² : (i : ι) → Module 𝕜 (α i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (β✝ i)<VAR>c : 𝕜<VAR>β : Type u_5<VAR>inst✝ : SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>b : β<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝⁷ : Fact (1 ≤ p)<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Semiring 𝕜<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (β✝ i)<VAR>inst✝² : (i : ι) → Module 𝕜 (α i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (β✝ i)<VAR>c : 𝕜<VAR>β : Type u_5<VAR>inst✝ : SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>b : β<VAR>h : p = ⊤<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝⁷ : Fact (1 ≤ p)<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Semiring 𝕜<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (β✝ i)<VAR>inst✝² : (i : ι) → Module 𝕜 (α i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (β✝ i)<VAR>c : 𝕜<VAR>β : Type u_5<VAR>inst✝ : SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>b : β<VAR>h : 1 ≤ p.toReal<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>m : Multiset α<GOAL>m.toList = [a] ↔ m = {a}
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>ι : Type u_2<VAR>f : ι → Subgroup α<GOAL>∀ (a₁ a₂ : α), (fun q i => quotientMapOfLE ⋯ q) (Quotient.mk'' a₁) = (fun q i => quotientMapOfLE ⋯ q) (Quotient.mk'' a₂) → Quotient.mk'' a₁ = Quotient.mk'' a₂
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>f : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf Mg mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>hMg : Mg ≤ mΩ<VAR>h_ind : Indep Mf Mg μ<VAR>h_meas_f : Measurable f<GOAL>∀ {g : Ω → ℝ≥0∞}, Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>f : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf Mg mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>hMg : Mg ≤ mΩ<VAR>h_ind : Indep Mf Mg μ<VAR>h_meas_f : Measurable f<VAR>h_measM_f : Measurable f<GOAL>∀ {g : Ω → ℝ≥0∞}, Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>f : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf Mg mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>hMg : Mg ≤ mΩ<VAR>h_ind : Indep Mf Mg μ<VAR>h_meas_f : Measurable f<VAR>h_measM_f : Measurable f<GOAL>∀ (c : ℝ≥0∞) ⦃s : Set Ω⦄, MeasurableSet s → ∫⁻ (ω : Ω), f ω * s.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun x => c) ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>f : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf Mg mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>hMg : Mg ≤ mΩ<VAR>h_ind : Indep Mf Mg μ<VAR>h_meas_f : Measurable f<VAR>h_measM_f : Measurable f<GOAL>∀ ⦃f_1 g : Ω → ℝ≥0∞⦄, Disjoint (Function.support f_1) (Function.support g) → Measurable f_1 → Measurable g → ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ → ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>f : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf Mg mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>hMg : Mg ≤ mΩ<VAR>h_ind : Indep Mf Mg μ<VAR>h_meas_f : Measurable f<VAR>h_measM_f : Measurable f<GOAL>∀ ⦃f_1 : ℕ → Ω → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f_1 n)) → Monotone f_1 → (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) → ∫⁻ (ω : Ω), f ω * (fun x => ⨆ n, f_1 n x) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x => ⨆ n, f_1 n x) ω ∂μ
<VAR>a b : ℤ<GOAL>Fintype.card ↑(Set.Ioo a b) = (b - a - 1).toNat
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<GOAL>IsDedekindDomain Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<GOAL>IsDedekindDomain Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<GOAL>IsDedekindDomain Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this✝ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<VAR>this : IsScalarTower A Aₘ (FractionRing A)<GOAL>IsDedekindDomain Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<VAR>this✝ : IsScalarTower A Aₘ (FractionRing A)<VAR>this : IsFractionRing Aₘ (FractionRing A)<GOAL>IsDedekindDomain Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<VAR>this✝ : IsScalarTower A Aₘ (FractionRing A)<VAR>this : IsFractionRing Aₘ (FractionRing A)<GOAL>IsDomain Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<VAR>this✝ : IsScalarTower A Aₘ (FractionRing A)<VAR>this : IsFractionRing Aₘ (FractionRing A)<GOAL>IsNoetherianRing Aₘ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization M Aₘ<VAR>h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)<VAR>this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra<VAR>this✝ : IsScalarTower A Aₘ (FractionRing A)<VAR>this : IsFractionRing Aₘ (FractionRing A)<GOAL>Ring.DimensionLEOne Aₘ