ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<GOAL>∫⁻ (a : α), i a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<GOAL>∫⁻ (a : α), i a ∂μ ≤ ⨆ (_ : (fun x => (f x)⁻¹ * i x) ≤ g), ∫⁻ (a : α), (fun x => (f x)⁻¹ * i x) a ∂μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<GOAL>∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (fun x => (f x)⁻¹ * i x) a ∂μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<GOAL>∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (f * fun a => (f a)⁻¹ * i a) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<GOAL>∀ᵐ (a : α) ∂μ, i a ≤ (f * fun a => (f a)⁻¹ * i a) a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<GOAL>∀ (a : α), f a < ⊤ → i a ≤ (f * fun a => (f a)⁻¹ * i a) a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<VAR>x : α<VAR>h'x : f x < ⊤<GOAL>i x ≤ (f * fun a => (f a)⁻¹ * i a) x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<VAR>x : α<VAR>h'x : f x < ⊤<VAR>hx : f x = 0<GOAL>i x ≤ (f * fun a => (f a)⁻¹ * i a) x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<VAR>A : (fun x => (f x)⁻¹ * i x) ≤ g<VAR>x : α<VAR>h'x : f x < ⊤<VAR>hx : f x ≠ 0<GOAL>i x ≤ (f * fun a => (f a)⁻¹ * i a) x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>m : ↥M<GOAL>m • ↑((toInvSubmonoid M S) m) = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>m : ↥M<GOAL>HSMul.hSMul m = HMul.hMul ((algebraMap R S) ↑m)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>m : ↥M<VAR>x✝ : S<GOAL>m • x✝ = (algebraMap R S) ↑m * x✝
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>m : ↥M<VAR>x✝ : S<GOAL>m • x✝ = ↑m • x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : γ) ∂ν a, Tendsto (fun n => κ.densityProcess ν n a x s) atTop (𝓝 (Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) x))
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>↑φ = 0 ↔ φ = 0
<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>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>h : b ∈ f.fix a<VAR>fa : Sum.inl b ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>(fixInduction h fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯) = hbase a fa
<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>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>h : b ∈ f.fix a<VAR>fa : Sum.inl b ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>Sum.casesOn (motive := fun x => (f a).get ⋯ = x → C a) ((f a).get ⋯) (fun b' e => let_fun e := ⋯; hbase a ⋯) (fun a'' e => let_fun e := ⋯; hind a a'' ⋯ e ((fun a' h' => fixInduction ⋯ fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯) a'' e)) ⋯ = hbase a fa
<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>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>h : b ∈ f.fix a<VAR>fa : Sum.inl b ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>(fun x e => Sum.casesOn (motive := fun x => (f a).get ⋯ = x → C a) x (fun b' e => let_fun e := ⋯; hbase a ⋯) (fun a'' e => let_fun e := ⋯; hind a a'' ⋯ e ((fun a' h' => fixInduction ⋯ fun a' h ih => Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯) (fun b' e => let_fun e := ⋯; hbase a' ⋯) (fun a'' e => let_fun e := ⋯; hind a' a'' ⋯ e (ih a'' e)) ⋯) a'' e)) ⋯ = hbase a fa) (Sum.inl b) ⋯
<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>inst✝ : MeasureSpace α<VAR>s✝ t s : Set α<VAR>hs : MeasurableSet s<GOAL>Measure.map Subtype.val volume = volume.restrict s
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u : Set V<VAR>c : (⊤.deleteVerts u).coe.ConnectedComponent<VAR>hM : M.IsPerfectMatching<VAR>codd : Odd (Nat.card ↑c.supp)<GOAL>∃ w ∈ u, ∃ v, M.Adj (↑v) w ∧ v ∈ c.supp
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u : Set V<VAR>c : (⊤.deleteVerts u).coe.ConnectedComponent<VAR>hM : M.IsPerfectMatching<VAR>codd : Odd (Nat.card ↑c.supp)<VAR>h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp<GOAL>False
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u : Set V<VAR>c : (⊤.deleteVerts u).coe.ConnectedComponent<VAR>hM : M.IsPerfectMatching<VAR>codd : Odd (Nat.card ↑c.supp)<VAR>h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp<VAR>hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching<GOAL>False
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u : Set V<VAR>c : (⊤.deleteVerts u).coe.ConnectedComponent<VAR>hM : M.IsPerfectMatching<VAR>codd : Odd (Nat.card ↑c.supp)<VAR>h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp<VAR>hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching<GOAL>Even (Nat.card ↑c.supp)
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u : Set V<VAR>c : (⊤.deleteVerts u).coe.ConnectedComponent<VAR>hM : M.IsPerfectMatching<VAR>codd : Odd (Nat.card ↑c.supp)<VAR>h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp<VAR>hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching<VAR>this : Fintype ↑(M.induce (Subtype.val '' c.supp)).verts<GOAL>Even (Nat.card ↑c.supp)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e : Pretrivialization F TotalSpace.proj<GOAL>IsOpen e.source
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e e' : Pretrivialization F TotalSpace.proj<VAR>x✝ : e' ∈ a.pretrivializationAtlas<GOAL>IsOpen e.source
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e e' : Pretrivialization F TotalSpace.proj<VAR>x✝ : e' ∈ a.pretrivializationAtlas<GOAL>Subtype.val ⁻¹' e.target = e'.setSymm ⁻¹' e.source
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e e' : Pretrivialization F TotalSpace.proj<VAR>x✝ : e' ∈ a.pretrivializationAtlas<VAR>x : B × F<VAR>hx : x ∈ e'.target<GOAL>⟨x, hx⟩ ∈ Subtype.val ⁻¹' e.target ↔ ⟨x, hx⟩ ∈ e'.setSymm ⁻¹' e.source
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<GOAL>Nat.card (Sylow p G) ≡ 1 [MOD p]
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>Nat.card (Sylow p G) ≡ 1 [MOD p]
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>this : fixedPoints (↥↑P) (Sylow p G) = {P}<GOAL>Nat.card (Sylow p G) ≡ 1 [MOD p]
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>this✝ : fixedPoints (↥↑P) (Sylow p G) = {P}<VAR>this : Nat.card ↑(fixedPoints (↥↑P) (Sylow p G)) = 1<GOAL>Nat.card (Sylow p G) ≡ 1 [MOD p]
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>X Y : C<VAR>f f' : X ⟶ Y<GOAL>f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>inst✝ : IsTrans β s<GOAL>WellFounded s ↔ ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>inst✝ : IsTrans β s<VAR>wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})<VAR>b b' : β<VAR>hb' : s b' b<GOAL>Acc s b'
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>inst✝ : IsTrans β s<VAR>wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})<VAR>b b' : β<VAR>hb' : s b' b<VAR>f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b<GOAL>Acc s b'
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>inst✝ : IsTrans β s<VAR>wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})<VAR>b : β<VAR>f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b<VAR>b' : ↑{b_1 | s b_1 b}<VAR>hb' : s (f.toRelEmbedding b') b<GOAL>Acc s (f.toRelEmbedding b')
<VAR>m : ℕ<VAR>n : ℕ∞<GOAL>↑m ≤ ↑n ↔ ↑m ≤ n
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>h : ∀ p > 0, ¬MixedCharZero R p<VAR>I : Ideal R<VAR>hI_ne_top : I ≠ ⊤<GOAL>CharZero (R ⧸ I)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>h : ∀ p > 0, ¬MixedCharZero R p<VAR>I : Ideal R<VAR>hI_ne_top : I ≠ ⊤<GOAL>CharP (R ⧸ I) 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.3297, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.3304, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.3311, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>α : ShiftedHom X Y a₁<VAR>β : ShiftedHom Y Z a₂<VAR>γ : ShiftedHom Z T a₃<VAR>h₁₂ : a₂ + a₁ = a₁₂<VAR>h₂₃ : a₃ + a₂ = a₂₃<VAR>h : a₃ + a₂ + a₁ = a<GOAL>a₃ + a₁₂ = a
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.3304, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.3311, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>α : ShiftedHom X Y a₁<VAR>β : ShiftedHom Y Z a₂<VAR>γ : ShiftedHom Z T a₃<VAR>h₁₂ : a₂ + a₁ = a₁₂<VAR>h₂₃ : a₃ + a₂ = a₂₃<VAR>h : a₃ + a₂ + a₁ = a<GOAL>(α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
<VAR>α : Type u_1<VAR>inst✝² : OrderedRing α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>n✝ n : ℕ<GOAL>(box (n + 1)).disjUnion (Icc (-↑n) ↑n) ⋯ = Icc (-↑n.succ) ↑n.succ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>h : ⊤.FG<VAR>s : Finset A<VAR>hs : span R ↑s = ⊤<GOAL>toSubmodule (Algebra.adjoin R ↑s) = toSubmodule ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>h : ⊤.FG<VAR>s : Finset A<VAR>hs : span R ↑s = ⊤<GOAL>↑s ⊆ ↑(toSubmodule (Algebra.adjoin R ↑s))
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<GOAL>↑(I.splitUpper i x) = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<GOAL>(univ.pi fun i_1 => Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y✝ y : ι → ℝ<GOAL>(y ∈ univ.pi fun i_1 => Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y✝ y : ι → ℝ<GOAL>(x < y i ∧ (∀ (b : ι), I.lower b < y b) ∧ ∀ (x : ι), y x ≤ I.upper x) ↔ ((∀ (x : ι), I.lower x < y x) ∧ ∀ (x : ι), y x ≤ I.upper x) ∧ x < y i
<VAR>m n : ℕ<GOAL>valMinAbs 0 = 0
<VAR>m n✝ n : ℕ<GOAL>valMinAbs 0 = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁰ : SeminormedAddCommGroup E<VAR>inst✝¹⁹ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁸ : SeminormedAddCommGroup F<VAR>inst✝¹⁷ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup G<VAR>inst✝¹⁵ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹² : NontriviallyNormedField 𝕜₃<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁹ : NormedSpace 𝕜₂ F<VAR>inst✝⁸ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁷ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : FunLike 𝓕 E F<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>𝕜' : Type u_11<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜₂ 𝕜' F<VAR>c : 𝕜'<VAR>f : E →SL[σ₁₂] F<VAR>x✝ : E<GOAL>‖(c • f) x✝‖ ≤ ‖c‖ * ‖f‖ * ‖x✝‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁰ : SeminormedAddCommGroup E<VAR>inst✝¹⁹ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁸ : SeminormedAddCommGroup F<VAR>inst✝¹⁷ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup G<VAR>inst✝¹⁵ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹² : NontriviallyNormedField 𝕜₃<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁹ : NormedSpace 𝕜₂ F<VAR>inst✝⁸ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁷ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : FunLike 𝓕 E F<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>𝕜' : Type u_11<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜₂ 𝕜' F<VAR>c : 𝕜'<VAR>f : E →SL[σ₁₂] F<VAR>x✝ : E<GOAL>‖c‖ * ‖f x✝‖ ≤ ‖c‖ * (‖f‖ * ‖x✝‖)
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>a / 2 + a / 2 = a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.val.base<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>h' : Epi f.val.base<GOAL>IsIso (forgetToSheafedSpace.map f)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0<VAR>this : Module.Finite K L<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>this : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>this : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ adjoin R {B.gen}<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<GOAL>z ∈ adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ (aeval B.gen).range<VAR>this✝ : Module.Finite K L<VAR>P : R[X] := minpoly R B.gen<VAR>hei : P.IsEisensteinAt (Submodule.span R {p})<VAR>hndiv : ¬p ^ 2 ∣ P.coeff 0<VAR>hP : P = minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>this : NoZeroSMulDivisors R L<VAR>x✝ : L[X] := Polynomial.map (algebraMap R L) P<GOAL>z ∈ adjoin R {B.gen}