ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n₂ : Int<VAR>d₂ : Nat<VAR>z₂ : d₂ ≠ 0<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝ * g₁ ≠ 0<VAR>e₁ : normalize (num✝ * ↑g₁) (den✝ * g₁) z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } + normalize n₂ d₂ z₂ = normalize (num✝ * ↑g₁ * ↑d₂ + n₂ * ↑(den✝ * g₁)) (den✝ * g₁ * d₂) ⋯
<VAR>n₂ : Int<VAR>d₂ : Nat<VAR>z₂ : d₂ ≠ 0<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>e₂ : normalize n₂ d₂ z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } + { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = normalize (num✝¹ * ↑g₁ * ↑d₂ + n₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * d₂) ⋯
<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₂ : Nat<VAR>zg₂ : g₂ ≠ 0<VAR>z₂ : den✝ * g₂ ≠ 0<VAR>e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } + { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = normalize (num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₂ : Nat<VAR>zg₂ : g₂ ≠ 0<VAR>z₂ : den✝ * g₂ ≠ 0<VAR>e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>normalize (num✝¹ * ↑den✝ + num✝ * ↑den✝¹) (den✝¹ * den✝) ⋯ = normalize (num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₂ : Nat<VAR>zg₂ : g₂ ≠ 0<VAR>z₂ : den✝ * g₂ ≠ 0<VAR>e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>normalize ((num✝¹ * ↑den✝ + num✝ * ↑den✝¹) * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) ⋯ = normalize (num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ n : ℕ<GOAL>(of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ n : ℕ<VAR>h : fract v = 0<GOAL>(of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ n : ℕ<VAR>h : fract v ≠ 0<GOAL>(of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ n : ℕ<VAR>h : fract v ≠ 0<VAR>h₁ : (of (fract v)⁻¹).s.get? n = none<GOAL>(of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n✝ n : ℕ<VAR>h : fract v ≠ 0<VAR>h₁ : (of (fract v)⁻¹).s.get? n ≠ none<GOAL>(of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>h : p.Separable<VAR>f : R →+* S<VAR>a b : R[X]<VAR>H : a * p + b * derivative p = 1<GOAL>Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * derivative (Polynomial.map f p) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>p : α<VAR>hp : Irreducible p<VAR>q' : α<VAR>hq : Irreducible (p * q')<GOAL>p * q' ∣ p
<VAR>n : ℕ<GOAL>φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)
<VAR>n : ℕ<GOAL>0 < ∏ p ∈ n.primeFactors, p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>h : IsAntichain r s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r a b<GOAL>r b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b x : α<VAR>h : IsAntichain r s<VAR>a : α<VAR>ha hb : a ∈ s<VAR>hab : r a a<GOAL>r a a
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ → Prop<VAR>a : ℝ<VAR>h : ∀ᶠ (x : ℝ) in 𝓝 a, p x<GOAL>0 < volume {x | p x}
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ → Prop<VAR>a : ℝ<VAR>h : ∀ᶠ (x : ℝ) in 𝓝 a, p x<VAR>l u : ℝ<VAR>hx : a ∈ Ioo l u<VAR>hs : Ioo l u ⊆ {x | p x}<GOAL>0 < volume {x | p x}
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>p : ℝ → Prop<VAR>a : ℝ<VAR>h : ∀ᶠ (x : ℝ) in 𝓝 a, p x<VAR>l u : ℝ<VAR>hx : a ∈ Ioo l u<VAR>hs : Ioo l u ⊆ {x | p x}<GOAL>0 < volume (Ioo l u)
<VAR>α : Type u_1<VAR>l₁ l₂ l₂' : List α<VAR>s : l₁ <+ l₂<VAR>p : l₂ ~ l₂'<GOAL>∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>(filter (fun u => u.card = m) (equitabilise h).parts).card = a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>(filter (fun u => u.card = m) (equitabilise h).parts).card * m + b * (m + 1) = a * m + b * (m + 1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>(filter (fun u => u.card = m) (equitabilise h).parts).card * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, i.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<VAR>hunion : (equitabilise h).parts = filter (fun u => u.card = m) (equitabilise h).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h).parts<GOAL>(filter (fun u => u.card = m) (equitabilise h).parts).card * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, i.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<VAR>hunion : (equitabilise h).parts = filter (fun u => u.card = m) (equitabilise h).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h).parts<GOAL>(filter (fun u => u.card = m) (equitabilise h).parts).card * m + b * (m + 1) = ∑ i ∈ filter (fun u => u.card = m) (equitabilise h).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h).parts, i.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<VAR>hunion : (equitabilise h).parts = filter (fun u => u.card = m) (equitabilise h).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h).parts<GOAL>Disjoint (filter (fun u => u.card = m) (equitabilise h).parts) (filter (fun u => u.card = m + 1) (equitabilise h).parts)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<VAR>hunion : (equitabilise h).parts = filter (fun u => u.card = m) (equitabilise h).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h).parts<GOAL>Disjoint (fun u => u.card = m) fun u => u.card = m + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h✝ : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<VAR>hunion : (equitabilise h✝).parts = filter (fun u => u.card = m) (equitabilise h✝).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h✝).parts<VAR>x : Finset α → Prop<VAR>ha : x ≤ fun u => u.card = m<VAR>hb : x ≤ fun u => u.card = m + 1<VAR>i : Finset α<VAR>h : x i<GOAL>⊥ i
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h✝ : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<VAR>hunion : (equitabilise h✝).parts = filter (fun u => u.card = m) (equitabilise h✝).parts ∪ filter (fun u => u.card = m + 1) (equitabilise h✝).parts<VAR>x : Finset α → Prop<VAR>ha : x ≤ fun u => u.card = m<VAR>hb : x ≤ fun u => u.card = m + 1<VAR>i : Finset α<VAR>h : x i<GOAL>m.succ = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a b : K<GOAL>-a⁻¹ = (-a)⁻¹
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>a : α<VAR>val✝¹ : Multiset α<VAR>s : List α<VAR>nodup✝¹ : Nodup (Quot.mk Setoid.r s)<VAR>val✝ : Multiset α<VAR>t : List α<VAR>nodup✝ : Nodup (Quot.mk Setoid.r t)<VAR>h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ }<GOAL>a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝¹ }.disjUnion { val := Quot.mk Setoid.r t, nodup := nodup✝ } h ↔ a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } ∨ a ∈ { val := Quot.mk Setoid.r t, nodup := nodup✝ }
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>inst✝ : Nonempty ι<VAR>f : ι → SimpleGraph V<GOAL>(⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<GOAL>IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Abelian C<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Abelian A<VAR>inst✝¹ : Abelian B<VAR>L : A ⥤ B<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact<VAR>X✝ Y✝ : A<VAR>f : X✝ ⟶ Y✝<VAR>hf : Mono f<GOAL>Mono (L.map f)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Abelian C<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Abelian A<VAR>inst✝¹ : Abelian B<VAR>L : A ⥤ B<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact<VAR>X✝ Y✝ : A<VAR>f : X✝ ⟶ Y✝<VAR>hf : Mono f<GOAL>(ShortComplex.mk 0 (L.map f) ⋯).Exact
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Abelian C<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Abelian A<VAR>inst✝¹ : Abelian B<VAR>L : A ⥤ B<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact<VAR>X✝ Y✝ : A<VAR>f : X✝ ⟶ Y✝<VAR>hf : Mono f<GOAL>(ShortComplex.mk 0 f ⋯).map L ≅ ShortComplex.mk 0 (L.map f) ⋯
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = ∑ t ∈ filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k), MvPolynomial.NewtonIdentities.weight σ R k t
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<GOAL>IntegrableOn f (Ioi a) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)<GOAL>IntegrableOn f (Ioi a) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))<GOAL>IntegrableOn f (Ioi a) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))<GOAL>∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))<VAR>i : ι<VAR>hbi : a ≤ b i<GOAL>∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Ioi a)) l fun i => Iic (b i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))<VAR>i : ι<VAR>hbi : a ≤ b i<GOAL>∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I
<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>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, ¬p x<GOAL>∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)
<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>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, ¬p x<GOAL>(∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (g x)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.43710, u_1} C<VAR>inst✝² : Category.{?u.43714, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)<VAR>n m : ι<VAR>h : ¬c.Rel n m<VAR>j : J<GOAL>colimit.ι (F ⋙ eval C c n) j ≫ (fun n m => colimMap { app := fun j => (F.obj j).d n m, naturality := ⋯ }) n m = colimit.ι (F ⋙ eval C c n) j ≫ 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.43710, u_1} C<VAR>inst✝² : Category.{?u.43714, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)<VAR>n m : ι<VAR>h : ¬c.Rel n m<VAR>j : J<GOAL>{ app := fun j => (F.obj j).d n m, naturality := ⋯ }.app j ≫ colimit.ι (F ⋙ eval C c m) j = colimit.ι (F ⋙ eval C c n) j ≫ 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.43710, u_1} C<VAR>inst✝² : Category.{?u.43714, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)<VAR>n m : ι<VAR>h : ¬c.Rel n m<VAR>j : J<GOAL>(F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j = colimit.ι (F ⋙ eval C c n) j ≫ 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.43710, u_1} C<VAR>inst✝² : Category.{?u.43714, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)<VAR>i j : J<VAR>φ : i ⟶ j<VAR>n : ι<GOAL>(F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i ≫ 𝟙 (colimit (F ⋙ eval C c n))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : PolishSpace X<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : BorelSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : SecondCountableTopology Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>hsurj : Surjective f<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<GOAL>MeasurableSpace.map f inst✝⁴ = borel Y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : H.index = 2<VAR>a : G<GOAL>a * a ∈ H
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.sublists = map reverse l.reverse.sublists'
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<GOAL>⌊↑n / ↑d⌋ = n / ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<GOAL>(↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<GOAL>(↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : 0 < d<GOAL>(↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : 0 < d<VAR>q : ℚ := ↑n / ↑d<VAR>q_eq : q = ↑n / ↑d<GOAL>q.num / ↑q.den = n / ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : 0 < d<VAR>q : ℚ := ↑n / ↑d<VAR>q_eq : q = ↑n / ↑d<VAR>c : ℤ<VAR>n_eq_c_mul_num : n = c * q.num<VAR>d_eq_c_mul_denom : ↑d = c * ↑q.den<GOAL>q.num / ↑q.den = n / ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : 0 < d<VAR>q : ℚ := ↑n / ↑d<VAR>q_eq : q = ↑n / ↑d<VAR>c : ℤ<VAR>n_eq_c_mul_num : n = c * q.num<VAR>d_eq_c_mul_denom : ↑d = c * ↑q.den<GOAL>q.num / ↑q.den = c * q.num / (c * ↑q.den)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : 0 < d<VAR>q : ℚ := ↑n / ↑d<VAR>q_eq : q = ↑n / ↑d<VAR>c : ℤ<VAR>n_eq_c_mul_num : n = c * q.num<VAR>d_eq_c_mul_denom : ↑d = c * ↑q.den<GOAL>0 < c * ↑q.den
<VAR>α : Type u_1<VAR>s t✝ : Finset α<VAR>n : ℕ<VAR>t : Finset α<VAR>val✝ : Multiset α<VAR>nodup✝ : val✝.Nodup<GOAL>{ val := val✝, nodup := nodup✝ } ∈ powersetCard n t ↔ { val := val✝, nodup := nodup✝ } ⊆ t ∧ { val := val✝, nodup := nodup✝ }.card = n
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>dist p1 p3 = |dist p1 p2 - dist p3 p2| ↔ ∠ p1 p2 p3 = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>‖p1 -ᵥ ?p₃ - (p3 -ᵥ ?p₃)‖ = |‖p1 -ᵥ p2‖ - ‖p3 -ᵥ p2‖| ↔ ∠ p1 p2 p3 = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>P
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atTop.IsMeasurablyGenerated<VAR>inst✝ : OrderBot α<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atTop.IsMeasurablyGenerated<VAR>inst✝ : OrderBot α<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<GOAL>StronglyMeasurableAtFilter f atTop μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>IndepFun (fun a => (f i a, f j a)) (f k) κ μ
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 1<GOAL>p = X + C (p.coeff 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Semigroup α<VAR>inst✝² : Semigroup β<VAR>F : Type u_3<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : MulEquivClass F α β<VAR>f✝ : F<VAR>a b : α<VAR>f : α ≃* β := ↑f✝<VAR>h : f✝ a ∣ f✝ b<GOAL>a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Semigroup α<VAR>inst✝² : Semigroup β<VAR>F : Type u_3<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : MulEquivClass F α β<VAR>f✝ : F<VAR>a b : α<VAR>f : α ≃* β := ↑f✝<VAR>h : f✝ a ∣ f✝ b<GOAL>f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<GOAL>f.inverse.graph = Submodule.map (LinearEquiv.prodComm R E F) f.graph
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>A : Matrix m n α<GOAL>‖(WithLp.equiv 2 (m → WithLp 2 (n → α))).symm fun i => (WithLp.equiv 2 (n → α)).symm fun j => A i j‖₊ = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a : R<GOAL>a • p = C a * p
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>val ⁻¹' t = ∅ ↔ s ∩ t = ∅
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i j : β<VAR>x : γ<GOAL>update f (inr i) x (inr j) = update (f ∘ inr) i x j