ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>p✝ : ?m.47193<VAR>u v : V<VAR>H : SimpleGraph V<VAR>p : G.Walk u v<VAR>q : G.Walk u u<VAR>qc : q.IsCycle<VAR>hq : ∀ e ∈ q.edges, e ∈ H.edgeSet<GOAL>(q.transfer H hq).IsCycle
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ : Subgroup α<VAR>a b : α<VAR>N : Subgroup α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ : Subgroup α<VAR>a b : α<VAR>N : Subgroup α<VAR>s : Set α<VAR>x : α<GOAL>(∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hB : M.Base B<GOAL>M.closure B = M.E
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hB : M.Basis B M.E<GOAL>M.closure B = M.E
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : LinearWeights R L M<VAR>χ : L → R<VAR>x y : L<VAR>d : ℕ := finrank R ↥↑(weightSpace M χ)<GOAL>((traceForm R L ↥↑(weightSpace M χ)) x) y = d • (χ x * χ y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : LinearWeights R L M<VAR>χ : L → R<VAR>x y : L<VAR>d : ℕ := finrank R ↥↑(weightSpace M χ)<VAR>h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0<GOAL>((traceForm R L ↥↑(weightSpace M χ)) x) y = d • (χ x * χ y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : LinearWeights R L M<VAR>χ : L → R<VAR>x y : L<VAR>d : ℕ := finrank R ↥↑(weightSpace M χ)<VAR>h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0<VAR>h₂ : χ x • d • χ y = d • (χ x * χ y)<GOAL>((traceForm R L ↥↑(weightSpace M χ)) x) y = d • (χ x * χ y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : LinearWeights R L M<VAR>χ : L → R<VAR>x y : L<VAR>d : ℕ := finrank R ↥↑(weightSpace M χ)<VAR>h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0<VAR>h₂ : χ x • d • χ y = d • (χ x * χ y)<VAR>this : traceForm R L ↥↑(shiftedWeightSpace R L M χ) = 0<GOAL>((traceForm R L ↥↑(weightSpace M χ)) x) y = d • (χ x * χ y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : LinearWeights R L M<VAR>χ : L → R<VAR>x y : L<VAR>d : ℕ := finrank R ↥↑(weightSpace M χ)<VAR>h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0<VAR>h₂ : χ x • d • χ y = d • (χ x * χ y)<VAR>this : ((traceForm R L ↥↑(shiftedWeightSpace R L M χ)) x) y = (0 x) y<GOAL>((traceForm R L ↥↑(weightSpace M χ)) x) y = d • (χ x * χ y)
<VAR>a : ℤ<VAR>n : ℕ<VAR>h : J(a | n) = -1<GOAL>∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
<VAR>a : ℤ<VAR>n : ℕ<VAR>h : J(a | n) = -1<VAR>hn₀ : n ≠ 0<GOAL>∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
<VAR>a : ℤ<VAR>n : ℕ<VAR>h : J(a | n) = -1<VAR>hn₀ : n ≠ 0<VAR>hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0<GOAL>∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
<VAR>a : ℤ<VAR>n : ℕ<VAR>h : (List.map (fun n => J(a | n)) n.primeFactorsList).prod = -1<VAR>hn₀ : n ≠ 0<VAR>hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0<GOAL>∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
<VAR>a : ℤ<VAR>n : ℕ<VAR>h : (List.map (fun n => J(a | n)) n.primeFactorsList).prod = -1<VAR>hn₀ : n ≠ 0<VAR>hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0<VAR>p : ℕ<VAR>hmem : p ∈ n.primeFactorsList<VAR>hj : J(a | p) = -1<GOAL>∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>a b : α<GOAL>a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>a b : α<GOAL>a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℝ<GOAL>logDeriv cos x✝ = (-tan) x✝
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ ↑π ↔ AffineIndependent ℝ ![p₁, p₂, p₃]
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔ LinearIndependent ℝ ((fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>(fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1) = ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯ }.toFun (f * g) = { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯ }.toFun f * { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯ }.toFun g
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<VAR>this : φ ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) = φ ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal)<GOAL>{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯ }.toFun (f * g) = { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯ }.toFun f * { toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯ }.toFun g
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<VAR>this : φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal = φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal<GOAL>φ (f * g).toNNReal - φ (-(f * g)).toNNReal = φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal - (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<VAR>this : φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal - (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal) = 0<GOAL>φ (f * g).toNNReal - φ (-(f * g)).toNNReal - (φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal - (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)) = 0
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<GOAL>(↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯ }).toFun (f + g) = (↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯ }).toFun f + (↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯ }).toFun g
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<VAR>this : φ ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = φ ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)<GOAL>(↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯ }).toFun (f + g) = (↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯ }).toFun f + (↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯ }).toFun g
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<VAR>this : φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal = φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal<GOAL>φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f g : C(X, ℝ)<VAR>this : φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal) = 0<GOAL>φ (f + g).toNNReal - φ (-(f + g)).toNNReal - (φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)) = 0
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>r : ℝ<GOAL>φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f : C(X, ℝ)<GOAL>(↑↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingHom).toFun (star f) = star ((↑↑{ toFun := fun f => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingHom).toFun f)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>(μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>this : ν = ν.restrict univ<GOAL>(μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Sieve X<VAR>Y✝ : E<VAR>f✝ : Y✝ ⟶ (F ⋙ G).obj X<GOAL>(functorPushforward (F ⋙ G) R).arrows f✝ ↔ (functorPushforward G (functorPushforward F R)).arrows f✝
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h✝ : Y ⟶ Z<VAR>w : f ≫ h✝ = g ≫ h✝<VAR>inst✝³ : HasCoequalizer f g<VAR>inst✝² : HasCoequalizer (G.map f) (G.map g)<VAR>inst✝¹ : PreservesColimit (parallelPair f g) G<VAR>X' Y' : D<VAR>f' g' : X' ⟶ Y'<VAR>inst✝ : HasCoequalizer f' g'<VAR>p : G.obj X ⟶ X'<VAR>q : G.obj Y ⟶ Y'<VAR>wf : G.map f ≫ q = p ≫ f'<VAR>wg : G.map g ≫ q = p ≫ g'<VAR>Z' : D<VAR>h : Y' ⟶ Z'<VAR>wh : f' ≫ h = g' ≫ h<GOAL>G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh = q ≫ h
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h✝ : Y ⟶ Z<VAR>w : f ≫ h✝ = g ≫ h✝<VAR>inst✝³ : HasCoequalizer f g<VAR>inst✝² : HasCoequalizer (G.map f) (G.map g)<VAR>inst✝¹ : PreservesColimit (parallelPair f g) G<VAR>X' Y' : D<VAR>f' g' : X' ⟶ Y'<VAR>inst✝ : HasCoequalizer f' g'<VAR>p : G.obj X ⟶ X'<VAR>q : G.obj Y ⟶ Y'<VAR>wf : G.map f ≫ q = p ≫ f'<VAR>wg : G.map g ≫ q = p ≫ g'<VAR>Z' : D<VAR>h : Y' ⟶ Z'<VAR>wh : f' ≫ h = g' ≫ h<GOAL>(q ≫ coequalizer.π f' g') ≫ coequalizer.desc h wh = q ≫ h
<GOAL>Function.Antiperiodic (fun x => cexp (x * I)) ↑π
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq σ<VAR>m n : σ →₀ ℕ<VAR>a : R<GOAL>(coeff R m) ((monomial R n) a) = if m = n then a else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq σ<VAR>m n : σ →₀ ℕ<VAR>a : R<GOAL>(LinearMap.stdBasis R (fun x => R) n) a m = if m = n then a else 0
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f✝ g : (a : α) → β a<VAR>a : α<VAR>b : β a<VAR>f : (a : α) → β a<VAR>a' : α<VAR>v v' : β a'<VAR>h : update f a' v = update f a' v'<VAR>this : update f a' v a' = update f a' v' a'<GOAL>v = v'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<VAR>ha : ⊥ < a<VAR>c : ι<VAR>t : Finset ι<VAR>hc : c ∉ t<GOAL>((∀ b ∈ t, f b < a) → t.sup f < a) → (∀ b ∈ cons c t hc, f b < a) → (cons c t hc).sup f < a
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>↑(normSq (a + b)) = ↑(normSq a) + a * star b + b * star a + ↑(normSq b)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S : IntermediateField K L<VAR>x : ↥S<GOAL>IsIntegral K x ↔ IsIntegral K ↑x
<VAR>m n : ℤ<GOAL>bitwise (fun a b => a && !b) m n = m.ldiff n
<VAR>m n : ℕ<GOAL>↑(Nat.bitwise (fun x y => x && !!y) m n) = ↑(m &&& n)
<VAR>m n : ℕ<GOAL>Nat.bitwise (fun x y => !(!x && !y)) m n = m ||| n
<VAR>m n : ℕ<GOAL>↑(Nat.bitwise (fun x y => !x && !!y) m n) = ↑(Nat.bitwise (fun a b => a && !b) n m)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ : Finmap β<VAR>s₁ : AList β<GOAL>∅ ∪ ⟦s₁⟧ = ⟦s₁⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ : Finmap β<VAR>s₁ : AList β<GOAL>⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hc : 0 < c<GOAL>a < b / c ↔ c * a < b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>x : α<GOAL>x ∈ f.toAList ↔ f x ≠ 0
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x : E<VAR>a b : ℝ<GOAL>(restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } = (reCLM.smulRight x + I • imCLM.smulRight x) { re := a, im := b }
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>x y : Quotient s<GOAL>x.out ≈ y.out ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : f =o[l] g<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(fun x => f x ^ n) =o[l] fun x => g x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : f =o[l] g<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>(fun x => f x ^ n.succ) =o[l] fun x => g x ^ n.succ
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<GOAL>Function.Bijective (characterSpaceToSpectrum a)
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>φ ψ : ↑(characterSpace ℂ ↥(elementalStarAlgebra ℂ a))<VAR>h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ<GOAL>Continuous ⇑φ
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>φ ψ : ↑(characterSpace ℂ ↥(elementalStarAlgebra ℂ a))<VAR>h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ<GOAL>Continuous ⇑ψ
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>φ ψ : ↑(characterSpace ℂ ↥(elementalStarAlgebra ℂ a))<VAR>h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ<GOAL>φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<GOAL>Function.Surjective (characterSpaceToSpectrum a)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>x y : X<VAR>h : (fun x => orbit G x) x ≠ (fun x => orbit G x) y<GOAL>(Disjoint on id) ((fun x => orbit G x) x) ((fun x => orbit G x) y)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>x y : X<VAR>h : ¬(Disjoint on id) (orbit G x) (orbit G y)<GOAL>orbit G x = orbit G y
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I : FractionalIdeal S P<GOAL>spanSingleton S ((algebraMap R P) ↑I.den) * I = ↑I.num
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I : FractionalIdeal S P<GOAL>(fun I => ↑I) (spanSingleton S ((algebraMap R P) ↑I.den) * I) = (fun I => ↑I) ↑I.num
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I : FractionalIdeal S P<GOAL>↑(spanSingleton S ((algebraMap R P) ↑I.den) * I) = ↑↑I.num
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I : FractionalIdeal S P<GOAL>(algebraMap R P) ↑I.den • ↑I = ↑↑I.num