ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → AddGroup (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.single i (x - y) = Pi.single i x - Pi.single i y
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → AddZeroClass (f i)<GOAL>Pairwise fun i j => ∀ (x : f i) (y : f j), AddCommute (Pi.single i x) (Pi.single j y)
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → MulOneClass (f i)<GOAL>Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (Pi.mulSingle i x) (Pi.mulSingle j y)
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → MulOneClass (f i)<VAR>x : (i : I) → f i<VAR>i j : I<GOAL>Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → AddZeroClass (f i)<VAR>x : (i : I) → f i<VAR>i j : I<GOAL>AddCommute (Pi.single i (x i)) (Pi.single j (x j))
<VAR>I : Type u<VAR>f : I → Type v<VAR>i : I<VAR>DecidableEq I<VAR>(i : I) → AddGroup (f i)<VAR>g : (i : I) → f i<VAR>x : f i<GOAL>Function.update g i x = g - Pi.single i (g i) + Pi.single i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>i : I<VAR>DecidableEq I<VAR>(i : I) → Group (f i)<VAR>g : (i : I) → f i<VAR>x : f i<GOAL>Function.update g i x = g / Pi.mulSingle i (g i) * Pi.mulSingle i x
<VAR>I : Type u<VAR>DecidableEq I<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>k l m n : I<VAR>u v : M<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
<VAR>I : Type u<VAR>DecidableEq I<VAR>M : Type u_3<VAR>CommMonoid M<VAR>k l m n : I<VAR>u v : M<VAR>hu : u ≠ 1<VAR>hv : v ≠ 1<GOAL>Pi.mulSingle k u * Pi.mulSingle l v = Pi.mulSingle m u * Pi.mulSingle n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>x y z : (i : I) → f i<VAR>h : ∀ (i : I), SemiconjBy (x i) (y i) (z i)<GOAL>SemiconjBy x y z
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>x y z : (i : I) → f i<VAR>h : ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)<GOAL>AddSemiconjBy x y z
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>x y z : (i : I) → f i<GOAL>AddSemiconjBy x y z ↔ ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>x y z : (i : I) → f i<GOAL>SemiconjBy x y z ↔ ∀ (i : I), SemiconjBy (x i) (y i) (z i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>x y : (i : I) → f i<VAR>h : ∀ (i : I), AddCommute (x i) (y i)<GOAL>AddCommute x y
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>x y : (i : I) → f i<VAR>h : ∀ (i : I), Commute (x i) (y i)<GOAL>Commute x y
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>x y : (i : I) → f i<GOAL>AddCommute x y ↔ ∀ (i : I), AddCommute (x i) (y i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>x y : (i : I) → f i<GOAL>Commute x y ↔ ∀ (i : I), Commute (x i) (y i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → One (f i)<VAR>DecidableEq I<VAR>i : I<GOAL>Function.update 1 i 1 = 1
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Zero (f i)<VAR>DecidableEq I<VAR>i : I<GOAL>Function.update 0 i 0 = 0
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>DecidableEq I<VAR>f₁ f₂ : (i : I) → f i<VAR>i : I<VAR>x₁ x₂ : f i<GOAL>Function.update (f₁ + f₂) i (x₁ + x₂) = Function.update f₁ i x₁ + Function.update f₂ i x₂
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>DecidableEq I<VAR>f₁ f₂ : (i : I) → f i<VAR>i : I<VAR>x₁ x₂ : f i<GOAL>Function.update (f₁ * f₂) i (x₁ * x₂) = Function.update f₁ i x₁ * Function.update f₂ i x₂
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Inv (f i)<VAR>DecidableEq I<VAR>f₁ : (i : I) → f i<VAR>i : I<VAR>x₁ : f i<GOAL>Function.update f₁⁻¹ i x₁⁻¹ = (Function.update f₁ i x₁)⁻¹
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Neg (f i)<VAR>DecidableEq I<VAR>f₁ : (i : I) → f i<VAR>i : I<VAR>x₁ : f i<GOAL>Function.update (-f₁) i (-x₁) = -Function.update f₁ i x₁
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Sub (f i)<VAR>DecidableEq I<VAR>f₁ f₂ : (i : I) → f i<VAR>i : I<VAR>x₁ x₂ : f i<GOAL>Function.update (f₁ - f₂) i (x₁ - x₂) = Function.update f₁ i x₁ - Function.update f₂ i x₂
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Div (f i)<VAR>DecidableEq I<VAR>f₁ f₂ : (i : I) → f i<VAR>i : I<VAR>x₁ x₂ : f i<GOAL>Function.update (f₁ / f₂) i (x₁ / x₂) = Function.update f₁ i x₁ / Function.update f₂ i x₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>Nonempty ι<VAR>a : α<GOAL>Function.const ι a = 1 ↔ a = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>Nonempty ι<VAR>a : α<GOAL>Function.const ι a = 0 ↔ a = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>Nonempty ι<VAR>a : α<GOAL>Function.const ι a ≠ 1 ↔ a ≠ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>Nonempty ι<VAR>a : α<GOAL>Function.const ι a ≠ 0 ↔ a ≠ 0
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>s : Set I<VAR>(i : I) → Decidable (i ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : I) → f i<GOAL>s.piecewise (f₁ + f₂) (g₁ + g₂) = s.piecewise f₁ g₁ + s.piecewise f₂ g₂
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>s : Set I<VAR>(i : I) → Decidable (i ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : I) → f i<GOAL>s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Inv (f i)<VAR>s : Set I<VAR>(i : I) → Decidable (i ∈ s)<VAR>f₁ g₁ : (i : I) → f i<GOAL>s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Neg (f i)<VAR>s : Set I<VAR>(i : I) → Decidable (i ∈ s)<VAR>f₁ g₁ : (i : I) → f i<GOAL>s.piecewise (-f₁) (-g₁) = -s.piecewise f₁ g₁
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Sub (f i)<VAR>s : Set I<VAR>(i : I) → Decidable (i ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : I) → f i<GOAL>s.piecewise (f₁ - f₂) (g₁ - g₂) = s.piecewise f₁ g₁ - s.piecewise f₂ g₂
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Div (f i)<VAR>s : Set I<VAR>(i : I) → Decidable (i ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : I) → f i<GOAL>s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂
<VAR>ι : Type u_1<VAR>η : Type v<VAR>R : Type w<VAR>s : ι → η<VAR>MulOneClass R<VAR>f : ι → R<GOAL>∀ (a : η), (Function.ExtendByOne.hom R s) f a = Function.extend s f 1 a
<VAR>ι : Type u_1<VAR>η : Type v<VAR>R : Type w<VAR>s : ι → η<VAR>AddZeroClass R<VAR>f : ι → R<GOAL>∀ (a : η), (Function.ExtendByZero.hom R s) f a = Function.extend s f 0 a
<VAR>I : Type u<VAR>f : I → Type v<VAR>i : I<VAR>DecidableEq I<VAR>(i : I) → Preorder (f i)<VAR>(i : I) → Zero (f i)<GOAL>Monotone (Pi.single i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>i : I<VAR>DecidableEq I<VAR>(i : I) → Preorder (f i)<VAR>(i : I) → One (f i)<GOAL>Monotone (Pi.mulSingle i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>i : I<VAR>DecidableEq I<VAR>(i : I) → Preorder (f i)<VAR>(i : I) → One (f i)<GOAL>StrictMono (Pi.mulSingle i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>i : I<VAR>DecidableEq I<VAR>(i : I) → Preorder (f i)<VAR>(i : I) → Zero (f i)<GOAL>StrictMono (Pi.single i)
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → One (γ a b)<GOAL>Sigma.curry 1 = 1
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Zero (γ a b)<GOAL>Sigma.curry 0 = 0
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Zero (γ a b)<GOAL>Sigma.uncurry 0 = 0
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → One (γ a b)<GOAL>Sigma.uncurry 1 = 1
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Add (γ a b)<VAR>x y : (i : (a : α) × β a) → γ i.fst i.snd<GOAL>Sigma.curry (x + y) = Sigma.curry x + Sigma.curry y
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Mul (γ a b)<VAR>x y : (i : (a : α) × β a) → γ i.fst i.snd<GOAL>Sigma.curry (x * y) = Sigma.curry x * Sigma.curry y
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Add (γ a b)<VAR>x y : (a : α) → (b : β a) → γ a b<GOAL>Sigma.uncurry (x + y) = Sigma.uncurry x + Sigma.uncurry y
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Mul (γ a b)<VAR>x y : (a : α) → (b : β a) → γ a b<GOAL>Sigma.uncurry (x * y) = Sigma.uncurry x * Sigma.uncurry y
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Neg (γ a b)<VAR>x : (i : (a : α) × β a) → γ i.fst i.snd<GOAL>Sigma.curry (-x) = -Sigma.curry x
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Inv (γ a b)<VAR>x : (i : (a : α) × β a) → γ i.fst i.snd<GOAL>Sigma.curry x⁻¹ = (Sigma.curry x)⁻¹
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Neg (γ a b)<VAR>x : (a : α) → (b : β a) → γ a b<GOAL>Sigma.uncurry (-x) = -Sigma.uncurry x
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>(a : α) → (b : β a) → Inv (γ a b)<VAR>x : (a : α) → (b : β a) → γ a b<GOAL>Sigma.uncurry x⁻¹ = (Sigma.uncurry x)⁻¹
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (β a)<VAR>(a : α) → (b : β a) → One (γ a b)<VAR>i : (a : α) × β a<VAR>x : γ i.fst i.snd<GOAL>Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.fst (Pi.mulSingle i.snd x)
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (β a)<VAR>(a : α) → (b : β a) → Zero (γ a b)<VAR>i : (a : α) × β a<VAR>x : γ i.fst i.snd<GOAL>Sigma.curry (Pi.single i x) = Pi.single i.fst (Pi.single i.snd x)
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (β a)<VAR>(a : α) → (b : β a) → One (γ a b)<VAR>a : α<VAR>b : β a<VAR>x : γ a b<GOAL>Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x
<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (β a)<VAR>(a : α) → (b : β a) → Zero (γ a b)<VAR>a : α<VAR>b : β a<VAR>x : γ a b<GOAL>Sigma.uncurry (Pi.single a (Pi.single b x)) = Pi.single ⟨a, b⟩ x
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>DecidablePred fun x => x ∈ s<GOAL>s.piecewise f 0 = s.indicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>DecidablePred fun x => x ∈ s<GOAL>s.piecewise f 1 = s.mulIndicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>Decidable (a ∈ s)<GOAL>s.mulIndicator f a = if a ∈ s then f a else 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>Decidable (a ∈ s)<GOAL>s.indicator f a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → M<GOAL>s.indicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → M<GOAL>s.mulIndicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<VAR>f : α → M<GOAL>s.indicator f a = 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<VAR>f : α → M<GOAL>s.mulIndicator f a = 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.indicator f a = 0 ∨ s.indicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.indicator f a = f a ↔ a ∉ s → f a = 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.mulIndicator f a = f a ↔ a ∉ s → f a = 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>s.indicator f = f ↔ Function.support f ⊆ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>s.mulIndicator f = f ↔ Function.mulSupport f ⊆ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s t : Set α<VAR>f : α → M<VAR>h1 : s.indicator f = f<VAR>h2 : s ⊆ t<GOAL>t.indicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s t : Set α<VAR>f : α → M<VAR>h1 : s.mulIndicator f = f<VAR>h2 : s ⊆ t<GOAL>t.mulIndicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.mulIndicator f a = 1 ↔ a ∈ s → f a = 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.indicator f a = 0 ↔ a ∈ s → f a = 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>(s.mulIndicator f = fun x => 1) ↔ Disjoint (Function.mulSupport f) s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>(s.indicator f = fun x => 0) ↔ Disjoint (Function.support f) s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>s.indicator f = 0 ↔ Disjoint (Function.support f) s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>s.mulIndicator f = 1 ↔ Disjoint (Function.mulSupport f) s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.indicator f a ≠ 0 ↔ a ∈ s ∩ Function.support f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ Function.mulSupport f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>Function.support (s.indicator f) = s ∩ Function.support f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>h : s.mulIndicator f a ≠ 1<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>h : s.indicator f a ≠ 0<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>Set.EqOn (s.mulIndicator f) f s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>Set.EqOn (s.indicator f) f s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>Function.support (s.indicator f) ⊆ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>Function.mulSupport (s.mulIndicator f) ⊆ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>f : α → M<GOAL>(Function.mulSupport f).mulIndicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>f : α → M<GOAL>(Function.support f).indicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>ι : Sort u_6<VAR>f : ι → α<VAR>g : α → M<GOAL>(Set.range f).indicator g ∘ f = g ∘ f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>ι : Sort u_6<VAR>f : ι → α<VAR>g : α → M<GOAL>(Set.range f).mulIndicator g ∘ f = g ∘ f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f g : α → M<VAR>h : Set.EqOn f g s<GOAL>s.mulIndicator f = s.mulIndicator g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f g : α → M<VAR>h : Set.EqOn f g s<GOAL>s.indicator f = s.indicator g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>f : α → M<GOAL>Set.univ.mulIndicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>f : α → M<GOAL>Set.univ.indicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>f : α → M<GOAL>∅.mulIndicator f = fun x => 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>f : α → M<GOAL>∅.indicator f = fun x => 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>f : α → M<GOAL>∅.mulIndicator f = 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>f : α → M<GOAL>∅.indicator f = 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<GOAL>(s.indicator fun x => 0) = fun x => 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<GOAL>(s.mulIndicator fun x => 1) = fun x => 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<GOAL>s.mulIndicator 1 = 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<GOAL>s.indicator 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s t : Set α<VAR>f : α → M<GOAL>s.indicator (t.indicator f) = (s ∩ t).indicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s t : Set α<VAR>f : α → M<GOAL>s.mulIndicator (t.mulIndicator f) = (s ∩ t).mulIndicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<GOAL>(s ∩ Function.support f).indicator f = s.indicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<GOAL>(s ∩ Function.mulSupport f).mulIndicator f = s.mulIndicator f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>h : M → β<VAR>f : α → M<VAR>s : Set α<VAR>x : α<VAR>DecidablePred fun x => x ∈ s<GOAL>h (s.indicator f x) = s.piecewise (h ∘ f) (Function.const α (h 0)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>h : M → β<VAR>f : α → M<VAR>s : Set α<VAR>x : α<VAR>DecidablePred fun x => x ∈ s<GOAL>h (s.mulIndicator f x) = s.piecewise (h ∘ f) (Function.const α (h 1)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : β → α<VAR>g : α → M<VAR>x : β<GOAL>(f ⁻¹' s).indicator (g ∘ f) x = s.indicator g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : β → α<VAR>g : α → M<VAR>x : β<GOAL>(f ⁻¹' s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : β → M<VAR>g : α → β<VAR>hg : Function.Injective g<VAR>x : α<GOAL>(g '' s).indicator f (g x) = s.indicator (f ∘ g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : β → M<VAR>g : α → β<VAR>hg : Function.Injective g<VAR>x : α<GOAL>(g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>s : Set α<VAR>f : α → M<VAR>g : M → N<VAR>hg : g 0 = 0<GOAL>s.indicator (g ∘ f) = g ∘ s.indicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>s : Set α<VAR>f : α → M<VAR>g : M → N<VAR>hg : g 1 = 1<GOAL>s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Zero M<VAR>Zero N<VAR>s : Set α<VAR>c : M<VAR>f : M → N<VAR>hf : f 0 = 0<GOAL>(fun x => f (s.indicator (fun x => c) x)) = s.indicator fun x => f c
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>One M<VAR>One N<VAR>s : Set α<VAR>c : M<VAR>f : M → N<VAR>hf : f 1 = 1<GOAL>(fun x => f (s.mulIndicator (fun x => c) x)) = s.mulIndicator fun x => f c
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>B : Set M<GOAL>s.mulIndicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>B : Set M<GOAL>s.indicator f ⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>t : Set α<VAR>s : Set M<GOAL>t.indicator 0 ⁻¹' s ∈ {Set.univ, ∅}
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>t : Set α<VAR>s : Set M<GOAL>t.mulIndicator 1 ⁻¹' s ∈ {Set.univ, ∅}
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>U : Set α<VAR>s : Set M<VAR>a : M<VAR>Decidable (a ∈ s)<VAR>Decidable (0 ∈ s)<GOAL>(U.indicator fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 0 ∈ s then Uᶜ else ∅
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>U : Set α<VAR>s : Set M<VAR>a : M<VAR>Decidable (a ∈ s)<VAR>Decidable (1 ∈ s)<GOAL>(U.mulIndicator fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>U : Set α<VAR>s : Set M<VAR>a : M<GOAL>(U.indicator fun x => a) ⁻¹' s ∈ {Set.univ, U, Uᶜ, ∅}
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>U : Set α<VAR>s : Set M<VAR>a : M<GOAL>(U.mulIndicator fun x => a) ⁻¹' s ∈ {Set.univ, U, Uᶜ, ∅}
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>Zero M<VAR>U : Set α<VAR>s : Set M<GOAL>U.indicator 1 ⁻¹' s ∈ {Set.univ, U, Uᶜ, ∅}
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>t : Set M<VAR>ht : 0 ∉ t<GOAL>s.indicator f ⁻¹' t = f ⁻¹' t ∩ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>t : Set M<VAR>ht : 1 ∉ t<GOAL>s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>r : M<VAR>s : Set α<VAR>f : α → M<GOAL>r ∈ Set.range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ Set.univ ∨ r ∈ f '' s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>r : M<VAR>s : Set α<VAR>f : α → M<GOAL>r ∈ Set.range (s.indicator f) ↔ r = 0 ∧ s ≠ Set.univ ∨ r ∈ f '' s
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Zero M<VAR>s : Set α<VAR>f g : α → M<VAR>a : α<VAR>r : M → M → Prop<VAR>h1 : r 0 0<VAR>ha : a ∈ s → r (f a) (g a)<GOAL>r (s.indicator f a) (s.indicator g a)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>One M<VAR>s : Set α<VAR>f g : α → M<VAR>a : α<VAR>r : M → M → Prop<VAR>h1 : r 1 1<VAR>ha : a ∈ s → r (f a) (g a)<GOAL>r (s.mulIndicator f a) (s.mulIndicator g a)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>f : α → M<VAR>s t : Set α<VAR>a : α<GOAL>(s ∪ t).indicator f a + (s ∩ t).indicator f a = s.indicator f a + t.indicator f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>f : α → M<VAR>s t : Set α<VAR>a : α<GOAL>(s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>f : α → M<VAR>s t : Set α<GOAL>(s ∪ t).mulIndicator f * (s ∩ t).mulIndicator f = s.mulIndicator f * t.mulIndicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>f : α → M<VAR>s t : Set α<GOAL>(s ∪ t).indicator f + (s ∩ t).indicator f = s.indicator f + t.indicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s t : Set α<VAR>a : α<VAR>h : a ∉ s ∩ t<VAR>f : α → M<GOAL>(s ∪ t).indicator f a = s.indicator f a + t.indicator f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s t : Set α<VAR>a : α<VAR>h : a ∉ s ∩ t<VAR>f : α → M<GOAL>(s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>f : α → M<GOAL>(s ∪ t).mulIndicator f = fun a => s.mulIndicator f a * t.mulIndicator f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>f : α → M<GOAL>(s ∪ t).indicator f = fun a => s.indicator f a + t.indicator f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s t : Set α<VAR>f : α → M<GOAL>(symmDiff s t).mulIndicator f = (s \ t).mulIndicator f * (t \ s).mulIndicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s t : Set α<VAR>f : α → M<GOAL>(symmDiff s t).indicator f = (s \ t).indicator f + (t \ s).indicator f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>f g : α → M<GOAL>(s.indicator fun a => f a + g a) = fun a => s.indicator f a + s.indicator g a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>f g : α → M<GOAL>(s.mulIndicator fun a => f a * g a) = fun a => s.mulIndicator f a * s.mulIndicator g a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>f g : α → M<GOAL>s.mulIndicator (f * g) = s.mulIndicator f * s.mulIndicator g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>f g : α → M<GOAL>s.indicator (f + g) = s.indicator f + s.indicator g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>sᶜ.mulIndicator f a * s.mulIndicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>sᶜ.indicator f a + s.indicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>f : α → M<GOAL>sᶜ.indicator f + s.indicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>f : α → M<GOAL>sᶜ.mulIndicator f * s.mulIndicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.mulIndicator f a * sᶜ.mulIndicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.indicator f a + sᶜ.indicator f a = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>f : α → M<GOAL>s.indicator f + sᶜ.indicator f = f