ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R M<VAR>w✝¹ : Submodule R N<VAR>hM : M' ≤ M₁<VAR>w✝ : w✝¹ ≤ N₁<VAR>hfin : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥w✝¹<VAR>h : s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion w✝)))<GOAL>∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R M<VAR>w✝¹ : Submodule R N<VAR>hM : M' ≤ M₁<VAR>w✝ : w✝¹ ≤ N₁<VAR>hfin : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥w✝¹<VAR>h : s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion w✝)))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R M<VAR>w✝¹ : Submodule R N<VAR>hM : M' ≤ M₁<VAR>w✝ : w✝¹ ≤ N₁<VAR>hfin : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥w✝¹<VAR>h : s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM) ∘ₗ LinearMap.lTensor (↥M') (inclusion w✝)))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>hp : Prime p<VAR>x✝ : Finite p a<GOAL>¬p ^ (0 + 1) ∣ a ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>hp : Prime p<VAR>k : ℕ<VAR>ha : Finite p a<GOAL>Finite p (a ^ (k + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>hp : Prime p<VAR>k : ℕ<VAR>ha : Finite p a<GOAL>Finite p (a * a ^ k)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : Mono 0<GOAL>IsZero X
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(volume (Icc a b)).toReal = ∏ i : ι, (b i - a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁✝ f₂✝ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f₁ f₂ : α → β<GOAL>EqOn f₁ f₂ univ ↔ f₁ = f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>p : PMF α<VAR>b✝ b : β<GOAL>b ∈ (map f p).support ↔ b ∈ f '' p.support
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocSemiring R✝<VAR>inst✝⁴ : NoZeroDivisors R✝<VAR>inst✝³ : Nontrivial R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<GOAL>CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocSemiring R✝<VAR>inst✝⁴ : NoZeroDivisors R✝<VAR>inst✝³ : Nontrivial R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>p : ℕ<VAR>hchar : CharP R p<GOAL>CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocSemiring R✝<VAR>inst✝⁴ : NoZeroDivisors R✝<VAR>inst✝³ : Nontrivial R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>p : ℕ<VAR>hchar : CharP R p<VAR>h : Nat.Prime p<GOAL>CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocSemiring R✝<VAR>inst✝⁴ : NoZeroDivisors R✝<VAR>inst✝³ : Nontrivial R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>hchar : CharP R 0<GOAL>CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>map f μ = 0 ↔ μ = 0
<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>η : P ⟶ Q<VAR>x✝ : Cᵒᵖ<GOAL>η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I => Q.map I.f.op) ⋯ ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤) = (Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I => P.map I.f.op) ⋯ ≫ colimit.ι (J.diagram P (unop x✝)) (op ⊤)) ≫ colimMap (J.diagramNatTrans η (unop x✝))
<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>η : P ⟶ Q<VAR>x✝ : Cᵒᵖ<GOAL>η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I => Q.map I.f.op) ⋯ ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤) = Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I => P.map I.f.op) ⋯ ≫ (J.diagramNatTrans η (unop x✝)).app (op ⊤) ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤)
<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>η : P ⟶ Q<VAR>x✝ : Cᵒᵖ<GOAL>(η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I => Q.map I.f.op) ⋯) ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤) = (Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I => P.map I.f.op) ⋯ ≫ (J.diagramNatTrans η (unop x✝)).app (op ⊤)) ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤)
<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>η : P ⟶ Q<VAR>x✝ : Cᵒᵖ<GOAL>η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I => Q.map I.f.op) ⋯ = Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I => P.map I.f.op) ⋯ ≫ (J.diagramNatTrans η (unop x✝)).app (op ⊤)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>motive : (⨂[R] (i : ι), s i) → Prop<VAR>z : ⨂[R] (i : ι), s i<VAR>smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r • (tprod R) f)<VAR>add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)<GOAL>motive z
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>motive : (⨂[R] (i : ι), s i) → Prop<VAR>z : ⨂[R] (i : ι), s i<VAR>add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)<VAR>smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R r f)<GOAL>motive z
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring A<VAR>a : A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module A M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : FaithfulSMul A M<VAR>p : R[X]<GOAL>p ∈ annihilator R[X] (AEval R M a) ↔ p ∈ RingHom.ker (aeval a)
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring A<VAR>a : A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module A M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : FaithfulSMul A M<VAR>p : R[X]<GOAL>(∀ (m : AEval R M a), p • m = 0) ↔ (aeval a) p = 0
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring A<VAR>a : A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module A M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : FaithfulSMul A M<VAR>p : R[X]<GOAL>(∀ (m : M), (aeval a) p • m = 0) ↔ (aeval a) p = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n < m<GOAL>1 / (↑m + 1) < 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n < m<GOAL>0 < ↑n + 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n < m<GOAL>↑n + 1 < ↑m + 1
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<GOAL>Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<GOAL>Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<VAR>H : ¬Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume<GOAL>False
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<GOAL>M ⊨ L.nonemptyTheory ↔ Nonempty M
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝³ : Fintype ι<VAR>inst✝² : MeasurableSpace E<VAR>μ : Measure E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>fundamentalDomain b =ᶠ[ae μ] parallelepiped ⇑b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>inst✝ : Fintype α<VAR>h : ∀ (a : α), (filter (fun x => a ∈ x) B).card ≤ n<GOAL>∑ s ∈ B, s.card = ∑ s ∈ B, (univ ∩ s).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a * mabs a = a⁺ᵐ ^ 2
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>α : ↥K<GOAL>lift (adjoin F {α}) = adjoin F {↑α}
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>A : WithSeminorms (schwartzSeminormFamily ℝ E F)<GOAL>WithSeminorms (schwartzSeminormFamily 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>A : nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0)<GOAL>nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily 𝕜 E F i)) (nhds 0)
<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>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>F.map (inv f) = inv (F.map 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>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<GOAL>(μ.prod ν).map Prod.swap = ν.prod μ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<GOAL>↑((μ.prod ν).map Prod.swap) = ↑(ν.prod μ)
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : StronglyMeasurable f<VAR>hfi : Integrable f μ<GOAL>μ[f|m] = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x y : α<VAR>S U Z : Set α<VAR>h : IsGenericPoint x S<VAR>hU : IsOpen U<GOAL>Disjoint S U ↔ x ∉ U
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : AddGroup A<VAR>s : Set G<VAR>N H : Subgroup G<VAR>inst✝ : N.Normal<GOAL>↑(N ⊔ H) = ↑N * ↑H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : One β<VAR>s : ι → Set α<VAR>hs : Antitone s<VAR>f : α → β<VAR>a : α<GOAL>(fun i => (s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋂ i, s i).mulIndicator f a
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : SeminormedRing 𝕜<VAR>inst✝⁴ : AddGroup E<VAR>inst✝³ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>c : 𝕜<VAR>x✝ y✝ : E<VAR>r✝ : ℝ<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : Seminorm 𝕜 E<VAR>x y : ℝ<GOAL>r • max x y = max (r • x) (r • y)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₃ : Type u_3<VAR>J : Type u_4<VAR>inst✝ : Zero I₂<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>i₁ : I₁<VAR>i₃ : I₃<GOAL>r (i₁, 0, i₃) = π (i₁, i₃)
<VAR>m n k : ℕ+<GOAL>k.Coprime n → (m * k).gcd n = m.gcd n
<VAR>m n k : ℕ+<GOAL>k.Coprime n → (k * m).gcd n = m.gcd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>f g : Filter α<GOAL>μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>f g : Filter α<GOAL>μ.FiniteAtFilter (f ⊓ ae μ) → μ.FiniteAtFilter f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t✝ : Set α<VAR>f g : Filter α<VAR>t : Set α<VAR>ht : t ∈ f<VAR>u : Set α<VAR>hu : u ∈ ae μ<VAR>hμ : μ (t ∩ u) < ⊤<GOAL>μ t ≤ μ (t ∩ u)
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p⁻¹ - 1 = -q⁻¹
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>ofReal |a| • Measure.map (fun x => x * a) volume = volume
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : r₂ ≤ 0<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : r₂ ≤ 0<VAR>h : r₁ ≤ r₂<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : r₂ ≤ 0<VAR>h : r₂ ≤ r₁<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>L : AddSubgroup E<VAR>inst✝² : DiscreteTopology ↥L<VAR>inst✝¹ : IsZlattice ℝ L<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝ : Measure.IsAddHaarMeasure μ<GOAL>covolume L μ ≠ 0
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>L : AddSubgroup E<VAR>inst✝² : DiscreteTopology ↥L<VAR>inst✝¹ : IsZlattice ℝ L<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝ : Measure.IsAddHaarMeasure μ<GOAL>μ (Zspan.fundamentalDomain (Basis.ofZlatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) ≠ 0 ∧ μ (Zspan.fundamentalDomain (Basis.ofZlatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) ≠ ⊤
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>L : AddSubgroup E<VAR>inst✝² : DiscreteTopology ↥L<VAR>inst✝¹ : IsZlattice ℝ L<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝ : Measure.IsAddHaarMeasure μ<GOAL>μ (Zspan.fundamentalDomain (Basis.ofZlatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) < ⊤
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : PosMulReflectLT α<VAR>h : 0 < a<GOAL>0 < a * b ↔ 0 < b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>x : M<VAR>hx : x ∉ p<VAR>hp' : Free R (M ⧸ p)<GOAL>∃ f, f x ≠ 0 ∧ map f p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>x : M<VAR>hx : x ∉ p<VAR>hp' : Free R (M ⧸ p)<GOAL>∃ f, f (p.mkQ x) ≠ 0
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>F G : W.Localization ⥤ D<VAR>τ₁ τ₂ : F ⟶ G<VAR>h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂<VAR>X : W.Localization<GOAL>τ₁.app X = τ₂.app X
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>F G : W.Localization ⥤ D<VAR>τ₁ τ₂ : F ⟶ G<VAR>h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂<VAR>X : W.Localization<VAR>eq : (objEquiv W).toFun ((objEquiv W).invFun X) = X<GOAL>τ₁.app X = τ₂.app X
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>F G : W.Localization ⥤ D<VAR>τ₁ τ₂ : F ⟶ G<VAR>h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂<VAR>X : W.Localization<VAR>eq : W.Q.obj X.as.obj = X<GOAL>τ₁.app X = τ₂.app X
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>j : J<VAR>r : R<GOAL>colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ (mkOfSMul (coconePointSMul F)).smul r = (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>j : J<VAR>r : R<GOAL>colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ (coconePointSMul F) r = (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>F.map f ≫ (fun j => homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j) ⋯) j = (fun j => homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j) ⋯) i ≫ ((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>(forget₂ (ModuleCat R) AddCommGrp).map (F.map f ≫ (fun j => homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j) ⋯) j) = (forget₂ (ModuleCat R) AddCommGrp).map ((fun j => homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j) ⋯) i ≫ ((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f)
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>(forget₂ (ModuleCat R) AddCommGrp).map (F.map f) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j = colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) i ≫ (forget₂ (ModuleCat R) AddCommGrp).map (((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f)
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>LinearMap.toAddMonoidHom (F.map f) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j = colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) i ≫ LinearMap.toAddMonoidHom (𝟙 (mkOfSMul (coconePointSMul F)))
<VAR>a b c d a' b' c' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<VAR>hc : c' ≤ c<GOAL>a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤ a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖