ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}<VAR>F : E → ℝ := fun x => if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0<GOAL>eLpNorm (fun x => {x | C ≤ ‖f i x‖}.indicator (fun a => ‖f i a‖) x) p μ = eLpNorm (fun x => {x | C ≤ ‖f j x‖}.indicator (fun a => ‖f j a‖) x) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}<VAR>F : E → ℝ := fun x => if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0<VAR>F_meas : Measurable F<GOAL>eLpNorm (fun x => {x | C ≤ ‖f i x‖}.indicator (fun a => ‖f i a‖) x) p μ = eLpNorm (fun x => {x | C ≤ ‖f j x‖}.indicator (fun a => ‖f j a‖) x) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>this✝ : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}<VAR>F : E → ℝ := fun x => if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0<VAR>F_meas : Measurable F<VAR>this : ∀ (k : ι), (fun x => {x | C ≤ ‖f k x‖}.indicator (fun a => ‖f k a‖) x) = F ∘ f k<GOAL>eLpNorm (fun x => {x | C ≤ ‖f i x‖}.indicator (fun a => ‖f i a‖) x) p μ = eLpNorm (fun x => {x | C ≤ ‖f j x‖}.indicator (fun a => ‖f j a‖) x) p μ
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>hz : 0 < z<GOAL>0 < z⁻¹
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>hz : ∃ x > 0, ↑x = z<GOAL>0 < z⁻¹
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x : ℝ<VAR>hx : x > 0<VAR>hx' : ↑x = z<GOAL>0 < z⁻¹
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x : ℝ<VAR>hx : x > 0<VAR>hx' : ↑x = z<GOAL>0 < x⁻¹
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝ : Fintype ↑(G'.neighborSet v)<GOAL>(G'.neighborSet v).toFinset.card = G'.degree v
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n m : ℕ<VAR>f : R⟦X⟧<VAR>hnm : autoParam (n ≤ m) _auto✝<VAR>d : ℕ<GOAL>(trunc n ↑(trunc m f)).coeff d = (trunc n f).coeff d
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n m : ℕ<VAR>f : R⟦X⟧<VAR>hnm : autoParam (n ≤ m) _auto✝<VAR>d : ℕ<GOAL>(if d < n then (trunc m f).coeff d else 0) = if d < n then (coeff R d) f else 0
<VAR>l m r : List Char<VAR>p : Char → Bool<GOAL>ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r) ({ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.takeWhile p)
<VAR>l m r : List Char<VAR>p : Char → Bool<GOAL>ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r) { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) } }
<VAR>l m r : List Char<VAR>p : Char → Bool<GOAL>m ++ r = List.takeWhile p m ++ (List.dropWhile p m ++ r)
<VAR>L✝ : Type u_1<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L✝<VAR>inst✝⁶ : Algebra K L✝<VAR>inst✝⁵ : FiniteDimensional K L✝<VAR>F : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : Algebra.IsSeparable K F<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : CharZero K<VAR>x : 𝓞 F<VAR>this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K<VAR>L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)<GOAL>IsUnit ((norm K) x) ↔ IsUnit x
<VAR>L✝ : Type u_1<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L✝<VAR>inst✝⁶ : Algebra K L✝<VAR>inst✝⁵ : FiniteDimensional K L✝<VAR>F : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : Algebra.IsSeparable K F<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : CharZero K<VAR>x : 𝓞 F<VAR>this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K<VAR>L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)<VAR>this : FiniteDimensional F ↥L<GOAL>IsUnit ((norm K) x) ↔ IsUnit x
<VAR>L✝ : Type u_1<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L✝<VAR>inst✝⁶ : Algebra K L✝<VAR>inst✝⁵ : FiniteDimensional K L✝<VAR>F : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : Algebra.IsSeparable K F<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : CharZero K<VAR>x : 𝓞 F<VAR>this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K<VAR>L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)<VAR>this✝ : FiniteDimensional F ↥L<VAR>this : IsAlgClosure K (AlgebraicClosure F)<GOAL>IsUnit ((norm K) x) ↔ IsUnit x
<VAR>L✝ : Type u_1<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L✝<VAR>inst✝⁶ : Algebra K L✝<VAR>inst✝⁵ : FiniteDimensional K L✝<VAR>F : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : Algebra.IsSeparable K F<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : CharZero K<VAR>x : 𝓞 F<VAR>this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K<VAR>L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)<VAR>this✝¹ : FiniteDimensional F ↥L<VAR>this✝ : IsAlgClosure K (AlgebraicClosure F)<VAR>this : IsGalois F ↥L<GOAL>IsUnit ((norm K) x) ↔ IsUnit x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f : Perm α<GOAL>f.cycleFactorsFinset = ∅ ↔ f = 1
<VAR>b x : ℝ<VAR>hb : 0 < b<GOAL>IntegrableOn (fun x => rexp (-(b * x))) (Ioc 0 x) ℙ
<VAR>b x : ℝ<VAR>hb : 0 < b<GOAL>IntegrableOn (fun x => rexp (-b * x)) (Ioc 0 x) ℙ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X Y Z : Bipointed<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X Y Z : Bipointed<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(g.toFun ∘ f.toFun) X.toProd.2 = Z.toProd.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep = edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep = min (edist x y) (edist x y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hxy : x ≠ y<GOAL>edist x y = edist y x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>s : Set (Set E)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, Orthonormal 𝕜 fun x => ↑x<GOAL>Orthonormal 𝕜 fun x => ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f pf x n<VAR>hg : HasFiniteFPowerSeriesAt g pg x m<GOAL>HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<GOAL>∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>j k : ℤ<VAR>hk₀ : 0 < k<VAR>hk₁ : k ≤ ↑n<VAR>h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)<GOAL>∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>j k : ℤ<VAR>hk₀ : 0 < k<VAR>hk₁ : k ≤ ↑n<VAR>h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)<VAR>hk : ↑k.toNat = k<GOAL>∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>j k : ℤ<VAR>hk₀ : 0 < ↑k.toNat<VAR>hk₁ : ↑k.toNat ≤ ↑n<VAR>h : |↑↑k.toNat * ξ - ↑j| ≤ 1 / (↑n + 1)<VAR>hk : ↑k.toNat = k<GOAL>∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : CommRing α<VAR>inst✝⁴ : CommRing β<VAR>inst✝³ : CommRing γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : CommRing α<VAR>inst✝⁴ : CommRing β<VAR>inst✝³ : CommRing γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det = (blockDiagonal fun x => A.map fun a => (f a) 1).det * (blockDiagonal fun x => B.map fun b => (f 1) b).det
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : CommRing α<VAR>inst✝⁴ : CommRing β<VAR>inst✝³ : CommRing γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>∀ (x : β), (f 0) x = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : CommRing α<VAR>inst✝⁴ : CommRing β<VAR>inst✝³ : CommRing γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>∀ (x : α), (f x) 0 = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Fintype m<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : CommRing α<VAR>inst✝⁴ : CommRing β<VAR>inst✝³ : CommRing γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(blockDiagonal fun x => A.map fun a => (f a) 1).det * (blockDiagonal fun x => B.map fun b => (f 1) b).det = (A.map fun a => (f a) 1).det ^ Fintype.card n * (B.map fun b => (f 1) b).det ^ Fintype.card m
<VAR>x : ℂ<VAR>hx : x.im < 0<GOAL>(x ^ 2⁻¹).im = -√((abs x - x.re) / 2)
<VAR>x : ℂ<VAR>hx : x.im < 0<GOAL>-(2 * π) ≤ x.arg
<VAR>x : ℂ<VAR>hx : x.im < 0<GOAL>x.arg ≤ 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b✝ : WithTop α<VAR>b : α<VAR>hb : b ≠ 0<GOAL>⊤ * ↑b = Option.bind ⊤ fun a => Option.some (a * b)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b✝ : WithTop α<VAR>b : α<VAR>hb : b ≠ 0<GOAL>⊤ = Option.bind ⊤ fun a => Option.some (a * b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι✝ κ✝ : Type w<VAR>inst✝⁴ : Fintype ι✝<VAR>b✝ : Basis ι✝ R S<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x✝ : T<GOAL>(trace R S ∘ₗ ↑R (trace S T)) x✝ = (trace R T) x✝
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic 0 R = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>hb : 0 ≤ b<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉₊ ⌊b⌋₊
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ (last n✝)<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.castSucc<VAR>i : Fin n✝<VAR>y : α✝ i.castSucc<VAR>z : α✝ (last n✝)<VAR>n m : ℕ<VAR>α : Type u_1<VAR>f : Fin (n + m) → α<VAR>a : α<GOAL>∀ (x : Fin n), snoc f a (castAdd (m + 1) x) = f (castAdd m x)
<VAR>I : Type u<VAR>inst✝³ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : GradedObject I C<VAR>inst✝ : X.HasTensor Y<GOAL>(mapMap (((mapBifunctor (curriedTensor C) I I).map (𝟙 X)).app Y ≫ ((mapBifunctor (curriedTensor C) I I).obj X).map (𝟙 Y)) fun x => x.1 + x.2) = 𝟙 (tensorObj X Y)
<VAR>I : Type u<VAR>inst✝³ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : GradedObject I C<VAR>inst✝ : X.HasTensor Y<GOAL>𝟙 ((((mapBifunctor (curriedTensor C) I I).obj X).obj Y).mapObj fun x => x.1 + x.2) = 𝟙 (tensorObj X Y)
<VAR>n : Nat<VAR>α : Type u_1<VAR>f : Fin n → α → α<VAR>x : α<GOAL>foldr n f x = List.foldr f x (list n)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S ≤ 1<VAR>inst✝ : Module.Free F ↥S<VAR>a✝ : Nontrivial E<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S ≤ 1<VAR>inst✝ : Module.Free F ↥S<VAR>a✝ : Nontrivial E<VAR>κ : Type u_2<VAR>b : Basis κ F ↥S<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S ≤ 1<VAR>inst✝ : Module.Free F ↥S<VAR>a✝ : Nontrivial E<VAR>κ : Type u_2<VAR>b : Basis κ F ↥S<VAR>h1 : ¬Module.rank F ↥S = 1<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S ≤ 1<VAR>inst✝ : Module.Free F ↥S<VAR>a✝ : Nontrivial E<VAR>κ : Type u_2<VAR>b : Basis κ F ↥S<VAR>h1 : ¬Module.rank F ↥S = 1<VAR>this : IsEmpty κ<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S ≤ 1<VAR>inst✝ : Module.Free F ↥S<VAR>a✝ : Nontrivial E<VAR>κ : Type u_2<VAR>b : Basis κ F ↥S<VAR>h1 : ¬Module.rank F ↥S = 1<VAR>this✝ : IsEmpty κ<VAR>this : Subsingleton ↥S<GOAL>S = ⊥
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(x \ y) \ z = x \ y ⊓ x \ z
<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁷ : Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A A' B B' : C<VAR>inst✝⁶ : HasBinaryProduct A B<VAR>inst✝⁵ : HasBinaryProduct A' B'<VAR>inst✝⁴ : HasBinaryProduct (F.obj A) (F.obj B)<VAR>inst✝³ : HasBinaryProduct (F.obj A') (F.obj B')<VAR>inst✝² : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))<VAR>inst✝¹ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)<VAR>inst✝ : IsIso (prodComparison F A B)<GOAL>inv (prodComparison F A B) ≫ F.map prod.fst = prod.fst
<VAR>m n : ℕ<VAR>x✝ : Fin m × Fin n<VAR>x : Fin m<VAR>y : Fin n<VAR>H : 0 < n<GOAL>↑y / n + ↑x = 0 + ↑x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>hx : f x ≠ x<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : AddZeroClass α<VAR>M N : o → Matrix m n α<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>blockDiagonal (M + N) i✝ j✝ = (blockDiagonal M + blockDiagonal N) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : AddZeroClass α<VAR>M N : o → Matrix m n α<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>(if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 else 0) = (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) + if i✝.2 = j✝.2 then N i✝.2 i✝.1 j✝.1 else 0
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} 𝒮<VAR>inst✝³ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S T : 𝒮<VAR>a b c : 𝒳<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>φ : a ⟶ b<VAR>ψ : b ⟶ c<VAR>inst✝² : p.IsStronglyCartesian g ψ<VAR>inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)<VAR>inst✝ : p.IsHomLift f φ<VAR>a' : 𝒳<VAR>h : p.obj a' ⟶ R<VAR>τ : a' ⟶ b<VAR>hτ : p.IsHomLift (h ≫ f) τ<VAR>h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)<GOAL>∃! χ, p.IsHomLift h χ ∧ χ ≫ φ = τ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} 𝒮<VAR>inst✝³ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S T : 𝒮<VAR>a b c : 𝒳<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>φ : a ⟶ b<VAR>ψ : b ⟶ c<VAR>inst✝² : p.IsStronglyCartesian g ψ<VAR>inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)<VAR>inst✝ : p.IsHomLift f φ<VAR>a' : 𝒳<VAR>h : p.obj a' ⟶ R<VAR>τ : a' ⟶ b<VAR>hτ : p.IsHomLift (h ≫ f) τ<VAR>h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)<GOAL>(fun χ => p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)) ∧ ∀ (y : a' ⟶ a), (fun χ => p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, succ a < o.blsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>sup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ↔ ∀ a < lsub (o.familyOfBFamily f), succ a < lsub (o.familyOfBFamily f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : SemilatticeInf α<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : InfHomClass F α β<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<GOAL>s ⊼ s = s ↔ InfClosed ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x✝ y✝ : α<GOAL>s(x✝, y✝) ∈ filter IsDiag (image Sym2.mk (s ×ˢ s)) ↔ s(x✝, y✝) ∈ image Sym2.mk s.diag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x✝ y✝ : α<GOAL>(∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ s(x✝, y✝).IsDiag ↔ ∃ a b, (a ∈ s ∧ a = b) ∧ s(a, b) = s(x✝, y✝)
<VAR>m n✝ : ℕ<GOAL>↑(-1) = n✝ + 1
<VAR>m n✝ : ℕ<GOAL>n✝ + 1 < n✝ + 1 + 1
<VAR>X✝ Y✝ Z✝ : CommRingCatᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun R => sheafedSpaceObj (unop R), map := fun {X Y} f => sheafedSpaceMap f.unop }.map (f ≫ g) = { obj := fun R => sheafedSpaceObj (unop R), map := fun {X Y} f => sheafedSpaceMap f.unop }.map f ≫ { obj := fun R => sheafedSpaceObj (unop R), map := fun {X Y} f => sheafedSpaceMap f.unop }.map g
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).dens + (s \ t).dens = s.dens
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>r : β<VAR>s : Set α<VAR>f : α →ₛ β<VAR>hs : MeasurableSet s<GOAL>r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ↑f '' s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝⁴ : DecidableEq o<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : (i : o) → DecidableEq (m' i)<VAR>inst✝ : One α<GOAL>(blockDiagonal' fun i => diagonal fun x => 1) = diagonal fun x => 1
<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 a₁ a₂ : α<VAR>s : Finset β<VAR>hf : mulSupport f ⊆ ↑s<GOAL>∏' (b : β), f b = ∏ b ∈ s, f b
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>y : β<GOAL>μ.prod (dirac y) = map (fun x => (x, y)) μ