ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t✝ : Set α<VAR>f✝ g f : α → E<VAR>s t : Set α<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ = ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ + ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t✝ : Set α<VAR>f✝ g f : α → E<VAR>s t : Set α<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<VAR>this : Fact (μ s < ⊤)<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ = ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ + ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t✝ : Set α<VAR>f✝ g f : α → E<VAR>s t : Set α<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<VAR>this✝ : Fact (μ s < ⊤)<VAR>this : Fact (μ t < ⊤)<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ = ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ + ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>G.IsNClique n ∅ ↔ n = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : StarRing R<VAR>x : R<VAR>hx : x ∈ skewAdjoint R<VAR>z : R<GOAL>star z * x * z ∈ skewAdjoint R
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>inst✝⁷ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁶ : SMul R ℝ≥0<VAR>inst✝⁵ : SMul R ℝ≥0∞<VAR>inst✝⁴ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : BorelSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν<GOAL>↑μ = ↑ν
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonUnitalCommSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype o<VAR>A : Matrix m n α<VAR>B : Matrix o n α<VAR>x : o → α<GOAL>A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNRat
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℚ<VAR>h : x < y<VAR>hy : 0 < y<GOAL>∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>IsClosed (range ENNReal.toEReal)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>IsClosed (Ici 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<GOAL>generateFrom (⋃ n, memPartition t n) = generateFrom (range t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>u : Set α<VAR>hu : u ∈ ⋃ n, memPartition t n<GOAL>MeasurableSet u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>u : Set α<VAR>hu : u ∈ range t<GOAL>MeasurableSet u
<VAR>R : Type u₁<VAR>inst✝¹ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>x : Ring.Perfection R p<VAR>n : ℕ<GOAL>(coeff R p n) (((frobenius (Ring.Perfection R p) p).comp (pthRoot R p)) x) = (coeff R p n) ((RingHom.id (Ring.Perfection R p)) x)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : SheafOfTypes (J.over Y)<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : Over Y<VAR>f₁ : W ⟶ (Over.map f).obj Y₁<VAR>f₂ : W ⟶ (Over.map f).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂<VAR>W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯<GOAL>F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : SheafOfTypes (J.over Y)<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : Over Y<VAR>f₁ : W ⟶ (Over.map f).obj Y₁<VAR>f₂ : W ⟶ (Over.map f).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂<VAR>W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯<VAR>g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯<GOAL>F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : SheafOfTypes (J.over Y)<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : Over Y<VAR>f₁ : W ⟶ (Over.map f).obj Y₁<VAR>f₂ : W ⟶ (Over.map f).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂<VAR>W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯<VAR>g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯<VAR>e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯<GOAL>F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : SheafOfTypes (J.over Y)<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : Over Y<VAR>f₁ : W ⟶ (Over.map f).obj Y₁<VAR>f₂ : W ⟶ (Over.map f).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂<VAR>W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯<VAR>g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯<VAR>e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯<GOAL>F.val.map f₁.op (x g₁ hg₁) = F.val.map e.inv.op (((Over.map f).op ⋙ F.val).map g₁'.op (x g₁ hg₁))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : SheafOfTypes (J.over Y)<VAR>Z : Over X<VAR>T : Presieve Z<VAR>x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : Over X<VAR>W : Over Y<VAR>f₁ : W ⟶ (Over.map f).obj Y₁<VAR>f₂ : W ⟶ (Over.map f).obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂<VAR>W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)<VAR>g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯<VAR>g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯<VAR>e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯<GOAL>F.val.map f₂.op (x g₂ hg₂) = F.val.map e.inv.op (((Over.map f).op ⋙ F.val).map g₂'.op (x g₂ hg₂))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝¹ : CommSemiring α<VAR>inst✝ : DecidableEq ι<VAR>f g : ι → α<VAR>s : Finset ι<GOAL>∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Surreal<GOAL>BddAbove (Set.range f)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Subtype Numeric<GOAL>BddAbove (Set.range fun i => ⟦f i⟧)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Subtype Numeric<VAR>g : ι → PGame := Subtype.val ∘ f<GOAL>BddAbove (Set.range fun i => ⟦f i⟧)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Subtype Numeric<VAR>g : ι → PGame := Subtype.val ∘ f<VAR>hg : ∀ (i : ι), (g i).Numeric<GOAL>BddAbove (Set.range fun i => ⟦f i⟧)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>g : ι → PGame<VAR>hg : ∀ (i : ι), (g i).Numeric<VAR>x : PGame := PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1} (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim<GOAL>BddAbove (Set.range fun i => mk (g i) ⋯)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>g : ι → PGame<VAR>hg : ∀ (i : ι), (g i).Numeric<VAR>x : PGame := PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1} (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim<VAR>i : ι<GOAL>mk (g i) ⋯ ≤ mk x ⋯
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>g : ι → PGame<VAR>hg : ∀ (i : ι), (g i).Numeric<VAR>x : PGame := PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1} (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim<VAR>i : ι<GOAL>(∀ (i_1 : (g ((equivShrink ι).symm ((equivShrink ι) i))).LeftMoves), (g ((equivShrink ι).symm ((equivShrink ι) i))).moveLeft i_1 ⧏ x) ∧ ∀ (j : x.RightMoves), g ((equivShrink ι).symm ((equivShrink ι) i)) ⧏ x.moveRight j
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s (closure s) = 0
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<GOAL>(f * g).signAux = f.signAux * g.signAux
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<GOAL>(f * g).signAux = f.signAux * g⁻¹.signAux
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<GOAL>(∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) = (∏ x ∈ finPairsLT n, if f x.fst ≤ f x.snd then -1 else 1) * ∏ x ∈ finPairsLT n, if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<GOAL>(∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) = ∏ x ∈ finPairsLT n, (if f x.fst ≤ f x.snd then -1 else 1) * if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<GOAL>∀ a ∈ finPairsLT n, (if (f * g) a.fst ≤ (f * g) a.snd then -1 else 1) = (if f (g.signBijAux a).fst ≤ f (g.signBijAux a).snd then -1 else 1) * if g⁻¹ (g.signBijAux a).fst ≤ g⁻¹ (g.signBijAux a).snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<VAR>a b : Fin n<VAR>hab : ⟨a, b⟩ ∈ finPairsLT n<GOAL>(if (f * g) a ≤ (f * g) b then -1 else 1) = (if f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤ f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then -1 else 1) * if g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤ g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<VAR>a b : Fin n<VAR>hab : ⟨a, b⟩ ∈ finPairsLT n<GOAL>(if f (g a) ≤ f (g b) then -1 else 1) = (if f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤ f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then -1 else 1) * if g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤ g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f g : Perm (Fin n)<VAR>a b : Fin n<VAR>hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst<GOAL>(if f (g a) ≤ f (g b) then -1 else 1) = (if f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤ f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then -1 else 1) * if g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤ g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then -1 else 1
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.131591<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i : ι₁<VAR>x : M₁ i<VAR>y : M₂'<GOAL>(directSumLeft R M₁ M₂').symm ((lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) = (lof R ι₁ M₁ i) x ⊗ₜ[R] y
<VAR>a x z : ℂ<GOAL>(-I).arg = -(π / 2)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g✝ : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>g' : S →ₗ[R] N<GOAL>map f g ∘ₗ lTensor M g' = map f (g ∘ₗ g')
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y z : α<VAR>h : x ∈ y :: z :: l<VAR>hx : x = y<GOAL>(y :: z :: l).prev x h = (z :: l).getLast ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ f a = (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 p4 p5 : P<VAR>hapc : ∠ p1 p5 p3 = π<VAR>hbpd : ∠ p2 p5 p4 = π<GOAL>∠ p1 p5 p2 = ∠ p3 p5 p4
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedAddCommGroup F<VAR>a b : ℝ<GOAL>IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ 0 ∉ [[a, b]]
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>map (↑(opLinearEquiv R)) (M * N) = map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>map (↑(opLinearEquiv R)) (M * N) ≤ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N : L.Substructure M<GOAL>N.CG ↔ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N : L.Substructure M<GOAL>(∃ S, S.Countable ∧ (closure L).toFun S = N) ↔ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>↑z.num ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<VAR>n : ℕ<VAR>hn : f ^ n = ↑z.den<GOAL>↑z.num ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<VAR>n : ℕ<VAR>hn : f ^ n = ↑z.den<VAR>this : f ^ n ≠ 0<GOAL>↑z.num ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<VAR>n : ℕ<VAR>hn : f ^ n = ↑z.den<VAR>this : f ^ n ≠ 0<GOAL>HomogeneousLocalization.mk z = HomogeneousLocalization.mk { deg := m * n, num := ⟨↑z.num, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>z : NumDenSameDeg 𝒜 (Submonoid.powers f)<VAR>n : ℕ<VAR>hn : f ^ n = ↑z.den<VAR>this : f ^ n ≠ 0<GOAL>↑z.num ∈ 𝒜 (n * m)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<GOAL>Splits φ P.toPoly ↔ card (map φ P).roots = 3
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : (map φ P).a ≠ 0<GOAL>Splits φ P.toPoly ↔ card (map φ P).roots = 3
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : (map φ P).a ≠ 0<GOAL>Splits ((RingHom.id K).comp φ) P.toPoly ↔ card (map φ P).roots = 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<GOAL>↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<GOAL>↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<GOAL>↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<GOAL>↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<GOAL>↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this : (2 * dValue N - 1) ^ n ≤ N<GOAL>↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this : (2 * dValue N - 1) ^ n ≤ N<GOAL>↑N * rexp (-4 * √(log ↑N)) ≤ (↑N ^ (↑(nValue N))⁻¹ / rexp 1) ^ (n - 2) / ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this : (2 * dValue N - 1) ^ n ≤ N<GOAL>↑N * rexp (-4 * √(log ↑N)) ≤ ↑N * (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this : (2 * dValue N - 1) ^ n ≤ N<GOAL>rexp (-4 * √(log ↑N)) ≤ (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this : (2 * dValue N - 1) ^ n ≤ N<GOAL>rexp (-4 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this✝ : (2 * dValue N - 1) ^ n ≤ N<VAR>this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))<GOAL>rexp (-4 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this✝ : (2 * dValue N - 1) ^ n ≤ N<VAR>this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))<GOAL>rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this✝ : (2 * dValue N - 1) ^ n ≤ N<VAR>this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))<GOAL>rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>hN : 4096 ≤ N<VAR>n : ℕ := nValue N<VAR>hn : 0 < ↑n<VAR>hd : 0 < dValue N<VAR>hN₀ : 0 < ↑N<VAR>hn₂ : 2 < n<VAR>this✝ : (2 * dValue N - 1) ^ n ≤ N<VAR>this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))<GOAL>1 < ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f g s t : ι → α<VAR>a b : α<VAR>inst✝ : Nonempty ι<GOAL>⨆ x, a = a