ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E 0)<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E ⊤)<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<VAR>hp : 0 < p.toReal<GOAL>‖-f‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x y : 𝕜<VAR>hx : x ∈ Ico a (a + p)<VAR>hy : y ∈ Ico a (a + p)<GOAL>↑x = ↑y ↔ x = y
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x y : 𝕜<VAR>hx : x ∈ Ico a (a + p)<VAR>hy : y ∈ Ico a (a + p)<VAR>h : ↑x = ↑y<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x y : 𝕜<VAR>hx : x ∈ Ico a (a + p)<VAR>hy : y ∈ Ico a (a + p)<VAR>h : (equivIco p a) ↑x = (equivIco p a) ↑y<GOAL>⟨x, hx⟩ = ⟨y, hy⟩
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x y : 𝕜<VAR>hx : x ∈ Ico a (a + p)<VAR>hy : y ∈ Ico a (a + p)<VAR>h : (equivIco p a) ↑x = (equivIco p a) ↑y<GOAL>(equivIco p a).toFun ((equivIco p a).invFun ⟨x, hx⟩) = (equivIco p a).toFun ((equivIco p a).invFun ⟨y, hy⟩)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : ι ≃ (L →ₐ[K] E)<GOAL>(algebraMap K E) (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>p : (s : Finset α) → s.Nonempty → Prop<VAR>h₀ : ∀ (a : α), p {a} ⋯<VAR>h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>p s hs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>p : (s : Finset α) → s.Nonempty → Prop<VAR>h₀ : ∀ (a : α), p {a} ⋯<VAR>h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯<VAR>a : α<VAR>hs : {a}.Nonempty<GOAL>p {a} hs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>p : (s : Finset α) → s.Nonempty → Prop<VAR>h₀ : ∀ (a : α), p {a} ⋯<VAR>h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯<VAR>s : Finset α<VAR>hs✝ : s.Nonempty<VAR>hs : s.Nontrivial<GOAL>p s hs✝
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S✝ : ComposableArrows C n<VAR>S : ComposableArrows C (n + 2)<VAR>h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : S.δ₀.Exact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S✝ : ComposableArrows C n<VAR>S : ComposableArrows C (n + 2)<VAR>h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : S.δ₀.Exact<GOAL>(mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>ball x 0 = ∅
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hi : I.IsPrimary<VAR>x y : R<VAR>x✝ : x * y ∈ I.radical<VAR>m : ℕ<VAR>hxy : (x * y) ^ m ∈ I<GOAL>x ∈ I.radical ∨ y ∈ I.radical
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hi : I.IsPrimary<VAR>x y : R<VAR>x✝ : x * y ∈ I.radical<VAR>m : ℕ<VAR>hxy : x ^ m * y ^ m ∈ I<GOAL>x ∈ I.radical ∨ y ∈ I.radical
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hi : I.IsPrimary<VAR>x y : R<VAR>x✝ : x * y ∈ I.radical<VAR>m : ℕ<VAR>hxy : x ^ m * y ^ m ∈ I<VAR>h : x ^ m ∈ I<GOAL>x ∈ I.radical ∨ y ∈ I.radical
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hi : I.IsPrimary<VAR>x y : R<VAR>x✝ : x * y ∈ I.radical<VAR>m : ℕ<VAR>hxy : x ^ m * y ^ m ∈ I<VAR>h : y ^ m ∈ I.radical<GOAL>x ∈ I.radical ∨ y ∈ I.radical
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋂₀ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋂ i ∈ s, i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝¹ : CommGroup β<VAR>inst✝ : TopologicalGroup β<VAR>hf : AEStronglyMeasurable f μ<VAR>h : AEStronglyMeasurable (f * g) μ<GOAL>g = f * g * f⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<VAR>a : α<VAR>hf : Injective f<VAR>ha : f^[m] a = f^[n] a<GOAL>f^[m - n] a = a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<VAR>a : α<VAR>hf : Injective f<VAR>ha : f^[m] a = f^[n] a<VAR>h : m ≤ n<GOAL>f^[m - n] a = a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<VAR>a : α<VAR>hf : Injective f<VAR>ha : f^[m] a = f^[n] a<VAR>h : n ≤ m<GOAL>f^[m - n] a = a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ s t : Multiset α<VAR>i : α<GOAL>(toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<GOAL>∑ i ∈ filter (fun x => j < c ^ x) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<GOAL>∑ i ∈ filter (fun x => j < c ^ x) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<VAR>A : 0 < c⁻¹ ^ 2<GOAL>∑ i ∈ filter (fun x => j < c ^ x) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<VAR>A : 0 < c⁻¹ ^ 2<VAR>B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹<GOAL>∑ i ∈ filter (fun x => j < c ^ x) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<VAR>A : 0 < c⁻¹ ^ 2<VAR>B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹<VAR>C : c⁻¹ ^ 2 < 1<GOAL>∑ i ∈ filter (fun x => j < c ^ x) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ Ici a ↔ a ≤ x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), cthickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type (max u v)<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>DirectSum.IsInternal fun p => torsionBy R M (IsPrincipal.generator ↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type (max u v)<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>x✝ : { x // x ∈ (factors ⊤.annihilator).toFinset }<GOAL>torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) = torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type (max u v)<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>x✝ : { x // x ∈ (factors ⊤.annihilator).toFinset }<VAR>p : M<GOAL>p ∈ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) ↔ p ∈ torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))
<VAR>x : ℝ<GOAL>x ∈ {x | Liouville x} ↔ x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : Monoid α<VAR>x : α<VAR>h : ¬IsUnit x<VAR>this : (p : Prop) → Decidable p<GOAL>Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : Monoid α<VAR>x : α<VAR>h : ¬IsUnit x<VAR>this : (p : Prop) → Decidable p<VAR>H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x<GOAL>Irreducible x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : Monoid α<VAR>x : α<VAR>h : ¬IsUnit x<VAR>this : (p : Prop) → Decidable p<VAR>H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x<GOAL>∀ (a b : α), x = a * b → IsUnit a ∨ IsUnit b
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : Monoid α<VAR>x : α<VAR>h✝ : ¬IsUnit x<VAR>this : (p : Prop) → Decidable p<VAR>H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x<VAR>a b : α<VAR>h : x = a * b<VAR>o : ¬(IsUnit a ∨ IsUnit b)<GOAL>False
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>inst✝ : Monoid α<VAR>x : α<VAR>h✝ : ¬IsUnit x<VAR>this : (p : Prop) → Decidable p<VAR>H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x<VAR>a b : α<VAR>h : x = a * b<VAR>o : ¬IsUnit a ∧ ¬IsUnit b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : PrimrecPred p<VAR>this : Primcodable (Subtype p) := Primcodable.subtype hp<GOAL>Primrec Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : PrimrecPred p<VAR>this : Primcodable (Subtype p) := Primcodable.subtype hp<VAR>n : ℕ<GOAL>encode (decode n) = encode (Option.map Subtype.val (decode n))
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c x : α<VAR>u₁ u₂ : αˣ<GOAL>x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
<VAR>n k : ℕ<VAR>h1 : MinFacHelper n k<VAR>h2 : 0 = n % k<GOAL>IsNat n.minFac k
<VAR>n k : ℕ<VAR>h1 : MinFacHelper n k<VAR>h2 : k ∣ n<GOAL>IsNat n.minFac k
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>c : E<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => ⟪c, f x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>c : E<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp (fun x => ⟪c, f x⟫_𝕜) 1 μ
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s✝ : Set M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : (closure L).toFun s = ⊤<VAR>Hs : ∀ x ∈ s, p x<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)<GOAL>p x
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s✝ : Set M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : (closure L).toFun s = ⊤<VAR>Hs : ∀ x ∈ s, p x<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)<VAR>this : ∀ x ∈ (closure L).toFun s, p x<GOAL>p x
<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>t : Set β<GOAL>f '' (f ⁻¹' t) = t ∩ range f
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Preregular C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<GOAL>IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Preregular C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)<GOAL>IsSheaf (regularTopology C) F
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Preregular C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)<GOAL>IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Preregular C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)<GOAL>F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>X : Set (C(α, β) × C(α, β))<GOAL>X ∈ 𝓤 C(α, β) ↔ ∃ K V, IsCompact K ∧ V ∈ 𝓤 β ∧ {fg | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X
<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₁ : a₁ ≤ a₂<VAR>h₂ : b₁ < b₂<GOAL>(a₁, b₁) < (a₂, b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R✝ : α → β → Prop<VAR>C✝ : Computation α → Computation β → Prop<VAR>R : α → β → Prop<VAR>C : Computation α → Computation β → Prop<VAR>b : β<VAR>ca : Computation α<GOAL>LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ a, a ∈ ca ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>a b : R<VAR>h : Commute a b<GOAL>a * a - b * b = (a + b) * (a - b)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y z : M<GOAL>Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y z : M<VAR>B : BilinMap R M N<VAR>h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y<GOAL>Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y z : M<VAR>B : BilinMap R M N<VAR>h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y<GOAL>Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y z : M<VAR>B : BilinMap R M N<VAR>h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y<GOAL>Q x + Q y + (B x) y + Q z + ((B x) z + (B y) z) + (Q x + Q y + Q z) = Q x + Q y + (B x) y + (Q y + Q z + (B y) z) + (Q x + Q z + (B x) z)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>q : P<GOAL>((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>q : P<VAR>hq : q ∈ affineSpan k (range ⇑b)<GOAL>((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>w : ι → k<VAR>hw : ∑ i : ι, w i = 1<VAR>hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)<GOAL>((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w)) = (Finset.affineCombination k Finset.univ ⇑b) w
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>w : ι → k<VAR>hw : ∑ i : ι, w i = 1<VAR>hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)<VAR>i : ι<GOAL>(b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w) = w i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : One γ<VAR>c : α<VAR>hc : c ≠ 0<VAR>f : β → γ<VAR>x : β<GOAL>(x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(monomial n) a * C b = (monomial n) (a * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : a₁ < a₂<GOAL>Ico a₂ b ⊆ Ioo a₁ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : a₁ < a₂<GOAL>Set.Ico a₂ b ⊆ Set.Ioo a₁ b
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>f : ContinuousMultilinearMap 𝕜 E₁ G<VAR>s : Set ι<VAR>e : α ≃ ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : (i : ι) → E₁ i<GOAL>‖f‖ * ∏ _i : { a // a ∉ s }, ‖x‖ = ‖f‖ * ‖x‖ ^ Fintype.card { a // a ∉ s }
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>f : ContinuousMultilinearMap 𝕜 E₁ G<VAR>s : Set ι<VAR>e : α ≃ ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : (i : ι) → E₁ i<GOAL>‖f‖ * ‖x‖ ^ Fintype.card { a // a ∉ s } = ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>h : LinearMap.range f' = ⊤<VAR>f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h<VAR>c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2<VAR>hc : c = f'symm.nnnorm⁻¹ / 2<GOAL>map f (𝓝 a) = 𝓝 (f a)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>h : LinearMap.range f' = ⊤<VAR>f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h<VAR>c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2<VAR>hc : c = f'symm.nnnorm⁻¹ / 2<VAR>f'symm_pos : 0 < f'symm.nnnorm<GOAL>map f (𝓝 a) = 𝓝 (f a)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>h : LinearMap.range f' = ⊤<VAR>f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h<VAR>c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2<VAR>hc : c = f'symm.nnnorm⁻¹ / 2<VAR>f'symm_pos : 0 < f'symm.nnnorm<VAR>cpos : 0 < c<GOAL>map f (𝓝 a) = 𝓝 (f a)