ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<GOAL>L.ElementarilyEquivalent M N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T : L.Theory<VAR>self : M ⊨ T<VAR>φ : L.Sentence<GOAL>φ ∈ T → M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T : L.Theory<GOAL>M ⊨ T ↔ ∀ φ ∈ T, M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T : L.Theory<VAR>M ⊨ T<VAR>φ : L.Sentence<VAR>h : φ ∈ T<GOAL>M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>T : L.Theory<GOAL>M ⊨ φ.onTheory T ↔ M ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T T' : L.Theory<VAR>_h : M ⊨ T'<VAR>hs : T ⊆ T'<GOAL>M ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T T' : L.Theory<VAR>h : M ⊨ T<VAR>h' : M ⊨ T'<GOAL>M ⊨ T ∪ T'
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T T' : L.Theory<GOAL>M ⊨ T ∪ T' ↔ M ⊨ T ∧ M ⊨ T'
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>φ : L.Sentence<GOAL>M ⊨ {φ} ↔ M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T : L.Theory<GOAL>M ⊨ T ↔ T ⊆ L.completeTheory M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>T : L.Theory<VAR>MT : M ⊨ T<GOAL>T ⊆ L.completeTheory M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>N ⊨ L.completeTheory M<VAR>φ : L.Sentence<GOAL>N ⊨ φ ↔ M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<GOAL>φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<GOAL>φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<GOAL>(FirstOrder.Language.Formula.iAlls f φ).Realize v ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iAlls f φ) v v' ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<GOAL>(FirstOrder.Language.Formula.iExs f φ).Realize v ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iExs f φ) v v' ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α ⊕ Fin n → M<GOAL>φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>s : Finset β<VAR>f : β → L.BoundedFormula α n<VAR>v : α → M<VAR>v' : Fin n → M<GOAL>(FirstOrder.Language.BoundedFormula.iSup s f).Realize v v' ↔ ∃ b ∈ s, (f b).Realize v v'
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>s : Finset β<VAR>f : β → L.BoundedFormula α n<VAR>v : α → M<VAR>v' : Fin n → M<GOAL>(FirstOrder.Language.BoundedFormula.iInf s f).Realize v v' ↔ ∀ b ∈ s, (f b).Realize v v'
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>α : Type u'<VAR>n : ℕ<VAR>g : L.Equiv M N<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>φ.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>α : Type u'<VAR>g : L.Equiv M N<VAR>φ : L.Formula α<VAR>v : α → M<GOAL>φ.Realize (⇑g ∘ v) ↔ φ.Realize v
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>g : L.Equiv M N<VAR>φ : L.Sentence<GOAL>M ⊨ φ ↔ N ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>T : L.Theory<VAR>g : L.Equiv M N<VAR>M ⊨ T<GOAL>N ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>g : L.Equiv M N<GOAL>L.ElementarilyEquivalent M N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>r : L.Relations 2<GOAL>M ⊨ r.reflexive ↔ Reflexive fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>r : L.Relations 2<GOAL>M ⊨ r.irreflexive ↔ Irreflexive fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>r : L.Relations 2<GOAL>M ⊨ r.symmetric ↔ Symmetric fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>r : L.Relations 2<GOAL>M ⊨ r.antisymmetric ↔ AntiSymmetric fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>r : L.Relations 2<GOAL>M ⊨ r.transitive ↔ Transitive fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>r : L.Relations 2<GOAL>M ⊨ r.total ↔ Total fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<GOAL>M ⊨ FirstOrder.Language.Sentence.cardGe L n ↔ ↑n ≤ Cardinal.mk M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>M ⊨ L.infiniteTheory ↔ Infinite M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>M ⊨ L.nonemptyTheory ↔ Nonempty M
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>M : Type w<VAR>(L.withConstants α).Structure M<VAR>s : Set α<GOAL>M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i => ↑(L.con i)) s
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>s : Set α<VAR>M : Type w<VAR>(L.withConstants α).Structure M<VAR>h : M ⊨ L.distinctConstantsTheory s<GOAL>Cardinal.lift.{w, u'} (Cardinal.mk ↑s) ≤ Cardinal.lift.{u', w} (Cardinal.mk M)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>h : L.ElementarilyEquivalent M N<GOAL>L.ElementarilyEquivalent N M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>MN : L.ElementarilyEquivalent M N<VAR>NP : L.ElementarilyEquivalent N P<GOAL>L.ElementarilyEquivalent M P
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>h : L.ElementarilyEquivalent M N<GOAL>L.completeTheory M = L.completeTheory N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>h : L.ElementarilyEquivalent M N<VAR>φ : L.Sentence<GOAL>M ⊨ φ ↔ N ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>T : L.Theory<VAR>h : L.ElementarilyEquivalent M N<GOAL>M ⊨ T ↔ N ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>T : L.Theory<VAR>MT : M ⊨ T<VAR>h : L.ElementarilyEquivalent M N<GOAL>N ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>h : L.ElementarilyEquivalent M N<GOAL>Nonempty M ↔ Nonempty N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>Mn : Nonempty M<VAR>h : L.ElementarilyEquivalent M N<GOAL>Nonempty N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>h : L.ElementarilyEquivalent M N<GOAL>Infinite M ↔ Infinite N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>Mi : Infinite M<VAR>h : L.ElementarilyEquivalent M N<GOAL>Infinite N
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable (∫⋯∫⁻_s, f ∂μ)
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>DecidableEq δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<GOAL>∫⋯∫⁻_∅, f ∂μ = f
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>x y : (i : δ) → π i<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>h : ∀ i ∉ s, x i = y i<GOAL>(∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>i : δ<VAR>hi : i ∈ s<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<VAR>y : π i<GOAL>(∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∂μ) x
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s t : Finset δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hst : Disjoint s t<GOAL>∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>s t : Finset δ<VAR>hst : Disjoint s t<GOAL>∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>DecidableEq δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>i : δ<GOAL>∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ) ∂μ i
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∉ s<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s, f ∂μ) (Function.update x i xᵢ) ∂μ i
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∈ s<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s.erase i, f ∂μ) (Function.update x i xᵢ) ∂μ i
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∉ s<GOAL>∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, fun x => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ) ∂μ i ∂μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∈ s<GOAL>∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ) ∂μ i ∂μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hfg : f ≤ g<GOAL>∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>Fintype δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<GOAL>∫⋯∫⁻_Finset.univ, f ∂μ = fun x => ∫⁻ (x : (i : δ) → π i), f x ∂MeasureTheory.Measure.pi μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>Fintype δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂MeasureTheory.Measure.pi μ = (∫⋯∫⁻_Finset.univ, f ∂μ) x
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>DecidableEq δ'<VAR>e : δ' → δ<VAR>he : Function.Injective e<VAR>s : Finset δ'<VAR>f : ((i : δ') → π (e i)) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_Finset.image e s, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x = (∫⋯∫⁻_s, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hi : i ∉ s<VAR>x : (i : δ) → π i<VAR>y : π i<GOAL>(∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∘ fun x => Function.update x i y ∂μ) x
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s t : Finset δ<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_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>s t : Finset δ<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_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂MeasureTheory.Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂MeasureTheory.Measure.pi μ
<VAR>δ : Type u_1<VAR>π : δ → Type u_3<VAR>(x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → MeasureTheory.Measure (π i)<VAR>∀ (i : δ), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq δ<VAR>Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂MeasureTheory.Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂MeasureTheory.Measure.pi μ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : List (L.Term α)<GOAL>FirstOrder.Language.Term.listDecode (l.bind FirstOrder.Language.Term.listEncode) = l
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>FirstOrder.Language.Term.encoding.Γ = (α ⊕ (i : ℕ) × L.Functions i)
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>∀ (a : L.Term α), FirstOrder.Language.Term.encoding.encode a = a.listEncode
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : List (α ⊕ (i : ℕ) × L.Functions i)<GOAL>FirstOrder.Language.Term.encoding.decode l = (do let a ← (FirstOrder.Language.Term.listDecode l).head? pure (some a)).join
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Function.Injective FirstOrder.Language.Term.listEncode
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Cardinal.mk (L.Term α) ≤ max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × L.Functions i))
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Cardinal.mk ((n : ℕ) × L.Term (α ⊕ Fin n)) = max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × L.Functions i))
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α (n + 1)<GOAL>FirstOrder.Language.BoundedFormula.sigmaAll ⟨n + 1, φ⟩ = ⟨n, φ.all⟩
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>FirstOrder.Language.BoundedFormula.sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ.imp ψ⟩
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : List ((n : ℕ) × L.BoundedFormula α n)<GOAL>FirstOrder.Language.BoundedFormula.listDecode (l.bind fun φ => φ.snd.listEncode) = l
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>FirstOrder.Language.BoundedFormula.encoding.Γ = ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)<GOAL>FirstOrder.Language.BoundedFormula.encoding.decode l = (FirstOrder.Language.BoundedFormula.listDecode l)[0]?
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>φ : (n : ℕ) × L.BoundedFormula α n<GOAL>FirstOrder.Language.BoundedFormula.encoding.encode φ = φ.snd.listEncode
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Function.Injective fun φ => φ.snd.listEncode
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>Cardinal.mk ((n : ℕ) × L.BoundedFormula α n) ≤ max Cardinal.aleph0 (Cardinal.lift.{max u v, u'} (Cardinal.mk α) + Cardinal.lift.{u', max u v} L.card)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module k V<VAR>ρ : G →* V →ₗ[k] V<GOAL>CoeSort.coe (Rep.of ρ) = V
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module k V<VAR>ρ : G →* V →ₗ[k] V<GOAL>(Rep.of ρ).ρ = ρ
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<GOAL>A.ρ = A.ρ
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : ↑(MonCat.of G)<GOAL>(Rep.of ρ).ρ g = ρ g
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>A : Rep k G<VAR>g : G<VAR>x : CoeSort.coe A<GOAL>(A.ρ g⁻¹) ((A.ρ g) x) = x
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>A : Rep k G<VAR>g : G<VAR>x : CoeSort.coe A<GOAL>(A.ρ g) ((A.ρ g⁻¹) x) = x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A B : Rep k G<VAR>f : A ⟶ B<VAR>g : G<VAR>x : CoeSort.coe A<GOAL>f.hom ((A.ρ g) x) = (B.ρ g) (f.hom x)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module k V<VAR>g : G<VAR>v : V<GOAL>((Rep.trivial k G V).ρ g) v = v
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A B : Rep k G<VAR>x : CoeSort.coe A<VAR>y : CoeSort.coe B<GOAL>(β_ A B).hom.hom (x ⊗ₜ[k] y) = y ⊗ₜ[k] x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A B : Rep k G<VAR>x : CoeSort.coe A<VAR>y : CoeSort.coe B<GOAL>(β_ A B).inv.hom (y ⊗ₜ[k] x) = x ⊗ₜ[k] y
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<VAR>x : X.V →₀ k<GOAL>(((Rep.linearization k G).obj X).ρ g) x = (Finsupp.lmapDomain k k (X.ρ g)) x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<VAR>x : X.V<GOAL>(((Rep.linearization k G).obj X).ρ g) (Finsupp.single x 1) = Finsupp.single (X.ρ g x) 1
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<VAR>x : X.V<VAR>r : k<GOAL>(((Rep.linearization k G).obj X).ρ g) (Finsupp.single x r) = Finsupp.single (X.ρ g x) r
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<GOAL>((Rep.linearization k G).map f).hom = Finsupp.lmapDomain k k f.hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>x : X.V<VAR>r : k<GOAL>((Rep.linearization k G).map f).hom (Finsupp.single x r) = Finsupp.single (f.hom x) r
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<GOAL>((Rep.linearization k G).μ X Y).hom = ↑(finsuppTensorFinsupp' k X.V Y.V)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<GOAL>(CategoryTheory.inv ((Rep.linearization k G).μ X Y)).hom = ↑(finsuppTensorFinsupp' k X.V Y.V).symm
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<GOAL>(Rep.linearization k G).ε.hom = Finsupp.lsingle PUnit.unit
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>r : k<GOAL>(CategoryTheory.inv (Rep.linearization k G).ε).hom (Finsupp.single PUnit.unit r) = r
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X : Type u<VAR>a : ↑((Rep.linearization k G).obj { V := X, ρ := 1 }).V<GOAL>(Rep.linearizationTrivialIso k G X).hom.hom a = a
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>X : Type u<VAR>a : ↑((Rep.linearization k G).obj { V := X, ρ := 1 }).V<GOAL>(Rep.linearizationTrivialIso k G X).inv.hom a = a
<VAR>k G A : Type u<VAR>CommRing k<VAR>Monoid G<VAR>AddCommGroup A<VAR>Module k A<VAR>DistribMulAction G A<VAR>SMulCommClass G k A<VAR>g : G<VAR>a : A<GOAL>((Rep.ofDistribMulAction k G A).ρ g) a = g • a
<VAR>M G : Type<VAR>Monoid M<VAR>CommGroup G<VAR>MulDistribMulAction M G<VAR>g : M<VAR>a : Additive G<GOAL>((Rep.ofMulDistribMulAction M G).ρ g) a = Additive.ofMul (g • Additive.toMul a)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>(A.leftRegularHom x).hom = (Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>(A.leftRegularHom x).hom (Finsupp.single 1 1) = x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<VAR>f : Rep.ofMulAction k G G ⟶ A<GOAL>A.leftRegularHomEquiv f = f.hom (Finsupp.single 1 1)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>A.leftRegularHomEquiv.symm x = A.leftRegularHom x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : G<GOAL>(A.leftRegularHomEquiv.symm x).hom (Finsupp.single g 1) = (A.ρ g) x
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B : Rep k G<GOAL>A.ihom.obj B = Rep.of (A.ρ.linHom B.ρ)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>X Y : Rep k G<VAR>f : X ⟶ Y<GOAL>(A.ihom.map f).hom = ModuleCat.ofHom ((LinearMap.llcomp k (CoeSort.coe A) (CoeSort.coe X) (CoeSort.coe Y)) f.hom)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B : Rep k G<VAR>g : G<VAR>x : CoeSort.coe A →ₗ[k] CoeSort.coe B<GOAL>((A.ihom.obj B).ρ g) x = B.ρ g ∘ₗ x ∘ₗ A.ρ g⁻¹
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C<GOAL>((A.homEquiv B C) f).hom = (TensorProduct.curry f.hom).flip
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<VAR>f : B ⟶ A.ihom.obj C<GOAL>((A.homEquiv B C).symm f).hom = (TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) (LinearMap.flip f.hom)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B : Rep k G<GOAL>((CategoryTheory.ihom A).obj B).ρ = (A.ihom.obj B).ρ
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<GOAL>(CategoryTheory.ihom.adjunction A).homEquiv B C = A.homEquiv B C
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B : Rep k G<GOAL>((CategoryTheory.ihom.ev A).app B).hom = (TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe A →ₗ[k] CoeSort.coe B) (CoeSort.coe B)) LinearMap.id.flip
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B : Rep k G<GOAL>((CategoryTheory.ihom.coev A).app B).hom = (TensorProduct.mk k (CoeSort.coe A) ↑((𝟭 (Rep k G)).obj B).V).flip
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C<GOAL>((Rep.MonoidalClosed.linearHomEquiv A B C) f).hom = (TensorProduct.curry f.hom).flip
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C<GOAL>((Rep.MonoidalClosed.linearHomEquivComm A B C) f).hom = TensorProduct.curry f.hom