ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌊0⌋₊ = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Balanced C<VAR>X✝ Y✝ : Cᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>fmono : Mono f<VAR>fepi : Epi f<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Balanced C<VAR>X✝ Y✝ : Cᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>fmono : Mono f<VAR>fepi : Epi f<GOAL>IsIso f.unop.op
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>(canonicalEquiv S P P).trans (canonicalEquiv S P P) = RingEquiv.refl (FractionalIdeal S P)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>canonicalEquiv S P P = (canonicalEquiv S P P).symm
<VAR>ι : Type u_1<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>G : ι → Type u_4<VAR>inst✝² : Semigroup G₁<VAR>inst✝¹ : Semigroup G₂<VAR>inst✝ : (i : ι) → Semigroup (G i)<VAR>x y : (i : ι) → G i<GOAL>x ∣ y ↔ ∀ (i : ι), x i ∣ y i
<VAR>ι : Type u_1<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>G : ι → Type u_4<VAR>inst✝² : Semigroup G₁<VAR>inst✝¹ : Semigroup G₂<VAR>inst✝ : (i : ι) → Semigroup (G i)<VAR>x y : (i : ι) → G i<GOAL>(∃ c, ∀ (a : ι), y a = (x * c) a) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>γ : Γ₀ˣ<VAR>x : hat K<VAR>γ₀ : Γ₀ := extensionValuation x<VAR>h : γ₀ ≠ 0<GOAL>x ∈ closure (↑K '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>γ : Γ₀ˣ<VAR>x : hat K<VAR>γ₀ : Γ₀ := extensionValuation x<VAR>h : γ₀ ≠ 0<VAR>hγ₀ : extension ⁻¹' {γ₀} ∈ 𝓝 x<GOAL>x ∈ closure (↑K '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>γ : Γ₀ˣ<VAR>x : hat K<VAR>γ₀ : Γ₀ := extensionValuation x<VAR>h : γ₀ ≠ 0<VAR>hγ₀ : extension ⁻¹' {γ₀} ∈ 𝓝 x<GOAL>(∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t) ↔ γ₀ < ↑γ
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<GOAL>inverse a = a⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<GOAL>inverse 0 = 0⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>inverse a = a⁻¹
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v w : Fin 3 → R<GOAL>-(crossProduct v) w = (crossProduct w) v
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Semigroup S<VAR>a b c✝ : S<VAR>h : Commute a b<VAR>c : S<GOAL>a * (b * c) = b * (a * c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t u v : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on s)<GOAL>∃ t, (∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Disjoint on fun i => s i \ t i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t u v : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>i : ι<GOAL>μ ((fun i => toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)) i) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t u v : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on s)<GOAL>Pairwise (Disjoint on fun i => s i \ (fun i => toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)) i)
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<VAR>posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<VAR>posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x<VAR>fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<VAR>posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x<VAR>fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)<VAR>f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → Memℒp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))<GOAL>Gamma (a * s + b * t) ≤ Gamma s ^ a * Gamma t ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<VAR>posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x<VAR>fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)<VAR>f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → Memℒp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (a * s + b * t - 1) ≤ (∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)) ^ a * (∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (t - 1)) ^ b
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<VAR>posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x<VAR>fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)<VAR>f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → Memℒp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (a * s + b * t - 1) = ∫ (a_1 : ℝ) in Ioi 0, f a s a_1 * f b t a_1
<VAR>s t a b : ℝ<VAR>hs : 0 < s<VAR>ht : 0 < t<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>f : ℝ → ℝ → ℝ → ℝ := fun c u x => rexp (-c * x) * x ^ (c * (u - 1))<VAR>e : (1 / a).IsConjExponent (1 / b)<VAR>hab' : b = 1 - a<VAR>hst : 0 < a * s + b * t<VAR>posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x<VAR>posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x<VAR>fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)<VAR>f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → Memℒp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))<GOAL>(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)) ^ a * (∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (t - 1)) ^ b = (∫ (a_1 : ℝ) in Ioi 0, f a s a_1 ^ (1 / a)) ^ (1 / (1 / a)) * (∫ (a : ℝ) in Ioi 0, f b t a ^ (1 / b)) ^ (1 / (1 / b))
<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>x₁ x₂ : M<VAR>y : ↥S<GOAL>f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>V : FDRep k G<VAR>g h : G<GOAL>V.character (h * g) = V.character (g * h)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>Fintype.card m.ToType = card m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>Fintype.card { x // x ∈ m.toEnumFinset } = card m
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<GOAL>(fun k l => ((NumberField.house.newBasis K).repr (a k.1 l.1 * (NumberField.house.newBasis K) l.2)) k.2) ≠ 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<GOAL>¬(fun k l => ((NumberField.house.newBasis K).repr (a k.1 l.1 * (NumberField.house.newBasis K) l.2)) k.2) = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<GOAL>¬∀ (a_1 : α × (K →+* ℂ)), (fun l => ((NumberField.house.newBasis K).repr (a a_1.1 l.1 * (NumberField.house.newBasis K) l.2)) a_1.2) = 0 a_1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>hs : ∀ (a_1 : α × (K →+* ℂ)), (fun l => ((NumberField.house.newBasis K).repr (a a_1.1 l.1 * (NumberField.house.newBasis K) l.2)) a_1.2) = 0 a_1<GOAL>False
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)<GOAL>False
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)<GOAL>a = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)<GOAL>∀ (i : α) (j : β), a i j = 0 i j
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>k' : α<VAR>l : β<VAR>hs : ∀ (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)<GOAL>a k' l = 0 k' l
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>k' : α<VAR>l : β<VAR>hs : ∀ (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)<VAR>b : K →+* ℂ<GOAL>a k' l = 0 k' l
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>k' : α<VAR>l : β<VAR>hs : ∀ (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)<VAR>b : K →+* ℂ<VAR>this : a k' l * (NumberField.house.newBasis K) b = 0<GOAL>a k' l = 0 k' l
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>k' : α<VAR>l : β<VAR>hs : ∀ (b : K →+* ℂ), (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)<VAR>b : K →+* ℂ<VAR>this : a k' l = 0 ∨ (NumberField.house.newBasis K) b = 0<GOAL>a k' l = 0 k' l
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>K : LinearOrder β<VAR>x y : (↑φ).Germ β<VAR>a b : α → β<GOAL>min ↑a ↑b = map₂ min ↑a ↑b
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>K : LinearOrder β<VAR>x y : (↑φ).Germ β<VAR>a b : α → β<VAR>h : ↑a ≤ ↑b<GOAL>min ↑a ↑b = map₂ min ↑a ↑b
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>K : LinearOrder β<VAR>x y : (↑φ).Germ β<VAR>a b : α → β<VAR>h : ↑b ≤ ↑a<GOAL>min ↑a ↑b = map₂ min ↑a ↑b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>inst✝ : BooleanAlgebra α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>Disjoint s (map { toFun := compl, inj' := ⋯ } s)
<VAR>α : Type u_1<VAR>inst✝ : BooleanAlgebra α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>∀ ⦃a : α⦄, a ∈ s → a ∉ map { toFun := compl, inj' := ⋯ } s
<VAR>α : Type u_1<VAR>inst✝ : BooleanAlgebra α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<VAR>x : α<VAR>hx : x ∈ s<VAR>hxc : x ∈ map { toFun := compl, inj' := ⋯ } s<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : BooleanAlgebra α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<VAR>x : α<VAR>hx' : x ∈ s<VAR>hx : { toFun := compl, inj' := ⋯ } x ∈ s<VAR>hxc : { toFun := compl, inj' := ⋯ } x ∈ map { toFun := compl, inj' := ⋯ } s<GOAL>False
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>finrank K ↥(span K {v}) = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>finrank K ↥(span K {v}) ≤ 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>1 ≤ finrank K ↥(span K {v})
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Trivialization F TotalSpace.proj<GOAL>ContinuousOn (fun z => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Trivialization F TotalSpace.proj<VAR>this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z<GOAL>ContinuousOn (fun z => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Trivialization F TotalSpace.proj<VAR>this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z<GOAL>ContinuousOn (↑e.symm) (e.baseSet ×ˢ univ)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Trivialization F TotalSpace.proj<VAR>this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z<GOAL>ContinuousOn (↑e.symm) e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l✝ : Filter α<VAR>f✝ g✝ h : α → β<VAR>l : Filter α<VAR>f : α → β<VAR>g : β → γ<VAR>b : β<VAR>hb : f =ᶠ[l] fun x => b<GOAL>(↑(g ∘ f)).IsConstant
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>x + 1 < rexp x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : 0 < x<GOAL>x + 1 < rexp x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : x < 0<GOAL>x + 1 < rexp x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : x < 0<VAR>h' : 1 ≤ -x<GOAL>x + 1 < rexp x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : x < 0<VAR>h' : -x < 1<GOAL>x + 1 < rexp x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : x < 0<VAR>h' : -x < 1<VAR>hx' : 0 < x + 1<GOAL>x + 1 < rexp x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P✝ : Presentation R S<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>P : Presentation R S<GOAL>Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) = RingHom.ker (aeval P.baseChange.val)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P✝ : Presentation R S<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>P : Presentation R S<GOAL>Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) ≤ RingHom.ker (aeval P.baseChange.val)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P✝ : Presentation R S<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>P : Presentation R S<GOAL>RingHom.ker (aeval P.baseChange.val) ≤ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))
<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 : α<VAR>inst✝¹ : Nonempty ι<VAR>s : Set α<VAR>f : α → ι<VAR>r : ι → ι → Prop<VAR>inst✝ : IsEquiv ι r<GOAL>s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
<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 : α<VAR>inst✝¹ : Nonempty ι<VAR>f : α → ι<VAR>r : ι → ι → Prop<VAR>inst✝ : IsEquiv ι r<GOAL>∅.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ ∅, r (f x) z
<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 : α<VAR>inst✝¹ : Nonempty ι<VAR>s : Set α<VAR>f : α → ι<VAR>r : ι → ι → Prop<VAR>inst✝ : IsEquiv ι r<VAR>hne : s.Nonempty<GOAL>s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}<VAR>o : Ordinal.{max u v}<GOAL>(type r).blsub f ≤ o ↔ (lsub fun a => f (typein r a) ⋯) ≤ o
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}<VAR>o : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f (typein r i) ⋯ < o
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>𝒢 : Filtration ι m<VAR>τ η : Ω → ι<VAR>i j : ι<VAR>s : Set Ω<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hτ_st : IsStoppingTime 𝒢 τ<VAR>hη_st : IsStoppingTime 𝒢 η<VAR>hτ : ∀ (ω : Ω), i ≤ τ ω<VAR>hη : ∀ (ω : Ω), i ≤ η ω<VAR>hs : MeasurableSet s<VAR>n : ι<GOAL>MeasurableSet {ω | s.piecewise τ η ω ≤ n}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>𝒢 : Filtration ι m<VAR>τ η : Ω → ι<VAR>i j : ι<VAR>s : Set Ω<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hτ_st : IsStoppingTime 𝒢 τ<VAR>hη_st : IsStoppingTime 𝒢 η<VAR>hτ : ∀ (ω : Ω), i ≤ τ ω<VAR>hη : ∀ (ω : Ω), i ≤ η ω<VAR>hs : MeasurableSet s<VAR>n : ι<VAR>this : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n}<GOAL>MeasurableSet {ω | s.piecewise τ η ω ≤ n}
<VAR>T : Type u<VAR>inst✝¹ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>inst✝ : IsIso sq<GOAL>sq.left ≫ (inv sq).left = 𝟙 f.left
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<GOAL>Set.Finite f.HasEigenvalue
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : minpoly K f ≠ 0<GOAL>Set.Finite f.HasEigenvalue
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : minpoly K f ≠ 0<GOAL>f.HasEigenvalue = (minpoly K f).rootSet K