ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<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>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>∀ (a : Fin (Classical.choose ⋯) → M), (¬Realize φ (fun x => Sum.elim (fun x => v x) (fun x => a (Fin.cast ⋯ ((Classical.choice ⋯) x))) (f x)) fun x => a (natAdd (Classical.choose ⋯) x)) ↔ ¬φ.Realize fun a_1 => Sum.elim v (?refine_1 a) (f a_1)
<VAR>d : ℤ<VAR>h₀ : d < 0<VAR>a : Solution₁ d<GOAL>a.x = 0 ∨ a.y = 0
<VAR>d : ℤ<VAR>h₀ : d < 0<VAR>a : Solution₁ d<VAR>h : a.x ^ 2 - d * a.y ^ 2 = 1<GOAL>a.x = 0 ∨ a.y = 0
<VAR>d : ℤ<VAR>h₀ : d < 0<VAR>a : Solution₁ d<VAR>h : a.x ≠ 0 ∧ a.y ≠ 0<GOAL>a.x ^ 2 - d * a.y ^ 2 ≠ 1
<VAR>d : ℤ<VAR>h₀ : d < 0<VAR>a : Solution₁ d<VAR>h : a.x ≠ 0 ∧ a.y ≠ 0<VAR>h1 : 0 < a.x ^ 2<GOAL>a.x ^ 2 - d * a.y ^ 2 ≠ 1
<VAR>d : ℤ<VAR>h₀ : d < 0<VAR>a : Solution₁ d<VAR>h : a.x ≠ 0 ∧ a.y ≠ 0<VAR>h1 : 0 < a.x ^ 2<VAR>h2 : 0 < a.y ^ 2<GOAL>a.x ^ 2 - d * a.y ^ 2 ≠ 1
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<GOAL>W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv = (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hsm : MeasurableSet s<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>inst✝ : CircularOrder α<VAR>a b c : α<GOAL>sbtw a b c ↔ ¬btw c b a
<VAR>α : Type u_1<VAR>inst✝ : CircularOrder α<VAR>a b c : α<GOAL>btw a b c ∧ ¬btw c b a ↔ ¬btw c b a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : IsKleinFour G<VAR>x y z : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<VAR>hz : z ≠ 1<VAR>hzx : z ≠ x<VAR>hzy : z ≠ y<GOAL>z = x * y
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<GOAL>ContinuousAt (fun p => p.1 * p.2) (b, a)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a b : EReal<VAR>h : ContinuousAt (fun p => p.1 * p.2) (a, b)<VAR>x✝ : EReal × EReal<GOAL>x✝.1 * x✝.2 = ((fun p => p.1 * p.2) ∘ Prod.swap) x✝
<VAR>a✝ b✝ c : Ordinal.{u}<VAR>a b : Ordinal.{u_1}<GOAL>a ♯ b = b ♯ a
<VAR>a✝ b✝ c : Ordinal.{u}<VAR>a b : Ordinal.{u_1}<GOAL>max (b.blsub fun b' x => a ♯ b') (a.blsub fun a' x => a' ♯ b) = max (b.blsub fun a' x => a' ♯ a) (a.blsub fun b' x => b ♯ b')
<VAR>α : Type u<VAR>c d : Cardinal.{u}<GOAL>toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : (exponent G).factorization p = 0<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : (exponent G).factorization p ≠ 0<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : (exponent G).factorization p ≠ 0<VAR>he : 0 < exponent G<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<VAR>g : G<VAR>hg : g ^ (exponent G / p) ≠ 1<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<VAR>g : G<VAR>hg : g ^ (exponent G / p) ≠ 1<VAR>k : ℕ<VAR>hk : exponent G = p ^ (exponent G).factorization p * k<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<VAR>g : G<VAR>hg : g ^ (exponent G / p) ≠ 1<VAR>k : ℕ<VAR>hk : exponent G = p ^ (exponent G).factorization p * k<VAR>t : ℕ<VAR>ht : (exponent G).factorization p = t.succ<GOAL>∃ g, orderOf g = p ^ (exponent G).factorization p
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<VAR>g : G<VAR>hg : g ^ (exponent G / p) ≠ 1<VAR>k : ℕ<VAR>hk : exponent G = p ^ (exponent G).factorization p * k<VAR>t : ℕ<VAR>ht : (exponent G).factorization p = t.succ<GOAL>orderOf (g ^ k) = p ^ t.succ
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<VAR>g : G<VAR>hg : g ^ (exponent G / p) ≠ 1<VAR>k : ℕ<VAR>hk : exponent G = p ^ (exponent G).factorization p * k<VAR>t : ℕ<VAR>ht : (exponent G).factorization p = t.succ<GOAL>¬(g ^ k) ^ p ^ t = 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>this : Fact (Nat.Prime p)<VAR>h : p ∈ (exponent G).factorization.support<VAR>he : 0 < exponent G<VAR>g : G<VAR>hg : g ^ (exponent G / p) ≠ 1<VAR>k : ℕ<VAR>hk : exponent G = p ^ (exponent G).factorization p * k<VAR>t : ℕ<VAR>ht : (exponent G).factorization p = t.succ<GOAL>(g ^ k) ^ p ^ (t + 1) = 1
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<VAR>x✝ : S<GOAL>(↑↑__src✝).toFun ((algebraMap S A) x✝) = (algebraMap S (RingQuot s)) x✝
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<VAR>x✝ : S<GOAL>{ toQuot := Quot.mk (Rel s) ((algebraMap S A) x✝) } = (algebraMap S (RingQuot s)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → β<VAR>φ : α → 𝕜<VAR>hf : Integrable f μ<VAR>hφ : Memℒp φ ⊤ μ<GOAL>Integrable (φ • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → β<VAR>φ : α → 𝕜<VAR>hf : Memℒp f 1 μ<VAR>hφ : Memℒp φ ⊤ μ<GOAL>Memℒp (φ • f) 1 μ
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x y z : α<VAR>s : Set α<VAR>hf : Isometry f<GOAL>EMetric.diam (range f) = EMetric.diam univ
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x y z : α<VAR>s : Set α<VAR>hf : Isometry f<GOAL>EMetric.diam (f '' univ) = EMetric.diam univ
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftComm X i j).symm.hom = (shiftComm X j i).hom
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x + y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity p (x ^ n + y ^ n) = multiplicity p (x + y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x + y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : ↑p ∣ ↑(x + y)<VAR>hx : ¬↑p ∣ ↑x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hx : ¬↑p ∣ ↑x<VAR>n : ℕ<VAR>hn : Odd n<VAR>hxy : ↑p ∣ ↑x + ↑y<GOAL>multiplicity (↑p) (↑x ^ n + ↑y ^ n) = multiplicity (↑p) (↑x + ↑y) + multiplicity p n
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>u : αˣ<VAR>h : a ∣ b<GOAL>a * ↑u * ↑u⁻¹ = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x 0 r<VAR>y : E<VAR>hy : y ∈ EMetric.ball x r<GOAL>f y = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x 0 r<VAR>y : E<VAR>hy : y ∈ EMetric.ball x r<GOAL>(∑ k ∈ Finset.range 0, (pf k) fun x_1 => y - x) = 0
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁹ : SeminormedAddCommGroup V<VAR>inst✝⁸ : PseudoMetricSpace P<VAR>inst✝⁷ : NormedAddTorsor V P<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : MetricSpace Q<VAR>inst✝⁴ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : Invertible 2<VAR>p₁ p₂ : P<GOAL>dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝¹ t✝ s✝ : Set α<VAR>t : Set β<VAR>f✝ f : α → β<VAR>s : Set α<GOAL>(f '' s).encard ≤ s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝¹ t✝ s✝ : Set α<VAR>t : Set β<VAR>f✝ f : α → β<VAR>s : Set α<VAR>h : IsEmpty α<GOAL>(f '' s).encard ≤ s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝¹ t✝ s✝ : Set α<VAR>t : Set β<VAR>f✝ f : α → β<VAR>s : Set α<VAR>h : Nonempty α<GOAL>(f '' s).encard ≤ s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝¹ t✝ s✝ : Set α<VAR>t : Set β<VAR>f✝ f : α → β<VAR>s : Set α<VAR>h : Nonempty α<GOAL>(Function.invFunOn f s '' (f '' s)).encard ≤ s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝¹ t✝ s✝ : Set α<VAR>t : Set β<VAR>f✝ f : α → β<VAR>s : Set α<VAR>h : Nonempty α<GOAL>Function.invFunOn f s '' (f '' s) ⊆ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>(∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>t' : k<VAR>a : MonoidAlgebra k G<GOAL>(sum (t' • a) fun m t => t • f m) = (MonoidHom.id k) t' • sum a fun m t => t • f m
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>t' : k<VAR>a : MonoidAlgebra k G<GOAL>(sum a fun i c => (t' • c) • f i) = sum a fun a b => (MonoidHom.id k) t' • b • f a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>t' : k<VAR>a : MonoidAlgebra k G<GOAL>∀ (i : G), 0 • f i = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<GOAL>{ toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun (a₁ * a₂) = { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun a₁ * { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun a₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<GOAL>{ toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun (a₁ * a₂) = { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun a₁ * { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun a₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<VAR>h₂ : ∀ (m : G) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂<GOAL>{ toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun (a₁ * a₂) = { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun a₁ * { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun a₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<VAR>h₂ : ∀ (m : G) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂<GOAL>(sum (sum a₁ fun a₁ b₁ => sum a₂ fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)) fun m t => t • f m) = sum a₁ fun x' v' => sum a₂ fun x v => (v' * v) • f (x' * x)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<VAR>h₂ : ∀ (m : G) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂<GOAL>(sum a₁ fun a b => sum (sum a₂ fun a₂ b₂ => single (a * a₂) (b * b₂)) g) = sum a₁ fun x' v' => sum a₂ fun x v => (v' * v) • f (x' * x)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<VAR>h₂ : ∀ (m : G) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂<VAR>x✝¹ : G<VAR>x✝ : k<GOAL>sum (sum a₂ fun a₂ b₂ => single (x✝¹ * a₂) (x✝ * b₂)) g = sum a₂ fun x v => (x✝ * v) • f (x✝¹ * x)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<VAR>h₂ : ∀ (m : G) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂<VAR>x✝¹ : G<VAR>x✝ : k<GOAL>(sum a₂ fun a b => sum (single (x✝¹ * a) (x✝ * b)) g) = sum a₂ fun x v => (x✝ * v) • f (x✝¹ * x)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>a₁ a₂ : MonoidAlgebra k G<VAR>g : G → k → A := fun m t => t • f m<VAR>h₁ : ∀ (m : G), g m 0 = 0<VAR>h₂ : ∀ (m : G) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂<VAR>x✝³ : G<VAR>x✝² : k<VAR>x✝¹ : G<VAR>x✝ : k<GOAL>sum (single (x✝³ * x✝¹) (x✝² * x✝)) g = (x✝² * x✝) • f (x✝³ * x✝¹)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>f : G →ₙ* A<VAR>m : G<GOAL>((fun F => F.toMulHom.comp (ofMagma k G)) ((fun f => let __src := liftAddHom fun x => (smulAddHom k A).flip (f x); { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }) f)) m = f m
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>F : MonoidAlgebra k G →ₙₐ[k] A<GOAL>(fun f => let __src := liftAddHom fun x => (smulAddHom k A).flip (f x); { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }) ((fun F => F.toMulHom.comp (ofMagma k G)) F) = F
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : Semiring k<VAR>inst✝⁵ : DistribSMul R k<VAR>inst✝⁴ : Mul G<VAR>A : Type u₃<VAR>inst✝³ : NonUnitalNonAssocSemiring A<VAR>inst✝² : Module k A<VAR>inst✝¹ : IsScalarTower k A A<VAR>inst✝ : SMulCommClass k A A<VAR>F : MonoidAlgebra k G →ₙₐ[k] A<VAR>m : G<GOAL>(((fun f => let __src := liftAddHom fun x => (smulAddHom k A).flip (f x); { toFun := fun a => sum a fun m t => t • f m, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }) ((fun F => F.toMulHom.comp (ofMagma k G)) F)).toMulHom.comp (ofMagma k G)) m = (F.toMulHom.comp (ofMagma k G)) m
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<VAR>hbc : b ^^^ c = a ^^^ v<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<VAR>hbc : b ^^^ c = a ^^^ v<VAR>i : ℕ<VAR>hi : (a ^^^ (b ^^^ c)).testBit i = true<VAR>hi' : ∀ (j : ℕ), i < j → (a ^^^ (b ^^^ c)).testBit j = false<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<VAR>hbc : b ^^^ c = a ^^^ v<VAR>i : ℕ<VAR>hi : (a ^^^ (b ^^^ c)).testBit i = true<VAR>hi' : ∀ (j : ℕ), i < j → (a ^^^ (b ^^^ c)).testBit j = false<VAR>this : a.testBit i = true ∨ b.testBit i = true ∨ c.testBit i = true<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h✝ : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<VAR>hbc : b ^^^ c = a ^^^ v<VAR>i : ℕ<VAR>hi : (a ^^^ (b ^^^ c)).testBit i = true<VAR>hi' : ∀ (j : ℕ), i < j → (a ^^^ (b ^^^ c)).testBit j = false<VAR>h : a.testBit i = true<GOAL>a ^^^ v < a
<VAR>a b c : ℕ<VAR>h✝ : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<VAR>hbc : b ^^^ c = a ^^^ v<VAR>i : ℕ<VAR>hi : (a ^^^ (b ^^^ c)).testBit i = true<VAR>hi' : ∀ (j : ℕ), i < j → (a ^^^ (b ^^^ c)).testBit j = false<VAR>h : b.testBit i = true<GOAL>b ^^^ v < b
<VAR>a b c : ℕ<VAR>h✝ : a ≠ b ^^^ c<VAR>v : ℕ := a ^^^ (b ^^^ c)<VAR>hv : v = a ^^^ (b ^^^ c)<VAR>hab : a ^^^ b = c ^^^ v<VAR>hac : a ^^^ c = b ^^^ v<VAR>hbc : b ^^^ c = a ^^^ v<VAR>i : ℕ<VAR>hi : (a ^^^ (b ^^^ c)).testBit i = true<VAR>hi' : ∀ (j : ℕ), i < j → (a ^^^ (b ^^^ c)).testBit j = false<VAR>h : c.testBit i = true<GOAL>c ^^^ v < c
<VAR>f g : CircleDeg1Lift<VAR>x : ℕ → ℝ<VAR>C : ℝ<VAR>H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C<GOAL>Tendsto (fun n => x (2 ^ n) / 2 ^ n) atTop (𝓝 (τ f))
<VAR>f g : CircleDeg1Lift<VAR>x : ℕ → ℝ<VAR>C : ℝ<VAR>H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C<GOAL>ℕ → ℝ
<VAR>f g : CircleDeg1Lift<VAR>x : ℕ → ℝ<VAR>C : ℝ<VAR>H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C<GOAL>∀ (t : ℕ), dist (f.transnumAuxSeq t) (x (2 ^ t) / 2 ^ t) ≤ ?m.120971 t
<VAR>f g : CircleDeg1Lift<VAR>x : ℕ → ℝ<VAR>C : ℝ<VAR>H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C<GOAL>Tendsto ?m.120971 atTop (𝓝 0)
<VAR>x : ℂ<GOAL>cexp x ∈ {0}ᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ n, some a ∈ s.get? n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons b s').get? n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∀ (s : WSeq α), (∃ n, some a ∈ s.get? n) → ∃ n, some a ∈ s.think.get? n
<VAR>q✝ q r : ℚ<GOAL>q / r = q.num * ↑r.den /. (↑q.den * r.num)
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A / B).card * (B * C).card