ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<VAR>xs_nonempty : xs.Nonempty<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<VAR>xs_nonempty : xs.Nonempty<VAR>k : ↑L := ⟨xs.inf' xs_nonempty fun x => ↑(h x), ⋯⟩<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<VAR>xs_nonempty : xs.Nonempty<VAR>k : ↑L := ⟨xs.inf' xs_nonempty fun x => ↑(h x), ⋯⟩<GOAL>dist (↑k) f < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<VAR>xs_nonempty : xs.Nonempty<VAR>k : ↑L := ⟨xs.inf' xs_nonempty fun x => ↑(h x), ⋯⟩<GOAL>∀ (x : X), dist (↑k x) (f x) < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<VAR>xs_nonempty : xs.Nonempty<VAR>k : ↑L := ⟨xs.inf' xs_nonempty fun x => ↑(h x), ⋯⟩<VAR>z : X<GOAL>dist (↑k z) (f z) < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<VAR>xs : Finset X := ⋯.choose<VAR>xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)<VAR>xs_nonempty : xs.Nonempty<VAR>k : ↑L := ⟨xs.inf' xs_nonempty fun x => ↑(h x), ⋯⟩<VAR>z : X<GOAL>↑k z < f z + ε ∧ f z - ε < ↑k z
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →L[𝕜] G<VAR>hf : ContDiff 𝕜 n f<VAR>x : E<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDeriv 𝕜 i (⇑g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →L[𝕜] G<VAR>hf : ContDiff 𝕜 n f<VAR>x : E<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f univ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>f✝ : R →+* S<VAR>g : R →+* T<VAR>f : R →+* S × T<VAR>x : R<GOAL>(((fst S T).comp f).prod ((snd S T).comp f)) x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Setoid α<GOAL>r ⊔ s = EqvGen.Setoid (r.Rel ⊔ s.Rel)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Setoid α<GOAL>(EqvGen.Setoid fun x y => r.Rel x y ∨ s.Rel x y) = EqvGen.Setoid (r.Rel ⊔ s.Rel)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>infDist x (closure s) = infDist x s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>R : Presieve X<VAR>f : Y ⟶ X<VAR>inst✝ : IsSplitEpi f<VAR>hf : R f<GOAL>generate R = ⊤
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>R : Presieve X<VAR>f : Y ⟶ X<VAR>inst✝ : IsSplitEpi f<VAR>hf : R f<GOAL>(generate R).arrows (𝟙 X)
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝¹⁰ : Ring 𝕜<VAR>n : ℕ<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousConstSMul 𝕜 E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜 F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1
<VAR>h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)<GOAL>False
<VAR>h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)<VAR>this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id<GOAL>False
<VAR>h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)<VAR>this✝ : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id<VAR>this : HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>t : Finset κ<VAR>f✝ : ι → α<VAR>g : κ → α<VAR>a✝ : α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>s.sup f ⊓ a = s.sup fun i => f i ⊓ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>t : Finset κ<VAR>f✝ : ι → α<VAR>g : κ → α<VAR>a✝ : α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(s.sup fun i => a ⊓ f i) = s.sup fun i => f i ⊓ a
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>(α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>(f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv = (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ 𝓒 u v s<VAR>ha : a ∉ s<GOAL>(a ⊔ v) \ u ∈ s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a<VAR>ha : a ∉ s<GOAL>(a ⊔ v) \ u ∈ s
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>x✝ : R⟦X⟧<VAR>n✝ : ℕ<GOAL>(coeff R n✝) ((rescale 1) x✝) = (coeff R n✝) ((RingHom.id R⟦X⟧) x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<GOAL>(single a b).support ⊆ {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : PartialOrder α<VAR>s : Set α<GOAL>IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ioi a ⊆ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹¹ : Category.{u_3, u_1} C<VAR>inst✝¹⁰ : Category.{u_4, u_2} D<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>inst✝⁸ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁷ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁶ : F.PreservesZeroMorphisms<VAR>inst✝⁵ : S₁.HasHomology<VAR>inst✝⁴ : S₂.HasHomology<VAR>inst✝³ : (S₁.map F).HasHomology<VAR>inst✝² : (S₂.map F).HasHomology<VAR>inst✝¹ : F.PreservesRightHomologyOf S₁<VAR>inst✝ : F.PreservesRightHomologyOf S₂<GOAL>F.map (homologyMap φ) ≫ (S₂.mapHomologyIso' F).inv = (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹¹ : CommSemiring R₂<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁸ : CommRing R₃<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq n<VAR>b : Basis n R₂ M₂<GOAL>toMatrix (Pi.basisFun R₂ n) = BilinForm.toMatrix'
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>x : K<VAR>h : K[X]<VAR>h_splits : Splits i h<VAR>h_roots : (map i h).roots = {i x}<GOAL>h = C h.leadingCoeff * (X - C x)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>x : K<VAR>h : K[X]<VAR>h_splits : Splits i h<VAR>h_roots : (map i h).roots = {i x}<GOAL>map i h = map i (C h.leadingCoeff * (X - C x))
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>x : K<VAR>h : K[X]<VAR>h_splits : Splits i h<VAR>h_roots : (map i h).roots = {i x}<GOAL>C (i h.leadingCoeff) * (Multiset.map (fun a => X - C a) {i x}).prod = map i (C h.leadingCoeff * (X - C x))
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hn : N.FG<VAR>hin : N ≤ I • N<GOAL>∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hn : ∃ S, S.Finite ∧ span R S = N<VAR>hin : N ≤ I • N<GOAL>∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s : Set M<VAR>hfs : s.Finite<GOAL>(∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s : Set M<VAR>hfs : s.Finite<VAR>H : ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R ∅) ∧ ∅ ⊆ ↑N<GOAL>∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>H : ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N<GOAL>∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>r : R<VAR>hr1 : r - 1 ∈ I<VAR>hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R (insert i s))<VAR>hs : insert i s ⊆ ↑N<GOAL>∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>r : R<VAR>hr1 : r - 1 ∈ I<VAR>hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)<VAR>hs : insert i s ⊆ ↑N<GOAL>∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>r : R<VAR>hr1 : r - 1 ∈ I<VAR>hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)<VAR>hs : i ∈ ↑N ∧ s ⊆ ↑N<GOAL>∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>r : R<VAR>hr1 : r - 1 ∈ I<VAR>hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)<VAR>hs : i ∈ ↑N ∧ s ⊆ ↑N<VAR>c : R<VAR>hc1 : c - 1 ∈ I<VAR>hci : c • i ∈ I • span R s<GOAL>∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>r : R<VAR>hr1 : r - 1 ∈ I<VAR>hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)<VAR>hs : i ∈ ↑N ∧ s ⊆ ↑N<VAR>c : R<VAR>hc1 : c - 1 ∈ I<VAR>hci : c • i ∈ I • span R s<GOAL>c * r - 1 ∈ I