ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<VAR>hu : univ.erase j₂ = {j₁, j₃}<VAR>hle : (altitude t₁ i₃).directionᗮ ≤ (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}).directionᗮ<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}).directionᗮ
<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>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<VAR>hu : univ.erase j₂ = {j₁, j₃}<VAR>hle : (altitude t₁ i₃).directionᗮ ≤ (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}).directionᗮ<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ vectorSpan ℝ (t₁.points '' ↑(univ.erase i₃))
<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>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<VAR>hu : univ.erase j₂ = {j₁, j₃}<VAR>hle : (altitude t₁ i₃).directionᗮ ≤ (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}).directionᗮ<VAR>hui : univ.erase i₃ = {i₁, i₂}<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ vectorSpan ℝ (t₁.points '' ↑(univ.erase i₃))
<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>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<VAR>hu : univ.erase j₂ = {j₁, j₃}<VAR>hle : (altitude t₁ i₃).directionᗮ ≤ (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}).directionᗮ<VAR>hui : univ.erase i₃ = {i₁, i₂}<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ vectorSpan ℝ {t₁.points i₁, t₁.points i₂}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝¹ : CommMonoid M<VAR>a✝ : M<VAR>l✝ l₁ l₂ : List M<VAR>inst✝ : DecidableEq α<VAR>f : α → M<VAR>a b : α<VAR>l : List α<VAR>h : a ∈ b :: l<GOAL>f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝¹ : CommMonoid M<VAR>a✝ : M<VAR>l✝ l₁ l₂ : List M<VAR>inst✝ : DecidableEq α<VAR>f : α → M<VAR>a : α<VAR>l : List α<VAR>h : a ∈ a :: l<GOAL>f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝¹ : CommMonoid M<VAR>a✝ : M<VAR>l✝ l₁ l₂ : List M<VAR>inst✝ : DecidableEq α<VAR>f : α → M<VAR>a b : α<VAR>l : List α<VAR>h✝ : a ∈ b :: l<VAR>ne : a ≠ b<VAR>h : a ∈ l<GOAL>f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>h : Disjoint p.vars q.vars<GOAL>(p + q).vars = p.vars ∪ q.vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>h : Disjoint p.vars q.vars<VAR>x : σ<VAR>hx : x ∈ p.vars ∪ q.vars<GOAL>x ∈ (p + q).vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>x : σ<VAR>h : p.degrees.Disjoint q.degrees<VAR>hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset<GOAL>x ∈ (p + q).degrees.toFinset
<VAR>x : PartENat<VAR>h : x.Dom<GOAL>↑(x.get h) = x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>f₂ : Subobject Y<GOAL>∀ (f₁ : Subobject Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>f₂ : Subobject Y<GOAL>∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>f₂ : Subobject Y<VAR>f₁ : MonoOver Y<GOAL>(pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>f₂ : Subobject Y<VAR>f₁ : MonoOver Y<GOAL>(map (pullback.snd f₁.arrow g)).obj ((pullback (pullback.snd f₁.arrow g ≫ g)).obj f₂) = (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)
<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>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>H : ∀ b < a, ∃ i, f i = b<GOAL>a ≤ mex f
<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>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>H : ∀ b < a, ∃ i, f i = b<VAR>h : mex f < a<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t : Set α<VAR>f✝ g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<VAR>hsc₀ : μ sᶜ ≠ 0<VAR>hfi : Integrable f μ<GOAL>⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasCoproduct f<VAR>inst✝ : HasCoproduct (f ∘ ⇑ε)<VAR>b : β<GOAL>ι (f ∘ ⇑ε) b ≫ (HasColimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun x => Iso.refl (f (ε x.as)))).hom = ι f (ε b)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasCoproduct f<VAR>inst✝ : HasCoproduct (f ∘ ⇑ε)<VAR>b : β<GOAL>(Discrete.functor (f ∘ ⇑ε)).map ((Discrete.equivalence ε).unit.app { as := b }) ≫ colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) } = ι f (ε b)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasCoproduct f<VAR>inst✝ : HasCoproduct (f ∘ ⇑ε)<VAR>b : β<VAR>h : (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } = colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }<GOAL>(Discrete.functor (f ∘ ⇑ε)).map ((Discrete.equivalence ε).unit.app { as := b }) ≫ colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) } = ι f (ε b)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasCoproduct f<VAR>inst✝ : HasCoproduct (f ∘ ⇑ε)<VAR>b : β<VAR>h : (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } = colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }<GOAL>eqToHom ⋯ ≫ colimit.ι (Discrete.functor f) { as := ε b } = ι f (ε b)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasCoproduct f<VAR>inst✝ : HasCoproduct (f ∘ ⇑ε)<VAR>b : β<VAR>h : (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } = colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }<GOAL>{ as := b } = { as := ε.symm (ε b) }
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>M.charpoly.coeff k = (∏ i : n, (X - C (M i i))).coeff k
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>M.charpoly.coeff k - (∏ i : n, (X - C (M i i))).coeff k = 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>(M.charpoly - ∏ i : n, (X - C (M i i))).coeff k = 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>(M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑k
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>↑(Fintype.card n - 1) ≤ ↑k
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>Fintype.card n - 1 ≤ k
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ≠ 0<GOAL>(fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => cexp (Complex.log x.1 * x.2)
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ≠ 0<GOAL>∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.1 ≠ 0
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ≠ 0<GOAL>IsOpen fun x => x.1 = 0 → False
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ≠ 0<GOAL>IsOpen {x | x.1 = 0}ᶜ
<VAR>α : Type u_1<VAR>p : ℂ × ℂ<VAR>hp_fst : p.1 ≠ 0<GOAL>IsClosed {x | x.1 = 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>r✝ : α → β → Prop<VAR>f : α → γ<VAR>g : β → δ<VAR>c : γ<VAR>d : δ<VAR>hf : Injective f<VAR>hg : Injective g<VAR>r : α → β → Prop<VAR>a : α<VAR>b : β<GOAL>Relation.Map r f g (f a) (g b) ↔ r a b
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<GOAL>∃ f ∈ B' \ B, B' = insert f B \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f✝ : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<VAR>f : α<VAR>hf : f ∈ B' \ B<VAR>hb : M.Base (insert f (B \ {e}))<GOAL>∃ f ∈ B' \ B, B' = insert f B \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f✝ : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<VAR>f : α<VAR>hf : f ∈ B' \ B<VAR>hb : M.Base (insert f (B \ {e}))<VAR>hne : f ≠ e<GOAL>∃ f ∈ B' \ B, B' = insert f B \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f✝ : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<VAR>f : α<VAR>hf : f ∈ B' \ B<VAR>hb : M.Base (insert f B \ {e})<VAR>hne : f ≠ e<GOAL>∃ f ∈ B' \ B, B' = insert f B \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f✝ : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<VAR>f : α<VAR>hf : f ∈ B' \ B<VAR>hb : M.Base (insert f B \ {e})<VAR>hne : f ≠ e<GOAL>insert f B \ {e} ⊆ B'
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f✝ : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<VAR>f : α<VAR>hf : f ∈ B' \ B<VAR>hb : M.Base (insert f B \ {e})<VAR>hne : f ≠ e<GOAL>f ∈ B' ∪ {e}
<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>β✝ : Type u_7<VAR>inst✝¹ : AddCommMonoid β✝<VAR>T✝ T' : Set α → β✝<VAR>β : Type u_8<VAR>inst✝ : AddCancelMonoid β<VAR>T : Set α → β<VAR>hT : FinMeasAdditive μ T<GOAL>T ∅ = 0
<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>β✝ : Type u_7<VAR>inst✝¹ : AddCommMonoid β✝<VAR>T✝ T' : Set α → β✝<VAR>β : Type u_8<VAR>inst✝ : AddCancelMonoid β<VAR>T : Set α → β<VAR>hT : FinMeasAdditive μ T<VAR>h_empty : μ ∅ ≠ ⊤<GOAL>T ∅ = 0
<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>β✝ : Type u_7<VAR>inst✝¹ : AddCommMonoid β✝<VAR>T✝ T' : Set α → β✝<VAR>β : Type u_8<VAR>inst✝ : AddCancelMonoid β<VAR>T : Set α → β<VAR>h_empty : μ ∅ ≠ ⊤<VAR>hT : T (∅ ∪ ∅) = T ∅ + T ∅<GOAL>T ∅ = 0
<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>β✝ : Type u_7<VAR>inst✝¹ : AddCommMonoid β✝<VAR>T✝ T' : Set α → β✝<VAR>β : Type u_8<VAR>inst✝ : AddCancelMonoid β<VAR>T : Set α → β<VAR>h_empty : μ ∅ ≠ ⊤<VAR>hT : T ∅ = T ∅ + T ∅<GOAL>T ∅ = 0
<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>β✝ : Type u_7<VAR>inst✝¹ : AddCommMonoid β✝<VAR>T✝ T' : Set α → β✝<VAR>β : Type u_8<VAR>inst✝ : AddCancelMonoid β<VAR>T : Set α → β<VAR>h_empty : μ ∅ ≠ ⊤<VAR>hT : T ∅ + 0 = T ∅ + T ∅<GOAL>T ∅ = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Monoid α<VAR>inst✝ : HasDistribNeg α<VAR>a : α<VAR>n : ℕ<VAR>h : Odd n<GOAL>(-1) ^ n = -1
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : Preorder ι<VAR>f✝ : Filtration ι m<VAR>τ π : Ω → ι<VAR>f : Filtration ι m<VAR>i : ι<VAR>s : Set Ω<GOAL>MeasurableSet s ↔ MeasurableSet s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : Preorder ι<VAR>f✝ : Filtration ι m<VAR>τ π : Ω → ι<VAR>f : Filtration ι m<VAR>i : ι<VAR>s : Set Ω<GOAL>(∀ (i_1 : ι), MeasurableSet (s ∩ {ω | i ≤ i_1})) ↔ MeasurableSet s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hs : IsCompact s<VAR>hmono : MonotoneOn f s<GOAL>IntegrableOn f s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hs : IsCompact ∅<VAR>hmono : MonotoneOn f ∅<GOAL>IntegrableOn f ∅ μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hs : IsCompact s<VAR>hmono : MonotoneOn f s<VAR>h : s.Nonempty<GOAL>IntegrableOn f s μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>re ⟪x, 0⟫_𝕜 = 0
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a✝ : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<VAR>a : A<VAR>ha : a ∈ approxOrderOf A n δ<GOAL>(fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a✝ : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<VAR>a : A<VAR>ha : a ∈ approxOrderOf A n δ<VAR>b : A<VAR>hb : orderOf b = n<VAR>hab : a ∈ ball b δ<GOAL>(fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a✝ : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<VAR>a : A<VAR>ha : a ∈ approxOrderOf A n δ<VAR>b : A<VAR>hab : a ∈ ball b δ<VAR>hb : b ^ m ∈ {u | orderOf u = n}<GOAL>(fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a✝ : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<VAR>a : A<VAR>ha : a ∈ approxOrderOf A n δ<VAR>b : A<VAR>hab : a ∈ ball b δ<VAR>hb : b ^ m ∈ {u | orderOf u = n}<GOAL>(fun y => y ^ m) a ∈ ball (b ^ m) (↑m • δ)
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a✝ : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<VAR>a : A<VAR>ha : a ∈ approxOrderOf A n δ<VAR>b : A<VAR>hab : a ∈ ball b δ<VAR>hb : b ^ m ∈ {u | orderOf u = n}<GOAL>ball (b ^ m) (↑m • δ) = ball (b ^ m) (m • δ)
<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 y : V<VAR>r : ℝ<GOAL>o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = ↑π ↔ o.oangle x y = 0 ∨ o.oangle x y = ↑π
<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 y : V<VAR>r : ℝ<GOAL>(∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, r • x + y] i = 0 ∧ ∃ i, g i ≠ 0) ↔ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
<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 y : V<VAR>r : ℝ<GOAL>(∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ ∃ i, g i ≠ 0) ↔ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
<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 y : V<VAR>r : ℝ<GOAL>(∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ ∃ i, g i ≠ 0) ↔ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ ∃ i, g i ≠ 0
<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 y : V<VAR>r : ℝ<GOAL>(∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ ∃ i, g i ≠ 0
<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 y : V<VAR>r : ℝ<GOAL>(∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset (ι →₀ M)<VAR>hs : (↑s).PairwiseDisjoint Finsupp.support<GOAL>(s.sum id).support = s.sup Finsupp.support
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.dblXYZ P = P x ^ 2 • ![1, 1, 0]
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝² : OrderedCommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>f g✝ : ι → α<VAR>a a₁ a₂ : α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Injective e<VAR>hs : ∀ c ∉ Set.range e, 1 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝² : OrderedCommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>f g✝ : ι → α<VAR>a a₁ a₂ : α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Injective e<VAR>hs : ∀ c ∉ Set.range e, 1 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : HasProd (extend e f 1) a₁<VAR>hg : HasProd g a₂<GOAL>a₁ ≤ a₂