ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : Fintype ι'<VAR>f : ι' ≃ ι<GOAL>Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' => μ (f i')) = Measure.pi μ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : Fintype ι'<VAR>f : ι' ≃ ι<VAR>s : (i : ι) → Set (α i)<VAR>x✝ : ∀ (i : ι), MeasurableSet (s i)<GOAL>(Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' => μ (f i'))) (univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>α : Type u_1<VAR>l₁ l₂ l : List α<GOAL>l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => ↑(f x).toNNReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>HasFiniteIntegral (fun x => ↑(f x).toNNReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>(fun a => ENNReal.ofReal ‖↑(f a).toNNReal‖) ≤ fun a => ENNReal.ofReal ‖f a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>x : α<GOAL>(fun a => ENNReal.ofReal ‖↑(f a).toNNReal‖) x ≤ (fun a => ENNReal.ofReal ‖f a‖) x
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<GOAL>∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<GOAL>∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<GOAL>∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<VAR>G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal<GOAL>∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<VAR>G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal<VAR>hG : Continuous G<GOAL>∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<VAR>G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal<VAR>hG : Continuous G<GOAL>∀ᶠ (c : ι) in l, (G ∘ id fun i => ↑(F i)) c ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<VAR>G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal<VAR>hG : Continuous G<GOAL>∀ (x : ι), ‖F x‖ ≤ C → (G ∘ id fun i => ↑(F i)) x ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<VAR>G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal<VAR>hG : Continuous G<VAR>k : ι<VAR>hCFk : ‖F k‖ ≤ C<GOAL>(G ∘ id fun i => ↑(F i)) k ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>s : Finset α<VAR>hp' : p ≠ 0<VAR>hp'' : 0 < p.toReal<VAR>G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal<VAR>hG : Continuous G<VAR>k : ι<VAR>hCFk : ‖F k‖ ≤ C<GOAL>‖F k‖ ^ p.toReal ≤ C ^ p.toReal
<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>j : N →* P<VAR>hj : ∀ (x : M), j (f.toMap x) = g x<VAR>x✝ : N<GOAL>(f.lift hg) x✝ = j x✝
<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>j : N →* P<VAR>hj : ∀ (x : M), j (f.toMap x) = g x<VAR>x✝ : N<GOAL>j (f.toMap (f.sec x✝).1) = j (f.toMap ↑(f.sec x✝).2 * x✝)
<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>j : N →* P<VAR>hj : ∀ (x : M), j (f.toMap x) = g x<VAR>x✝ : N<GOAL>f.toMap (f.sec x✝).1 = f.toMap ↑(f.sec x✝).2 * x✝
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪(o.rotation ↑(π / 2)) x, r • x⟫_ℝ = 0
<VAR>p✝ q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>p q : ℚ≥0<GOAL>p < q ↔ p.num * q.den < q.num * p.den
<VAR>p✝ q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>p q : ℚ≥0<GOAL>(↑p).num * ↑(↑q).den < (↑q).num * ↑(↑p).den ↔ p.num * q.den < q.num * p.den
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : ModP K v O hv p<GOAL>v ↑p < preVal K v O hv p x ↔ x ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : ModP K v O hv p<VAR>h : x ≠ 0<VAR>hp : preVal K v O hv p x ≤ v ↑p<GOAL>x = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0<VAR>hp : preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ≤ v ↑p<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0<VAR>hp : ↑p ∣ r<GOAL>(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0<VAR>hp : ↑p ∣ r<GOAL>↑p ∣ r
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>l : Products I<GOAL>isGood (π C fun x => ord I x < o) l ↔ ∃ o' < o, isGood (π C fun x => ord I x < o') l
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>l : Products I<VAR>h : isGood (π C fun x => ord I x < o) l<GOAL>∃ o' < o, isGood (π C fun x => ord I x < o') l
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>l : Products I<VAR>h : isGood (π C fun x => ord I x < o) l<GOAL>((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o ∧ isGood (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>l : Products I<VAR>h : isGood (π C fun x => ord I x < o) l<VAR>ha : ⊥ < o<GOAL>((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o ∧ isGood (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>l : Products I<VAR>h : isGood (π C fun x => ord I x < o) l<VAR>ha : ⊥ < o<VAR>hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o<VAR>he : eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})<GOAL>eval (π C fun x => ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o) '' {m | m < l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : contained C o<VAR>l : Products I<VAR>h : isGood (π C fun x => ord I x < o) l<VAR>ha : ⊥ < o<VAR>hslt : ((↑l).toFinset.sup fun a => Order.succ (ord I a)) < o<VAR>he : eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < (↑l).toFinset.sup fun a => Order.succ (ord I a)) '' {m | m < l})<VAR>hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a => Order.succ (ord I a)<GOAL>eval (π C fun x => ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o) '' {m | m < l})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s s' t : Set α<VAR>ht : s ∩ frontier t = s' ∩ frontier t<GOAL>t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s s' t : Set α<VAR>ht : s ∩ frontier t = s' ∩ frontier t<GOAL>s' ∩ frontier tᶜ = s ∩ frontier tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<GOAL>r.preimage (s ∩ r.codom) = r.preimage s
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : AddCommMonoid M✝<VAR>inst✝¹⁷ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁶ : CommRing R₁<VAR>inst✝¹⁵ : AddCommGroup M₁<VAR>inst✝¹⁴ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹³ : CommSemiring R₂<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹⁰ : CommRing R₃<VAR>inst✝⁹ : AddCommGroup M₃<VAR>inst✝⁸ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>A : Type u_11<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Module A M₃<VAR>B₃ : BilinForm A M₃<VAR>ι : Type u_12<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>M : Matrix ι ι A<GOAL>(toBilin' M).Nondegenerate ↔ M.det ≠ 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<GOAL>hurwitzZeta a (1 - s) = (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (-↑π * I * s / 2) * expZeta a s + cexp (↑π * I * s / 2) * expZeta (-a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>hs' : a ≠ 0 ∨ s ≠ 1<GOAL>2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s + 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) * sinZeta a s = (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) + cexp (↑π * I * s / 2) * (cosZeta a s + I * -sinZeta a s))
<VAR>x y : ℕ<GOAL>x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>m : M<GOAL>m ∈ posFittingComp R L M ↔ m ∈ ⨆ x, posFittingCompOf R M x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>h : e ∉ G.incidenceSet a<GOAL>incMatrix R G a e = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a / ⊤ = 0
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : P3 x₃ x₂ y₂ y₃<VAR>h₂ : P3 x₁ x₃ y₂ y₁<GOAL>P1 x₁ x₂ x₃ y₁ y₂ y₃
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : P3 x₃ x₂ y₂ y₃<VAR>h₂ : P3 x₁ x₃ y₂ y₁<GOAL>⟦x₃ * y₂⟧ + (⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ + ⟦x₃ * y₃⟧) < ⟦x₃ * y₂⟧ + (⟦x₃ * y₁⟧ + ⟦x₂ * y₃⟧ + ⟦x₁ * y₂⟧)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>f : α → β<GOAL>Tendsto (fun x => f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>f : α → β<GOAL>(∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>f : α → β<VAR>u : Set β<VAR>hu : u ∈ lb<GOAL>(∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>f : α → β<VAR>u : Set β<VAR>hu : u ∈ lb<GOAL>(∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la
<VAR>X : Scheme<VAR>U : (Opens ↑↑((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>(Opens.map (adjunction.unit.app X).val.base).obj (unop U) ≤ ⊤
<VAR>X : Scheme<VAR>U : (Opens ↑↑((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>toOpen (↑(unop (Scheme.Γ.rightOp.obj X))) (unop U) ≫ (adjunction.unit.app X).val.c.app U = X.presheaf.map (homOfLE ⋯).op
<VAR>X : Scheme<VAR>U : (Opens ↑↑((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>toOpen ↑(unop (Scheme.Γ.rightOp.obj X)) ⊤ ≫ (adjunction.unit.app X).val.c.app (op ⊤) ≫ ((pushforward CommRingCat (adjunction.unit.app X).val.base).obj ((𝟭 Scheme).obj X).presheaf).map (homOfLE ⋯).op = X.presheaf.map (homOfLE ⋯).op
<VAR>X : Scheme<VAR>U : (Opens ↑↑((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>(adjunction.counit.app (Scheme.Γ.rightOp.obj X)).unop ≫ (Scheme.Γ.rightOp.map (adjunction.unit.app X)).unop ≫ ((pushforward CommRingCat (adjunction.unit.app X).val.base).obj ((𝟭 Scheme).obj X).presheaf).map (homOfLE ⋯).op = X.presheaf.map (homOfLE ⋯).op
<VAR>X : Scheme<VAR>U : (Opens ↑↑((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>(𝟙 (Scheme.Γ.rightOp.obj X)).unop ≫ ((pushforward CommRingCat (adjunction.unit.app X).val.base).obj ((𝟭 Scheme).obj X).presheaf).map (homOfLE ⋯).op = X.presheaf.map (homOfLE ⋯).op
<VAR>X : Scheme<VAR>U : (Opens ↑↑((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>𝟙 Γ(X, ⊤) ≫ X.presheaf.map (homOfLE ⋯).op = X.presheaf.map (homOfLE ⋯).op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<GOAL>edist (f 0) a ≤ ∑' (m : ℕ), d m
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<GOAL>J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ∩ ↑J'
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : Finite ι<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝ : PseudoMetrizableSpace X<VAR>s : Set X<VAR>hs : IsSeparable s<VAR>this : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X<GOAL>SecondCountableTopology ↑s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : Finite ι<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝ : PseudoMetrizableSpace X<VAR>s : Set X<VAR>hs : IsSeparable s<VAR>this✝ : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X<VAR>this : SeparableSpace ↑s<GOAL>SecondCountableTopology ↑s
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>P.nextCoeff = -P.roots.sum
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>(Multiset.map (fun a => X - C a) P.roots).prod.nextCoeff = -P.roots.sum
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>(Multiset.map (fun i => (X - C i).nextCoeff) P.roots).sum = -P.roots.sum
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>∀ a ∈ P.roots, (X - C a).Monic
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.append q).IsPath → p.IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.support ++ q.support.tail).Nodup → p.support.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f ≈ g<VAR>gh : g < h<GOAL>f < h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f ≈ g<VAR>gh : g < h<VAR>this : (h - g + -(f - g)).Pos<GOAL>f < h
<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 : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<GOAL>s.secondInter (s.secondInter p v) v = 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>s : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<VAR>hv' : ⟪v, v⟫_ℝ ≠ 0<GOAL>s.secondInter (s.secondInter p v) v = 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>s : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<VAR>hv' : ⟪v, v⟫_ℝ ≠ 0<GOAL>(-2 * (-2 * ⟪v, p -ᵥ s.center⟫_ℝ + ⟪v, p -ᵥ s.center⟫_ℝ) / ⟪v, v⟫_ℝ) • v + (-2 * ⟪v, p -ᵥ s.center⟫_ℝ / ⟪v, v⟫_ℝ) • v +ᵥ 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>s : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<VAR>hv' : ⟪v, v⟫_ℝ ≠ 0<GOAL>((-2 * (-2 * ⟪v, p -ᵥ s.center⟫_ℝ + ⟪v, p -ᵥ s.center⟫_ℝ) + -2 * ⟪v, p -ᵥ s.center⟫_ℝ) / ⟪v, v⟫_ℝ) • v = 0
<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 : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<VAR>hv' : ⟪v, v⟫_ℝ ≠ 0<GOAL>(-2 * (-2 * ⟪v, p -ᵥ s.center⟫_ℝ + ⟪v, p -ᵥ s.center⟫_ℝ) + -2 * ⟪v, p -ᵥ s.center⟫_ℝ) / ⟪v, v⟫_ℝ = 0
<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 : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<VAR>hv' : ⟪v, v⟫_ℝ ≠ 0<GOAL>-2 * (-2 * ⟪v, p -ᵥ s.center⟫_ℝ + ⟪v, p -ᵥ s.center⟫_ℝ) + -2 * ⟪v, p -ᵥ s.center⟫_ℝ = 0