ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<VAR>x : 𝓞 K<VAR>h_nz : x ≠ 0<VAR>h_bd : ↑|(Algebra.norm ℚ) ↑x| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<VAR>x : 𝓞 K<VAR>h_nz : x ≠ 0<VAR>h_bd : ↑|(Algebra.norm ℚ) ↑x| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<VAR>h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|<GOAL>4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<VAR>x : 𝓞 K<VAR>h_nz : x ≠ 0<VAR>h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|<VAR>h_bd : 1 ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<VAR>x : 𝓞 K<VAR>h_nz : x ≠ 0<VAR>h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|<VAR>h_bd : ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (NrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|<GOAL>4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<VAR>x : 𝓞 K<VAR>h_nz : x ≠ 0<VAR>h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|<VAR>h_bd : ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (NrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|<GOAL>4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (NrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2)
<VAR>R : Type u<VAR>inst✝⁶ : Ring R<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z✝ : DirectLimit G f<VAR>ind : ι<VAR>z p q : DirectSum ι fun i => G i<VAR>x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p<VAR>x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q<VAR>i : ι<VAR>x : G i<VAR>ihx : (of R ι G f i) x = Quotient.mk'' p<VAR>j : ι<VAR>y : G j<VAR>ihy : (of R ι G f j) y = Quotient.mk'' q<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(of R ι G f k) ((f i k hik) x + (f j k hjk) y) = Quotient.mk'' (p + q)
<VAR>R : Type u<VAR>inst✝⁶ : Ring R<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>z✝ : DirectLimit G f<VAR>ind : ι<VAR>z p q : DirectSum ι fun i => G i<VAR>x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p<VAR>x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q<VAR>i : ι<VAR>x : G i<VAR>ihx : (of R ι G f i) x = Quotient.mk'' p<VAR>j : ι<VAR>y : G j<VAR>ihy : (of R ι G f j) y = Quotient.mk'' q<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ᵐ (c : β) ∂ν a, ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ (i i_1 : ℚ), i ≤ i_1 → ∀ᵐ (a_1 : β) ∂ν a, f (a, a_1) i ≤ f (a, a_1) i_1
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b✝ b' b₁ b₂ b₃ c c₁ : R<VAR>ea₁ b : ℕ<VAR>xa₁ : R<GOAL>(xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹³ : Zero β<VAR>inst✝¹² : One β<VAR>inst✝¹¹ : Add β<VAR>inst✝¹⁰ : Mul β<VAR>inst✝⁹ : Neg β<VAR>inst✝⁸ : Sub β<VAR>inst✝⁷ : SMul ℕ β<VAR>inst✝⁶ : SMul ℤ β<VAR>inst✝⁵ : Pow β ℕ<VAR>inst✝⁴ : NatCast β<VAR>inst✝³ : IntCast β<VAR>f : β → α<VAR>hf : Injective f<VAR>inst✝² : Mul α<VAR>inst✝¹ : Add α<VAR>inst✝ : RightDistribClass α<VAR>add : ∀ (x y : β), f (x + y) = f x + f y<VAR>mul : ∀ (x y : β), f (x * y) = f x * f y<VAR>x y z : β<GOAL>f ((x + y) * z) = f (x * z + y * z)
<VAR>α : Type u_1<VAR>f : List α → List α<VAR>n : Nat<VAR>l₁ l₂ : List α<GOAL>modifyNthTail f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyNthTail f n l₂
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>y ∈ {y | s.WOppSide x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>s.WOppSide x y ↔ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>j : J<VAR>k : K<GOAL>(colimit.ι F j).app k ≫ (preservesColimitIso ((evaluation K C).obj k) F).hom = colimit.ι (F ⋙ (evaluation K C).obj k) j
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>j : J<VAR>k : K<GOAL>(colimit.ι F j).app k = colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∉ ball 0 (1 + D)<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∉ ball 0 (1 + D)<VAR>B : ∀ y ∈ ball x D, φ y = 0<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∉ ball 0 (1 + D)<VAR>B : ∀ y ∈ ball x D, φ y = 0<VAR>Bx : φ x = 0<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∉ ball 0 (1 + D)<VAR>B : ∀ y ∈ ball x D, φ y = 0<VAR>Bx : φ x = 0<VAR>B' : ∀ y ∈ ball x D, φ y = φ x<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∉ ball 0 (1 + D)<VAR>B : ∀ y ∈ ball x D, φ y = 0<VAR>Bx : φ x = 0<VAR>B' : ∀ y ∈ ball x D, φ y = φ x<GOAL>∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ✝ : Filtration ℕ m0<VAR>n : ℕ<VAR>R : ℝ≥0<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : Filtration ℕ m0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ✝ : Filtration ℕ m0<VAR>n : ℕ<VAR>R : ℝ≥0<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : Filtration ℕ m0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ω : Ω<VAR>hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ ↑R<VAR>i : ℕ<GOAL>|martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ✝ : Filtration ℕ m0<VAR>n : ℕ<VAR>R : ℝ≥0<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : Filtration ℕ m0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ω : Ω<VAR>hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ ↑R<VAR>i : ℕ<GOAL>|f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| ≤ ↑(R + R)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ✝ : Filtration ℕ m0<VAR>n : ℕ<VAR>R : ℝ≥0<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : Filtration ℕ m0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>ω : Ω<VAR>hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ ↑R<VAR>i : ℕ<VAR>this : |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| = |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)|<GOAL>|f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| ≤ ↑(R + R)
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<GOAL>↑u * a = 1 ↔ ↑u⁻¹ = a
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>Nat.card ↥H * H.index = Nat.card G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>⊥.relindex H * H.index = ⊥.index
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<GOAL>T R (-↑(k + 1) + 2) = 2 * X * T R (-↑(k + 1) + 1) - T R (-↑(k + 1))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i : ι<VAR>inst✝ : DecidableEq ι<GOAL>(indicator s f) i = if hi : i ∈ s then f i hi else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i : ι<VAR>inst✝ : DecidableEq ι<GOAL>(if H : i ∈ s then f i H else 0) = if hi : i ∈ s then f i hi else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>I : Finset ι<VAR>κ : ι → Kernel α β<VAR>a : α<VAR>s : Set β<GOAL>((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).b₈ = ↑C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) - ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) + ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 - (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) ^ 2 = ↑C.u⁻¹ ^ 8 * (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 + 3 * C.r * (W.a₃ ^ 2 + 4 * W.a₆) + 3 * C.r ^ 2 * (2 * W.a₄ + W.a₁ * W.a₃) + C.r ^ 3 * (W.a₁ ^ 2 + 4 * W.a₂) + 3 * C.r ^ 4)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Nontrivial A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>Function.Injective ⇑(algebraMap R A)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>e : Sym2 V<VAR>h : e ∈ G.edgeSet<GOAL>Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom ⟨e, h⟩) = ⟨e, h⟩
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>e : Sym2 V<VAR>h : e ∈ G.edgeSet<GOAL>Sym2.map (fun x => { toFun := ⇑f.symm, map_rel' := ⋯ } ({ toFun := ⇑f, map_rel' := ⋯ } x)) e = e
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>e : Sym2 V<VAR>h : e ∈ G.edgeSet<VAR>x✝ : V<VAR>a✝ : x✝ ∈ e<GOAL>{ toFun := ⇑f.symm, map_rel' := ⋯ } ({ toFun := ⇑f, map_rel' := ⋯ } x✝) = id x✝
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>e : Sym2 W<VAR>h : e ∈ G'.edgeSet<GOAL>Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom ⟨e, h⟩) = ⟨e, h⟩
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>e : Sym2 W<VAR>h : e ∈ G'.edgeSet<GOAL>Sym2.map (fun x => { toFun := ⇑f, map_rel' := ⋯ } ({ toFun := ⇑f.symm, map_rel' := ⋯ } x)) e = e
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>e : Sym2 W<VAR>h : e ∈ G'.edgeSet<VAR>x✝ : W<VAR>a✝ : x✝ ∈ e<GOAL>{ toFun := ⇑f, map_rel' := ⋯ } ({ toFun := ⇑f.symm, map_rel' := ⋯ } x✝) = id x✝
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<GOAL>contDiffGroupoid 0 I = continuousGroupoid H
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<GOAL>⊤ ≤ contDiffGroupoid 0 I
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>u : PartialHomeomorph H H<VAR>a✝ : u ∈ ⊤.members<GOAL>u ∈ contDiffGroupoid 0 I
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>u : PartialHomeomorph H H<VAR>a✝ : u ∈ ⊤.members<GOAL>{ property := fun f s => ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }.property (↑u) u.source ∧ { property := fun f s => ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }.property (↑u.symm) u.target
<VAR>m n : ℕ∞<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>u : PartialHomeomorph H H<VAR>a✝ : u ∈ ⊤.members<GOAL>ContinuousOn (↑I ∘ ↑u ∘ ↑I.symm) (↑I.symm ⁻¹' u.source ∩ range ↑I) ∧ ContinuousOn (↑I ∘ ↑u.symm ∘ ↑I.symm) (↑I.symm ⁻¹' u.target ∩ range ↑I)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>inst✝ : LinearOrderedCancelCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = hs.min hsn * ht.min htn
<VAR>α : Type u_1<VAR>s t : Set α<VAR>inst✝ : LinearOrderedCancelCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>hs.min hsn * ht.min htn ≤ ⋯.min ⋯
<VAR>α : Type u_1<VAR>s t : Set α<VAR>inst✝ : LinearOrderedCancelCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>∀ b ∈ s * t, hs.min hsn * ht.min htn ≤ b
<VAR>α : Type u_1<VAR>s t : Set α<VAR>inst✝ : LinearOrderedCancelCommMonoid α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ t<GOAL>hs.min hsn * ht.min htn ≤ (fun x x_1 => x * x_1) x y
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : Nontrivial R<GOAL>(nodal s v).degree = ↑s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LE α<VAR>inst✝¹ : MulOneClass α<VAR>i : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : MulLECancellable a<GOAL>b * a ≤ a ↔ b ≤ 1
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>a ∈ closedBall 1 r ↔ ‖a‖ ≤ r
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U✝ : Set Y<VAR>a : X<VAR>U : Set Y<VAR>hU : IsOpen U<GOAL>IsOpen ((fun f => f a) ⁻¹' U)
<VAR>R : Type u_1<VAR>s : Multiset ℕ<VAR>h0 : s.prod ≠ 0<GOAL>Ω s.prod = (Multiset.map (⇑Ω) s).sum
<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>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedAddCommGroup 𝔸<VAR>inst✝¹ : Module 𝕜 𝔸<VAR>inst✝ : BoundedSMul 𝕜 𝔸<VAR>l : Filter ι<VAR>ε : ι → 𝕜<VAR>f : ι → 𝔸<VAR>hε : Tendsto ε l (𝓝 0)<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<GOAL>Tendsto (ε • f) l (𝓝 0)
<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>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedAddCommGroup 𝔸<VAR>inst✝¹ : Module 𝕜 𝔸<VAR>inst✝ : BoundedSMul 𝕜 𝔸<VAR>l : Filter ι<VAR>ε : ι → 𝕜<VAR>f : ι → 𝔸<VAR>hε : ε =o[l] fun _x => 1<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<GOAL>(ε • f) =o[l] fun _x => 1
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>r : R<GOAL>(expand R p) ((expand R q) (C r)) = (expand R (p * q)) (C r)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f✝ f g : R[X]<VAR>ihf : (expand R p) ((expand R q) f) = (expand R (p * q)) f<VAR>ihg : (expand R p) ((expand R q) g) = (expand R (p * q)) g<GOAL>(expand R p) ((expand R q) (f + g)) = (expand R (p * q)) (f + g)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>n : ℕ<VAR>r : R<VAR>x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)<GOAL>(expand R p) ((expand R q) (C r * X ^ (n + 1))) = (expand R (p * q)) (C r * X ^ (n + 1))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{u₂, u₁} C<VAR>inst✝ : GaloisCategory C<VAR>X : C<VAR>h : IsInitial X<GOAL>∃ x, (∀ (i : Empty), IsConnected ((fun x => X) i)) ∧ Finite Empty
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{u₂, u₁} C<VAR>inst✝ : GaloisCategory C<VAR>X : C<VAR>h : IsInitial X<GOAL>(∀ (i : Empty), IsConnected ((fun x => X) i)) ∧ Finite Empty
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ x : E<VAR>a b : ℝ<VAR>hf : ‖f‖ ≤ a<VAR>hx : ‖x‖ ≤ b<GOAL>0 ≤ a
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f✝ g : ι → α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>s : Multiset ι<VAR>f : α → β → γ<VAR>hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d<VAR>hf' : f 1 1 = 1<VAR>f₁ : ι → α<VAR>f₂ : ι → β<VAR>l : List ι<GOAL>(map (fun i => f (f₁ i) (f₂ i)) ⟦l⟧).prod = f (map f₁ ⟦l⟧).prod (map f₂ ⟦l⟧).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>inst✝¹ : MeasurableSingletonClass β<VAR>s : Set β<VAR>inst✝ : Decidable (g a ∈ s)<GOAL>∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f ≈ g<VAR>hf : f ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f ≈ g<VAR>hf : f ≈ 0<VAR>hg : g ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f ≈ g<VAR>hf : ¬f ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f ≈ g<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f ≈ g<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq β<GOAL>image2 f (↑s) (insert b ↑t) = (fun a => f a b) '' ↑s ∪ image2 f ↑s ↑t
<VAR>R✝ : Type u_1<VAR>inst✝² : Semiring R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : NoZeroDivisors R<VAR>f g : R[X]<VAR>f0 : ¬f = 0<VAR>g0 : ¬g = 0<GOAL>(f * g).reverse = f.reverse * g.reverse