ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α<VAR>b : ↥t<GOAL>(fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)) ((fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, Quotient.mk'' b)) = (Quotient.mk'' a, Quotient.mk'' b)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α<VAR>b : ↥t<VAR>key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a<GOAL>(fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)) ((fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, Quotient.mk'' b)) = (Quotient.mk'' a, Quotient.mk'' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>a ∈ Ι b c → b ∈ Ι a c → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>IsHomogeneous 𝒜 I.radical
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>IsHomogeneous 𝒜 (InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
<VAR>A B : CommGrp<VAR>f : A ⟶ B<GOAL>Epi f ↔ Function.Surjective ⇑f
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card<VAR>A' : Finset α<VAR>hAA' : A' ⊆ A<GOAL>(A * C).card * A'.card ≤ (A' * C).card * A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card<VAR>hAA' : ∅ ⊆ A<GOAL>(A * C).card * ∅.card ≤ (∅ * C).card * A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card<VAR>A' : Finset α<VAR>hAA' : A' ⊆ A<VAR>hA' : A'.Nonempty<GOAL>(A * C).card * A'.card ≤ (A' * C).card * A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card<VAR>A' : Finset α<VAR>hAA' : A' ⊆ A<VAR>hA' : A'.Nonempty<VAR>hA₀ : 0 < ↑A.card<GOAL>(A * C).card * A'.card ≤ (A' * C).card * A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hA : A.Nonempty<VAR>hAB : A ⊆ B<VAR>h : ∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card<VAR>A' : Finset α<VAR>hAA' : A' ⊆ A<VAR>hA' : A'.Nonempty<VAR>hA₀ : 0 < ↑A.card<VAR>hA₀' : 0 < ↑A'.card<GOAL>(A * C).card * A'.card ≤ (A' * C).card * A.card
<VAR>x : CliffordAlgebra Q<GOAL>reverse x = x
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (⇑g) (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>I : 0 < ε ^ (1 / p)<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (⇑g) (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>I : 0 < ε ^ (1 / p)<VAR>A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (⇑g) (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>I : 0 < ε ^ (1 / p)<VAR>A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0<VAR>B : ENNReal.ofReal p ≠ 0<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (⇑g) (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>I : 0 < ε ^ (1 / p)<VAR>A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0<VAR>B : ENNReal.ofReal p ≠ 0<VAR>g : α →ᵇ E<VAR>hg : eLpNorm (f - ⇑g) (↑p.toNNReal) μ ≤ ENNReal.ofReal (ε ^ (1 / p))<VAR>g_mem : Memℒp (⇑g) (↑p.toNNReal) μ<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (⇑g) (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>I : 0 < ε ^ (1 / p)<VAR>A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0<VAR>B : ENNReal.ofReal p ≠ 0<VAR>g : α →ᵇ E<VAR>g_mem : Memℒp (⇑g) (↑p.toNNReal) μ<VAR>hg : eLpNorm (f - ⇑g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))<GOAL>∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>I : 0 < ε ^ (1 / p)<VAR>A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0<VAR>B : ENNReal.ofReal p ≠ 0<VAR>g : α →ᵇ E<VAR>g_mem : Memℒp (⇑g) (↑p.toNNReal) μ<VAR>hg : (∫ (a : α), ‖(f - ⇑g) a‖ ^ p ∂μ) ^ p⁻¹ ≤ ε ^ p⁻¹<GOAL>0 ≤ ∫ (a : α), ‖(f - ⇑g) a‖ ^ p ∂μ
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>Tendsto (fun δ => (thickening δ E).mulIndicator f) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f))
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>∀ (x : α), Tendsto (fun i => (thickening i E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>Tendsto (fun i => (thickening i E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>Tendsto (fun x_1 => (closure E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))
<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>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M✝ : Type u_9<VAR>M₁ : Type u_10<VAR>M₂✝ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>R : outParam (Type u_17)<VAR>M : outParam (Type u_18)<VAR>M₂ : outParam (Type u_19)<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>F : Type u_20<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : LinearMapClass F R M M₂<VAR>f : F<VAR>r : R<VAR>x : M<GOAL>f (r • x) = r • f x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : Center C<GOAL>(α_ X Y Z).inv.f = (α_ X.fst Y.fst Z.fst).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : Center C<GOAL>(α_ X.fst Y.fst Z.fst).hom ≫ (α_ X Y Z).inv.f = 𝟙 ((X ⊗ Y) ⊗ Z).fst
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : Center C<GOAL>(𝟙 ((X ⊗ Y) ⊗ Z)).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop<VAR>ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1), P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ evenOdd Q 1<GOAL>P x hx
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop<VAR>ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1), P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ evenOdd Q 1<VAR>ιv : CliffordAlgebra Q<GOAL>∀ (h : ιv ∈ LinearMap.range (CliffordAlgebra.ι Q) ^ ZMod.val 1), P ιv ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop<VAR>ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1), P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ evenOdd Q 1<VAR>ιv : CliffordAlgebra Q<VAR>h : ιv ∈ LinearMap.range (CliffordAlgebra.ι Q) ^ ZMod.val 1<GOAL>P ιv ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop<VAR>ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1), P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ evenOdd Q 1<VAR>ιv : CliffordAlgebra Q<VAR>h✝ : ιv ∈ LinearMap.range (CliffordAlgebra.ι Q) ^ ZMod.val 1<VAR>h : ιv ∈ LinearMap.range (CliffordAlgebra.ι Q)<GOAL>P ιv ⋯
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>(μ.toFinite.withDensity fun x => if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1).restrict μ.sigmaFiniteSet = μ.restrict μ.sigmaFiniteSet
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : μ.restrict μ.sigmaFiniteSet = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSet<GOAL>(μ.toFinite.withDensity fun x => if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1).restrict μ.sigmaFiniteSet = μ.restrict μ.sigmaFiniteSet
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : μ.restrict μ.sigmaFiniteSet = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSet<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((μ.toFinite.withDensity fun x => if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1).restrict μ.sigmaFiniteSet) s = ((μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSet) s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : μ.restrict μ.sigmaFiniteSet = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSet<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s ∩ μ.sigmaFiniteSet, if μ.densityToFinite a ≠ ⊤ then μ.densityToFinite a else 1 ∂μ.toFinite = ∫⁻ (a : α) in s ∩ μ.sigmaFiniteSet, μ.densityToFinite a ∂μ.toFinite
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : μ.restrict μ.sigmaFiniteSet = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSet<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ s ∩ μ.sigmaFiniteSet<GOAL>μ.densityToFinite x = if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : μ.restrict μ.sigmaFiniteSet = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSet<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : x ∈ s ∧ ¬μ.densityToFinite x = ⊤<GOAL>μ.densityToFinite x = if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1
<VAR>G : Type u_1<VAR>inst✝¹ : CommSemigroup G<VAR>inst✝ : IsCancelMul G<VAR>g x✝ : G<GOAL>(mulLeftEmbedding g) x✝ = (mulRightEmbedding g) x✝
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>n : ℕ<VAR>v : Vector G n<GOAL>v.toList.prod⁻¹ ::ᵥ v ∈ vectorsProdEqOne G (n + 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>n : ℕ<VAR>v : ↑(vectorsProdEqOne G (n + 1))<GOAL>(↑v).head * (↑v).tail.toList.prod = 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>n : ℕ<VAR>v : ↑(vectorsProdEqOne G (n + 1))<GOAL>(↑v).toList.prod = 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.80198, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<GOAL>Epi S.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.80198, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<VAR>this : IsSplitEpi S.g<GOAL>Epi S.g
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ₁ χ₂ : MulChar R R'<VAR>a : Rˣ<GOAL>(equivToUnitHom (χ₁ * χ₂)) a = (equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ₁ χ₂ : MulChar R R'<VAR>a : Rˣ<GOAL>↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ₁ χ₂ : MulChar R R'<VAR>a : Rˣ<GOAL>↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a) * ↑((equivToUnitHom χ₂) a)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N P : Matrix m m R<GOAL>(M * N * P).det = (M * P * N).det
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>f : G ↪ H<VAR>mul : ∀ (x y : G), f (x * y) = f x * f y<GOAL>UniqueMul (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x z - o.oangle y z = o.oangle x y
<VAR>xl xr : Type u<VAR>s : Set PGame<VAR>inst✝ : Small.{u, u + 1} ↑s<GOAL>BddBelow s
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a✝ b c a : α<GOAL>a / b < a / c ↔ c < b
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C₁<VAR>inst✝⁶ : Category.{u_8, u_2} C₂<VAR>inst✝⁵ : Category.{u_5, u_3} D₁<VAR>inst✝⁴ : Category.{u_7, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G' : D₁ ⥤ D₂<VAR>F' : D₂ ⥤ D₁<VAR>inst✝¹ : CatCommSq G L₁ L₂ G'<VAR>inst✝ : CatCommSq F L₂ L₁ F'<VAR>X₁ : C₁<GOAL>(adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) = L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α✝<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ b✝ : α✝<VAR>s : Finset β✝<VAR>inst✝⁵ : ContinuousMul α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>a a' : α<VAR>hf : HasProd f a<VAR>b : β<VAR>x : α<VAR>hf' : HasProd (update f b x) a'<VAR>this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1<GOAL>a * x = a' * f b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α✝<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ b✝ : α✝<VAR>s : Finset β✝<VAR>inst✝⁵ : ContinuousMul α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>a a' : α<VAR>hf : HasProd f a<VAR>b : β<VAR>x : α<VAR>hf' : HasProd (update f b x) a'<VAR>this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1<VAR>h : HasProd (fun b_1 => f b_1 * if b_1 = b then x else 1) (a * x)<GOAL>a * x = a' * f b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α✝<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ b✝ : α✝<VAR>s : Finset β✝<VAR>inst✝⁵ : ContinuousMul α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>a a' : α<VAR>hf : HasProd f a<VAR>b : β<VAR>x : α<VAR>hf' : HasProd (update f b x) a'<VAR>this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1<VAR>h : HasProd (fun b_1 => update f b x b_1 * if b_1 = b then f b else 1) (a * x)<GOAL>a * x = a' * f b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<GOAL>quadraticCharFun F 0 = 0
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>a b : D<VAR>mcf : HasMaxCutPropertyAt f a b<VAR>hab : a ≠ b<VAR>ω : FractionalOperation D 2<VAR>symmega : ω.IsSymmetric<VAR>r : Fin 2 → D<VAR>rin : r ∈ ω.tt ![![a, b], ![b, a]]<GOAL>f ![a, b] < f r
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>a b : D<VAR>mcf : HasMaxCutPropertyAt f a b<VAR>hab : a ≠ b<VAR>ω : FractionalOperation D 2<VAR>symmega : ω.IsSymmetric<VAR>r : Fin 2 → D<VAR>rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r<GOAL>f ![a, b] < f r
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>a b : D<VAR>mcf : HasMaxCutPropertyAt f a b<VAR>hab : a ≠ b<VAR>ω : FractionalOperation D 2<VAR>symmega : ω.IsSymmetric<VAR>r : Fin 2 → D<VAR>rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r<GOAL>f ![a, b] < f ![r 0, r 1]
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>a b : D<VAR>mcf : HasMaxCutPropertyAt f a b<VAR>hab : a ≠ b<VAR>ω : FractionalOperation D 2<VAR>symmega : ω.IsSymmetric<VAR>r : Fin 2 → D<VAR>rin : ∃ a_1 ∈ ω, (fun i => a_1 (swap ![![a, b], ![b, a]] i)) = r<GOAL>f ![a, b] ≠ f ![r 0, r 1]
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>a b : D<VAR>mcf : HasMaxCutPropertyAt f a b<VAR>hab : a ≠ b<VAR>ω : FractionalOperation D 2<VAR>symmega : ω.IsSymmetric<VAR>o : (Fin 2 → D) → D<VAR>in_omega : o ∈ ω<VAR>equ : f ![a, b] = f ![(fun i => o (swap ![![a, b], ![b, a]] i)) 0, (fun i => o (swap ![![a, b], ![b, a]] i)) 1]<VAR>asymm : (fun i => o (swap ![![a, b], ![b, a]] i)) 0 ≠ (fun i => o (swap ![![a, b], ![b, a]] i)) 1<GOAL>(o fun j => ![![a, b], ![b, a]] j 0) = o fun j => ![![a, b], ![b, a]] j 1
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>F_int k (↑a) t = F_nat k a t + F_nat k (1 - a) t
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>∑' (n : ℤ), f_int k a t n = ∑' (n : ℕ), f_nat k a t n + ∑' (n : ℕ), f_nat k (1 - a) t n
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>t : ℝ<VAR>ht : 0 < t<VAR>n : ℤ<GOAL>f_int k a t n = Int.rec (f_nat k a t) (f_nat k (1 - a) t) n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>p q r : R[X]<VAR>f : A →ₐ[R] B<GOAL>mapAlgHom f = eval₂AlgHom' (CAlgHom.comp f) X ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>p q r : R[X]<VAR>f : A →ₐ[R] B<GOAL>∀ (x : A[X]), (mapAlgHom f) x = (eval₂AlgHom' (CAlgHom.comp f) X ⋯) x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>a : α<VAR>l : List α<VAR>h : f a = none<GOAL>lookmap f (a :: l) = a :: lookmap f l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>a : α<VAR>l : List α<VAR>h : f a = none<GOAL>(match f a with | some b => b :: l | none => lookmap.go f l (#[].push a)) = a :: lookmap.go f l #[]