ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = ((A.X ◁ f.hom ≫ f.hom ▷ B.X) ▷ M.X ≫ B.mul ▷ M.X) ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = (A.mul ≫ f.hom) ▷ M.X ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>X✝ Y✝ : Mod_ B<VAR>g : X✝ ⟶ Y✝<GOAL>(f.hom ▷ X✝.X ≫ X✝.act) ≫ g.hom = A.X ◁ g.hom ≫ f.hom ▷ Y✝.X ≫ Y✝.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>X✝ Y✝ : Mod_ B<VAR>g : X✝ ⟶ Y✝<GOAL>(f.hom ▷ X✝.X ≫ X✝.act) ≫ g.hom = (f.hom ▷ X✝.X ≫ B.X ◁ g.hom) ≫ Y✝.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>X✝ Y✝ : Mod_ B<VAR>g : X✝ ⟶ Y✝<GOAL>(f.hom ▷ X✝.X ≫ X✝.act) ≫ g.hom = f.hom ▷ X✝.X ≫ X✝.act ≫ g.hom
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ i : ι<VAR>xi : β i<GOAL>single i xi = 0 ↔ xi = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ i : ι<VAR>xi : β i<GOAL>i = i ∧ HEq xi 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hst : s ⊆ t<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ<GOAL>∫⋯∫⁻_t, f ∂μ ≤ ∫⋯∫⁻_t, g ∂μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hst : s ⊆ t<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ<GOAL>∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, f ∂μ ∂μ ≤ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, g ∂μ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : α → β<VAR>e : γ ≃ᵐ α<VAR>h : MeasurePreserving (⇑e) μc μa<GOAL>MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasurePreserving g μa μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : α → β<VAR>e : γ ≃ᵐ α<VAR>h : MeasurePreserving (⇑e) μc μa<VAR>hg : MeasurePreserving (g ∘ ⇑e) μc μb<GOAL>MeasurePreserving g μa μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : α → β<VAR>e : γ ≃ᵐ α<VAR>h : MeasurePreserving (⇑e) μc μa<VAR>hg : MeasurePreserving (g ∘ ⇑e) μc μb<GOAL>g = (g ∘ ⇑e) ∘ ⇑e.symm
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Finite V<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Finite V<VAR>val✝ : Fintype V<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ✝ : Measure G<VAR>f✝ : G → E<VAR>g : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>f : G → E<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>x' : G<GOAL>∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ✝ : Measure G<VAR>f✝ : G → E<VAR>g : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>f : G → E<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>x' : G<GOAL>∫ (x : G), f (x' * x⁻¹) ∂μ = ∫ (x : G), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : IsFiniteMeasure μ<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : IsFiniteMeasure μ<VAR>this : ∀ (n : ℕ), ∃ g, Measurable g ∧ g ≤ f ∧ g ≤ ↑n ∧ ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g a ∂μ<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : IsFiniteMeasure μ<VAR>g : ℕ → α → ℝ≥0∞<VAR>hgm : ∀ (n : ℕ), Measurable (g n)<VAR>hgf : ∀ (n : ℕ), g n ≤ f<VAR>hgle : ∀ (n : ℕ), g n ≤ ↑n<VAR>hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x<VAR>hφm : Measurable φ<VAR>hφle : φ ≤ f<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, φ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : IsFiniteMeasure μ<VAR>g : ℕ → α → ℝ≥0∞<VAR>hgm : ∀ (n : ℕ), Measurable (g n)<VAR>hgf : ∀ (n : ℕ), g n ≤ f<VAR>hgle : ∀ (n : ℕ), g n ≤ ↑n<VAR>hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x<VAR>hφm : Measurable φ<VAR>hφle : φ ≤ f<VAR>s : Set α<GOAL>⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : IsFiniteMeasure μ<VAR>g : ℕ → α → ℝ≥0∞<VAR>hgm : ∀ (n : ℕ), Measurable (g n)<VAR>hgf : ∀ (n : ℕ), g n ≤ f<VAR>hgle : ∀ (n : ℕ), g n ≤ ↑n<VAR>hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x<VAR>hφm : Measurable φ<VAR>hφle : φ ≤ f<VAR>s : Set α<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<GOAL>(SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h : IsFiniteMeasure μ<VAR>g : ℕ → α → ℝ≥0∞<VAR>hgm : ∀ (n : ℕ), Measurable (g n)<VAR>hgf : ∀ (n : ℕ), g n ≤ f<VAR>hgle : ∀ (n : ℕ), g n ≤ ↑n<VAR>hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x<VAR>hφm : Measurable φ<VAR>hφle : φ ≤ f<VAR>s : Set α<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<VAR>n : ℕ<VAR>hn : ∀ (x : α), ↑ψ x ≤ ↑n<GOAL>(SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-x ≈ y ↔ x ≈ -y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommRing S<VAR>abv : AbsoluteValue R S<VAR>x : ℤˣ<VAR>y : R<GOAL>abv (x • y) = abv y
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>s : ∀ {x y : α}, R x y → R y x<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>s : ∀ {x y : α}, R x y → R y x<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(Pairwise (fun {x y} => R x y) ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ l₁ ++ [a] → ∀ (b : α), b ∈ l₂ → R a_1 b) ↔ Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ [a] ++ l₁ → ∀ (b : α), b ∈ l₂ → R a_1 b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i xy.1, (u ∘ Subtype.val) i xy.2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<GOAL>∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i xy.1, (u ∘ Subtype.val) i xy.2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<GOAL>∀ (a : β × β), (∀ (i : ↑A), ((u ∘ Subtype.val) i a.1, (u ∘ Subtype.val) i a.2) ∈ V) → a ∈ S ×ˢ S → ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i a.1, (u ∘ Subtype.val) i a.2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x y : β<VAR>hxy : ∀ (i : ↑A), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ V<VAR>hxS : (x, y).1 ∈ S<VAR>hyS : (x, y).2 ∈ S<GOAL>∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x y : β<VAR>hxy : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ V<VAR>hxS : (x, y).1 ∈ S<VAR>hyS : (x, y).2 ∈ S<GOAL>∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x y : β<VAR>hxS : (x, y).1 ∈ S<VAR>hyS : (x, y).2 ∈ S<VAR>hxy : A ⊆ (fun f => (u f x, u f y)) ⁻¹' V<GOAL>∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x y : β<VAR>hxS : (x, y).1 ∈ S<VAR>hyS : (x, y).2 ∈ S<VAR>hxy : A ⊆ (fun f => (u f x, u f y)) ⁻¹' V<GOAL>Continuous fun f => u f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x y : β<VAR>hxS : (x, y).1 ∈ S<VAR>hyS : (x, y).2 ∈ S<VAR>hxy : A ⊆ (fun f => (u f x, u f y)) ⁻¹' V<GOAL>Continuous fun f => u f y
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>↑(re z) = (z + (starRingEnd K) z) / 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanHom n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanHom n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hsA : ∀ ⦃x : α₁ × α₂⦄, x ∈ s → x ∈ A₁ ×ˢ A₂<VAR>htA : ∀ ⦃x : α₁ × α₂⦄, x ∈ t → x ∈ A₁ ×ˢ A₂<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>(map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanHom n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanHom n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<VAR>hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂<VAR>htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂<GOAL>(map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanHom n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanHom n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hs : card s = n<VAR>ht : card t = n<VAR>hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂<VAR>htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂<VAR>h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod<GOAL>(map (fun x => f₁ x.1) s).prod = (map (fun x => f₁ x.1) t).prod ∧ (map (fun x => f₂ x.2) s).prod = (map (fun x => f₂ x.2) t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanHom n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanHom n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hs : card s = n<VAR>ht : card t = n<VAR>hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂<VAR>htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂<VAR>h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod<GOAL>(map f₁ (map Prod.fst s)).prod = (map f₁ (map Prod.fst t)).prod ∧ (map f₂ (map Prod.snd s)).prod = (map f₂ (map Prod.snd t)).prod
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>¬n % 2 = 0 ↔ n % 2 = 1
<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 Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.dblXYZ P = W.dblZ P • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<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 Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<VAR>hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)<GOAL>W.dblXYZ P = W.dblZ P • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Opens X<GOAL>(idealOfSet 𝕜 ↑s).IsMaximal ↔ IsCoatom s
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Opens X<GOAL>IsCoatom (idealOfSet 𝕜 ↑s) ↔ IsCoatom s
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Opens X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsCoatom I<GOAL>idealOfSet 𝕜 ↑(opensOfIdeal I) = I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Opens X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : I.IsMaximal<GOAL>idealOfSet 𝕜 ↑(opensOfIdeal I) = I
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r✝ : X<VAR>s✝ : ↥S<GOAL>0 + r✝ /ₒ s✝ = r✝ /ₒ s✝
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r✝ : X<VAR>s✝ : ↥S<GOAL>(0 + r✝) /ₒ s✝ = r✝ /ₒ s✝
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MulAction G α<VAR>inst✝⁶ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁵ : Countable G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : SMulInvariantMeasure G α ν<VAR>inst✝² : MeasurableSMul G α<VAR>hasFun : HasFundamentalDomain G α ν<VAR>μ μ' : Measure (Quotient α_mod_G)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ'<GOAL>μ = μ'
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MulAction G α<VAR>inst✝⁶ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁵ : Countable G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : SMulInvariantMeasure G α ν<VAR>inst✝² : MeasurableSMul G α<VAR>hasFun : HasFundamentalDomain G α ν<VAR>μ μ' : Measure (Quotient α_mod_G)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ'<VAR>𝓕 : Set α<VAR>h𝓕 : IsFundamentalDomain G 𝓕 ν<GOAL>μ = μ'
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>ι : Sort u_4<VAR>p : ι → Subsemigroup M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>ι : Sort u_4<VAR>p : ι → Subsemigroup M<VAR>m : M<GOAL>(∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Preorder α<VAR>a✝ b c a : α<GOAL>⋃ b, Icc a b = Ici a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α✝<VAR>α : Type u_1<VAR>s : Set α<VAR>x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}<VAR>x y z : α<VAR>hxy : x ≠ y<VAR>hyz : x ≠ z<VAR>hxz : y ≠ z<VAR>hs : s = {x, y, z}<GOAL>s.encard = 3
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>eLpNormEssSup f μ * μ Set.univ ^ (1 / q) = eLpNormEssSup f μ
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<GOAL>re (x * (starRingEnd K) x) = ‖x * (starRingEnd K) x‖
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<GOAL>re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p < p.succAbove i ↔ p < i.succ