ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<VAR>hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯<VAR>wι : kernel.ι (cokernel.π γ) ≫ g' = 0<GOAL>S.RightHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<VAR>hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯<VAR>wι : kernel.ι (cokernel.π γ) ≫ g' = 0<VAR>e : cokernel γ ≅ Abelian.coimage S.g := (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso S.cokernelToAbelianCoimageIsCokernel<GOAL>S.RightHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<VAR>hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯<VAR>wι : kernel.ι (cokernel.π γ) ≫ g' = 0<VAR>e : cokernel γ ≅ Abelian.coimage S.g := (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso S.cokernelToAbelianCoimageIsCokernel<VAR>he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage<GOAL>S.RightHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<VAR>hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯<VAR>wι : kernel.ι (cokernel.π γ) ≫ g' = 0<VAR>e : cokernel γ ≅ Abelian.coimage S.g := (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso S.cokernelToAbelianCoimageIsCokernel<VAR>he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage<VAR>fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g<GOAL>S.RightHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<VAR>hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯<VAR>wι : kernel.ι (cokernel.π γ) ≫ g' = 0<VAR>e : cokernel γ ≅ Abelian.coimage S.g := (colimit.isColimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0)).coconePointUniqueUpToIso S.cokernelToAbelianCoimageIsCokernel<VAR>he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage<VAR>fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g<VAR>hι : IsLimit (KernelFork.ofι (kernel.ι (cokernel.π γ)) wι)<GOAL>S.RightHomologyData
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>s t : Finset α<GOAL>(filter p s).Nonempty ↔ ∃ a ∈ s, p a
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (exp 𝕂) (exp 𝕂 x • 1) x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<GOAL>(fun h => exp 𝕂 (x + h) - exp 𝕂 x - (exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<GOAL>(fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h => exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) h
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>(fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h => exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) h
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>a✝ : 𝔸<VAR>hh : a✝ ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>exp 𝕂 x * (exp 𝕂 (0 + a✝) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) = exp 𝕂 (x + a✝) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) a✝
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedCommRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>a✝ : 𝔸<VAR>hh : a✝ ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>exp 𝕂 x * (exp 𝕂 a✝ - 1 - a✝) = exp 𝕂 x * exp 𝕂 a✝ - exp 𝕂 x - exp 𝕂 x * a✝
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>Measurable fun ω => ((condexpKernel μ m) ω) s
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>Measurable fun ω => ((condDistrib id id μ) (id ω)) s
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>m ⊓ mΩ = MeasurableSpace.comap id (m ⊓ mΩ)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (of v).partDens.get? n = some b<GOAL>∃ z, b = ↑z
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (of v).partDens.get? n = some b<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<VAR>gp_b_eq_b_n : gp.b = b<GOAL>∃ z, b = ↑z
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (of v).partDens.get? n = some b<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<VAR>gp_b_eq_b_n : gp.b = b<VAR>this : ∃ z, gp.b = ↑z<GOAL>∃ z, b = ↑z
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s✝ : Set (Sym2 V)<VAR>s : Set (Sym2 ↑G'.verts)<VAR>v : V<VAR>hv : v ∈ G'.verts<VAR>w : V<VAR>hw : w ∈ G'.verts<GOAL>(G'.coe.deleteEdges s).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s✝ : Set (Sym2 V)<VAR>s : Set (Sym2 ↑G'.verts)<VAR>v : V<VAR>hv : v ∈ G'.verts<VAR>w : V<VAR>hw : w ∈ G'.verts<GOAL>G'.Adj v w → (s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s ↔ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w))
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H
<VAR>n : ℕ<VAR>h : 0 < n + 1<GOAL>⟨0, h⟩.cycleRange = 1
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>L : List (Γ k)<VAR>L₁ : ListBlank Γ'<VAR>L₂ : List (Γ k)<VAR>H₁ : L₁ ∈ TM1.eval (tr M) (trInit k L)<VAR>H₂ : L₂ ∈ TM2.eval M k L<GOAL>∃ S L', addBottom L' = L₁ ∧ (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = L₂
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>L L₂ : List (Γ k)<VAR>H₂ : L₂ ∈ TM2.eval M k L<VAR>c₁ : TM1.Cfg Γ' Λ' σ<VAR>h₁ : c₁ ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))<VAR>H₁ : c₁.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)<GOAL>∃ S L', addBottom L' = c₁.Tape.right₀ ∧ (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = L₂
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>L : List (Γ k)<VAR>c₁ : TM1.Cfg Γ' Λ' σ<VAR>h₁ : c₁ ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))<VAR>H₁ : c₁.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)<VAR>c₂ : Cfg₂<VAR>h₂ : c₂ ∈ eval (TM2.step M) (TM2.init k L)<VAR>H₂ : c₂.stk k ∈ TM2.eval M k L<GOAL>∃ S L', addBottom L' = c₁.Tape.right₀ ∧ (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = c₂.stk k
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>L : List (Γ k)<VAR>c₁ : TM1.Cfg Γ' Λ' σ<VAR>h₁ : c₁ ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))<VAR>H₁ : c₁.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)<VAR>q✝ : Option Λ<VAR>v✝ : σ<VAR>S✝ : (k : K) → List (Γ k)<VAR>L' : ListBlank ((k : K) → Option (Γ k))<VAR>hT : ∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S✝ k)).reverse<VAR>h₂ : { l := q✝, var := v✝, stk := S✝ } ∈ eval (TM2.step M) (TM2.init k L)<VAR>H₂ : { l := q✝, var := v✝, stk := S✝ }.stk k ∈ TM2.eval M k L<VAR>h₃ : { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))<GOAL>∃ S L', addBottom L' = c₁.Tape.right₀ ∧ (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = { l := q✝, var := v✝, stk := S✝ }.stk k
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>L : List (Γ k)<VAR>q✝ : Option Λ<VAR>v✝ : σ<VAR>S✝ : (k : K) → List (Γ k)<VAR>L' : ListBlank ((k : K) → Option (Γ k))<VAR>hT : ∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S✝ k)).reverse<VAR>h₂ : { l := q✝, var := v✝, stk := S✝ } ∈ eval (TM2.step M) (TM2.init k L)<VAR>H₂ : { l := q✝, var := v✝, stk := S✝ }.stk k ∈ TM2.eval M k L<VAR>h₃ : { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))<VAR>h₁ : { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))<VAR>H₁ : { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') }.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)<GOAL>∃ S L'_1, addBottom L'_1 = { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') }.Tape.right₀ ∧ (∀ (k : K), ListBlank.map (proj k) L'_1 = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = { l := q✝, var := v✝, stk := S✝ }.stk k
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>I J K L : Ideal R<VAR>inst✝ : IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>I * span {x} ≤ J * span {x} ↔ I ≤ J
<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>∑ x : α, a x * b x ^ Function.invFun (fun p => ∑ i : α, a i * b i ^ p) 1 = 1
<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>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f✝ : ι → α<VAR>g : κ → α<VAR>a✝ : α<VAR>f : ι → α<VAR>a : α<GOAL>a ⊓ s.sup' hs f = s.sup' hs fun i => a ⊓ f i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain R<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : Nontrivial L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsDomain S<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>minpoly K ((algebraMap S L) s) = map (algebraMap R K) (minpoly R s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain R<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : Nontrivial L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsDomain S<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>Irreducible (map (algebraMap R K) (minpoly R s))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain R<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : Nontrivial L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsDomain S<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>(Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain R<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : Nontrivial L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsDomain S<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>(map (algebraMap R K) (minpoly R s)).Monic
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<GOAL>⋃ i, Set.range ⇑(𝒰.map i).val.base = Set.univ
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<GOAL>∀ (x : ↑↑X.toPresheafedSpace), x ∈ ⋃ i, Set.range ⇑(𝒰.map i).val.base
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ ⋃ i, Set.range ⇑(𝒰.map i).val.base
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x : ↑↑X.toPresheafedSpace<GOAL>∃ i, x ∈ Set.range ⇑(𝒰.map i).val.base
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v w : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hw : ∀ (i : ι), w i = v i ∨ w i = -v i<GOAL>Orthonormal 𝕜 w
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : Tendsto (fun n => EMetric.diam (A (res x n))) atTop (𝓝 0)<GOAL>∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<GOAL>∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<GOAL>∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<GOAL>∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<VAR>y : α<VAR>hy : y ∈ A (res x n)<VAR>z : α<VAR>hz : z ∈ A (res x n)<GOAL>dist y z < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<VAR>y : α<VAR>hy : y ∈ A (res x n)<VAR>z : α<VAR>hz : z ∈ A (res x n)<GOAL>edist y z < ENNReal.ofReal ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<VAR>y : α<VAR>hy : y ∈ A (res x n)<VAR>z : α<VAR>hz : z ∈ A (res x n)<GOAL>EMetric.diam (A (res x n)) < ENNReal.ofReal ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<VAR>y : α<VAR>hy : y ∈ A (res x n)<VAR>z : α<VAR>hz : z ∈ A (res x n)<GOAL>ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝ : PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<VAR>hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, EMetric.diam (A (res x n)) ≤ ε<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)<VAR>y : α<VAR>hy : y ∈ A (res x n)<VAR>z : α<VAR>hz : z ∈ A (res x n)<GOAL>ε / 2 < ε
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>h : IsTerminal (colimit (F ⋙ yoneda))<GOAL>F.Final
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>h : IsTerminal (colimit (F ⋙ yoneda))<VAR>d : D<GOAL>colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : t ∈ 𝓝 x<GOAL>HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : t ∈ 𝓝 x<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt I x) x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass M'<VAR>inst✝¹ : MulOneClass N'<VAR>inst✝ : MulOneClass P<GOAL>Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass M'<VAR>inst✝¹ : MulOneClass N'<VAR>inst✝ : MulOneClass P<GOAL>Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = Submonoid.closure (Set.range ((⇑mk ∘ of) ∘ Sum.inl) ∪ Set.range ((⇑mk ∘ of) ∘ Sum.inr))