ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K V₂<VAR>inst✝³ : Fintype ι₁<VAR>inst✝² : Fintype ι₂<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>B₁ : Basis ι₁ K V₁<VAR>B₂ : Basis ι₂ K V₂<VAR>M : Matrix ι₁ ι₂ K<GOAL>(LinearMap.toMatrix B₁.dualBasis B₂.dualBasis) ((toLin B₁.dualBasis B₂.dualBasis) Mᵀ) = (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis) (Module.Dual.transpose ((toLin B₂ B₁) M))
<VAR>q : ℍ<GOAL>(exp ℝ q).re = exp ℝ q.re * Real.cos ‖q - ↑q.re‖
<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(bit b ↑n).testBit m.succ = (↑n).testBit m
<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m
<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(match bit b -[n+1], m.succ with | ofNat m, n => m.testBit n | -[m+1], n => !m.testBit n) = !n.testBit m
<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m
<VAR>x✝ y x : ℝ<GOAL>arcsin (-x) = -arcsin x
<VAR>x✝ y x : ℝ<VAR>hx₁ : x ≤ -1<GOAL>arcsin (-x) = -arcsin x
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<GOAL>arcsin (-x) = -arcsin x
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : 1 ≤ x<GOAL>arcsin (-x) = -arcsin x
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>arcsin (-x) = -arcsin x
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>sin (-arcsin x) = -x
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>-arcsin x ∈ Icc (-(π / 2)) (π / 2)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖integral f‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤ MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
<VAR>m n : ℕ<VAR>_h : 0 < n + 1<GOAL>ack (m + 1) 0 < ack (m + 1) (n + 1)
<VAR>m n : ℕ<VAR>_h : 0 < n + 1<GOAL>ack m 1 < ack m (ack (m + 1) n)
<VAR>m n₁ n₂ : ℕ<VAR>h : n₁ + 1 < n₂ + 1<GOAL>ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)
<VAR>m n₁ n₂ : ℕ<VAR>h : n₁ + 1 < n₂ + 1<GOAL>ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
<VAR>m n₁ n₂ : ℕ<VAR>h : n₁ + 1 < n₂ + 1<GOAL>n₁ < n₂
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>(S'.a + S'.b) * (S'.a + ↑η * S'.b) * (S'.a + ↑η ^ 2 * S'.b) = S'.a ^ 3 + S'.b ^ 3
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>s₁ s₂ : Set α<VAR>hs₁ : IsOpen s₁<VAR>hs₂ : IsOpen s₂<VAR>h₁ : TendstoLocallyUniformlyOn F f p s₁<VAR>h₂ : TendstoLocallyUniformlyOn F f p s₂<GOAL>TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>s₁ s₂ : Set α<VAR>hs₁ : IsOpen s₁<VAR>hs₂ : IsOpen s₂<VAR>h₁ : TendstoLocallyUniformlyOn F f p s₁<VAR>h₂ : TendstoLocallyUniformlyOn F f p s₂<GOAL>TendstoLocallyUniformlyOn F f p (⋃₀ {s₁, s₂})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Tendsto m f (𝓝 b)<VAR>hb : b ≠ ⊤ ∨ a ≠ ⊤<GOAL>Tendsto (fun b => a / m b) f (𝓝 (a / b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Tendsto m f (𝓝 b)<VAR>hb : b ≠ ⊤ ∨ a ≠ ⊤<GOAL>b⁻¹ ≠ 0 ∨ a ≠ ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module K V<VAR>inst✝² : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>inst✝¹ : Fintype K<VAR>inst✝ : Fintype V<GOAL>∃ n, card V = card K ^ n
<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>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>x : α<VAR>y y' : γ<GOAL>(fun y => (f y, x)) y = (fun y => (f y, x)) y' → y = y'
<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>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>x : α<VAR>y y' : γ<GOAL>f y = f y' → y = y'
<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>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>x : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ((fun y => (f y, x)) '' s)
<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>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>x : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(fun y => (f y, x)) '' s = (f '' s) ×ˢ {x}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>a b : ℕ<VAR>hn : 0 < a * b<VAR>h : IsPrimitiveRoot ζ (a * b)<GOAL>IsPrimitiveRoot (ζ ^ a) b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>a b : ℕ<VAR>hn : 0 < a * b<VAR>h : IsPrimitiveRoot ζ (a * b)<GOAL>∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>a b : ℕ<VAR>hn : 0 < a * b<VAR>h : IsPrimitiveRoot ζ (a * b)<VAR>l : ℕ<VAR>hl : ζ ^ (a * l) = 1<GOAL>b ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>a b : ℕ<VAR>hn : 0 < a * b<VAR>h : IsPrimitiveRoot ζ (a * b)<VAR>l : ℕ<VAR>hl : ζ ^ (a * l) = 1<VAR>ha0 : a ≠ 0<GOAL>b ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>a b : ℕ<VAR>hn : 0 < a * b<VAR>h : IsPrimitiveRoot ζ (a * b)<VAR>l : ℕ<VAR>hl : ζ ^ (a * l) = 1<VAR>ha0 : a ≠ 0<GOAL>a * b ∣ a * l
<VAR>x : PartENat<VAR>y : ℕ<VAR>h : x ≤ ↑y<GOAL>x.Dom
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑θ = ↑ψ<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑θ = -↑ψ<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑θ = -↑ψ<VAR>hs : ↑θ = ↑ψ<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑θ = -↑ψ<VAR>hs : ↑θ + ↑ψ = ↑π<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑π = 0<VAR>hs : ↑θ + ↑ψ = ↑π<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑π = 0<VAR>hs : ↑θ + ↑ψ = ↑π<VAR>n : ℤ<VAR>hn : n • (2 * π) = -π + 0<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑π = 0<VAR>hs : ↑θ + ↑ψ = ↑π<VAR>n : ℤ<VAR>hn : n * 2 + 1 = 0<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑π = 0<VAR>hs : ↑θ + ↑ψ = ↑π<VAR>n : ℤ<VAR>hn : n * 2 + 1 = 0<VAR>this : (n * 2 + 1) % 2 = 0 % 2<GOAL>↑θ = ↑ψ
<VAR>θ ψ : ℝ<VAR>Hcos : cos θ = cos ψ<VAR>Hsin : sin θ = sin ψ<VAR>hc : ↑π = 0<VAR>hs : ↑θ + ↑ψ = ↑π<VAR>n : ℤ<VAR>hn : n * 2 + 1 = 0<VAR>this : 1 % 2 = 0 % 2<GOAL>↑θ = ↑ψ
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x y : M × ↥S<GOAL>(f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<GOAL>{a, b}.Pairwise r ↔ a ≠ b → r a b ∧ r b a
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝¹ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝ : DecidableEq α<VAR>P : Finpartition s<VAR>t : Finset β<GOAL>(interedges r s t).card = ∑ a ∈ P.parts, (interedges r a t).card
<VAR>z τ : ℂ<GOAL>(starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>z τ : ℂ<GOAL>∑' (b : ℤ), -(starRingEnd ℂ) (jacobiTheta₂'_term b z τ) = ∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>-(starRingEnd ℂ) (jacobiTheta₂'_term n z τ) = jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>-(↑2 * ↑π * -I * ↑↑n * cexp (↑2 * ↑π * -I * ↑↑n * (starRingEnd ℂ) z + ↑π * -I * ↑↑n ^ 2 * (starRingEnd ℂ) τ)) = ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<GOAL>span 1 = ⊤
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.684544, u_1} C<VAR>X Y Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<VAR>inst✝ : HasPullback i₁ i₂<GOAL>(i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.684544, u_1} C<VAR>X Y Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<VAR>inst✝ : HasPullback i₁ i₂<GOAL>(i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝³ : SFinite μ<VAR>inst✝² : IsSFiniteKernel κ<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>f : α × β → E<VAR>hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)<GOAL>∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝³ : SFinite μ<VAR>inst✝² : IsSFiniteKernel κ<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>f : α × β → E<VAR>hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)<GOAL>∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
<VAR>m n : ℕ<VAR>x : ZMod n<GOAL>(-x).cast = -x.cast % ↑n
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>s t : Set E<GOAL>IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
<VAR>m✝ n✝ n m : ℕ<GOAL>m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| = |b| ↔ a * a = b * b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| = |b| ↔ |a| * |a| = |b| * |b|
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>h : EqOn f g (sphere c R)<VAR>θ : ℝ<VAR>x✝ : θ ∈ [[0, 2 * π]]<GOAL>deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ) = deriv (circleMap c R) θ • (fun z => g z) (circleMap c R θ)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>Set.range rexp = Set.Ioi 0
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>x✝ : R<GOAL>x✝ ∈ ker (Quotient.mk I) ↔ x✝ ∈ I
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m v : E<VAR>h : v ∈ span ℤ (Set.range ⇑b)<GOAL>fract b (m + v) = fract b m
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Fintype V<GOAL>⊤.chromaticNumber = ↑(card V)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Fintype V<GOAL>∀ (C : ⊤.Coloring V), Surjective ⇑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>inst✝ : Fintype V<VAR>C : ⊤.Coloring V<GOAL>Surjective ⇑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>inst✝ : Fintype V<VAR>C : ⊤.Coloring V<GOAL>Injective ⇑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>inst✝ : Fintype V<VAR>C : ⊤.Coloring V<VAR>v w : V<GOAL>C v = C w → v = w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>inst✝ : Fintype V<VAR>C : ⊤.Coloring V<VAR>v w : V<GOAL>¬v = w → ¬C v = C w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C✝ : G.Coloring α<VAR>inst✝ : Fintype V<VAR>C : ⊤.Coloring V<VAR>v w : V<VAR>h : ¬v = w<GOAL>¬C v = C w
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>(∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : ContMDiffWithinAt IM IB n f s x<VAR>hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => e.coordChange e' (f y) (g y)) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : ContMDiffWithinAt IM IB n f s x<VAR>hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>(fun y => e.coordChange e' (f y) (g y)) =ᶠ[𝓝[s] x] fun x => ↑(Trivialization.coordChangeL 𝕜 e e' (f x)) (g x)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : ContMDiffWithinAt IM IB n f s x<VAR>hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>e.coordChange e' (f x) (g x) = ↑(Trivialization.coordChangeL 𝕜 e e' (f x)) (g x)
<VAR>s : ℝ<GOAL>(fun x => x ^ s) =o[atTop] rexp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>this : ⊥.Colorable 1<GOAL>⊥.chromaticNumber = 1
<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₂ : P<VAR>v₁ v₂ v₃ v : V<GOAL>∠ (v₁ - v) (v₂ - v) (v₃ - v) = ∠ v₁ v₂ v₃
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₃' : P<VAR>h : Collinear ℝ {p₃, p₂, p₃'}<VAR>hp₃p₂ : p₃ ≠ p₂<VAR>hp₃'p₂ : p₃' ≠ p₂<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁ p₂ p₃'
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>s : Set M<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total M M R id))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Set α<VAR>ht : t ⊆ s<GOAL>t.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>t : Set α<VAR>ht : t ⊆ s<VAR>this : Finite ↑s<GOAL>t.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<GOAL>N ≤r M ↔ ∃ R ⊆ M.E, N = M ↾ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<GOAL>(∃ R ⊆ M.E, N = M ↾ R) → N ≤r M
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>hR : R ⊆ M.E<GOAL>M ↾ R ≤r M
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>a ⊓ (a ⊔ c) ⊓ (b ⊔ c) = a ⊓ (a ⊓ b ⊔ c)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>a ⊓ (a ⊓ b ⊔ c) = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>(a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>(a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = a ⊓ b ⊔ a ⊓ c