ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α β γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>F2 : Functor F<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<VAR>toLawfulFunctor✝¹ : LawfulFunctor F<VAR>seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<VAR>toLawfulFunctor✝ : LawfulFunctor F<VAR>seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<GOAL>mk = mk
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α β γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>toLawfulFunctor✝¹ : LawfulFunctor F<VAR>seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<VAR>toLawfulFunctor✝ : LawfulFunctor F<VAR>seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<GOAL>mk = mk
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α✝ β✝ γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>toLawfulFunctor✝¹ : LawfulFunctor F<VAR>seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<VAR>toLawfulFunctor✝ : LawfulFunctor F<VAR>seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<VAR>α β : Type u<VAR>x : F α<VAR>y : Unit → F β<GOAL>sl1 x y = sl2 x y
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α✝ β✝ γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>toLawfulFunctor✝¹ : LawfulFunctor F<VAR>seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<VAR>toLawfulFunctor✝ : LawfulFunctor F<VAR>seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y<VAR>seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y<VAR>pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x<VAR>seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g<VAR>seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x<VAR>α β : Type u<VAR>x : F α<VAR>y : Unit → F β<GOAL>sr1 x y = sr2 x y
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>S : Type v<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ lifts f ↔ p ∈ liftsRing f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>h : (s.pi t).Nonempty<GOAL>MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝¹ l✝ : List α<VAR>x : α<VAR>l : List α<VAR>y : α<VAR>hp : l.reverse = l → l.Palindrome<VAR>hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])<GOAL>(x :: (l ++ [y])).Palindrome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝¹ l✝ : List α<VAR>x : α<VAR>l : List α<VAR>y : α<VAR>hp : l.reverse = l → l.Palindrome<VAR>hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])<GOAL>(x :: (l ++ [y])).Palindrome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝¹ l✝ : List α<VAR>x : α<VAR>l : List α<VAR>y : α<VAR>hp : l.reverse = l → l.Palindrome<VAR>hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])<GOAL>(x :: (l ++ [x])).Palindrome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝¹ l✝ : List α<VAR>x : α<VAR>l : List α<VAR>y : α<VAR>hp : l.reverse = l → l.Palindrome<VAR>hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])<VAR>this : l.Palindrome<GOAL>(x :: (l ++ [x])).Palindrome
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j✝ : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<GOAL>(b.coord i) (b j) = if i = j then 1 else 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>inj : Function.Injective ⇑(algebraMap R P)<VAR>I : Ideal R<VAR>h : IsUnit ↑I<GOAL>I.FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>inj : Function.Injective ⇑(algebraMap R P)<VAR>I : Ideal R<VAR>h : IsUnit ↑I<GOAL>(↑↑I).FG
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Monotone f<GOAL>⨆ a ∈ s, f a ≤ f (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Monotone f<GOAL>⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)
<VAR>U : Type u_1<VAR>inst✝⁵ : Quiver U<VAR>V : Type u_2<VAR>inst✝⁴ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.19860<VAR>inst✝³ : Quiver W<VAR>ψ : V ⥤q W<VAR>inst✝² : HasInvolutiveReverse U<VAR>inst✝¹ : HasInvolutiveReverse V<VAR>inst✝ : φ.MapReverse<VAR>u : U<GOAL>Bijective (φ.costar u) ↔ Bijective (φ.star u)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulMono α<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>ha : a ≤ 0<VAR>h : 1 ≤ b<GOAL>a * b ≤ a
<VAR>x p : ℝ<VAR>hx_nonneg : 0 ≤ x<VAR>hp_nonneg : 0 ≤ p<VAR>hp0 : ¬p = 0<VAR>hx0 : x ≠ 0<GOAL>ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
<VAR>ι✝ : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : Measure ℝ<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>F : ι → ℝ → E<VAR>bound : ι → ℝ → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))<VAR>h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t<VAR>bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n => bound n t<VAR>bound_integrable : IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b<VAR>h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)<GOAL>HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
<VAR>ι✝ : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : Measure ℝ<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>F : ι → ℝ → E<VAR>bound : ι → ℝ → ℝ<VAR>hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))<VAR>h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x<VAR>bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable fun n => bound n x<VAR>bound_integrable : IntegrableOn (fun t => ∑' (n : ι), bound n t) (Ι a b) μ<VAR>h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun n => F n x) (f x)<GOAL>HasSum (fun n => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F n t ∂μ) ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, f t ∂μ)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>f : α → β<VAR>m : ι → OuterMeasure β<GOAL>(map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>this : Nonempty ↑I<GOAL>(map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>this : Nonempty ↑I<GOAL>(map f) (⨅ i, (comap f) (m ↑i)) = ⨅ i, (map f) ((comap f) (m ↑i))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n✝ : ℕ<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (n % Nat.card G) = a ^ n
<VAR>x x₁ x₂ x₃ x' y y₁✝ y₂✝ y₃ y' y₁ y₂ : PGame<VAR>h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂<VAR>hl : x₁ < x₂<GOAL>P3 x₁ x₂ y₁ y₂
<VAR>x x₁ x₂ x₃ x' y y₁✝ y₂✝ y₃ y' y₁ y₂ : PGame<VAR>h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂<VAR>hl : x₁ < x₂<VAR>i : x₂.LeftMoves<VAR>hi : x₁ ≤ x₂.moveLeft i<GOAL>P3 x₁ x₂ y₁ y₂
<VAR>x x₁ x₂ x₃ x' y y₁✝ y₂✝ y₃ y' y₁ y₂ : PGame<VAR>h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂<VAR>hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂<VAR>hl : x₁ < x₂<VAR>i : x₁.RightMoves<VAR>hi : x₁.moveRight i ≤ x₂<GOAL>P3 x₁ x₂ y₁ y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>s : Set α<VAR>f : β → M<VAR>g : α → β<VAR>hg : Injective g<VAR>x : α<GOAL>(g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ : ℕ<VAR>n : R<VAR>hn✝ : IsPrimePow n<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>p : R<VAR>k' : ℕ<VAR>hp : Prime p<VAR>hk' : 0 < k'<VAR>hn : p ^ k' = n<GOAL>p ^ (k * k') = n ^ k
<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>r✝ n r k : ℕ<GOAL>(k + 1) * eval (k + 1 + 1) (ascPochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (ascPochhammer ℕ r)
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>x : ℂ<VAR>f' : E<VAR>h : HasDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt f (reCLM.smulRight f' + I • imCLM.smulRight f') s x
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin n → α<VAR>i : Fin (n + 1)<GOAL>vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin n → α<VAR>i : Fin (n + 1)<GOAL>vecCons x u (i + i) = (vecCons x u ∘ fun n_1 => n_1 + n_1) i
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x = y ^ (1 / z) ↔ x ^ z = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<GOAL>IsTorsionBy R M a ↔ torsionBy R M a = ⊤
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>∀ (i : ι), MeasurableSet ({ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<GOAL>MeasurableSet ({ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j}<GOAL>MeasurableSet ({ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j}<GOAL>MeasurableSet ({ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j}<GOAL>MeasurableSet {ω | min (τ ω) j ≤ min (π ω) j}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j}<GOAL>Measurable fun a => min (τ a) j
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j}<GOAL>Measurable fun a => min (π a) j
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>a + star a = ↑(2 * a.re)
<VAR>x✝ x : ℝ<VAR>h : cos x ≠ 0<GOAL>HasDerivAt (fun y => tan y - y) (1 / cos x ^ 2 - 1) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm (x :: xs)[xs.length] = x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hb : t.card • b ≤ ↑s.card<GOAL>∃ y ∈ t, b ≤ ↑(filter (fun x => f x = y) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Nonempty<VAR>hb : t.card • b ≤ ∑ a ∈ s, 1<GOAL>∃ y ∈ t, b ≤ ∑ a ∈ filter (fun x => f x = y) s, 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>x : ℝ<GOAL>0 ≤ sSupNormIm f x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>x : ℝ<GOAL>∀ x_1 ∈ norm ∘ f '' (re ⁻¹' {x}), 0 ≤ x_1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>x y : ℝ<VAR>z1 : ℂ<VAR>left✝ : z1 ∈ re ⁻¹' {x}<VAR>hz2 : (norm ∘ f) z1 = y<GOAL>0 ≤ y
<GOAL>typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)
<GOAL>typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.obj
<GOAL>(Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))).sieves = typesGrothendieckTopology.sieves
<VAR>α : Type u<GOAL>(Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))).sieves α = typesGrothendieckTopology.sieves α
<VAR>α : Type u<VAR>S : Sieve α<GOAL>S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))).sieves α ↔ S ∈ typesGrothendieckTopology.sieves α
<VAR>α : Type u<VAR>S : Sieve α<VAR>hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))).sieves α<VAR>x : α<GOAL>S.arrows fun x_1 => x
<VAR>α : Type u<VAR>S : Sieve α<VAR>hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))).sieves α<VAR>x : α<VAR>hsx : ¬S.arrows fun x_1 => x<GOAL>False
<VAR>α : Type u<VAR>S : Sieve α<VAR>hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))).sieves α<VAR>x : α<VAR>hsx : ¬S.arrows fun x_1 => x<VAR>this : (fun x => { down := true }) = fun x => { down := false }<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>k : Rˣ<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp (k • z₂) h = k • z₁.comp z₂ h
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>μ ν : Measure α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>map f (μ + ν) = map f μ + map f ν
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ℕ<GOAL>toAddCircle ↑j = ↑(↑j / ↑N)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝² : RankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>Fintype.card ι ≤ Fintype.card ↑w