ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<VAR>pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n<VAR>Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m<VAR>Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m<VAR>x : ℕ → ℕ := fun n => (↑(p (n + 1))).2.1 n<VAR>hx : x = fun n => (↑(p (n + 1))).2.1 n<VAR>y : ℕ → ℕ := fun n => (↑(p (n + 1))).2.2 n<VAR>hy : y = fun n => (↑(p (n + 1))).2.2 n<VAR>M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)<VAR>u v : Set α<VAR>u_open : IsOpen u<VAR>v_open : IsOpen v<VAR>xu : f x ∈ u<VAR>yv : g y ∈ v<VAR>huv : Disjoint u v<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<VAR>pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n<VAR>Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m<VAR>Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m<VAR>x : ℕ → ℕ := fun n => (↑(p (n + 1))).2.1 n<VAR>hx : x = fun n => (↑(p (n + 1))).2.1 n<VAR>y : ℕ → ℕ := fun n => (↑(p (n + 1))).2.2 n<VAR>hy : y = fun n => (↑(p (n + 1))).2.2 n<VAR>M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)<VAR>u v : Set α<VAR>u_open : IsOpen u<VAR>v_open : IsOpen v<VAR>xu : f x ∈ u<VAR>yv : g y ∈ v<VAR>huv : Disjoint u v<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<VAR>pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n<VAR>Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m<VAR>Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m<VAR>x : ℕ → ℕ := fun n => (↑(p (n + 1))).2.1 n<VAR>hx : x = fun n => (↑(p (n + 1))).2.1 n<VAR>y : ℕ → ℕ := fun n => (↑(p (n + 1))).2.2 n<VAR>hy : y = fun n => (↑(p (n + 1))).2.2 n<VAR>M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)<VAR>u v : Set α<VAR>u_open : IsOpen u<VAR>v_open : IsOpen v<VAR>xu : f x ∈ u<VAR>yv : g y ∈ v<VAR>huv : Disjoint u v<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>εx : ℝ<VAR>εxpos : εx > 0<VAR>hεx : ball x εx ⊆ f ⁻¹' u<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<VAR>pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n<VAR>Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m<VAR>Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m<VAR>x : ℕ → ℕ := fun n => (↑(p (n + 1))).2.1 n<VAR>hx : x = fun n => (↑(p (n + 1))).2.1 n<VAR>y : ℕ → ℕ := fun n => (↑(p (n + 1))).2.2 n<VAR>hy : y = fun n => (↑(p (n + 1))).2.2 n<VAR>M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)<VAR>u v : Set α<VAR>u_open : IsOpen u<VAR>v_open : IsOpen v<VAR>xu : f x ∈ u<VAR>yv : g y ∈ v<VAR>huv : Disjoint u v<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>εx : ℝ<VAR>εxpos : εx > 0<VAR>hεx : ball x εx ⊆ f ⁻¹' u<VAR>εy : ℝ<VAR>εypos : εy > 0<VAR>hεy : ball y εy ⊆ g ⁻¹' v<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<VAR>pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n<VAR>Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m<VAR>Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m<VAR>x : ℕ → ℕ := fun n => (↑(p (n + 1))).2.1 n<VAR>hx : x = fun n => (↑(p (n + 1))).2.1 n<VAR>y : ℕ → ℕ := fun n => (↑(p (n + 1))).2.2 n<VAR>hy : y = fun n => (↑(p (n + 1))).2.2 n<VAR>M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)<VAR>u v : Set α<VAR>u_open : IsOpen u<VAR>v_open : IsOpen v<VAR>xu : f x ∈ u<VAR>yv : g y ∈ v<VAR>huv : Disjoint u v<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>εx : ℝ<VAR>εxpos : εx > 0<VAR>hεx : ball x εx ⊆ f ⁻¹' u<VAR>εy : ℝ<VAR>εypos : εy > 0<VAR>hεy : ball y εy ⊆ g ⁻¹' v<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < min εx εy<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>r : α → α → Prop<VAR>inst✝¹ : IsIrrefl α r<VAR>inst✝ : Subsingleton α<GOAL>∀ (a b : α), r a b = EmptyRelation a b
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>x y : G<VAR>hx : orderOf x = 2<VAR>hy : orderOf y = 2<VAR>hxy : x ≠ y<GOAL>x * y ∉ {x, y, 1}
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>x y : G<VAR>hx : orderOf x = 2<VAR>hy : orderOf y = 2<VAR>hxy : x ≠ y<GOAL>¬y = 1 ∧ ¬x = 1 ∧ ¬x = y
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>h'f : 0 ≤ f<VAR>A : ℝ<GOAL>∫ (x : α), truncation f A x ∂μ ≤ ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>h'f : 0 ≤ f<VAR>A : ℝ<VAR>x : α<GOAL>0 x ≤ truncation f A x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>h'f : 0 ≤ f<VAR>A : ℝ<VAR>x : α<GOAL>truncation f A x ≤ f x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M : ModuleCat R<VAR>N : ModuleCat R<GOAL>tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M : ModuleCat R<VAR>N : ModuleCat R<GOAL>(TensorProduct.mk R ↑M ↑N).compr₂ (tensorHom (𝟙 M) (𝟙 N)) = (TensorProduct.mk R ↑M ↑N).compr₂ (𝟙 (of R (↑M ⊗[R] ↑N)))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>h : φ.order.Dom<VAR>n : ℕ<GOAL>(coeff R n) φ = (coeff R n) (X ^ φ.order.get h * mk fun n => (coeff R (n + φ.order.get h)) φ)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>h : φ.order.Dom<VAR>n : ℕ<GOAL>(coeff R n) φ = ∑ x ∈ Finset.filter (fun x => x.1 = φ.order.get h) (antidiagonal n), (coeff R (x.2 + φ.order.get h)) φ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>h : φ.order.Dom<VAR>n : ℕ<GOAL>(coeff R n) φ = ∑ x ∈ if φ.order.get h ≤ n then {(φ.order.get h, n - φ.order.get h)} else ∅, (coeff R (x.2 + φ.order.get h)) φ
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>inst✝ : NeZero n<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>a.succAbove 0 = 0
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>inst✝ : NeZero n<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>castSucc 0 = 0
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>inst✝ : NeZero n<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>castSucc 0 < a
<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>K L M : CochainComplex C ℤ<VAR>n✝ n' a : ℤ<VAR>γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<GOAL>δ n (n + 1) ((↑γ).rightUnshift n hn) = 0
<VAR>d n n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>z : d ≠ 0<VAR>h : n /. d = { num := n', den := d', den_nz := z', reduced := c }<GOAL>∃ m, m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m
<VAR>n n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>w✝ : Nat<VAR>z : ¬w✝ = 0<VAR>h : mkRat n w✝ = { num := n', den := d', den_nz := z', reduced := c }<GOAL>∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m
<VAR>n n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>w✝ : Nat<VAR>z : ¬w✝ = 0<VAR>h : mkRat (-n) w✝ = { num := n', den := d', den_nz := z', reduced := c }<GOAL>∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>b✝ : ℤ<VAR>fr✝ : K<VAR>stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }<VAR>nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0<GOAL>IntFractPair.stream v (n + 1) = some (IntFractPair.of { b := b✝, fr := fr✝ }.fr⁻¹)
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>b✝ : ℤ<VAR>fr✝ : K<VAR>stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }<VAR>nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0<GOAL>fr✝ = 0 → False
<VAR>n : ℤ<VAR>h : ¬3 ∣ n<GOAL>↑n ^ 3 = 1 ∨ ↑n ^ 3 = 8
<VAR>n : ℤ<VAR>h : ¬3 ∣ n<GOAL>(castHom ⋯ (ZMod 3)) ↑n ≠ 0
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<GOAL>∀ (x y : Cofix F α), r x y → x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<GOAL>∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : Cofix F α<VAR>rxy : r x y<GOAL>(TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : Cofix F α<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ fun {i} => (α ::: Cofix F α) i<VAR>dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩<VAR>dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩<VAR>h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)<GOAL>(TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : Cofix F α<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ fun {i} => (α ::: Cofix F α) i<VAR>dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩<VAR>dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩<VAR>h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)<GOAL>MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ f₀⟩ = MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ f₁⟩
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : Cofix F α<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ fun {i} => (α ::: Cofix F α) i<VAR>dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩<VAR>dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩<VAR>h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)<GOAL>MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ splitFun (dropFun f₀) (lastFun f₀)⟩ = MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ splitFun (dropFun f₁) (lastFun f₁)⟩
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : Cofix F α<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ fun {i} => (α ::: Cofix F α) i<VAR>dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩<VAR>dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩<VAR>h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)<GOAL>MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ = MvQPF.abs ⟨a, splitFun (TypeVec.id ⊚ dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : Cofix F α<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ fun {i} => (α ::: Cofix F α) i<VAR>dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩<VAR>dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩<VAR>h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)<GOAL>MvQPF.abs ⟨a, splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀)⟩ = MvQPF.abs ⟨a, splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁)⟩
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : Y ⟶ X<GOAL>f ≫ α.hom = 𝟙 Y ↔ f = α.inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n k : ℕ<GOAL>Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n k : ℕ<GOAL>Fintype.card (Sym (Fin 0) (k + 1)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ n k : ℕ<GOAL>Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 2).multichoose (k + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ n k : ℕ<GOAL>Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ n k : ℕ<GOAL>Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℂ<VAR>hy : y.re ≠ 0<GOAL>abs (↑x ^ y) = x ^ y.re
<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>∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε ↑n
<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>n : ℕ<VAR>hn : 0 < 1 + ε ↑n<GOAL>0 ≤ 1 + ε ↑n
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>(o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x)).tan = r⁻¹
<VAR>n p : ℕ<GOAL>eval (↑n) (bernoulli p.succ) = _root_.bernoulli p.succ + (↑p + 1) * ∑ k ∈ range n, ↑k ^ p
<VAR>n p : ℕ<GOAL>eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ = (↑p + 1) * ∑ k ∈ range n, ↑k ^ p
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>k : ℕ<GOAL>↑(((AlgebraTensorModule.curry (↑(piEquivOfFintype I fun x => R) ∘ₗ ofTensorProduct I (ι → R))) 1 ∘ₗ LinearMap.single i) 1 j) k = ↑(((AlgebraTensorModule.curry ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) 1 ∘ₗ LinearMap.single i) 1 j) k
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>k : ℕ<GOAL>(if j = i then 1 else 0) = ↑(if j = i then 1 else 0) k
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₁₂ : p₁ = p₂<VAR>h₂₃ : p₂ = p₃<GOAL>eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>f g : R[X]<GOAL>derivative (f * g) = derivative f * g + f * derivative g
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>coeff 1 0 = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<GOAL>∑ i : ι, ⟪b i, x⟫_𝕜 • b i = x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<GOAL>∑ i : ι, ⟪b i, x⟫_𝕜 • b i = ∑ i : ι, b.repr x i • b i
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>K : Type (max v u)<VAR>inst✝ : SmallCategory K<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>W : J.Cover X<VAR>i : W.Arrow<VAR>E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W))<VAR>a b : K<VAR>f : a ⟶ b<GOAL>𝟙 E.pt ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i = (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F.map f).app (op i.Y)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>K : Type (max v u)<VAR>inst✝ : SmallCategory K<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>W : J.Cover X<VAR>i : W.Arrow<VAR>E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W))<VAR>a b : K<VAR>f : a ⟶ b<GOAL>(E.π.app a ≫ (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W)).map f) ≫ Multiequalizer.ι (W.index (F.obj b)) i = E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>K : Type (max v u)<VAR>inst✝ : SmallCategory K<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>W : J.Cover X<VAR>i : W.Arrow<VAR>E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj (op W))<VAR>a b : K<VAR>f : a ⟶ b<GOAL>(E.π.app a ≫ Multiequalizer.lift (W.index (F.obj b)) (multiequalizer (W.index (F.obj a))) (fun i => Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)) ⋯) ≫ Multiequalizer.ι (W.index (F.obj b)) i = E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>r : R<VAR>hr : ∃ x, Irreducible x<GOAL>Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>r : R<VAR>hr : ∃ x, Irreducible x<GOAL>Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h : μ ≤ ν<GOAL>μ ≤ 0 + ν
<VAR>x : EReal<VAR>h : x ≠ ⊥<GOAL>x + ⊤ = ⊤
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inr g₃ g₄ ≫ pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯