ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : t ∈ γ ⁻¹' (extChartAt I (γ t₀)).source<GOAL>HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (↑(extChartAt I (γ t₀)) ∘ γ) t (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>(mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t))) = ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>∀ (x : TangentSpace 𝓘(ℝ, ℝ) t), ((mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t)))) x = (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<VAR>a : TangentSpace 𝓘(ℝ, ℝ) t<GOAL>((mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t)))) a = (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) a
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<VAR>a : TangentSpace 𝓘(ℝ, ℝ) t<GOAL>(ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a) = (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>p : c.Quotientˣ → Prop<VAR>H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }<VAR>val✝ inv✝ : c.Quotient<VAR>x y : M<VAR>h₁ : Quot.mk r x * Quot.mk r y = 1<VAR>h₂ : Quot.mk r y * Quot.mk r x = 1<GOAL>p { val := Quot.mk r x, inv := Quot.mk r y, val_inv := h₁, inv_val := h₂ }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A<VAR>inst✝ : IsDenseSubsite J K G<VAR>Y : Sheaf J A<VAR>U : C<VAR>X : A<GOAL>IsIso ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A<VAR>inst✝ : IsDenseSubsite J K G<VAR>Y : Sheaf J A<VAR>U : C<VAR>X : A<GOAL>Function.Bijective ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Denumerable α<VAR>inst✝¹ : Denumerable β<VAR>γ : α → Type u_3<VAR>inst✝ : (a : α) → Denumerable (γ a)<VAR>n : ℕ<GOAL>some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Denumerable α<VAR>inst✝¹ : Denumerable β<VAR>γ : α → Type u_3<VAR>inst✝ : (a : α) → Denumerable (γ a)<VAR>n : ℕ<GOAL>((decode (unpair n).1).bind fun a => Option.map (Sigma.mk a) (decode (unpair n).2)) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : T<VAR>p₁ p₂ : LocalizedModule S A<GOAL>x • p₁ * p₂ = x • (p₁ * p₂)
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : T<VAR>a₁ s₁ : A<VAR>a₂ s₂ : ↥S<GOAL>x • mk a₁ a₂ * mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I J : Ideal A<VAR>this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)<VAR>hgcd : gcd I J = I ⊔ J<VAR>hlcm : lcm I J = I ⊓ J<GOAL>(I ⊔ J) * (I ⊓ J) = I * J
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ f : α → β<VAR>g₁ g₂ : β → α<VAR>h₁ : LeftInverse g₁ f<VAR>h₂ : RightInverse g₂ f<GOAL>g₁ = g₁ ∘ f ∘ g₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ f : α → β<VAR>g₁ g₂ : β → α<VAR>h₁ : LeftInverse g₁ f<VAR>h₂ : RightInverse g₂ f<GOAL>g₁ ∘ f ∘ g₂ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b✝ : β<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>GameAdd rα s(a₁, b) s(b, a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b✝ : β<VAR>a₁ a₂ b : α<VAR>h : rα a₁ a₂<GOAL>GameAdd rα s(b, a₁) s(b, a₂)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (x * z + y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>β : Type u_9<VAR>i : Finset β<VAR>f : β → Multiset α<GOAL>i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → (f x).Disjoint (f y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>β : Type u_9<VAR>f : β → Multiset α<GOAL>∅.sum f = ∅.sup f ↔ ∀ x ∈ ∅, ∀ y ∈ ∅, x ≠ y → (f x).Disjoint (f y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>β : Type u_9<VAR>f : β → Multiset α<VAR>z : β<VAR>i : Finset β<VAR>hz : z ∉ i<VAR>hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → (f x).Disjoint (f y)<GOAL>(Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔ ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → (f x).Disjoint (f 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>c : ℝ<VAR>hc : 0 < c<VAR>x : α<GOAL>x ∈ {x | (fun x => ‖0‖ ≤ c * ‖g' x‖) x}
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>eval 0 M.charpolyRev = 1
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = det 1
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>this : (1 - X • M.map ⇑C).map (eval 0) = 1<GOAL>((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = det 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m1 m2 m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m1 ≤ m<VAR>h2 : m2 ≤ m<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m1 = generateFrom p1<VAR>hpm2 : m2 = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ {s | MeasurableSet s}<VAR>ht2 : t2 ∈ {s | MeasurableSet s}<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m1 m2 m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m1 ≤ m<VAR>h2 : m2 ≤ m<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m1 = generateFrom p1<VAR>hpm2 : m2 = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ {s | MeasurableSet s}<VAR>ht2 : t2 ∈ {s | MeasurableSet s}<GOAL>(fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2) ∅
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m1 m2 m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m1 ≤ m<VAR>h2 : m2 ≤ m<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m1 = generateFrom p1<VAR>hpm2 : m2 = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ {s | MeasurableSet s}<VAR>ht2 : t2 ∈ {s | MeasurableSet s}<GOAL>∀ t ∈ p1, (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m1 m2 m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m1 ≤ m<VAR>h2 : m2 ≤ m<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m1 = generateFrom p1<VAR>hpm2 : m2 = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ {s | MeasurableSet s}<VAR>ht2 : t2 ∈ {s | MeasurableSet s}<GOAL>∀ (t : Set Ω), MeasurableSet t → (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2) t → (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2) tᶜ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m1 m2 m : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m1 ≤ m<VAR>h2 : m2 ≤ m<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m1 = generateFrom p1<VAR>hpm2 : m2 = generateFrom p2<VAR>hyp : IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ {s | MeasurableSet s}<VAR>ht2 : t2 ∈ {s | MeasurableSet s}<GOAL>∀ (f : ℕ → Set Ω), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2) (f i)) → (fun t => ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2) (⋃ i, f i)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : One R<VAR>inst✝ : AddGroup R<VAR>f : ι → R<GOAL>mulSupport (1 - f) = support f
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>#((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ max ℵ₀ L.card
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>#((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<GOAL>CompactSpace ↑↑X.toPresheafedSpace ↔ QuasiCompact (terminal.from X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>φ P.d = φ P.a * -(x * y * z)
<VAR>q a b c : ℚ<VAR>n d : ℤ<GOAL>n /. d = ↑n / ↑d
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯<VAR>n : ℕ<VAR>n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx<VAR>x : A<GOAL>∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯<VAR>n : ℕ<VAR>n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx<VAR>x : A<GOAL>∀ (hx : x ∈ M ^ n * M), C (n + 1) x ⋯
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop<VAR>algebraMap : ∀ (r : R), C 0 ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯<VAR>mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯<VAR>n : ℕ<VAR>n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx<VAR>x : A<VAR>hx : x ∈ M ^ n * M<GOAL>C (n + 1) x ⋯
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Abelian C<VAR>K : CochainComplex C ℕ<VAR>X : C<VAR>φ : X ⟶ K.X 0<VAR>inst✝ : HomologicalComplex.HasHomology K 0<VAR>hφ✝ : φ ≫ K.d 0 1 = 0<VAR>hφ : φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0) = 0<VAR>α : ShortComplex.mk 0 0 ⋯ ⟶ HomologicalComplex.sc K 0 := { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }<GOAL>IsIso (HomologicalComplex.liftCycles K φ ((ComplexShape.up ℕ).next 0) ⋯ hφ) ↔ (ShortComplex.mk φ (K.d 0 ((ComplexShape.up ℕ).next 0)) hφ).Exact ∧ Mono φ
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsIrrefl α r<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : Lex r l₁ l₂<GOAL>Lex r l₁ l₂
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsIrrefl α r<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : r a a<GOAL>Lex r l₁ l₂
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>a b : n<VAR>ha : a ≠ i<VAR>c : R<VAR>M : Matrix n n R<GOAL>(transvection i j c * M) a b = M a b
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>I : WithBot (Box ι)<GOAL>⋃ J, ⋃ (_ : ↑J = I), ↑J = ↑I
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<GOAL>⨍⁻ (x : α) in s ∪ t, f x ∂μ = μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f x ∂μ
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : SubMulAction R M<VAR>r : R<VAR>x y : M<VAR>h : -x ∈ p<GOAL>x ∈ p
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : SubMulAction R M<VAR>r : R<VAR>x y : M<VAR>h : -x ∈ p<GOAL>- -x ∈ p
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>h : F.IsMittagLeffler<VAR>f : j ⟶ i<GOAL>F.eventualRange i ⊆ F.map f '' F.eventualRange j
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>h : F.IsMittagLeffler<VAR>f : j ⟶ i<VAR>k : J<VAR>g : k ⟶ j<VAR>hg : F.eventualRange j = range (F.map g)<GOAL>F.eventualRange i ⊆ F.map f '' F.eventualRange j
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>h : F.IsMittagLeffler<VAR>f : j ⟶ i<VAR>k : J<VAR>g : k ⟶ j<VAR>hg : F.eventualRange j = range (F.map g)<VAR>x : F.obj i<VAR>hx : x ∈ F.eventualRange i<GOAL>x ∈ F.map f '' range (F.map g)
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>h : F.IsMittagLeffler<VAR>f : j ⟶ i<VAR>k : J<VAR>g : k ⟶ j<VAR>hg : F.eventualRange j = range (F.map g)<VAR>x : F.obj k<VAR>hx : F.map (g ≫ f) x ∈ F.eventualRange i<GOAL>F.map (g ≫ f) x ∈ F.map f '' range (F.map g)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>cyclesMap φ = cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>cyclesMap φ = cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f.hom ⊗ g) ≫ (f.inv ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>𝟙 V ⊗ g ≫ h = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p✝ : ℝ<VAR>s : Set ℝ<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun x => x ^ p) =Θ[atTop] fun x => x ^ (p - 1)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f x)<VAR>n : ℕ<GOAL>∀ (x : α), p x ↔ p ((f ^ Int.negSucc n) x)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f x)<VAR>n : ℕ<GOAL>∀ (x : α), p x ↔ p ((f ^ (n + 1))⁻¹ x)
<VAR>p : ℕ<VAR>h : 1 < p<VAR>n : ℕ<GOAL>1 / (-1) ^ p * (1 / ↑n ^ p) = 1 / ↑(-↑n) ^ p
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<GOAL>swap hammingDist = hammingDist
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<GOAL>swap hammingDist x y = hammingDist x y
<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>t : Triangle ℝ P<GOAL>t.orthocenter = 3 • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
<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>t : Triangle ℝ P<GOAL>(↑(2 + 1) / ↑(2 - 1)) • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t = 3 • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)