ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<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>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<VAR>L_emb : MeasurableEmbedding ⇑L<GOAL>∀ (x : E' × ℝ), HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<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>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<VAR>L_emb : MeasurableEmbedding ⇑L<GOAL>∀ (x : E' × ℝ), HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{u}<GOAL>sum f ≤ #ι * iSup f
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{u}<GOAL>sum f ≤ lift.{u, u} #ι * iSup f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : Ring A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Ring C<VAR>f : A →+* B<VAR>f_inv : B → A<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : A →+* C<VAR>hg : ker f ≤ ker g<VAR>h : B →+* C<VAR>hh : h.comp f = g<GOAL>h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩
<GOAL>completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1
<VAR>this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / (1 - 1)<GOAL>completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1
<VAR>this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1<GOAL>completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p % 4 = 3<VAR>hq : q % 4 = 3<GOAL>legendreSym q ↑p = -legendreSym p ↑q
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p % 4 = 3<VAR>hq : q % 4 = 3<VAR>nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four<GOAL>legendreSym q ↑p = -legendreSym p ↑q
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀<VAR>inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>v : AddValuation R Γ₀<VAR>x✝ y✝ z x y : R<GOAL>v x ≤ v (x + y) ∨ v y ≤ v (x + y)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀<VAR>inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>v : AddValuation R Γ₀<VAR>x✝ y✝ z x y : R<GOAL>v (x + y) ≥ min (v x) (v y)
<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✝ : DecidableEq α<VAR>l : List α<GOAL>∑ a ∈ l.toFinset, count a l = l.length
<VAR>m n : Num<VAR>x✝ : ↑m ∣ ↑n<VAR>k : ℕ<VAR>e : ↑n = ↑m * k<GOAL>n = m * ↑k
<VAR>m n : Num<VAR>x✝ : ↑m ∣ ↑n<VAR>k : ℕ<VAR>e : ↑n = ↑m * k<GOAL>↑(↑m * k) = m * ↑k
<VAR>m n : Num<VAR>x✝ : m ∣ n<VAR>k : Num<VAR>e : n = m * k<GOAL>↑n = ↑m * ↑k
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>b (min_bi b) / 2 < 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<GOAL>b (min_bi b) / 2 < 1
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctor C a).obj X = (shiftFunctor C (0 + a)).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd C 0 a).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X) ≫ eqToHom ⋯
<VAR>α✝ : Type u_1<VAR>l₁✝ l₂ l₁ l₂✝ : List α✝<VAR>a✝ : α✝<VAR>h : l₁ <+ l₂✝<GOAL>l₁.reverse <+ (a✝ :: l₂✝).reverse
<VAR>α✝ : Type u_1<VAR>l₁✝ l₂ l₁ l₂✝ : List α✝<VAR>a✝ : α✝<VAR>h : l₁ <+ l₂✝<GOAL>l₁.reverse <+ l₂✝.reverse ++ [a✝]
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l₁✝ l₂✝ : List α✝<VAR>a✝ : α✝<VAR>h : l₁✝ <+ l₂✝<GOAL>(a✝ :: l₁✝).reverse <+ (a✝ :: l₂✝).reverse
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l₁✝ l₂✝ : List α✝<VAR>a✝ : α✝<VAR>h : l₁✝ <+ l₂✝<GOAL>l₁✝.reverse ++ [a✝] <+ l₂✝.reverse ++ [a✝]
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>z x y : α<GOAL>dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>z x y : α<GOAL>‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : α → ℕ<VAR>p : Poly α<VAR>ps : List (Poly α)<GOAL>0 ≤ (p * p + sumsq ps) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MetricSpace α<VAR>s : Set α<VAR>inst✝ : Finite ↑s<GOAL>s.infsep = 0 ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MetricSpace α<VAR>s : Set α<VAR>inst✝ : Finite ↑s<GOAL>s.einfsep = 0 → s.Subsingleton
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<VAR>k : ℕ<VAR>hk : 1 < k<GOAL>IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝² : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>g : G<VAR>hg : g ∈ P<VAR>k : ℕ<VAR>g₀ : G<VAR>h : g₀⁻¹ * g ^ k * g₀ ∈ P<GOAL>g₀⁻¹ * g ^ k * g₀ = g ^ k
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝² : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>g : G<VAR>hg : g ∈ P<VAR>k : ℕ<VAR>g₀ : G<VAR>h : g₀⁻¹ * g ^ k * g₀ ∈ P<VAR>this : (↑P).IsCommutative<GOAL>g₀⁻¹ * g ^ k * g₀ = g ^ k
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝² : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>g : G<VAR>k : ℕ<VAR>g₀ : G<VAR>h : g₀⁻¹ * g ^ k * g₀ ∈ P<VAR>this : (↑P).IsCommutative<VAR>hg : g ^ k ∈ ↑P<GOAL>g₀⁻¹ * g ^ k * g₀ = g ^ k
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝² : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>g : G<VAR>k : ℕ<VAR>g₀ : G<VAR>h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P<VAR>this : (↑P).IsCommutative<VAR>hg : g ^ k ∈ ↑P<VAR>n : G<VAR>hn : n ∈ (↑P).normalizer<VAR>h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n<GOAL>g₀⁻¹ * g ^ k * g₀ = g ^ k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>η : Type x<VAR>inst✝ : Semiring R<VAR>s : ι → η<VAR>r : R<VAR>f : ι → R<GOAL>{ toFun := fun f => extend s f 0, map_add' := ⋯ }.toFun (r • f) = (RingHom.id R) r • { toFun := fun f => extend s f 0, map_add' := ⋯ }.toFun f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : NoZeroDivisors R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite ↑(commutatorSet G)<GOAL>Group.rank ↥(commutator G) ≤ Nat.card ↑(commutatorSet G)
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite ↑(commutatorSet G)<GOAL>Group.rank ↥(Subgroup.closure (commutatorSet G)) ≤ Nat.card ↑(commutatorSet G)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ✝ σ : Perm α<VAR>hσ : σ.IsCycle<GOAL>(fun τ => τ⁻¹.cycleType = τ.cycleType) σ
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ✝ σ τ : Perm α<VAR>hστ : σ.Disjoint τ<VAR>x✝ : σ.IsCycle<VAR>hσ : (fun τ => τ⁻¹.cycleType = τ.cycleType) σ<VAR>hτ : (fun τ => τ⁻¹.cycleType = τ.cycleType) τ<GOAL>(fun τ => τ⁻¹.cycleType = τ.cycleType) (σ * τ)
<VAR>ι : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset ι<VAR>s : Multiset (ZMod n)<VAR>hs : 2 * n - 1 ≤ Multiset.card s<GOAL>∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0
<VAR>ι : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset ι<VAR>s : Multiset (ZMod n)<VAR>hs : 2 * n - 1 ≤ Multiset.card s<VAR>t : Finset (ZMod n × ℕ)<VAR>hts : t ⊆ s.toEnumFinset<VAR>ht : t.card = n ∧ ∑ i ∈ t, i.1 = 0<GOAL>∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>H : K.IsPrime<VAR>x y : R<VAR>h : x * y ∈ comap f K<GOAL>f x * f y ∈ K
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>g : γ → α<GOAL>TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (comap g p')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)<VAR>g : γ → α<GOAL>Tendsto (fun q => ((f ∘ g) q.2, (F q.1 ∘ g) q.2)) (p ×ˢ comap g 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>t : Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<GOAL>t.orthocenter ∈ altitude t i₁
<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>t : Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<GOAL>mongePoint t ∈ mongePlane t i₂ i₃
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : AddGroup E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : DistribMulAction 𝕜 E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>ht : IsVonNBounded 𝕜 t<GOAL>IsVonNBounded 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : AddGroup E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : DistribMulAction 𝕜 E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>ht : IsVonNBounded 𝕜 t<GOAL>IsVonNBounded 𝕜 (s + -t)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>M : Matrix n n α<VAR>hM : Commute (stdBasisMatrix i j 1) M<GOAL>M i i = M j j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>M : Matrix n n α<VAR>hM : Commute (stdBasisMatrix i j 1) M<VAR>this : (stdBasisMatrix i j 1 * M) i j = (M * stdBasisMatrix i j 1) i j<GOAL>M i i = M j j
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<GOAL>x ^ (-1) = x⁻¹
<VAR>A : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : DivisionCommMonoid M<VAR>ψ : AddChar A M<VAR>x : A<GOAL>ψ⁻¹ x = (ψ x)⁻¹
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 1 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<GOAL>C x hx
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 1 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<GOAL>∃ (Hx : x ∈ ⨆ i, S i), C x Hx
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 1 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ ⨆ i, S i<VAR>i : ι<VAR>x : M<VAR>hx : x ∈ S i<GOAL>(fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) x
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 1 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<GOAL>(fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) 1
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 1 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x✝ : M<VAR>hx : x✝ ∈ ⨆ i, S i<VAR>x y : M<GOAL>(fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) x → (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) y → (fun m => ∃ (hm : m ∈ ⨆ i, S i), C m hm) (x * y)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>a : 𝕜<VAR>ha : 0 < a<GOAL>Ioo 0 a = ((fun i => Inv.inv '' Ioi i) ∘ Inv.inv) a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hdeg : ↑n ≤ p.degree<GOAL>↑n ≤ ↑p.natDegree
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : c ≤ 0<VAR>hf : Supermartingale f ℱ μ<GOAL>Submartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : c ≤ 0<VAR>hf : Supermartingale f ℱ μ<GOAL>Submartingale (-(-c • f)) ℱ μ
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>a : Fin (n + 2)<VAR>b : Fin (n + 1)<VAR>ha : a ≠ last (n + 1)<GOAL>a.succAbove b = last (n + 1) ↔ b = last n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>M✝ : Type u_3<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>b : ι → M✝<VAR>inst✝² : Finite ι<VAR>O : Type u_4<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<VAR>this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>ϕ : ↥M →ₗ[R] R := this.choose<VAR>ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>a_mem : a ∈ ϕ.submoduleImage N<VAR>a_zero : ¬a = 0<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))