ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<VAR>e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm<VAR>F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e<VAR>F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'<VAR>φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)<VAR>hφ : φ.IsHomogeneous n<GOAL>F (p.coeff i) = ((finSuccEquiv R k) φ).coeff i
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<VAR>e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm<VAR>F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e<VAR>F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'<VAR>φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)<VAR>hφ : φ.IsHomogeneous n<GOAL>(rename ⇑e) (p.coeff i) = ((finSuccEquiv R k) ((rename ⇑e') ((optionEquivLeft R σ).symm p))).coeff i
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<VAR>e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm<VAR>F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e<VAR>F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'<VAR>φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)<VAR>hφ : φ.IsHomogeneous n<GOAL>(rename ⇑e) (p.coeff i) = (Polynomial.map (rename ⇑e).toRingHom p).coeff i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s.einfsep ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.einfsep = ⊤<GOAL>¬s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.einfsep = ⊤<GOAL>s.Subsingleton
<VAR>α✝ : Type u_1<VAR>R : α✝ → α✝ → Prop<VAR>l : List α✝<VAR>S : α✝ → α✝ → Prop<VAR>hR : Pairwise R l<VAR>hS : Pairwise S l<GOAL>Pairwise (fun a b => R a b ∧ S a b) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite<GOAL>∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite<VAR>hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset<GOAL>∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite<VAR>hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset<GOAL>∏ y ∈ s, ∏ x ∈ ⋯.toFinset, f x y = ∏ b ∈ s, ∏ᶠ (a : α), f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b✝ : α<VAR>s✝ t : Set α<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite<VAR>hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset<VAR>b : β<VAR>hb : b ∈ s<GOAL>(mulSupport fun x => f x b) ⊆ ↑⋯.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a✝ b✝ : α<VAR>s✝ t : Set α<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite<VAR>hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset<VAR>b : β<VAR>hb : b ∈ s<VAR>a : α<VAR>ha : a ∈ mulSupport fun x => f x b<GOAL>a ∈ ↑⋯.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a✝ b✝ : α<VAR>s✝ t : Set α<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite<VAR>hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset<VAR>b : β<VAR>hb : b ∈ s<VAR>a : α<VAR>ha : a ∈ mulSupport fun x => f x b<GOAL>∃ i, ∃ (_ : i ∈ ↑s), a ∈ mulSupport fun a => f a i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁸ : AddCommMonoid M'✝<VAR>inst✝⁷ : AddCommMonoid M''<VAR>inst✝⁶ : Module R M'✝<VAR>inst✝⁵ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : FiniteDimensional K V<VAR>ι : Type u_10<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>b : Basis ι K V<VAR>i j : ι<GOAL>(B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁸ : AddCommMonoid M'✝<VAR>inst✝⁷ : AddCommMonoid M''<VAR>inst✝⁶ : Module R M'✝<VAR>inst✝⁵ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : FiniteDimensional K V<VAR>ι : Type u_10<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>b : Basis ι K V<VAR>i j : ι<VAR>this : FiniteDimensional K V<GOAL>(B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<GOAL>μ[|s] t = (μ s)⁻¹ * μ[|t] s * μ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h₁ : x.1 ≤ y.1<VAR>h₂ : x.2 < y.2<GOAL>x < y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>m : F<VAR>s✝ t✝ : Set α<VAR>s t : Set β<VAR>w✝¹ : α<VAR>left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s<VAR>w✝ : α<VAR>left✝ : w✝ ∈ ⇑m ⁻¹' t<GOAL>(fun x x_1 => x / x_1) w✝¹ w✝ ∈ ⇑m ⁻¹' (s / t)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ prod.snd = prod.snd ≫ prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>inst✝ : Unique α<VAR>f g : α →₀ M<VAR>h : f default = g default<VAR>a : α<GOAL>f a = g a
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>p : ℤ<VAR>hp : Prime p<VAR>a b c : ℤ<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<VAR>HF : a ^ n + b ^ n + c ^ n = 0<GOAL>p ∣ c
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n : ℕ<VAR>p : ℤ<VAR>hp : Prime p<VAR>a b c : ℤ<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<VAR>HF : a ^ 0 + b ^ 0 + c ^ 0 = 0<GOAL>p ∣ c
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>p : ℤ<VAR>hp : Prime p<VAR>a b c : ℤ<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<VAR>HF : a ^ n + b ^ n + c ^ n = 0<VAR>hn : n ≠ 0<GOAL>p ∣ c
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>p : ℤ<VAR>hp : Prime p<VAR>a b c : ℤ<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<VAR>HF : a ^ n + b ^ n + c ^ n = 0<VAR>hn : n ≠ 0<GOAL>p ∣ -c ^ n
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>p : ℤ<VAR>hp : Prime p<VAR>a b c : ℤ<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<VAR>HF : a ^ n + b ^ n = -c ^ n<VAR>hn : n ≠ 0<GOAL>p ∣ -c ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → SemilatticeInf (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<VAR>j : ι<GOAL>update f i (a ⊓ b) j = (update f i a ⊓ update f i b) j
<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>x : E<GOAL>thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<GOAL>∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume<GOAL>∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume<GOAL>∫ (x : ι → ℝ), cexp (-b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2 + c * ↑⟪w, (EuclideanSpace.measurableEquiv ι).symm x⟫_ℝ) ∂volume = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume<GOAL>∫ (x : ι → ℝ), cexp (-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2) + c * ↑⟪w, (EuclideanSpace.measurableEquiv ι).symm x⟫_ℝ) ∂volume = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume<VAR>y : ι → ℝ<GOAL>-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm y‖ ^ 2) = -b * ∑ i : ι, ↑(y i) ^ 2
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume<VAR>y : ι → ℝ<GOAL>c * ↑⟪w, (EuclideanSpace.measurableEquiv ι).symm y⟫_ℝ = ∑ i : ι, c * ↑(w i) * ↑(y i)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume<GOAL>c ^ 2 * ↑‖w‖ ^ 2 = ∑ i : ι, (c * ↑(w i)) ^ 2
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>g : S →+* P<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>W : Opens ↑(PrimeSpectrum.Top P)<VAR>hUV : ∀ p ∈ V, (PrimeSpectrum.comap f) p ∈ U<VAR>hVW : ∀ p ∈ W, (PrimeSpectrum.comap g) p ∈ V<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op W))<GOAL>↑((comap (g.comp f) U W ⋯) s) p = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>g : S →+* P<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>W : Opens ↑(PrimeSpectrum.Top P)<VAR>hUV : ∀ p ∈ V, (PrimeSpectrum.comap f) p ∈ U<VAR>hVW : ∀ p ∈ W, (PrimeSpectrum.comap g) p ∈ V<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op W))<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap (g.comp f)) ↑p).asIdeal (↑p).asIdeal (g.comp f) ⋯) (↑s ⟨(PrimeSpectrum.comap (g.comp f)) ↑p, ⋯⟩) = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.57383, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝ : K.HasHomology i<VAR>A A' : C<VAR>k : K.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : K.d j i ≫ k = 0<VAR>α : A ⟶ A'<GOAL>K.d j i ≫ k ≫ α = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝ : K.HasHomology i<VAR>A A' : C<VAR>k : K.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : K.d j i ≫ k = 0<VAR>α : A ⟶ A'<GOAL>K.descOpcycles k j hj hk ≫ α = K.descOpcycles (k ≫ α) j hj ⋯
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : AddCommMonoid B<VAR>inst✝¹ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝¹ : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝ : AddCommMonoid M<VAR>s✝ : Multiset M<VAR>a✝ : α<VAR>a : M<VAR>s : Multiset M<VAR>ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum<GOAL>single a✝ (a ::ₘ s).sum = (Multiset.map (single a✝) (a ::ₘ s)).sum
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb✝ hb : Submodule.span R (Set.range b) = ⊤<VAR>x y : Module.End R M<VAR>e : (fromEnd R b) x = (fromEnd R b) y<VAR>m : M<GOAL>x m = y m
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb✝ hb : Submodule.span R (Set.range b) = ⊤<VAR>x y : Module.End R M<VAR>e : (fromEnd R b) x = (fromEnd R b) y<VAR>m : ι → R<GOAL>x (((Fintype.total R R) b) m) = y (((Fintype.total R R) b) m)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : y ∈ t<VAR>H : hausdorffDist s t < r<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>∃ x ∈ s, dist x y < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : y ∈ t<VAR>H : hausdorffDist t s < r<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>∃ x ∈ s, dist x y < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : y ∈ t<VAR>H : hausdorffDist t s < r<VAR>fin : hausdorffEdist t s ≠ ⊤<GOAL>∃ x ∈ s, dist x y < r
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk (-m) s) = -(fromLocalizedModule S f) (LocalizedModule.mk m s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : ι → α<VAR>x : α<GOAL>range f ⊆ {x} ↔ f = const ι x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<GOAL>ContinuousWithinAt f s b ↔ Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → α<VAR>g✝ : β → β<VAR>x : α × β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<VAR>f : α → α<VAR>g : β → β<VAR>fst✝ : α<VAR>snd✝ : β<GOAL>∀ (c : ℕ), minimalPeriod (Prod.map f g) (fst✝, snd✝) ∣ c ↔ (minimalPeriod f (fst✝, snd✝).1).lcm (minimalPeriod g (fst✝, snd✝).2) ∣ c
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(P.isoLeftDerivedObj F n).inv ≫ (F.leftDerived n).map f = (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map φ ≫ (Q.isoLeftDerivedObj F n).inv
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : UniformSpace X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsGδ s
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : UniformSpace X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>hs : IsClosed s<VAR>U : ℕ → Set (X × X)<VAR>hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)<VAR>hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)<GOAL>IsGδ s
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : UniformSpace X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>hs : IsClosed s<VAR>U : ℕ → Set (X × X)<VAR>hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)<VAR>hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)<GOAL>IsGδ (⋂ i, ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : UniformSpace X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>hs : IsClosed s<VAR>U : ℕ → Set (X × X)<VAR>hUo : ∀ (i : ℕ), U i ∈ 𝓤 X ∧ IsOpen (U i)<VAR>hU : (𝓤 X).HasBasis (fun x => True) fun i => id (U i)<VAR>n : ℕ<VAR>x✝ : n ∈ fun i => True<GOAL>IsOpen (⋃ x ∈ s, UniformSpace.ball x (id (U n)))
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F✝ α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F✝ α β<VAR>C : ℝ<VAR>f✝ g : α →C₀ β<VAR>ι : Type u_2<VAR>F : ι → α →C₀ β<VAR>f : α →C₀ β<VAR>l : Filter ι<GOAL>Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys : List α<VAR>n : ℕ<GOAL>List.sym 1 xs = map (fun x => x ::ₛ Sym.nil) xs
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → β → α<VAR>hα : (𝓤 α).HasBasis p s<GOAL>UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → β → α<VAR>hα : (𝓤 α).HasBasis p s<GOAL>(∀ (i : κ), p i → ∀ᶠ (x : β × β) in 𝓤 β, ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hx : x ∉ periodicPts f<GOAL>minimalPeriod f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>p : β → Prop<GOAL>(∀ y ∈ f.range, p y) ↔ ∀ (x : α), p (↑f x)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) = multinomial {a, b} (Function.update f a (f a).succ) + multinomial {a, b} (Function.update f b (f b).succ)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + f b).choose (f a).succ + (f a + (f b).succ).choose (f a)