ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this : DecidableEq ι<VAR>disj : Disjoint s (image (fun z => ↑z) s')<GOAL>s'.card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this✝ : DecidableEq ι<VAR>disj : Disjoint s (image (fun z => ↑z) s')<VAR>this : s'.card = (s ∪ image (fun z => ↑z) s').card - s.card<GOAL>s'.card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this✝ : DecidableEq ι<VAR>disj : Disjoint s (image (fun z => ↑z) s')<VAR>this : s'.card = (s ∪ image (fun z => ↑z) s').card - s.card<GOAL>(s ∪ image (fun z => ↑z) s').card - (s.biUnion t).card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this✝ : DecidableEq ι<VAR>disj : Disjoint s (image (fun z => ↑z) s')<VAR>this : s'.card = (s ∪ image (fun z => ↑z) s').card - s.card<GOAL>((s ∪ image (fun z => ↑z) s').biUnion t).card - (s.biUnion t).card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this✝ : DecidableEq ι<VAR>disj : Disjoint s (image (fun z => ↑z) s')<VAR>this : s'.card = (s ∪ image (fun z => ↑z) s').card - s.card<GOAL>((s ∪ image (fun z => ↑z) s').biUnion t \ s.biUnion t).card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this✝ : DecidableEq ι<VAR>disj : Disjoint s (image (fun z => ↑z) s')<VAR>this : s'.card = (s ∪ image (fun z => ↑z) s').card - s.card<GOAL>s.biUnion t ⊆ (s ∪ image (fun z => ↑z) s').biUnion t
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ClosedIciTopology α<VAR>f : β → α<VAR>a✝ b : α<VAR>s✝ s : Set α<VAR>a : α<GOAL>a ∈ lowerBounds (closure s) ↔ a ∈ lowerBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Field L<VAR>nf : NumberField K<VAR>x : 𝓞 K<GOAL>IsIntegral ℤ x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Field L<VAR>nf : NumberField K<VAR>x : 𝓞 K<VAR>P : Polynomial ℤ<VAR>hPm : P.Monic<VAR>hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0<GOAL>IsIntegral ℤ x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Field L<VAR>nf : NumberField K<VAR>x : 𝓞 K<VAR>P : Polynomial ℤ<VAR>hPm : P.Monic<VAR>hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0<GOAL>Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c d a b : G<GOAL>a * b / a = b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>n : ℕ<VAR>hn : (⇑φ)^[n] = _root_.id<VAR>g : G<GOAL>(List.map (fun k => (⇑φ)^[k] g) (List.range n)).prod = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>n : ℕ<VAR>hn : (⇑φ)^[n] = _root_.id<VAR>g : G<GOAL>(List.map (fun k => (⇑φ)^[k] (commutatorMap (⇑φ) g)) (List.range n)).prod = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>n : ℕ<VAR>hn : (⇑φ)^[n] = _root_.id<VAR>g : G<GOAL>(List.map (fun k => (⇑φ)^[k] g / (⇑φ)^[k.succ] g) (List.range n)).prod = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<GOAL>∃ x, induce (↑x) G = ⊤ ∧ x.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<GOAL>induce (↑(map f.toEmbedding univ)) G = ⊤ ∧ (map f.toEmbedding univ).card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<GOAL>induce (↑(map f.toEmbedding univ)) G = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<VAR>v : α<VAR>hv : v ∈ ↑(map f.toEmbedding univ)<VAR>w : α<VAR>hw : w ∈ ↑(map f.toEmbedding univ)<GOAL>(induce (↑(map f.toEmbedding univ)) G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<VAR>v : α<VAR>hv✝ : v ∈ ↑(map f.toEmbedding univ)<VAR>w : α<VAR>hw✝ : w ∈ ↑(map f.toEmbedding univ)<VAR>hv : ∃ x, f.toEmbedding x = v<VAR>hw : ∃ x, f.toEmbedding x = w<GOAL>(induce (↑(map f.toEmbedding univ)) G).Adj ⟨v, hv✝⟩ ⟨w, hw✝⟩ ↔ ⊤.Adj ⟨v, hv✝⟩ ⟨w, hw✝⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<VAR>v' : Fin n<VAR>hv : f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)<VAR>w' : Fin n<VAR>hw : f.toEmbedding w' ∈ ↑(map f.toEmbedding univ)<GOAL>(induce (↑(map f.toEmbedding univ)) G).Adj ⟨f.toEmbedding v', hv⟩ ⟨f.toEmbedding w', hw⟩ ↔ ⊤.Adj ⟨f.toEmbedding v', hv⟩ ⟨f.toEmbedding w', hw⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<VAR>v' : Fin n<VAR>hv : f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)<VAR>w' : Fin n<VAR>hw : f.toEmbedding w' ∈ ↑(map f.toEmbedding univ)<GOAL>G.Adj ((Embedding.subtype fun x => x ∈ ↑(map f.toEmbedding univ)) ⟨f v', ⋯⟩) ((Embedding.subtype fun x => x ∈ ↑(map f.toEmbedding univ)) ⟨f w', ⋯⟩) ↔ ¬v' = w'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<VAR>v' : Fin n<VAR>hv : f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)<VAR>w' : Fin n<VAR>hw : f.toEmbedding w' ∈ ↑(map f.toEmbedding univ)<GOAL>⊤.Adj v' w' ↔ ¬v' = w'
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>x y z : ℝ<VAR>hfs : HasConstantSpeedOnWith f (Icc x y) l<VAR>hft : HasConstantSpeedOnWith f (Icc y z) l<GOAL>HasConstantSpeedOnWith f (Icc x z) l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>x y z : ℝ<VAR>hfs : HasConstantSpeedOnWith f (Icc x y) l<VAR>hft : HasConstantSpeedOnWith f (Icc y z) l<VAR>xy : x ≤ y<GOAL>HasConstantSpeedOnWith f (Icc x z) l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>x y z : ℝ<VAR>hfs : HasConstantSpeedOnWith f (Icc x y) l<VAR>hft : HasConstantSpeedOnWith f (Icc y z) l<VAR>yx : y ≤ x<GOAL>HasConstantSpeedOnWith f (Icc x z) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b : α<VAR>inst✝ : OrderBot α<GOAL>a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
<VAR>f : ℕ → ℝ≥0<VAR>hf : Summable f<GOAL>Tendsto f atTop (𝓝 0)
<VAR>f : ℕ → ℝ≥0<VAR>hf : Summable f<GOAL>Tendsto f cofinite (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<GOAL>_root_.Disjoint s t ∨ (s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<GOAL>_root_.Disjoint s t ∨ ¬_root_.Disjoint s t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : DenselyOrdered α<GOAL>Ioo a b = ∅ ↔ ¬a < b
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>terminates : (of v).Terminates<GOAL>∃ q, v = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ : ℕ<VAR>terminates : (of v).Terminates<VAR>n : ℕ<VAR>v_eq_conv : v = (of v).convs n<GOAL>∃ q, v = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ : ℕ<VAR>terminates : (of v).Terminates<VAR>n : ℕ<VAR>v_eq_conv : v = (of v).convs n<VAR>q : ℚ<VAR>conv_eq_q : (of v).convs n = ↑q<GOAL>∃ q, v = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ : ℕ<VAR>terminates : (of v).Terminates<VAR>n : ℕ<VAR>v_eq_conv : v = (of v).convs n<VAR>q : ℚ<VAR>conv_eq_q : (of v).convs n = ↑q<VAR>this : v = ↑q<GOAL>∃ q, v = ↑q
<VAR>x : PSet<VAR>a : ZFSet<VAR>h : a ∈ (mk x).toSet<GOAL>x.Nonempty
<VAR>x a✝ : PSet<VAR>h : ⟦a✝⟧ ∈ (mk x).toSet<GOAL>x.Nonempty
<VAR>w : uliftFunctor.{u, v}.EssSurj<VAR>α : Type (max u v)<GOAL>Small.{v, max u v} α
<VAR>w : uliftFunctor.{u, v}.EssSurj<VAR>α : Type (max u v)<VAR>a' : Type v<VAR>m : uliftFunctor.{u, v}.obj a' ≅ α<GOAL>Small.{v, max u v} α
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>L : Type u_3<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>S : Set K<VAR>hprim : adjoin F S = ⊤<GOAL>restrictScalars F (adjoin E S) = restrictScalars F ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<GOAL>(Imp.mapVal f m).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<VAR>h₁ : m.size = m.buckets.size<VAR>h₂ : m.buckets.WF<GOAL>(Imp.mapVal f m).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<VAR>h₁ : m.size = m.buckets.size<VAR>h₂ : m.buckets.WF<GOAL>m.buckets.size = Buckets.size ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩ ∧ Buckets.WF ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>a : 𝒜 0<VAR>b : ⨁ (i : ι), ℬ i<GOAL>(gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 0) a ⊗ₜ[R] b) = b ⊗ₜ[R] (lof R ι 𝒜 0) a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>a : 𝒜 0<VAR>b : ⨁ (i : ι), ℬ i<GOAL>↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) ((lof R ι 𝒜 0) a) = (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)).flip ((lof R ι 𝒜 0) a)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>a : 𝒜 0<VAR>b✝ : ⨁ (i : ι), ℬ i<VAR>i : ι<VAR>b : ℬ i<GOAL>(gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 0) a ⊗ₜ[R] (lof R ι ℬ i) b) = (lof R ι ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Tendsto (fun m => κ.densityProcess ν n a x (seq m)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Tendsto (fun m => κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → β<VAR>h : β → G γ<VAR>x : Multiset α<GOAL>traverse h (map g x) = traverse (h ∘ g) x
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → β<VAR>h : β → G γ<VAR>x : Multiset α<GOAL>∀ (a : List α), traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → β<VAR>h : β → G γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>traverse h (map g ⟦a✝⟧) = traverse (h ∘ g) ⟦a✝⟧
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → β<VAR>h : β → G γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>Coe.coe <$> Traversable.traverse h (List.map g a✝) = Coe.coe <$> Traversable.traverse (h ∘ g) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>ha : Multipliable f<GOAL>HasProd f (∏' (b : β), f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>ha : Multipliable f<GOAL>HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<GOAL>a * c ≤ b * c
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>a * c ≤ b * c
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
<GOAL>closure (range fun x => x * x) = nonneg ℤ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivAt I I' f x f'<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasMFDerivAt I I' f₁ x f'
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivWithinAt I I' f univ x f'<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasMFDerivWithinAt I I' f₁ univ x f'
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivWithinAt I I' f univ x f'<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>f₁ =ᶠ[𝓝[univ] x] f
<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>T : Type u_1<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>U : Type u_2<VAR>inst✝¹ : CommRing U<VAR>inst✝ : Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot U f<VAR>e : S ≃ₐ[R] T<VAR>a : T<GOAL>((h.ofEquiv e).aequiv h') a = (e.symm.trans (h.aequiv h')) a
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>v : M<VAR>x fx : CliffordAlgebra Q<GOAL>((contractLeftAux Q d) v) ((ι Q) v * x, ((contractLeftAux Q d) v) (x, fx)) = Q v • fx
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>v : M<VAR>x fx : CliffordAlgebra Q<GOAL>d v • ((ι Q) v * x) - (ι Q) v * (d v • x - (ι Q) v * fx) = Q v • fx
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>t u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : α ≃ᵐ β<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(Measure.comap (⇑e.symm) μ) s = (Measure.map (⇑e) μ) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : α ≃ᵐ β<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ (s : Set β), MeasurableSet s → MeasurableSet (⇑e.symm '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<GOAL>derivative (C a * X ^ 2) = C (a * 2) * X
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<GOAL>LinearIndependent R x