ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>W₂ : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>Q₂ : Type u_8<VAR>inst✝¹⁶ : NormedAddCommGroup V<VAR>inst✝¹⁵ : MetricSpace P<VAR>inst✝¹⁴ : NormedAddTorsor V P<VAR>inst✝¹³ : NormedAddCommGroup W<VAR>inst✝¹² : MetricSpace Q<VAR>inst✝¹¹ : NormedAddTorsor W Q<VAR>inst✝¹⁰ : NormedAddCommGroup W₂<VAR>inst✝⁹ : MetricSpace Q₂<VAR>inst✝⁸ : NormedAddTorsor W₂ Q₂<VAR>inst✝⁷ : NormedField R<VAR>inst✝⁶ : NormedSpace R V<VAR>inst✝⁵ : NormedSpace R W<VAR>inst✝⁴ : NormedSpace R W₂<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : NormedSpace 𝕜 W₂<VAR>f : P →ᴬ[R] Q<VAR>h₁ : f.contLinear = 0 ↔ f.linear = 0<VAR>h₂ : ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q<GOAL>f.linear = 0 ↔ ∃ q, f.toAffineMap = AffineMap.const R P q
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<GOAL>DFinsupp.equivFunOnFintype.symm (Pi.single i m) = (lof R ι M i) m
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<GOAL>DFinsupp.single i m = (lof R ι M i) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω✝ : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>inst✝² : NormedAddCommGroup F✝<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ✝<VAR>X✝ : α → β<VAR>Y : α → Ω✝<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω✝<VAR>t : Set β<VAR>f✝ : β × Ω✝ → F✝<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : Measure Ω<VAR>inst✝ : TopologicalSpace F<VAR>f : Ω → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω✝ : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>inst✝² : NormedAddCommGroup F✝<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ✝<VAR>X✝ : α → β<VAR>Y : α → Ω✝<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω✝<VAR>t : Set β<VAR>f✝ : β × Ω✝ → F✝<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : Measure Ω<VAR>inst✝ : TopologicalSpace F<VAR>f : Ω → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>(fun x => f x.2) =ᶠ[ae (Measure.map (fun ω => (X ω, ω)) μ)] fun x => AEStronglyMeasurable.mk f hf x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω✝ : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>inst✝² : NormedAddCommGroup F✝<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ✝<VAR>X✝ : α → β<VAR>Y : α → Ω✝<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω✝<VAR>t : Set β<VAR>f✝ : β × Ω✝ → F✝<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : Measure Ω<VAR>inst✝ : TopologicalSpace F<VAR>f : Ω → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>Measure.QuasiMeasurePreserving Prod.snd (Measure.map (fun ω => (X ω, ω)) μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω✝ : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>inst✝² : NormedAddCommGroup F✝<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ✝<VAR>X✝ : α → β<VAR>Y : α → Ω✝<VAR>mβ : MeasurableSpace β<VAR>s✝ : Set Ω✝<VAR>t : Set β<VAR>f✝ : β × Ω✝ → F✝<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : Measure Ω<VAR>inst✝ : TopologicalSpace F<VAR>f : Ω → F<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>hμs : μ s = 0<GOAL>(Measure.map Prod.snd (Measure.map (fun ω => (X ω, ω)) μ)) s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω✝ : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>inst✝² : NormedAddCommGroup F✝<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ✝<VAR>X✝ : α → β<VAR>Y : α → Ω✝<VAR>mβ : MeasurableSpace β<VAR>s✝ : Set Ω✝<VAR>t : Set β<VAR>f✝ : β × Ω✝ → F✝<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : Measure Ω<VAR>inst✝ : TopologicalSpace F<VAR>f : Ω → F<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>hμs : μ s = 0<GOAL>(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω✝ : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>inst✝² : NormedAddCommGroup F✝<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ✝<VAR>X✝ : α → β<VAR>Y : α → Ω✝<VAR>mβ : MeasurableSpace β<VAR>s✝ : Set Ω✝<VAR>t : Set β<VAR>f✝ : β × Ω✝ → F✝<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : Measure Ω<VAR>inst✝ : TopologicalSpace F<VAR>f : Ω → F<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>hμs : μ s = 0<GOAL>Measurable Prod.snd
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.2905, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>n : ℕ<VAR>i : [n] ⟶ [n + 1]<VAR>inst✝ : Mono i<VAR>hi : Isδ₀ i<GOAL>i = SimplexCategory.δ 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.2905, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>inst✝ : Mono (SimplexCategory.δ j)<VAR>hi : Isδ₀ (SimplexCategory.δ j)<GOAL>SimplexCategory.δ j = SimplexCategory.δ 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.2905, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>inst✝ : Mono (SimplexCategory.δ j)<VAR>hi : j = 0<GOAL>SimplexCategory.δ j = SimplexCategory.δ 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<GOAL>extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<GOAL>extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<VAR>eq3 : (extendIdealTo i f h y) (r - snd i x) = ↑(extensionOfMax i f).toLinearPMap ⟨(r - snd i x) • y, ⋯⟩<GOAL>extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<VAR>eq3 : (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)<GOAL>extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<VAR>eq3 : (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)<GOAL>↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<VAR>eq3 : (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)<GOAL>↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) = ↑(extensionOfMax i f).toLinearPMap ⟨a + (r • y - snd i x • y), ⋯⟩ + (extendIdealTo i f h y) (snd i x)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<VAR>eq3 : (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)<GOAL>↑(fst i x) = a + (r • y - snd i x • y)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>r : R<VAR>a : N<VAR>ha : a ∈ (extensionOfMax i f).domain<VAR>eq1 : ↑x = ↑⟨a, ha⟩ + r • y<VAR>eq2 : ↑(fst i x) - a = (r - snd i x) • y<VAR>eq3 : (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)<GOAL>↑(fst i x) = ↑x - snd i x • y
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>1 ≤ o ↔ 0 < o
<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>ι : Type u_11<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K V<VAR>i : ι<GOAL>(B.dualBasis hB (B.flip.dualBasis ⋯ b)) i = b 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>ι : Type u_11<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι K V<VAR>i j : ι<GOAL>(B ((B.dualBasis hB (B.flip.dualBasis ⋯ b)) i)) ((B.flip.dualBasis ⋯ b) j) = (B (b i)) ((B.flip.dualBasis ⋯ b) j)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>f : R[X]<VAR>h : IsAdjoinRoot S f<VAR>x : S<GOAL>(lift (algebraMap R S) h.root ⋯ h) x = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsIntegralClosure A R B<VAR>x y : B<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>(algebraMap A B) (mk' A (x + y) ⋯) = (algebraMap A B) (mk' A x hx + mk' A y hy)
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = a + c<VAR>ha : a < ℵ₀<GOAL>b = c
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = a + c<VAR>ha : a < ℵ₀<VAR>hb : ℵ₀ ≤ b<GOAL>b = c
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = a + c<VAR>ha : a < ℵ₀<VAR>hb : b < ℵ₀<GOAL>b = c
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ G'<VAR>hfs : ContinuousWithinAt f s x<VAR>hxe' : f x ∈ e'.source<GOAL>P (↑e' ∘ f) s x ↔ P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ G'<VAR>hfs : ContinuousWithinAt f s x<VAR>hxe' : f x ∈ e'.source<VAR>h2f : f ⁻¹' e'.source ∈ 𝓝[s] x<GOAL>P (↑e' ∘ f) s x ↔ P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ G'<VAR>hfs : ContinuousWithinAt f s x<VAR>hxe' : f x ∈ e'.source<VAR>h2f : f ⁻¹' e'.source ∈ 𝓝[s] x<VAR>h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x<GOAL>P (↑e' ∘ f) s x ↔ P f s x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b c a : α<GOAL>￢⊥ ≤ a ↔ ⊤ ≤ a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.97033, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>i j : ℤ<VAR>hij : i + 1 = j<GOAL>homotopyCofiber.d φ i j ≫ (Cochain.ofHoms (homotopyCofiber.sndX φ)).v j j ⋯ = homotopyCofiber.fstX φ i j hij ≫ φ.f j + (Cochain.ofHoms (homotopyCofiber.sndX φ)).v i i ⋯ ≫ G.d i j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.97033, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>i j : ℤ<VAR>hij : i + 1 = j<GOAL>homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j = homotopyCofiber.fstX φ i j hij ≫ φ.f j + homotopyCofiber.sndX φ i ≫ G.d i j
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : J.IsGeneratedByOneHypercovers<VAR>P : Cᵒᵖ ⥤ A<GOAL>IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork P))
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
<VAR>α : Type u_1<VAR>inst✝ : OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Ioo (a + ↑n) (a + ↑n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>f : β → ℝ≥0∞<GOAL>(∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>f : β → ℝ≥0∞<GOAL>(∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<GOAL>(toMatrixAlgEquiv v₁) id = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>n : ℕ<VAR>a : R<VAR>p : R[ℕ]<GOAL>({ toFinsupp := p } * C a).coeff n = { toFinsupp := p }.coeff n * a
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>n : ℕ<VAR>a : R<VAR>p : R[ℕ]<GOAL>(p * Finsupp.single 0 a) n = p n * a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>r : R<VAR>hr : r * x.leadingCoeff = 1<VAR>hx : ¬x = 0<GOAL>0 < (1 - (single (-x.order)) r * x).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>r : R<VAR>hr : r * x.leadingCoeff = 1<VAR>hx : ¬x = 0<VAR>hrz : r ≠ 0<GOAL>0 < (1 - (single (-x.order)) r * x).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>r : R<VAR>hr : r * x.leadingCoeff = 1<VAR>hx : ¬x = 0<VAR>hrz : r ≠ 0<GOAL>0 ≤ min (orderTop 1) ((single (-x.order)) r * x).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>r : R<VAR>hr : r * x.leadingCoeff = 1<VAR>hx : ¬x = 0<VAR>hrz : r ≠ 0<VAR>h : 0 = (1 - (single (-x.order)) r * x).orderTop<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ι → ℝ<GOAL>volume (Icc a b) = ∏ i : ι, ofReal (b i - a i)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ι → ℝ<GOAL>∏ i : ι, volume (Icc (a i) (b i)) = ∏ i : ι, ofReal (b i - a i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c ≤ 0<VAR>h : b ≤ a<GOAL>a / c ≤ b / c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c ≤ 0<VAR>h : b ≤ a<GOAL>a * (1 / c) ≤ b * (1 / c)
<VAR>R : Type u<VAR>n : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>J✝ : Matrix n n R<VAR>u : Rˣ<VAR>J A : Matrix n n R<GOAL>A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
<VAR>R : Type u<VAR>n : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>J✝ : Matrix n n R<VAR>u : Rˣ<VAR>J A : Matrix n n R<GOAL>Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A