ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>j : J<GOAL>(T.η.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>j : J<GOAL>c.π.app j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>j : J<GOAL>(T.μ.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = (T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c)) ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>j : J<GOAL>(T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a = T.map (T.map (c.π.app j)) ≫ T.map (D.obj j).a ≫ (D.obj j).a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<GOAL>∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<VAR>hr : 0 < r<GOAL>∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<VAR>hr : 0 < r<VAR>h_int : ∀ x ∈ Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))<GOAL>∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<VAR>hr : 0 < r<VAR>h_int : ∀ x ∈ Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))<GOAL>∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n))) < ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<VAR>hr : 0 < r<VAR>h_int : ∀ x ∈ Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))<GOAL>IntegrableOn (fun x => x ^ (-(r⁻¹ * ↑n))) (Ioc 0 1) volume
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<VAR>hr : 0 < r<VAR>h_int : ∀ x ∈ Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))<GOAL>IntervalIntegrable (fun x => x ^ (-(r⁻¹ * ↑n))) volume 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<VAR>hr : 0 < r<VAR>h_int : ∀ x ∈ Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))<GOAL>-1 < -(r⁻¹ * ↑n)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.length w⁻¹ = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.length w⁻¹ ≤ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.length w ≤ cs.length w⁻¹
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>s : σ →₀ ℕ<VAR>x : MvPolynomial σ R<VAR>d : σ →₀ ℕ<VAR>h : ¬s ≤ s + d<GOAL>False
<VAR>x : ℝ<GOAL>(log ↑x).re = Real.log x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>t₁ : UniformSpace α<VAR>t₂ : UniformSpace β<VAR>a : Set (α × α)<VAR>b : Set (β × β)<VAR>ha : a ∈ 𝓤 α<VAR>hb : b ∈ 𝓤 β<GOAL>{p | (p.1.1, p.2.1) ∈ a ∧ (p.1.2, p.2.2) ∈ b} ∈ 𝓤 (α × β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>t₁ : UniformSpace α<VAR>t₂ : UniformSpace β<VAR>a : Set (α × α)<VAR>b : Set (β × β)<VAR>ha : a ∈ 𝓤 α<VAR>hb : b ∈ 𝓤 β<GOAL>{p | (p.1.1, p.2.1) ∈ a ∧ (p.1.2, p.2.2) ∈ b} ∈ comap (fun p => (p.1.1, p.2.1)) (𝓤 α) ⊓ comap (fun p => (p.1.2, p.2.2)) (𝓤 β)
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<GOAL>x + 1 ≤ rexp x
<VAR>x y : ℝ<VAR>hx : 0 ≤ 0<GOAL>0 + 1 ≤ rexp 0
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<VAR>h : 0 < x<GOAL>x + 1 ≤ rexp x
<VAR>n a : ℕ<VAR>h' : n * a ≠ 0<GOAL>n.primeFactorsList <+ (n * a).primeFactorsList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>a✝ a : α<VAR>ha : a ∉ s<GOAL>s ⋖ insert a s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ c : α<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>(Ico a b).erase a = Ioo a b
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hwU : w ∈ closure U<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hwU : w ∈ interior U ∨ w ∈ frontier U<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<VAR>hwU : w ∈ interior U<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<VAR>hwU : w ∈ interior U<VAR>this : interior U ≠ univ<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<VAR>hwU : w ∈ interior U<VAR>this : interior U ≠ univ<VAR>z : E<VAR>hzU : z ∈ frontier (interior U)<VAR>hzw : infDist w (interior U)ᶜ = dist w z<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<VAR>hwU : w ∈ interior U<VAR>this : interior U ≠ univ<VAR>z : E<VAR>hzU : z ∈ frontier (interior U)<VAR>hzw : infDist w (interior U)ᶜ = dist w z<VAR>x : E<VAR>hx : x ∈ closure U<GOAL>(norm ∘ f) w = (norm ∘ f) z
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<VAR>hwU : w ∈ interior U<VAR>this : interior U ≠ univ<VAR>z : E<VAR>hzU : z ∈ frontier (interior U)<VAR>hzw : infDist w (interior U)ᶜ = dist w z<VAR>x : E<VAR>hx : x ∈ closure U<GOAL>ball w (dist z w) ⊆ U
<VAR>E : Type u<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<VAR>hc : IsCompact (closure U)<VAR>w : E<VAR>hle : IsMaxOn (norm ∘ f) (closure U) w<VAR>hwU : w ∈ interior U<VAR>this : interior U ≠ univ<VAR>z : E<VAR>hzU : z ∈ frontier (interior U)<VAR>hzw : infDist w (interior U)ᶜ = dist w z<VAR>x : E<VAR>hx : x ∈ closure U<GOAL>ball w (infDist w (interior U)ᶜ) ⊆ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>a ∈ ⨆ i, f i ↔ ∃ i, a ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>inst✝ : ConcreteCategory D<VAR>F G : C ⥤ D<VAR>φ : F ⟶ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : (forget D).obj (F.obj X)<GOAL>(φ.app Y) ((F.map f) x) = (G.map f) ((φ.app X) x)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LinearOrder G<VAR>inst✝² : LinearOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<VAR>a : G<VAR>b : P<GOAL>(a, b) ∈ SMulAntidiagonal ⋯ ⋯ (hs.min hns • ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LinearOrder G<VAR>inst✝² : LinearOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<VAR>a : G<VAR>b : P<GOAL>a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt ↔ a = hs.min hns ∧ b = ht.min hnt
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<GOAL>mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset α<VAR>hus : u ⊆ s<VAR>hucard : u.card = mulRothNumber s<VAR>hu : ThreeGPFree ↑u<GOAL>mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset α<VAR>hus : u ⊆ s<VAR>hucard : u.card = mulRothNumber s<VAR>hu : ThreeGPFree ↑u<VAR>v : Finset β<VAR>hvt : v ⊆ t<VAR>hvcard : v.card = mulRothNumber t<VAR>hv : ThreeGPFree ↑v<GOAL>mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset α<VAR>hus : u ⊆ s<VAR>hucard : u.card = mulRothNumber s<VAR>hu : ThreeGPFree ↑u<VAR>v : Finset β<VAR>hvt : v ⊆ t<VAR>hvcard : v.card = mulRothNumber t<VAR>hv : ThreeGPFree ↑v<GOAL>(u ×ˢ v).card ≤ mulRothNumber (s ×ˢ t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset α<VAR>hus : u ⊆ s<VAR>hucard : u.card = mulRothNumber s<VAR>hu : ThreeGPFree ↑u<VAR>v : Finset β<VAR>hvt : v ⊆ t<VAR>hvcard : v.card = mulRothNumber t<VAR>hv : ThreeGPFree ↑v<GOAL>ThreeGPFree ↑(u ×ˢ v)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<VAR>u : Finset α<VAR>hus : u ⊆ s<VAR>hucard : u.card = mulRothNumber s<VAR>hu : ThreeGPFree ↑u<VAR>v : Finset β<VAR>hvt : v ⊆ t<VAR>hvcard : v.card = mulRothNumber t<VAR>hv : ThreeGPFree ↑v<GOAL>ThreeGPFree (↑u ×ˢ ↑v)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<GOAL>(∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H✝ : M.LinearDisjoint N<VAR>H : M.LinearDisjoint M<VAR>inst✝ : Module.Flat R ↥M<VAR>hc : ∀ (m n : ↥M), Commute ↑m ↑n<GOAL>Module.rank R ↥M ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H✝ : M.LinearDisjoint N<VAR>H : M.LinearDisjoint M<VAR>inst✝ : Module.Flat R ↥M<VAR>hc : ∀ (m n : ↥(M ⊓ M)), Commute ↑m ↑n<GOAL>Module.rank R ↥(M ⊓ M) ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<GOAL>Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows<VAR>hx : x.SieveCompatible<VAR>inst✝ : HasPullbacks C<VAR>K : Pretopology C<GOAL>(∀ (E : A), Presieve.IsSheaf (Pretopology.toGrothendieck C K) (P ⋙ coyoneda.obj (op E))) ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows<VAR>hx : x.SieveCompatible<VAR>inst✝ : HasPullbacks C<VAR>K : Pretopology C<GOAL>(∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ coyoneda.obj (op E)) R) ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
<VAR>x y : PartENat<VAR>n : ℕ<VAR>h : x + y = ↑n<GOAL>x = ↑(n - y.get ⋯)
<VAR>y : PartENat<VAR>n x : ℕ<VAR>h : ↑x + y = ↑n<GOAL>↑x = ↑(n - y.get ⋯)
<VAR>n x y : ℕ<VAR>h : ↑x + ↑y = ↑n<GOAL>↑x = ↑(n - (↑y).get ⋯)
<VAR>n x y : ℕ<VAR>h✝ : ↑x + ↑y = ↑n<VAR>h : x + y = n<GOAL>↑x = ↑(n - (↑y).get ⋯)
<VAR>n : ℕ<VAR>a : Fin n<GOAL>(Ici a).card = n - ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝³ : Countable ι✝<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, StronglyMeasurable (f i)<GOAL>StronglyMeasurable fun a => ∏ i ∈ s, f i a
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : Y × Z → W<VAR>g : X → Y<VAR>h : X → Z<VAR>x : X<VAR>y : Y × Z<VAR>hf : ContinuousAt f (g x, h x)<VAR>hg : ContinuousAt g x<VAR>hh : ContinuousAt h x<VAR>e : (g x, h x) = y<GOAL>ContinuousAt (fun x => f (g x, h x)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : StronglyMeasurable f<GOAL>∫⁻ (a : β × γ), ↑‖f a‖₊ ∂(κ ⊗ₖ η) a < ⊤ ↔ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂η (a, x) < ⊤) ∧ ∫⁻ (a_1 : β), ↑‖∫ (y : γ), ‖f (a_1, y)‖ ∂η (a, a_1)‖₊ ∂κ a < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : StronglyMeasurable f<GOAL>∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂η (a, b) ∂κ a < ⊤ ↔ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂η (a, x) < ⊤) ∧ ∫⁻ (a_1 : β), ↑‖∫ (y : γ), ‖f (a_1, y)‖ ∂η (a, a_1)‖₊ ∂κ a < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : StronglyMeasurable f<VAR>this : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖<GOAL>∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂η (a, b) ∂κ a < ⊤ ↔ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂η (a, x) < ⊤) ∧ ∫⁻ (a_1 : β), ↑‖∫ (y : γ), ‖f (a_1, y)‖ ∂η (a, a_1)‖₊ ∂κ a < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : StronglyMeasurable f<VAR>this : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖<GOAL>∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂η (a, b) ∂κ a < ⊤ ↔ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂η (a, x) < ⊤) ∧ ∫⁻ (a_1 : β), ENNReal.ofReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂η (a, a_1)).toReal ∂κ a < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : StronglyMeasurable f<VAR>this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂η (a, x), 0 ≤ ‖f (x, y)‖<VAR>this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))<GOAL>∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂η (a, b) ∂κ a < ⊤ ↔ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂η (a, x) < ⊤) ∧ ∫⁻ (a_1 : β), ENNReal.ofReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂η (a, a_1)).toReal ∂κ a < ⊤
<VAR>α : Type u_1<VAR>s✝ t✝ s t : Finset α<VAR>a : α<VAR>ht : t ∈ s.powerset<VAR>h : a ∉ s<GOAL>a ∉ t
<VAR>α : Type u_1<VAR>s✝ t✝ s t : Finset α<VAR>a : α<VAR>ht : t ∈ s.powerset<VAR>h : a ∉ s<GOAL>a ∈ t → a ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Nonempty α<VAR>T : Set α → F →L[ℝ] F'<VAR>x : F<VAR>m : MeasurableSpace α<GOAL>setToSimpleFunc T (const α x) = (T Set.univ) x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>i : ι<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(p i).ball 0 r = ({i}.sup p).ball 0 r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<GOAL>Disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : Disjoint (ball x δ) (ball y ε)<VAR>hxy : dist x y < δ + ε<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : Disjoint (ball x δ) (ball y ε)<VAR>hxy : dist x y < ε + δ<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : Disjoint (ball x δ) (ball y ε)<VAR>hxy : dist x y < ε + δ<VAR>z : E<VAR>hxz : dist x z < δ<VAR>hzy : dist z y < ε<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : Disjoint (ball x δ) (ball y ε)<VAR>hxy : dist x y < ε + δ<VAR>z : E<VAR>hxz : dist z x < δ<VAR>hzy : dist z y < ε<GOAL>False
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>H : Type u_6<VAR>inst✝ : Monoid H<VAR>f : G →* H<VAR>hf : Injective ⇑f<VAR>x : G<GOAL>orderOf (f x) = orderOf x
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : CompactSpace G<GOAL>UniformContinuous fun p => p.1 / p.2
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : CompactSpace G<GOAL>Continuous fun p => p.1 / p.2
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a / b * c = a * (c / b)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Preorder α<VAR>a b✝ c b : α<GOAL>⋃ a, Ico a b = Iio b
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<VAR>e✝ : Perm σ<GOAL>(rename ⇑e✝) (esymm σ R n) = esymm σ R n
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hp : ∀ n' ≥ n, ¬p n'<GOAL>nth p n = 0