ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>X : Type u<VAR>inst✝³ : MulAction M X<VAR>x : X<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>H : Type u_3<VAR>inst✝ : Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<VAR>z : X<VAR>γ₁ γ₂ : G<VAR>hy : ⟨(), γ₁⁻¹ • z⟩ = ⟨(), γ₁⁻¹ • z⟩<GOAL>{ obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map ((eqToHom ⋯ ≫ homOfPair (γ₁⁻¹ • z) γ₂ ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ homOfPair z γ₁ ≫ eqToHom ⋯) = { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (eqToHom ⋯ ≫ homOfPair (γ₁⁻¹ • z) γ₂ ≫ eqToHom ⋯) ≫ { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (eqToHom ⋯ ≫ homOfPair z γ₁ ≫ eqToHom ⋯)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>a : R<VAR>p q : R[X]<VAR>h : C a ∣ p - q<GOAL>gcd a p.content = gcd a q.content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>a : R<VAR>p q : R[X]<VAR>h : C a ∣ p - q<GOAL>gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) = gcd a q.content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>a : R<VAR>p q : R[X]<VAR>h : C a ∣ p - q<GOAL>gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) = gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>a : R<VAR>p q : R[X]<VAR>h : C a ∣ p - q<GOAL>∀ x ∈ Finset.range (max p.natDegree q.natDegree).succ, a ∣ p.coeff x - q.coeff x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>a : R<VAR>p q : R[X]<VAR>x : ℕ<VAR>a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ<VAR>w : R[X]<VAR>hw : p - q = C a * w<GOAL>a ∣ p.coeff x - q.coeff x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>a : R<VAR>p q : R[X]<VAR>x : ℕ<VAR>a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ<VAR>w : R[X]<VAR>hw : p - q = C a * w<GOAL>p.coeff x - q.coeff x = a * w.coeff x
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | X ω ≤ ε}).toReal ≤ rexp (-t * ε + cgf X μ t)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ 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>x ∈ Submodule.span ℤ (Set.range ⇑(integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>ha : ρ.fst {a} ≠ 0<GOAL>(ρCond a) univ = 1
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<GOAL>∀ᵐ (x : ℝ) ∂μ.restrict s, p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<GOAL>∀ᵐ (x : ℝ) ∂μ.restrict s, p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<GOAL>∀ᵐ (x : ℝ) ∂μ.restrict s, p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<VAR>this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p<GOAL>∀ᵐ (x : ℝ) ∂μ.restrict s, p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<VAR>this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p<GOAL>∀ᵐ (x : ℝ) ∂μ.restrict (s \ u ∪ ⋃ p ∈ A, s ∩ T p), p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<VAR>this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p<GOAL>(∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>s ⊆ insert a t ↔ s.erase a ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>(∀ ⦃x : α⦄, x ∈ s → ¬x = a → x ∈ t) ↔ ∀ ⦃x : α⦄, x ≠ a → x ∈ s → x ∈ t
<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>r✝ p q : α → α → Prop<VAR>f g : ι → α<VAR>s✝ t u : Set α<VAR>a b : α<VAR>r : α → α → Prop<VAR>s : Set (Set α)<VAR>h : DirectedOn (fun x x_1 => x ⊆ x_1) s<GOAL>(⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>n : ℕ<VAR>h : s.Nodup<VAR>hn : n ≠ 0<GOAL>s ≤ n • t ↔ s ≤ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s✝ t : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>n : α<VAR>h : ∀ x ∈ s, x ≤ n<GOAL>s.prod ≤ n ^ card s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a n : α<VAR>a✝ : List α<VAR>h : ∀ x ∈ ⟦a✝⟧, x ≤ n<GOAL>prod ⟦a✝⟧ ≤ n ^ card ⟦a✝⟧
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>f : { x // x ∈ m } → β<VAR>g : α → β<VAR>hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x<GOAL>∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m✝ : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b m : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>ho : m ∈ foldl (argAux r) o (tl ++ [a])<GOAL>¬r b m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m✝ : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b m : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c<GOAL>¬r b m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m✝ : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b m : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c<VAR>c : α<VAR>hf : foldl (argAux r) o tl = some c<GOAL>¬r b m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m✝ : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b m : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>c : α<VAR>ho : (Option.casesOn (some c) (some a) fun c => if r a c then some a else some c) = some m<VAR>hf : foldl (argAux r) o tl = some c<GOAL>¬r b m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m✝ : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b m : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>c : α<VAR>ho : (if r a c then some a else some c) = some m<VAR>hf : foldl (argAux r) o tl = some c<GOAL>¬r b m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>c : α<VAR>hf : foldl (argAux r) o tl = some c<VAR>hac : r a c<VAR>h : b ∈ tl<GOAL>¬r b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>c : α<VAR>hf : foldl (argAux r) o tl = some c<VAR>hac : r a c<VAR>h : b ∈ [a]<GOAL>¬r b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>c : α<VAR>hf : foldl (argAux r) o tl = some c<VAR>hac : ¬r a c<VAR>h : b ∈ tl<GOAL>¬r b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o✝ : Option α<VAR>a✝ m : α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>tl : List α<VAR>a : α<VAR>ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m<VAR>b : α<VAR>o : Option α<VAR>hb : b ∈ tl ++ [a]<VAR>c : α<VAR>hf : foldl (argAux r) o tl = some c<VAR>hac : ¬r a c<VAR>h : b ∈ [a]<GOAL>¬r b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype ↑s<VAR>hs : s.Nontrivial<GOAL>s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝¹ : CompleteLinearOrder γ<VAR>inst✝ : DenselyOrdered γ<VAR>f : α → γ<GOAL>f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>h : (f ^ n) x = x + ↑m<VAR>hn : 0 < n<GOAL>τ f = ↑m / ↑n
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>h : (f ^ n) x = x + ↑m<VAR>hn : 0 < n<VAR>this : τ (f ^ n) = ↑m<GOAL>τ f = ↑m / ↑n
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>h : (f ^ n) x = x + ↑m<VAR>hn : 0 < n<VAR>this : τ f * ↑n = ↑m<GOAL>↑n ≠ 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<GOAL>((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom = (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<GOAL>(TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom) = (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<GOAL>(TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) = (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<GOAL>∀ (a : X), (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle a = (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<GOAL>(TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x = (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<GOAL>((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 = ((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<GOAL>∀ (a : Y), ((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle a = ((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<GOAL>((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y = ((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<GOAL>(((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 = (((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<GOAL>∀ (a : Z), (((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle a = (((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<GOAL>(((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle z = (((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle z
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<GOAL>((((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle z) 1 = ((((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle z) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<GOAL>∀ (a : X ⊗ Y ⊗ Z), (((((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle z) 1) a = (((((TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y)).compr₂ ((TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z)).compr₂ ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)) ∘ₗ Finsupp.lsingle x) 1 ∘ₗ Finsupp.lsingle y) 1 ∘ₗ Finsupp.lsingle z) 1) a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<VAR>a : X ⊗ Y ⊗ Z<GOAL>(Finsupp.mapDomain (α_ X Y Z).hom ((finsuppTensorFinsupp' R (X ⊗ Y) Z) ((finsuppTensorFinsupp' R X Y) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) ⊗ₜ[R] Finsupp.single z 1))) a = ((finsuppTensorFinsupp' R X (Y ⊗ Z)) (Finsupp.single x 1 ⊗ₜ[R] (finsuppTensorFinsupp' R Y Z) (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1))) a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<VAR>a : X ⊗ Y ⊗ Z<GOAL>(Finsupp.single (x, y, z) 1) a = (Finsupp.single (x, y, z) 1) a
<VAR>a b m✝ n✝ p : ℕ<VAR>β : Type u_1<VAR>inst✝ : CommMonoid β<VAR>m n : ℕ<VAR>f : ℕ → β<GOAL>(m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
<VAR>a b m n✝ p : ℕ<VAR>β : Type u_1<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>f : ℕ → β<GOAL>(gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f
<VAR>a b m✝ n✝ p : ℕ<VAR>β : Type u_1<VAR>inst✝ : CommMonoid β<VAR>m n : ℕ<VAR>f : ℕ → β<VAR>hm₀ : m ≠ 0<GOAL>(m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
<VAR>a b m✝ n p : ℕ<VAR>β : Type u_1<VAR>inst✝ : CommMonoid β<VAR>m : ℕ<VAR>f : ℕ → β<VAR>hm₀ : m ≠ 0<GOAL>(m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f
<VAR>a b m✝ n✝ p : ℕ<VAR>β : Type u_1<VAR>inst✝ : CommMonoid β<VAR>m n : ℕ<VAR>f : ℕ → β<VAR>hm₀ : m ≠ 0<VAR>hn₀ : n ≠ 0<GOAL>(m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<GOAL>chaar K₀ K₁ ≤ chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>chaar K₀ K₁ ≤ chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>0 ≤ chaar K₀ K₂ - chaar K₀ K₁
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>chaar K₀ ∈ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0