ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<GOAL>(s.support.biUnion fun a => {f a}) ⊆ image f s.support
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n m : ℕ<GOAL>m.succ + n - 1 = m + n
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<GOAL>(map f l).tail = map f l.tail
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<GOAL>(map f (cons l.head l.tail)).tail = map f l.tail
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>w : Word M<GOAL>(equivPair i) (of m • w) = { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>w : Word M<GOAL>(equivPair i) ((equivPair i).symm (let __src := (equivPair i) w; { head := m * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })) = { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }
<VAR>α✝ : Type u_1<VAR>l l₁ l₂ : List α✝<GOAL>(l₁ ++ l₂).Disjoint l ↔ l.Disjoint l₁ ∧ l.Disjoint l₂
<VAR>α✝ : Type u_1<VAR>l l₁ l₂ : List α✝<GOAL>l₁.Disjoint l ∧ l₂.Disjoint l ↔ l.Disjoint l₁ ∧ l.Disjoint l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>c : β<VAR>hf : f ≤ᶠ[ae μ] fun x => c<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q : Karoubi C<VAR>f : P.Hom Q<GOAL>f.f ≫ Q.p = f.f
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>h : IsUnit a<GOAL>a * ↑h.unit⁻¹ = 1
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>h : IsUnit a<GOAL>a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹
<VAR>Z : Type u_1<VAR>N : Type u_2<VAR>R : Type u_3<VAR>inst✝ : PseudoMetricSpace R<VAR>d : N → ℝ<VAR>j : Z → N → R<VAR>f : R → R<VAR>α : R<VAR>ε M : ℝ<VAR>d0 : ∀ (a : N), 1 ≤ d a<VAR>e0 : 0 < ε<VAR>B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M<VAR>L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))<GOAL>∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
<VAR>Z : Type u_1<VAR>N : Type u_2<VAR>R : Type u_3<VAR>inst✝ : PseudoMetricSpace R<VAR>d : N → ℝ<VAR>j : Z → N → R<VAR>f : R → R<VAR>α : R<VAR>ε M : ℝ<VAR>d0 : ∀ (a : N), 1 ≤ d a<VAR>e0 : 0 < ε<VAR>B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M<VAR>L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))<VAR>me0 : 0 < max (1 / ε) M<GOAL>∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R₂ M₂<VAR>hp : ⨆ i ∈ s, p i = ⊤<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : Surjective ⇑f<VAR>k : ι<VAR>hk : k ∈ s<GOAL>⨆ i ∈ s, comap f (p i) = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R₂ M₂<VAR>hp : ⨆ i ∈ s, p i = ⊤<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : Surjective ⇑f<VAR>k : ι<VAR>hk : k ∈ s<GOAL>(⨆ i ∈ s, comap f (p i)) ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R₂ M₂<VAR>hp : ⨆ x, p ↑x = ⊤<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : Surjective ⇑f<VAR>k : ι<VAR>hk : k ∈ s<GOAL>(⨆ x, comap f (p ↑x)) ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<VAR>x : S<VAR>hx : B.gen ∈ adjoin R {x}<GOAL>adjoin R {x} = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<VAR>x : S<VAR>hx : B.gen ∈ adjoin R {x}<GOAL>adjoin R {B.gen} ≤ adjoin R {x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<VAR>x : S<VAR>hx : B.gen ∈ adjoin R {x}<GOAL>{B.gen} ⊆ ↑(adjoin R {x})
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>A : (i : ι) → Finset (α i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>h : ∑ i : ι, (A i).card = n<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<VAR>B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})<VAR>C : (a : ι) → Finset (α a) := update A i₀ {j₂}<VAR>B_subset_A : ∀ (i : ι), B i ⊆ A i<VAR>C_subset_A : ∀ (i : ι), C i ⊆ A i<VAR>A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)<VAR>Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j<VAR>Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<VAR>B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})<VAR>C : (a : ι) → Finset (α a) := update A i₀ {j₂}<VAR>B_subset_A : ∀ (i : ι), B i ⊆ A i<VAR>C_subset_A : ∀ (i : ι), C i ⊆ A i<VAR>A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)<VAR>Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j<VAR>Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j<VAR>Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<VAR>B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})<VAR>C : (a : ι) → Finset (α a) := update A i₀ {j₂}<VAR>B_subset_A : ∀ (i : ι), B i ⊆ A i<VAR>C_subset_A : ∀ (i : ι), C i ⊆ A i<VAR>A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)<VAR>Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j<VAR>Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j<VAR>Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)<VAR>Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i)<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<VAR>B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})<VAR>C : (a : ι) → Finset (α a) := update A i₀ {j₂}<VAR>B_subset_A : ∀ (i : ι), B i ⊆ A i<VAR>C_subset_A : ∀ (i : ι), C i ⊆ A i<VAR>A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)<VAR>Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j<VAR>Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j<VAR>Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)<VAR>Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i)<VAR>D : Disjoint (piFinset B) (piFinset C)<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<VAR>B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})<VAR>C : (a : ι) → Finset (α a) := update A i₀ {j₂}<VAR>B_subset_A : ∀ (i : ι), B i ⊆ A i<VAR>C_subset_A : ∀ (i : ι), C i ⊆ A i<VAR>A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)<VAR>Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j<VAR>Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j<VAR>Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)<VAR>Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i)<VAR>D : Disjoint (piFinset B) (piFinset C)<VAR>pi_BC : piFinset A = piFinset B ∪ piFinset C<GOAL>f (update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)) = ∑ r ∈ piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)<VAR>n : ℕ<VAR>IH : ∀ m < n, ∀ (A : (i : ι) → Finset (α i)), ∑ i : ι, (A i).card = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)<VAR>A : (i : ι) → Finset (α i)<VAR>h : ∑ i : ι, (A i).card = n<VAR>Ai_empty : ∀ (i : ι), A i ≠ ∅<VAR>i₀ : ι<VAR>hi₀ : 1 < (A i₀).card<VAR>j₁ j₂ : α i₀<VAR>left✝ : j₁ ∈ A i₀<VAR>hj₂ : j₂ ∈ A i₀<VAR>right✝ : j₁ ≠ j₂<VAR>B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})<VAR>C : (a : ι) → Finset (α a) := update A i₀ {j₂}<VAR>B_subset_A : ∀ (i : ι), B i ⊆ A i<VAR>C_subset_A : ∀ (i : ι), C i ⊆ A i<VAR>A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)<VAR>Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j<VAR>Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j<VAR>Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)<VAR>Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i)<VAR>D : Disjoint (piFinset B) (piFinset C)<VAR>pi_BC : piFinset A = piFinset B ∪ piFinset C<GOAL>((∑ r ∈ piFinset B, f fun i => g i (r i)) + ∑ r ∈ piFinset C, f fun i => g i (r i)) = ∑ r ∈ piFinset B ∪ piFinset C, f fun i => g i (r i)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ✝ ℱ : Filtration ι m0<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>x : E<VAR>i j : ι<VAR>x✝ : i ≤ j<GOAL>μ[(fun x_1 x_2 => x) j|↑ℱ i] =ᶠ[ae μ] (fun x_1 x_2 => x) i
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝¹⁴ : LinearOrderedField R<VAR>inst✝¹³ : LinearOrderedField R'<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup F<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup α<VAR>inst✝⁹ : Module R E<VAR>inst✝⁸ : Module R F<VAR>inst✝⁷ : Module R α<VAR>inst✝⁶ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c✝ : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>c : R'<VAR>inst✝⁵ : Module R' R<VAR>inst✝⁴ : Module R' E<VAR>inst✝³ : SMulCommClass R' R R<VAR>inst✝² : IsScalarTower R' R R<VAR>inst✝¹ : SMulCommClass R R' E<VAR>inst✝ : IsScalarTower R' R E<VAR>hc : c ≠ 0<GOAL>t.centerMass (c • w) z = t.centerMass w z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>p q : α → Prop<VAR>x : α<GOAL>{x | x ∈ s ∧ p x} = ∅ ↔ ∀ x ∈ s, ¬p x
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>μs_lim : Tendsto μs ⊥ (𝓝 μ)<GOAL>limsup (fun i => ↑(μs i) F) ⊥ ≤ ↑μ F