ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>inst✝³ : Functor F<VAR>inst✝² : Functor G<VAR>inst✝¹ : LawfulFunctor F<VAR>inst✝ : LawfulFunctor G<VAR>α β γ : Type v<VAR>g' : α → β<VAR>h : β → γ<VAR>x : F (G α)<GOAL>Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>t : R<GOAL>eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>hp : p ≠ 0<GOAL>eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>hp : p ≠ 0<VAR>mul_eq : (X - C t) ^ rootMultiplicity t p * (p /ₘ (X - C t) ^ rootMultiplicity t p) = p<GOAL>eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>hp : p ≠ 0<VAR>m : ℕ := rootMultiplicity t p<VAR>g : R[X] := p /ₘ (X - C t) ^ m<VAR>mul_eq : (X - C t) ^ m * g = p<GOAL>eval t g = (p.comp (X + C t)).trailingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>hp : p ≠ 0<VAR>m : ℕ := rootMultiplicity t p<VAR>g : R[X] := p /ₘ (X - C t) ^ m<VAR>mul_eq : (X - C t) ^ m * g = p<VAR>this : (g.comp (X + C t)).coeff 0 = eval t g<GOAL>eval t g = (p.comp (X + C t)).trailingCoeff
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : β → σ<VAR>m : β → ℕ<VAR>l : β → List β<VAR>g : β → List σ → Option σ<VAR>hm : Primrec m<VAR>hl : Primrec l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b<VAR>H : ∀ (b : β), g b (List.map f (l b)) = some (f b)<VAR>this : DecidableEq β<VAR>mapGraph : List (β × σ) → List β → List σ := fun M bs => bs.bind fun x => (List.lookup x M).toList<VAR>bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => bs.bind l) n<VAR>graph : β → ℕ → List (β × σ) := fun b i => Nat.rec [] (fun i ih => List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i))) i<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : β → σ<VAR>m : β → ℕ<VAR>l : β → List β<VAR>g : β → List σ → Option σ<VAR>hm : Primrec m<VAR>hl : Primrec l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b<VAR>H : ∀ (b : β), g b (List.map f (l b)) = some (f b)<VAR>this : DecidableEq β<VAR>mapGraph : List (β × σ) → List β → List σ := fun M bs => bs.bind fun x => (List.lookup x M).toList<VAR>bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => bs.bind l) n<VAR>graph : β → ℕ → List (β × σ) := fun b i => Nat.rec [] (fun i ih => List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i))) i<VAR>mapGraph_primrec : Primrec₂ mapGraph<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : β → σ<VAR>m : β → ℕ<VAR>l : β → List β<VAR>g : β → List σ → Option σ<VAR>hm : Primrec m<VAR>hl : Primrec l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b<VAR>H : ∀ (b : β), g b (List.map f (l b)) = some (f b)<VAR>this : DecidableEq β<VAR>mapGraph : List (β × σ) → List β → List σ := fun M bs => bs.bind fun x => (List.lookup x M).toList<VAR>bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => bs.bind l) n<VAR>graph : β → ℕ → List (β × σ) := fun b i => Nat.rec [] (fun i ih => List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i))) i<VAR>mapGraph_primrec : Primrec₂ mapGraph<VAR>bindList_primrec : Primrec₂ bindList<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : β → σ<VAR>m : β → ℕ<VAR>l : β → List β<VAR>g : β → List σ → Option σ<VAR>hm : Primrec m<VAR>hl : Primrec l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b<VAR>H : ∀ (b : β), g b (List.map f (l b)) = some (f b)<VAR>this : DecidableEq β<VAR>mapGraph : List (β × σ) → List β → List σ := fun M bs => bs.bind fun x => (List.lookup x M).toList<VAR>bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => bs.bind l) n<VAR>graph : β → ℕ → List (β × σ) := fun b i => Nat.rec [] (fun i ih => List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i))) i<VAR>mapGraph_primrec : Primrec₂ mapGraph<VAR>bindList_primrec : Primrec₂ bindList<VAR>graph_primrec : Primrec₂ graph<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : β → σ<VAR>m : β → ℕ<VAR>l : β → List β<VAR>g : β → List σ → Option σ<VAR>hm : Primrec m<VAR>hl : Primrec l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b<VAR>H : ∀ (b : β), g b (List.map f (l b)) = some (f b)<VAR>this✝ : DecidableEq β<VAR>mapGraph : List (β × σ) → List β → List σ := fun M bs => bs.bind fun x => (List.lookup x M).toList<VAR>bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => bs.bind l) n<VAR>graph : β → ℕ → List (β × σ) := fun b i => Nat.rec [] (fun i ih => List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i))) i<VAR>mapGraph_primrec : Primrec₂ mapGraph<VAR>bindList_primrec : Primrec₂ bindList<VAR>graph_primrec : Primrec₂ graph<VAR>this : Primrec fun b => Option.map Prod.snd ((graph b (m b + 1)).get? 0)<GOAL>Primrec f
<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>s : σ →₀ ℕ<VAR>a : R<VAR>ha : a ≠ 0<GOAL>((monomial s) a).degrees = toMultiset s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>U : WSeq α → WSeq β → Prop<VAR>ST : LiftRel (LiftRel R) S T<VAR>HU : ∀ (s1 : WSeq α) (s2 : WSeq β), (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2<VAR>a : Option (α × WSeq α)<VAR>ma : a ∈ S.join.destruct<GOAL>∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>U : WSeq α → WSeq β → Prop<VAR>ST : LiftRel (LiftRel R) S T<VAR>HU : ∀ (s1 : WSeq α) (s2 : WSeq β), (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2<VAR>a : Option (α × WSeq α)<VAR>ma : a ∈ S.join.destruct<VAR>n : ℕ<VAR>h : S.join.destruct.Results a n<GOAL>∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>U : WSeq α → WSeq β → Prop<VAR>HU : ∀ (s1 : WSeq α) (s2 : WSeq β), (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2<VAR>n : ℕ<VAR>IH : ∀ (m : ℕ), m < n → ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)}, LiftRel (LiftRel R) S T → ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>ST : LiftRel (LiftRel R) S T<VAR>a : Option (α × WSeq α)<VAR>ra : S.join.destruct.Results a n<GOAL>∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>U : WSeq α → WSeq β → Prop<VAR>HU : ∀ (s1 : WSeq α) (s2 : WSeq β), (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2<VAR>n : ℕ<VAR>IH : ∀ (m : ℕ), m < n → ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)}, LiftRel (LiftRel R) S T → ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>ST : LiftRel (LiftRel R) S T<VAR>a : Option (α × WSeq α)<VAR>ra : (S.destruct.bind destruct_join.aux).Results a n<GOAL>∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q.IsOrtho 0 x
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>a b : ℝ<VAR>n : ℕ<VAR>H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n := fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)<GOAL>∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q : R[X]<VAR>a b : R<VAR>p : R[X]<GOAL>a - b ∣ eval a p - eval b p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q : R[X]<VAR>a b : R<VAR>p : R[X]<GOAL>X - C b ∣ p - C (eval b p)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.199564, u_1} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝³ : HasKernels C<VAR>inst✝² : HasCokernels C<VAR>inst✝¹ : HasKernels Cᵒᵖ<VAR>inst✝ : HasCokernels Cᵒᵖ<GOAL>∀ {X Y : (ShortComplex C)ᵒᵖ} (f : X ⟶ Y), (rightHomologyFunctor C).op.map f ≫ ((fun S => (Opposite.unop S).leftHomologyOpIso.symm) Y).hom = ((fun S => (Opposite.unop S).leftHomologyOpIso.symm) X).hom ≫ (opFunctor C ⋙ leftHomologyFunctor Cᵒᵖ).map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>hf : Measurable f<VAR>a : α<VAR>g' : γ → ℝ≥0∞<VAR>hg : Measurable g'<GOAL>∫⁻ (b : γ), g' b ∂(κ.map f hf) a = ∫⁻ (a : β), g' (f a) ∂κ a
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : OplaxNatTrans F G<VAR>θ : OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : G.obj c ⟶ a'<GOAL>η.naturality (f ≫ g) ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ G.mapComp f g ▷ h = F.mapComp f g ▷ η.app c ▷ h ≫ (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫ (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫ F.map f ◁ η.naturality g ▷ h ≫ (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫ (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫ η.naturality f ▷ G.map g ▷ h ≫ (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : OplaxNatTrans F G<VAR>θ : OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : G.obj c ⟶ a'<GOAL>(F.mapComp f g ▷ η.app c ≫ (α_ (F.map f) (F.map g) (η.app c)).hom ≫ F.map f ◁ η.naturality g ≫ (α_ (F.map f) (η.app b) (G.map g)).inv ≫ η.naturality f ▷ G.map g ≫ (α_ (η.app a) (G.map f) (G.map g)).hom) ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom = F.mapComp f g ▷ η.app c ▷ h ≫ (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫ (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫ F.map f ◁ η.naturality g ▷ h ≫ (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫ (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫ η.naturality f ▷ G.map g ▷ h ≫ (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>m : ↥M<GOAL>M.rTensorOne' (m ⊗ₜ[R] 1) = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : IsSimpleOrder α<VAR>inst✝ : DecidableEq α<GOAL>Finset.map { toFun := ⇑IsSimpleOrder.equivBool.symm, inj' := ⋯ } Finset.univ = {⊤, ⊥}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : IsSimpleOrder α<VAR>inst✝ : DecidableEq α<GOAL>Finset.map { toFun := ⇑IsSimpleOrder.equivBool.symm, inj' := ⋯ } {true, false} = {⊤, ⊥}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : IsSimpleOrder α<VAR>inst✝ : DecidableEq α<GOAL>{IsSimpleOrder.equivBool.symm true, IsSimpleOrder.equivBool.symm false} = {⊤, ⊥}
<VAR>x y : ℂ<GOAL>cos (x + y) = cos x * cos y - sin x * sin y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>Ι a b = Ioc a b ∪ Ioc b a
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S T : Subgroupoid C<GOAL>S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S T : Subgroupoid C<GOAL>(∀ (a : C) (b : (d : C) × (a ⟶ d)), ⟨a, b⟩ ∈ S → ⟨a, b⟩ ∈ T) ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
<VAR>a b c d x y z w : ℕ<GOAL>(↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 + (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 + (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
<VAR>a b c d x y z w : ℕ<GOAL>↑((↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 + (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 + (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2) = ↑((a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2))
<VAR>a b c d x y z w : ℕ<GOAL>|↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w| ^ 2 + |↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z| ^ 2 + |↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y| ^ 2 + |↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x| ^ 2 = (↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2) * (↑x ^ 2 + ↑y ^ 2 + ↑z ^ 2 + ↑w ^ 2)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<VAR>hI : I ≤ 1<GOAL>I * I ≤ I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<VAR>hI : I ≤ 1<GOAL>I = (fun x => I * x) 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.plusObj P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toPlus P ≫ η = J.toPlus P ≫ γ<GOAL>η = γ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.plusObj P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toPlus P ≫ η = J.toPlus P ≫ γ<VAR>this : γ = J.plusLift (J.toPlus P ≫ γ) hQ<GOAL>η = γ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.plusObj P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toPlus P ≫ η = J.toPlus P ≫ γ<VAR>this : γ = J.plusLift (J.toPlus P ≫ γ) hQ<GOAL>η = J.plusLift (J.toPlus P ≫ γ) hQ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.plusObj P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toPlus P ≫ η = J.toPlus P ≫ γ<VAR>this : γ = J.plusLift (J.toPlus P ≫ γ) hQ<GOAL>J.toPlus P ≫ η = J.toPlus P ≫ γ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<GOAL>orderOf χ ∣ Fintype.card F - 1
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : Prepartition I<GOAL>∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : Prepartition I<VAR>this : ∀ (J : Box ι), ∃ π, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧ (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧ π.distortion = J.distortion<GOAL>∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>πip : ∀ (J : Box ι), (πi J).IsPartition<VAR>πiH : ∀ (J : Box ι), (πi J).IsHenstock<VAR>πir : ∀ (J : Box ι), (πi J).IsSubordinate r<VAR>h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m<VAR>πid : ∀ (J : Box ι), (πi J).distortion = J.distortion<GOAL>∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>πip : ∀ (J : Box ι), (πi J).IsPartition<VAR>πiH : ∀ (J : Box ι), (πi J).IsHenstock<VAR>πir : ∀ (J : Box ι), (πi J).IsSubordinate r<VAR>h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m<VAR>πid : ∀ (J : Box ι), (πi J).distortion = J.distortion<GOAL>(π.biUnionTagged πi).distortion = π.distortion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>πip : ∀ (J : Box ι), (πi J).IsPartition<VAR>πiH : ∀ (J : Box ι), (πi J).IsHenstock<VAR>πir : ∀ (J : Box ι), (πi J).IsSubordinate r<VAR>h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m<VAR>πid : ∀ (J : Box ι), (πi J).distortion = J.distortion<GOAL>(π.boxes.sup fun J => (πi J).distortion) = π.distortion
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : MetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : MetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C(X, ℝ≥0)<VAR>hδ0 : ∀ (x : X), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : MetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C(X, ℝ≥0)<VAR>hδ0 : ∀ (x : X), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i<VAR>i : ι<VAR>x : X<VAR>hx : x ∈ K i<GOAL>closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : MetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C(X, ℝ≥0)<VAR>hδ0 : ∀ (x : X), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i<VAR>i : ι<VAR>x : X<VAR>hx : x ∈ K i<GOAL>EMetric.closedBall x ↑(δ x) ⊆ U i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (cocompact ℝ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>DiscreteTopology ↥((zmultiplesHom ℝ) a).range
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>DiscreteTopology ↥(AddSubgroup.zmultiples a)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>h1 : 1 ∈ S<VAR>hg : g ∈ T<VAR>this : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g<GOAL>(hST.equiv g).2 = ⟨g, hg⟩
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x✝ y✝ : M<VAR>f✝ : M →* P<VAR>f : c.Quotient →* P<VAR>x y : M<VAR>h : c x y<GOAL>f ↑x = f ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<GOAL>(map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<GOAL>∑ x ∈ Finset.image g f.range, x * μ (↑(map g f) ⁻¹' {x}) = ∑ x ∈ f.range, g x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<VAR>b : β<VAR>hb : b ∈ f.range<GOAL>g b * μ (↑(map g f) ⁻¹' {g b}) = ∑ x ∈ Finset.filter (fun c' => g c' = g b) f.range, g x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<VAR>a : α<VAR>hb : ↑f a ∈ f.range<GOAL>g (↑f a) * μ (↑(map g f) ⁻¹' {g (↑f a)}) = ∑ x ∈ Finset.filter (fun c' => g c' = g (↑f a)) f.range, g x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<VAR>a : α<VAR>hb : ↑f a ∈ f.range<GOAL>∑ i ∈ Finset.filter (fun b => g b = g (↑f a)) f.range, g (↑f a) * μ (↑f ⁻¹' {i}) = ∑ x ∈ Finset.filter (fun c' => g c' = g (↑f a)) f.range, g x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<VAR>a : α<VAR>hb : ↑f a ∈ f.range<GOAL>Finset.filter (fun b => g b = g (↑f a)) f.range = Finset.filter (fun c' => g c' = g (↑f a)) f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>g : β → ℝ≥0∞<VAR>f : α →ₛ β<VAR>a : α<VAR>hb : ↑f a ∈ f.range<GOAL>∀ x ∈ Finset.filter (fun c' => g c' = g (↑f a)) f.range, g (↑f a) * μ (↑f ⁻¹' {x}) = g x * μ (↑f ⁻¹' {x})
<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>m : M<VAR>p : Subsemigroup M<GOAL>closure {m} ≤ p ↔ m ∈ p
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)