ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semifield R<VAR>DivisionSemiring A<VAR>Algebra R A<VAR>r s : R<GOAL>↑(r / s) = ↑r / ↑s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semifield R<VAR>DivisionSemiring A<VAR>Algebra R A<VAR>r : R<VAR>z : ℤ<GOAL>↑(r ^ z) = ↑r ^ z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Field R<VAR>DivisionRing A<VAR>Algebra R A<VAR>q : ℚ<GOAL>↑↑q = ↑q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>Algebra ℚ R<VAR>Algebra ℚ S<VAR>f : R →+* S<VAR>r : ℚ<GOAL>f ((algebraMap ℚ R) r) = (algebraMap ℚ S) r
<GOAL>algebraMap ℚ ℚ = RingHom.id ℚ
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>i : I<VAR>(i : I) → Zero (f i)<GOAL>0 i = 0
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>i : I<VAR>(i : I) → One (f i)<GOAL>1 i = 1
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>(i : I) → One (f i)<GOAL>1 = fun x => 1
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>(i : I) → Zero (f i)<GOAL>0 = fun x => 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<GOAL>Function.const α 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<GOAL>Function.const α 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One γ<VAR>x : α → β<GOAL>1 ∘ x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero γ<VAR>x : α → β<GOAL>0 ∘ x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero β<VAR>x : β → γ<GOAL>x ∘ 0 = Function.const α (x 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One β<VAR>x : β → γ<GOAL>x ∘ 1 = Function.const α (x 1)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>i : I<VAR>(i : I) → Add (f i)<GOAL>(x + y) i = x i + y i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>i : I<VAR>(i : I) → Mul (f i)<GOAL>(x * y) i = x i * y i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>(i : I) → Mul (f i)<GOAL>x * y = fun i => x i * y i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>(i : I) → Add (f i)<GOAL>x + y = fun i => x i + y i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul β<VAR>a b : β<GOAL>Function.const α a * Function.const α b = Function.const α (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>a b : β<GOAL>Function.const α a + Function.const α b = Function.const α (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Mul γ<VAR>x y : β → γ<VAR>z : α → β<GOAL>(x * y) ∘ z = x ∘ z * y ∘ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Add γ<VAR>x y : β → γ<VAR>z : α → β<GOAL>(x + y) ∘ z = x ∘ z + y ∘ z
<VAR>I : Type u<VAR>β : Type u_2<VAR>f : I → Type v₁<VAR>(i : I) → SMul β (f i)<VAR>b : β<VAR>x : (i : I) → f i<VAR>i : I<GOAL>(b • x) i = b • x i
<VAR>I : Type u<VAR>β : Type u_2<VAR>f : I → Type v₁<VAR>(i : I) → VAdd β (f i)<VAR>b : β<VAR>x : (i : I) → f i<VAR>i : I<GOAL>(b +ᵥ x) i = b +ᵥ x i
<VAR>I : Type u<VAR>β : Type u_2<VAR>f : I → Type v₁<VAR>(i : I) → Pow (f i) β<VAR>x : (i : I) → f i<VAR>b : β<VAR>i : I<GOAL>(x ^ b) i = x i ^ b
<VAR>I : Type u<VAR>β : Type u_2<VAR>f : I → Type v₁<VAR>(i : I) → SMul β (f i)<VAR>b : β<VAR>x : (i : I) → f i<GOAL>b • x = fun i => b • x i
<VAR>I : Type u<VAR>β : Type u_2<VAR>f : I → Type v₁<VAR>(i : I) → Pow (f i) β<VAR>x : (i : I) → f i<VAR>b : β<GOAL>x ^ b = fun i => x i ^ b
<VAR>I : Type u<VAR>β : Type u_2<VAR>f : I → Type v₁<VAR>(i : I) → VAdd β (f i)<VAR>b : β<VAR>x : (i : I) → f i<GOAL>b +ᵥ x = fun i => b +ᵥ x i
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : β<GOAL>Function.const I a ^ b = Function.const I (a ^ b)
<VAR>I : Type u<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : α<GOAL>b • Function.const I a = Function.const I (b • a)
<VAR>I : Type u<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : α<GOAL>b +ᵥ Function.const I a = Function.const I (b +ᵥ a)
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Pow γ α<VAR>x : β → γ<VAR>a : α<VAR>y : I → β<GOAL>(x ^ a) ∘ y = x ∘ y ^ a
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>VAdd α γ<VAR>a : α<VAR>x : β → γ<VAR>y : I → β<GOAL>(a +ᵥ x) ∘ y = a +ᵥ x ∘ y
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>SMul α γ<VAR>a : α<VAR>x : β → γ<VAR>y : I → β<GOAL>(a • x) ∘ y = a • x ∘ y
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x : (i : I) → f i<VAR>i : I<VAR>(i : I) → Neg (f i)<GOAL>(-x) i = -x i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x : (i : I) → f i<VAR>i : I<VAR>(i : I) → Inv (f i)<GOAL>x⁻¹ i = (x i)⁻¹
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x : (i : I) → f i<VAR>(i : I) → Inv (f i)<GOAL>x⁻¹ = fun i => (x i)⁻¹
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x : (i : I) → f i<VAR>(i : I) → Neg (f i)<GOAL>-x = fun i => -x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Neg β<VAR>a : β<GOAL>-Function.const α a = Function.const α (-a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Inv β<VAR>a : β<GOAL>(Function.const α a)⁻¹ = Function.const α a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Neg γ<VAR>x : β → γ<VAR>y : α → β<GOAL>(-x) ∘ y = -x ∘ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Inv γ<VAR>x : β → γ<VAR>y : α → β<GOAL>x⁻¹ ∘ y = (x ∘ y)⁻¹
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>i : I<VAR>(i : I) → Sub (f i)<GOAL>(x - y) i = x i - y i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>i : I<VAR>(i : I) → Div (f i)<GOAL>(x / y) i = x i / y i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>(i : I) → Sub (f i)<GOAL>x - y = fun i => x i - y i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>x y : (i : I) → f i<VAR>(i : I) → Div (f i)<GOAL>x / y = fun i => x i / y i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Div γ<VAR>x y : β → γ<VAR>z : α → β<GOAL>(x / y) ∘ z = x ∘ z / y ∘ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Sub γ<VAR>x y : β → γ<VAR>z : α → β<GOAL>(x - y) ∘ z = x ∘ z - y ∘ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Sub β<VAR>a b : β<GOAL>Function.const α a - Function.const α b = Function.const α (a - b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Div β<VAR>a b : β<GOAL>Function.const α a / Function.const α b = Function.const α (a / b)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i : I<VAR>x : f i<GOAL>Pi.single i x i = x
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i : I<VAR>x : f i<GOAL>Pi.mulSingle i x i = x
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i i' : I<VAR>h : i' ≠ i<VAR>x : f i<GOAL>Pi.mulSingle i x i' = 1
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i i' : I<VAR>h : i' ≠ i<VAR>x : f i<GOAL>Pi.single i x i' = 0
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i i' : I<VAR>h : i ≠ i'<VAR>x : f i<GOAL>Pi.single i x i' = 0
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i i' : I<VAR>h : i ≠ i'<VAR>x : f i<GOAL>Pi.mulSingle i x i' = 1
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i : I<GOAL>Pi.single i 0 = 0
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i : I<GOAL>Pi.mulSingle i 1 = 1
<VAR>I : Type u<VAR>β : Type u_2<VAR>DecidableEq I<VAR>One β<VAR>i : I<VAR>x : β<VAR>i' : I<GOAL>Pi.mulSingle i x i' = if i' = i then x else 1
<VAR>I : Type u<VAR>β : Type u_2<VAR>DecidableEq I<VAR>Zero β<VAR>i : I<VAR>x : β<VAR>i' : I<GOAL>Pi.single i x i' = if i' = i then x else 0
<VAR>I : Type u<VAR>β : Type u_2<VAR>DecidableEq I<VAR>Zero β<VAR>i : I<VAR>x : β<VAR>i' : I<GOAL>Pi.single i x i' = Pi.single i' x i
<VAR>I : Type u<VAR>β : Type u_2<VAR>DecidableEq I<VAR>One β<VAR>i : I<VAR>x : β<VAR>i' : I<GOAL>Pi.mulSingle i x i' = Pi.mulSingle i' x i
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>(i : I) → One (g i)<VAR>f' : (i : I) → f i → g i<VAR>hf' : ∀ (i : I), f' i 1 = 1<VAR>i : I<VAR>x : f i<VAR>j : I<GOAL>f' j (Pi.mulSingle i x j) = Pi.mulSingle i (f' i x) j
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>(i : I) → Zero (g i)<VAR>f' : (i : I) → f i → g i<VAR>hf' : ∀ (i : I), f' i 0 = 0<VAR>i : I<VAR>x : f i<VAR>j : I<GOAL>f' j (Pi.single i x j) = Pi.single i (f' i x) j
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>(i : I) → Zero (g i)<VAR>(i : I) → Zero (h i)<VAR>f' : (i : I) → f i → g i → h i<VAR>hf' : ∀ (i : I), f' i 0 0 = 0<VAR>i : I<VAR>x : f i<VAR>y : g i<VAR>j : I<GOAL>f' j (Pi.single i x j) (Pi.single i y j) = Pi.single i (f' i x y) j
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>(i : I) → One (g i)<VAR>(i : I) → One (h i)<VAR>f' : (i : I) → f i → g i → h i<VAR>hf' : ∀ (i : I), f' i 1 1 = 1<VAR>i : I<VAR>x : f i<VAR>y : g i<VAR>j : I<GOAL>f' j (Pi.mulSingle i x j) (Pi.mulSingle i y j) = Pi.mulSingle i (f' i x y) j
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>g : I → Type u_4<VAR>(i : I) → Zero (g i)<VAR>op : (i : I) → f i → g i<VAR>h : ∀ (i : I), op i 0 = 0<VAR>i : I<VAR>x : f i<GOAL>Pi.single i (op i x) = fun j => op j (Pi.single i x j)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>g : I → Type u_4<VAR>(i : I) → One (g i)<VAR>op : (i : I) → f i → g i<VAR>h : ∀ (i : I), op i 1 = 1<VAR>i : I<VAR>x : f i<GOAL>Pi.mulSingle i (op i x) = fun j => op j (Pi.mulSingle i x j)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>g₁ : I → Type u_4<VAR>g₂ : I → Type u_5<VAR>(i : I) → One (g₁ i)<VAR>(i : I) → One (g₂ i)<VAR>op : (i : I) → g₁ i → g₂ i → f i<VAR>h : ∀ (i : I), op i 1 1 = 1<VAR>i : I<VAR>x₁ : g₁ i<VAR>x₂ : g₂ i<GOAL>Pi.mulSingle i (op i x₁ x₂) = fun j => op j (Pi.mulSingle i x₁ j) (Pi.mulSingle i x₂ j)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>g₁ : I → Type u_4<VAR>g₂ : I → Type u_5<VAR>(i : I) → Zero (g₁ i)<VAR>(i : I) → Zero (g₂ i)<VAR>op : (i : I) → g₁ i → g₂ i → f i<VAR>h : ∀ (i : I), op i 0 0 = 0<VAR>i : I<VAR>x₁ : g₁ i<VAR>x₂ : g₂ i<GOAL>Pi.single i (op i x₁ x₂) = fun j => op j (Pi.single i x₁ j) (Pi.single i x₂ j)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i : I<GOAL>Function.Injective (Pi.mulSingle i)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i : I<GOAL>Function.Injective (Pi.single i)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.mulSingle i x = Pi.mulSingle i y ↔ x = y
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.single i x = Pi.single i y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Pi.prod Prod.fst Prod.snd = id
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Pi.prod Prod.snd Prod.fst = Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero γ<VAR>f : α → β<GOAL>Function.extend f 0 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One γ<VAR>f : α → β<GOAL>Function.extend f 1 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Mul γ<VAR>f : α → β<VAR>g₁ g₂ : α → γ<VAR>e₁ e₂ : β → γ<GOAL>Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Add γ<VAR>f : α → β<VAR>g₁ g₂ : α → γ<VAR>e₁ e₂ : β → γ<GOAL>Function.extend f (g₁ + g₂) (e₁ + e₂) = Function.extend f g₁ e₁ + Function.extend f g₂ e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Inv γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<GOAL>Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Neg γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<GOAL>Function.extend f (-g) (-e) = -Function.extend f g e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Sub γ<VAR>f : α → β<VAR>g₁ g₂ : α → γ<VAR>e₁ e₂ : β → γ<GOAL>Function.extend f (g₁ - g₂) (e₁ - e₂) = Function.extend f g₁ e₁ - Function.extend f g₂ e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Div γ<VAR>f : α → β<VAR>g₁ g₂ : α → γ<VAR>e₁ e₂ : β → γ<GOAL>Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>F : (i : I) → f i → g i<VAR>hF : ∀ (i : I), Function.Surjective (F i)<GOAL>Function.Surjective fun x i => F i (x i)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>F : (i : I) → f i → g i<VAR>hF : ∀ (i : I), Function.Injective (F i)<GOAL>Function.Injective fun x i => F i (x i)
<VAR>I : Type u<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>F : (i : I) → f i → g i<VAR>hF : ∀ (i : I), Function.Bijective (F i)<GOAL>Function.Bijective fun x i => F i (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>b : β<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Function.Injective g<GOAL>g ∘ f = Function.const α (g b) ↔ f = Function.const α b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One β<VAR>One γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Function.Injective g<VAR>hg0 : g 1 = 1<GOAL>g ∘ f = 1 ↔ f = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero β<VAR>Zero γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Function.Injective g<VAR>hg0 : g 0 = 0<GOAL>g ∘ f = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero β<VAR>Zero γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Function.Injective g<VAR>hg0 : g 0 = 0<GOAL>g ∘ f ≠ 0 ↔ f ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One β<VAR>One γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Function.Injective g<VAR>hg0 : g 1 = 1<GOAL>g ∘ f ≠ 1 ↔ f ≠ 1
<VAR>I : Type u<VAR>α : Type u_4<VAR>DecidableEq I<VAR>Subsingleton I<VAR>Zero α<VAR>i : I<VAR>x : α<GOAL>Pi.single i x = fun x_1 => x
<VAR>I : Type u<VAR>α : Type u_4<VAR>DecidableEq I<VAR>Subsingleton I<VAR>One α<VAR>i : I<VAR>x : α<GOAL>Pi.mulSingle i x = fun x_1 => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One γ<GOAL>Sum.elim 1 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero γ<GOAL>Sum.elim 0 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>One γ<VAR>i : α<VAR>c : γ<GOAL>Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (Sum.inl i) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Zero γ<VAR>i : α<VAR>c : γ<GOAL>Sum.elim (Pi.single i c) 0 = Pi.single (Sum.inl i) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Zero γ<VAR>i : β<VAR>c : γ<GOAL>Sum.elim 0 (Pi.single i c) = Pi.single (Sum.inr i) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>One γ<VAR>i : β<VAR>c : γ<GOAL>Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α → γ<VAR>b : β → γ<VAR>Inv γ<GOAL>Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α → γ<VAR>b : β → γ<VAR>Neg γ<GOAL>Sum.elim (-a) (-b) = -Sum.elim a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α → γ<VAR>b b' : β → γ<VAR>Add γ<GOAL>Sum.elim (a + a') (b + b') = Sum.elim a b + Sum.elim a' b'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α → γ<VAR>b b' : β → γ<VAR>Mul γ<GOAL>Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α → γ<VAR>b b' : β → γ<VAR>Div γ<GOAL>Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α → γ<VAR>b b' : β → γ<VAR>Sub γ<GOAL>Sum.elim (a - a') (b - b') = Sum.elim a b - Sum.elim a' b'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>c : R<VAR>x : RestrictScalars R S M<GOAL>c • x = (RestrictScalars.addEquiv R S M).symm ((algebraMap R S) c • (RestrictScalars.addEquiv R S M) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>c : R<VAR>x : RestrictScalars R S M<GOAL>(RestrictScalars.addEquiv R S M) (c • x) = (algebraMap R S) c • (RestrictScalars.addEquiv R S M) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>r : R<VAR>x : M<GOAL>(RestrictScalars.addEquiv R S M).symm ((algebraMap R S) r • x) = r • (RestrictScalars.addEquiv R S M).symm x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>r : R<VAR>s : S<VAR>x : M<GOAL>(RestrictScalars.addEquiv R S M).symm ((r • s) • x) = r • (RestrictScalars.addEquiv R S M).symm (s • x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>s : S<VAR>x : RestrictScalars R S M<GOAL>((RestrictScalars.lsmul R S M) s) x = (RestrictScalars.addEquiv R S M).symm (s • (RestrictScalars.addEquiv R S M) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>CommSemiring S<VAR>Algebra S A<VAR>CommSemiring R<VAR>Algebra R S<VAR>r : R<VAR>x : RestrictScalars R S A<GOAL>(RestrictScalars.ringEquiv R S A) (r • x) = (algebraMap R S) r • (RestrictScalars.ringEquiv R S A) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>CommSemiring S<VAR>Algebra S A<VAR>CommSemiring R<VAR>Algebra R S<VAR>r : R<GOAL>(RestrictScalars.ringEquiv R S A) ((algebraMap R (RestrictScalars R S A)) r) = (algebraMap S A) ((algebraMap R S) r)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One β<VAR>Nonempty α<GOAL>Set.range 1 = {1}
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero β<VAR>Nonempty α<GOAL>Set.range 0 = {0}
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero β<VAR>s : Set β<VAR>Decidable (0 ∈ s)<GOAL>0 ⁻¹' s = if 0 ∈ s then Set.univ else ∅
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One β<VAR>s : Set β<VAR>Decidable (1 ∈ s)<GOAL>1 ⁻¹' s = if 1 ∈ s then Set.univ else ∅
<VAR>M : Type u_3<VAR>N : Type u_4<GOAL>∀ {x : Mul M} {x_1 : CommSemigroup N} (f g : M →ₙ* N), ⇑f * ⇑g = fun x_2 => f x_2 * g x_2
<VAR>M : Type u_3<VAR>N : Type u_4<GOAL>∀ {x : Add M} {x_1 : AddCommSemigroup N} (f g : AddHom M N), ⇑f + ⇑g = fun x_2 => f x_2 + g x_2
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>(i : I) → Mul (f i)<VAR>Mul γ<VAR>g : (i : I) → γ →ₙ* f i<VAR>x : γ<VAR>i : I<GOAL>(Pi.mulHom g) x i = (g i) x
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>(i : I) → Add (f i)<VAR>Add γ<VAR>g : (i : I) → AddHom γ (f i)<VAR>x : γ<VAR>i : I<GOAL>(Pi.addHom g) x i = (g i) x
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>Nonempty I<VAR>(i : I) → Add (f i)<VAR>Add γ<VAR>g : (i : I) → AddHom γ (f i)<VAR>hg : ∀ (i : I), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Pi.addHom g)
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>Nonempty I<VAR>(i : I) → Mul (f i)<VAR>Mul γ<VAR>g : (i : I) → γ →ₙ* f i<VAR>hg : ∀ (i : I), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Pi.mulHom g)
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>(i : I) → MulOneClass (f i)<VAR>MulOneClass γ<VAR>g : (i : I) → γ →* f i<VAR>x : γ<VAR>i : I<GOAL>(Pi.monoidHom g) x i = (g i) x
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>(i : I) → AddZeroClass (f i)<VAR>AddZeroClass γ<VAR>g : (i : I) → γ →+ f i<VAR>x : γ<VAR>i : I<GOAL>(Pi.addMonoidHom g) x i = (g i) x
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>Nonempty I<VAR>(i : I) → MulOneClass (f i)<VAR>MulOneClass γ<VAR>g : (i : I) → γ →* f i<VAR>hg : ∀ (i : I), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Pi.monoidHom g)
<VAR>I : Type u<VAR>f : I → Type v<VAR>γ : Type w<VAR>Nonempty I<VAR>(i : I) → AddZeroClass (f i)<VAR>AddZeroClass γ<VAR>g : (i : I) → γ →+ f i<VAR>hg : ∀ (i : I), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Pi.addMonoidHom g)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Add (f i)<VAR>i : I<VAR>g : (i : I) → f i<GOAL>(Pi.evalAddHom f i) g = g i
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Mul (f i)<VAR>i : I<VAR>g : (i : I) → f i<GOAL>(Pi.evalMulHom f i) g = g i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Add β<VAR>a : β<GOAL>∀ (a_1 : α), (Pi.constAddHom α β) a a_1 = Function.const α a a_1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Mul β<VAR>a : β<GOAL>∀ (a_1 : α), (Pi.constMulHom α β) a a_1 = Function.const α a a_1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Mul α<VAR>CommSemigroup β<VAR>g : α →ₙ* β<VAR>a : α<GOAL>(MulHom.coeFn α β) g a = g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Add α<VAR>AddCommSemigroup β<VAR>g : AddHom α β<VAR>a : α<GOAL>(AddHom.coeFn α β) g a = g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Add α<VAR>Add β<VAR>f : AddHom α β<VAR>I : Type u_5<VAR>h : I → α<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Mul α<VAR>Mul β<VAR>f : α →ₙ* β<VAR>I : Type u_5<VAR>h : I → α<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → MulOneClass (f i)<VAR>i : I<VAR>g : (i : I) → f i<GOAL>(Pi.evalMonoidHom f i) g = g i
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → AddZeroClass (f i)<VAR>i : I<VAR>g : (i : I) → f i<GOAL>(Pi.evalAddMonoidHom f i) g = g i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>MulOneClass β<VAR>a : β<GOAL>∀ (a_1 : α), (Pi.constMonoidHom α β) a a_1 = Function.const α a a_1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddZeroClass β<VAR>a : β<GOAL>∀ (a_1 : α), (Pi.constAddMonoidHom α β) a a_1 = Function.const α a a_1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>MulOneClass α<VAR>CommMonoid β<VAR>g : α →* β<VAR>a : α<GOAL>(MonoidHom.coeFn α β) g a = g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddZeroClass α<VAR>AddCommMonoid β<VAR>g : α →+ β<VAR>a : α<GOAL>(AddMonoidHom.coeFn α β) g a = g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+ β<VAR>I : Type u_5<VAR>h : I → α<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>I : Type u_5<VAR>h : I → α<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → Zero (f i)<VAR>i : I<VAR>x : f i<GOAL>(ZeroHom.single f i) x = Pi.single i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → One (f i)<VAR>i : I<VAR>x : f i<GOAL>(OneHom.mulSingle f i) x = Pi.mulSingle i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → MulOneClass (f i)<VAR>i : I<VAR>x : f i<GOAL>(MonoidHom.mulSingle f i) x = Pi.mulSingle i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → AddZeroClass (f i)<VAR>i : I<VAR>x : f i<GOAL>(AddMonoidHom.single f i) x = Pi.single i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → SemilatticeSup (f i)<VAR>(i : I) → One (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.mulSingle i (x ⊔ y) = Pi.mulSingle i x ⊔ Pi.mulSingle i y
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → SemilatticeSup (f i)<VAR>(i : I) → Zero (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) → SemilatticeInf (f i)<VAR>(i : I) → One (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.mulSingle i (x ⊓ y) = Pi.mulSingle i x ⊓ Pi.mulSingle i y
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → SemilatticeInf (f i)<VAR>(i : I) → Zero (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) → MulOneClass (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.mulSingle i (x * y) = Pi.mulSingle i x * Pi.mulSingle i y
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → AddZeroClass (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) → AddGroup (f i)<VAR>i : I<VAR>x : f i<GOAL>Pi.single i (-x) = -Pi.single i x
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → Group (f i)<VAR>i : I<VAR>x : f i<GOAL>Pi.mulSingle i x⁻¹ = (Pi.mulSingle i x)⁻¹
<VAR>I : Type u<VAR>f : I → Type v<VAR>DecidableEq I<VAR>(i : I) → Group (f i)<VAR>i : I<VAR>x y : f i<GOAL>Pi.mulSingle i (x / y) = Pi.mulSingle i x / Pi.mulSingle i y