ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hu₀ : 0 < u - ⌊ξ⌋ * v<VAR>huv : u - ⌊ξ⌋ * v < v<GOAL>|(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hu₀ : 0 < u - ⌊ξ⌋ * v<VAR>huv : u - ⌊ξ⌋ * v < v<VAR>hξ₀ : 0 < fract ξ<GOAL>|(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u' = ↑u - ↑⌊ξ⌋ * ↑v<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<VAR>H₁ : 0 < ↑v / ↑u' / fract ξ<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<VAR>H₁ : 0 < ↑v / ↑u' / fract ξ<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<VAR>H₁ : 0 < ↑v / ↑u' / fract ξ<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<VAR>H₁ : 0 < ↑v / ↑u' / fract ξ<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<VAR>H₁ : 0 < ↑v / ↑u' / fract ξ<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ<VAR>help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hξ₀ : 0 < fract ξ<VAR>u' : ℤ := u - ⌊ξ⌋ * v<VAR>hu₀ : 0 < u'<VAR>huv : u' < v<VAR>hu' : u' = u - ⌊ξ⌋ * v<VAR>hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v<VAR>Hu : 0 < ↑u'<VAR>Hu' : 0 < 2 * ↑u' - 1<VAR>Hv : 0 < ↑v<VAR>Hv' : 0 < 2 * ↑v - 1<VAR>H₁ : 0 < ↑v / ↑u' / fract ξ<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ<VAR>help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|<VAR>help₂ : ∀ {a b c d : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (b * c)⁻¹ * (b / d / a) = (d * c * a)⁻¹<GOAL>|(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
<VAR>x y : ℝ<GOAL>cosh x + sinh x = rexp x
<VAR>x y : ℝ<GOAL>↑(cosh x + sinh x) = ↑(rexp x)
<VAR>R : Type u_2<VAR>K : Type ?u.21569<VAR>L : Type ?u.21572<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>eval x (minpolyDiv R x) = (aeval x) (derivative (minpoly R x))
<VAR>R : Type u_2<VAR>K : Type ?u.21569<VAR>L : Type ?u.21572<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>eval x (minpolyDiv R x) = eval x (derivative (minpolyDiv R x * (X - C x)))
<VAR>y z : ℝ<VAR>x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>h'x : ↑x ≠ ⊤<VAR>this : x ≠ 0<GOAL>↑x ^ (y + z) = ↑x ^ y * ↑x ^ z
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(ascPochhammer ℕ k).smeval (-r) = (-1) ^ k * (descPochhammer ℤ k).smeval r
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>b₁ b₂ : β<VAR>l : List α<VAR>h : b₁ ∈ map (const α b₂) l<GOAL>b₁ = b₂
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>b₁ b₂ : β<VAR>l : List α<VAR>h : b₁ ∈ replicate l.length b₂<GOAL>b₁ = b₂
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>hε : 0 ≤ ε<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<GOAL>↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) ≤ ↑(G.edgeDensity s t) - ε
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>hε : 0 ≤ ε<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<GOAL>↑(↑(G.interedges (SimpleGraph.badVertices G ε s t) t).card / (↑(SimpleGraph.badVertices G ε s t).card * ↑t.card)) ≤ ↑(G.edgeDensity s t) - ε
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>hε : 0 ≤ ε<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<GOAL>↑(G.interedges (SimpleGraph.badVertices G ε s t) t).card / (↑(SimpleGraph.badVertices G ε s t).card * ↑t.card) ≤ ↑(G.edgeDensity s t) - ε
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>hε : 0 ≤ ε<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<GOAL>↑(G.interedges (SimpleGraph.badVertices G ε s t) t).card ≤ (↑(G.edgeDensity s t) - ε) * (↑(SimpleGraph.badVertices G ε s t).card * ↑t.card)
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>hε : 0 ≤ ε<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<GOAL>↑(G.interedges (SimpleGraph.badVertices G ε s t) t).card ≤ ↑(SimpleGraph.badVertices G ε s t).card * ↑t.card * (↑(G.edgeDensity s t) - ε)
<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✝⁴ : Fintype n<VAR>inst✝³ : NonAssocSemiring α<VAR>inst✝² : NonAssocSemiring β<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : NonAssocSemiring S<VAR>f : R →+* S<VAR>M : Matrix n m R<VAR>v : n → R<VAR>i : m<GOAL>f ((v ᵥ* M) i) = (⇑f ∘ v ᵥ* M.map ⇑f) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>v : ι →₀ R<GOAL>(v.sum fun i vi => b.repr.symm (Finsupp.single i vi)) = (Finsupp.total ι M R ⇑b) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g : α → β<VAR>inst✝¹ : SMul 𝕜 β<VAR>inst✝ : ContinuousConstSMul 𝕜 β<VAR>c : 𝕜<VAR>f' : α → β<VAR>h_f'_meas : StronglyMeasurable f'<VAR>hff' : f =ᶠ[ae μ] f'<GOAL>AEStronglyMeasurable' m (c • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g : α → β<VAR>inst✝¹ : SMul 𝕜 β<VAR>inst✝ : ContinuousConstSMul 𝕜 β<VAR>c : 𝕜<VAR>f' : α → β<VAR>h_f'_meas : StronglyMeasurable f'<VAR>hff' : f =ᶠ[ae μ] f'<GOAL>c • f =ᶠ[ae μ] c • f'
<VAR>x y : ℝ<VAR>hy : 0 ≤ y<GOAL>(x / y).toNNReal = x.toNNReal / y.toNNReal
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]<VAR>i : ℕ<VAR>hi : i < l.length<VAR>j : ℕ<VAR>hj : j < l.length<VAR>hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩<GOAL>⟨i, hi⟩ = ⟨j, hj⟩
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]<VAR>i : ℕ<VAR>hi : i < l.length<VAR>j : ℕ<VAR>hj : j < l.length<VAR>hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩<VAR>hij : i < j<GOAL>⟨i, hi⟩ = ⟨j, hj⟩
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]<VAR>i : ℕ<VAR>hi hj : i < l.length<VAR>hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨i, hj⟩<GOAL>⟨i, hi⟩ = ⟨i, hj⟩
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]<VAR>i : ℕ<VAR>hi : i < l.length<VAR>j : ℕ<VAR>hj : j < l.length<VAR>hg : (fun i => l[↑i]) ⟨i, hi⟩ = (fun i => l[↑i]) ⟨j, hj⟩<VAR>hji : j < i<GOAL>⟨i, hi⟩ = ⟨j, hj⟩
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<GOAL>(1 / A) ^ n = 1 / A ^ n
<VAR>q✝ q : ℚ<VAR>n : ℕ<GOAL>q ^ n = mkRat (q.num ^ n) (q.den ^ n)
<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>s : AffineSubspace ℝ P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<VAR>r1 r2 : ℝ<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) = ‖p1 -ᵥ p2 + (r1 - r2) • v‖ * ‖p1 -ᵥ p2 + (r1 - r2) • v‖
<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>s : AffineSubspace ℝ P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<VAR>r1 r2 : ℝ<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + ‖(r1 - r2) • v‖ * ‖(r1 - r2) • v‖ = ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * |r1 - r2| * ‖v‖ * ‖v‖
<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>s : AffineSubspace ℝ P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<VAR>r1 r2 : ℝ<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * ‖v‖ * (|r1 - r2| * ‖v‖) = ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * |r1 - r2| * ‖v‖ * ‖v‖
<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>s : AffineSubspace ℝ P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<VAR>r1 r2 : ℝ<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * |r1 - r2| * ‖v‖ * ‖v‖ = dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (‖v‖ * ‖v‖)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y : Dial C<GOAL>(X.tensorObj Y).rel = (Subobject.pullback (prod.map (prod.braiding X.src Y.src).hom (prod.braiding X.tgt Y.tgt).hom)).obj (Y.tensorObj X).rel
<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>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : α → β<VAR>e : β ≃ᵐ γ<VAR>h : MeasurePreserving (⇑e) μb μc<GOAL>MeasurePreserving (⇑e ∘ g) μa μc ↔ MeasurePreserving g μa μb
<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>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : α → β<VAR>e : β ≃ᵐ γ<VAR>h : MeasurePreserving (⇑e) μb μc<VAR>hg : MeasurePreserving (⇑e ∘ g) μa μc<GOAL>MeasurePreserving g μa μb
<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>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : α → β<VAR>e : β ≃ᵐ γ<VAR>h : MeasurePreserving (⇑e) μb μc<VAR>hg : MeasurePreserving (⇑e ∘ g) μa μc<GOAL>g = ⇑e.symm ∘ ⇑e ∘ g
<VAR>p q : Prop<VAR>α : Sort u_1<VAR>s : α → Prop<GOAL>¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonAssocSemiring α<VAR>n : ℕ<VAR>a : α<GOAL>n • a = ↑n * a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.11180, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<GOAL>IsIso S.g ↔ IsZero S.X₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.11180, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<VAR>this : HasZeroObject C<GOAL>IsIso S.g ↔ IsZero S.X₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.11180, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<VAR>this✝ : HasZeroObject C<VAR>this : Mono S.f<GOAL>IsIso S.g ↔ IsZero S.X₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.11180, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<VAR>this✝¹ : HasZeroObject C<VAR>this✝ : Mono S.f<VAR>this : Epi S.g<GOAL>IsIso S.g ↔ IsZero S.X₁
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<VAR>inst✝ : SemilatticeSup β<VAR>hf : QuasiconvexOn 𝕜 s f<VAR>hg : QuasiconvexOn 𝕜 s g<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<VAR>inst✝ : SemilatticeSup β<VAR>hf : QuasiconvexOn 𝕜 s f<VAR>hg : QuasiconvexOn 𝕜 s g<VAR>r : β<GOAL>Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<GOAL>automorphize (g ∘ Quotient.mk' • f) x = (g • automorphize f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<GOAL>∀ (a : β), automorphize (g ∘ Quotient.mk' • f) (Quotient.mk'' a) = (g • automorphize f) (Quotient.mk'' a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<GOAL>automorphize (g ∘ Quotient.mk' • f) (Quotient.mk'' b) = (g • automorphize f) (Quotient.mk'' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<GOAL>Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (Quotient.mk'' b) = g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a • b)) ⋯ (Quotient.mk'' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<VAR>π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)<GOAL>Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (Quotient.mk'' b) = g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a • b)) ⋯ (Quotient.mk'' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<VAR>π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)<VAR>H₁ : ∀ (a : α), π (a • b) = π b<GOAL>Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (Quotient.mk'' b) = g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a • b)) ⋯ (Quotient.mk'' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<VAR>π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)<VAR>H₁ : ∀ (a : α), π (a • b) = π b<GOAL>∑' (a : α), g (π b) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>(x ◃⁻¹ x) ◃ y = x ◃ y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<VAR>h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y<GOAL>(x ◃⁻¹ x) ◃ y = x ◃ y
<VAR>x x' : PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : x' ≤ x<GOAL>(x.insertLeft x').Numeric
<VAR>x x' : PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : (∀ (i : x'.LeftMoves), x'.moveLeft i < x) ∧ ∀ (j : x.RightMoves), x' < x.moveRight j<GOAL>(x.insertLeft x').Numeric
<VAR>x' : PGame<VAR>x'_num : x'.Numeric<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>h : (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧ ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j<VAR>x_num : match mk xl xr xL xR with | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric<GOAL>match (mk xl xr xL xR).insertLeft x' with | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric
<VAR>x' : PGame<VAR>x'_num : x'.Numeric<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>h : (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧ ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j<VAR>x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric<GOAL>((∀ (a : xl) (j : xr), xL a < xR j) ∧ ∀ (j : xr), x' < xR j) ∧ ((∀ (a : xl), (xL a).Numeric) ∧ x'.Numeric) ∧ ∀ (j : xr), (xR j).Numeric
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → F<VAR>u : Fˣ<GOAL>toAffine W ((fun m => m • Q) u) = toAffine W Q
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>x : 𝕎 R<GOAL>(x * ↑p).coeff 0 = 0
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s✝ s t : Set (Sym2 V)<VAR>v w : V<GOAL>(fromEdgeSet (s ∪ t)).Adj v w ↔ (fromEdgeSet s ⊔ fromEdgeSet t).Adj v w
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>N : Type u_3<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : Module R N<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommMonoid P<VAR>inst✝⁸ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>g : M₂ →ₗ[R] M<VAR>x✝ : ι → M₂<GOAL>(compLinearMap 0 g) x✝ = 0 x✝
<VAR>p : ZFSet → Prop<VAR>x y : ZFSet<GOAL>Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : LinearOrderedField R<VAR>x : V → R<GOAL>(((toLinearMap₂' R) (lapMatrix R G)) x) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
<VAR>s : Finset ℕ<VAR>m n p : ℕ<VAR>hn : Squarefree n<GOAL>∏ p ∈ n.primeFactors, p = n
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l l' : List ι<VAR>hl : l.Perm l'<VAR>hs : ∀ i ∈ l, s i ≠ 0<VAR>co : List.Pairwise (Coprime on s) l<GOAL>↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)