ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C✝ K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>C : X → ℝ≥0<VAR>t : X → Set X<VAR>htn : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)<VAR>u : Set X<VAR>hus : u ⊆ s<VAR>huc : u.Countable<VAR>huU : s ⊆ ⋃ x ∈ u, t x<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C✝ K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>C : X → ℝ≥0<VAR>t : X → Set X<VAR>htn : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)<VAR>u : Set X<VAR>hus : u ⊆ s<VAR>huc : u.Countable<VAR>huU : s ∩ ⋃ x ∈ u, t x = s<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C✝ K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>C : X → ℝ≥0<VAR>t : X → Set X<VAR>htn : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)<VAR>u : Set X<VAR>hus : u ⊆ s<VAR>huc : u.Countable<VAR>huU : ⋃ i ∈ u, s ∩ t i = s<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C✝ K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>C : X → ℝ≥0<VAR>t : X → Set X<VAR>htn : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)<VAR>u : Set X<VAR>hus : u ⊆ s<VAR>huc : u.Countable<VAR>huU : ⋃ i ∈ u, s ∩ t i = s<GOAL>⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C✝ K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>C : X → ℝ≥0<VAR>t : X → Set X<VAR>htn : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)<VAR>u : Set X<VAR>hus : u ⊆ s<VAR>huc : u.Countable<VAR>huU : ⋃ i ∈ u, s ∩ t i = s<GOAL>⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ ⨆ i ∈ u, dimH (s ∩ t i) / ↑r
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hna : IsNonarchimedean ⇑f<VAR>x y : R<GOAL>seminormFromConst' hf1 hc hpm (x + y) ≤ max (seminormFromConst' hf1 hc hpm x) (seminormFromConst' hf1 hc hpm y)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hna : IsNonarchimedean ⇑f<VAR>x y : R<GOAL>∀ (x_1 : ℕ), seminormFromConst_seq c f (x + y) x_1 ≤ max (seminormFromConst_seq c f x x_1) (seminormFromConst_seq c f y x_1)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hna : IsNonarchimedean ⇑f<VAR>x y : R<VAR>n : ℕ<VAR>hmax : f ((x + y) * c ^ n) ≤ max (f (x * c ^ n)) (f (y * c ^ n))<GOAL>seminormFromConst_seq c f (x + y) n ≤ max (seminormFromConst_seq c f x n) (seminormFromConst_seq c f y n)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hna : IsNonarchimedean ⇑f<VAR>x y : R<VAR>n : ℕ<VAR>hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)<GOAL>seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ∨ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f y n
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ✝ : IsPrimitiveRoot ζ ↑p<VAR>h : p ≠ 2<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))<GOAL>(Algebra.norm ℤ) (hζ✝.toInteger - 1) = ↑↑p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>p✝ p'✝ : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<GOAL>map p'.subtype (range (inclusion h)) = p
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ.withDensity (r • f) = r • μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity (r • f)) s = (r • μ.withDensity f) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cocone (Discrete.functor f)<VAR>j : Discrete β<GOAL>{ pt := f default, ι := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.ι.app j ≫ (fun s => s.ι.app default) s = s.ι.app j
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cocone (Discrete.functor f)<VAR>j : Discrete β<VAR>h : j = default<GOAL>{ pt := f default, ι := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.ι.app j ≫ (fun s => s.ι.app default) s = s.ι.app j
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cocone (Discrete.functor f)<GOAL>{ pt := f default, ι := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.ι.app default ≫ (fun s => s.ι.app default) s = s.ι.app default
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cocone (Discrete.functor f)<VAR>m : { pt := f default, ι := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.pt ⟶ s.pt<VAR>w : { pt := f default, ι := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.ι.app default ≫ m = s.ι.app default<GOAL>m = (fun s => s.ι.app default) s
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Unique β<VAR>f : β → C<VAR>s : Cocone (Discrete.functor f)<VAR>m : { pt := f default, ι := Discrete.natTrans fun x => match x with | { as := j } => eqToHom ⋯ }.pt ⟶ s.pt<VAR>w : m = s.ι.app default<GOAL>m = (fun s => s.ι.app default) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>l : List α<GOAL>countP (fun a => p ↑a) (attach ⟦l⟧) = countP p ⟦l⟧
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>l : List α<GOAL>countP (fun a => p ↑a) (↑l).attach = List.countP (fun b => decide (p b)) l
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>l : List α<GOAL>countP (fun a => p ↑a) ↑l.attach = List.countP (fun b => decide (p b)) l
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>l : List α<GOAL>List.countP (fun b => decide (p ↑b)) l.attach = List.countP (fun b => decide (p b)) l
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>l : List α<GOAL>List.countP (fun b => decide (p ↑b)) l.attach = List.countP (fun a => decide (p ↑a)) l.attach
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>4 ^ n = (1 + 1) ^ (2 * n)
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>(1 + 1) ^ (2 * n) = ∑ m ∈ range (2 * n + 1), (2 * n).choose m
<VAR>R : Type u_1<VAR>n i✝ : ℕ<VAR>a✝ : i✝ ∈ range (2 * n + 1)<GOAL>(2 * n).choose i✝ ≤ (2 * n).choose (2 * n / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>a b : α<GOAL>r a b ↔ (⇑f ⁻¹'o s) a b
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<GOAL>IsLocalHomeomorphOn f (f ⁻¹' s)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<VAR>x : E<VAR>hx : x ∈ f ⁻¹' s<GOAL>∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<VAR>x : E<VAR>hx : x ∈ f ⁻¹' s<VAR>e : Trivialization (↑(f ⁻¹' {f x})) f := ⋯.toTrivialization<GOAL>∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<VAR>x : E<VAR>hx : x ∈ f ⁻¹' s<VAR>e : Trivialization (↑(f ⁻¹' {f x})) f := ⋯.toTrivialization<VAR>h : f x ∈ ⋯.toTrivialization.baseSet<GOAL>∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMapOn f s<VAR>x : E<VAR>hx : x ∈ f ⁻¹' s<VAR>e : Trivialization (↑(f ⁻¹' {f x})) f := ⋯.toTrivialization<VAR>h : f x ∈ ⋯.toTrivialization.baseSet<VAR>he : x ∈ e.source := (Trivialization.mem_source e).mpr h<GOAL>∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>inst✝ : Subsingleton R<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>inst✝ : Subsingleton R<VAR>this : Subsingleton S<GOAL>M.LinearDisjoint N
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<VAR>v : E<VAR>hv : v ∈ s<VAR>w : E<VAR>hw : w ∈ t<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ t<VAR>h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • (fun x x_1 => x + x_1) v w + b • (fun x x_1 => x + x_1) x y ∈ interior (s + t)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<VAR>v : E<VAR>hv : v ∈ s<VAR>w : E<VAR>hw : w ∈ t<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ t<VAR>h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • v + b • x + (a • w + b • y) ∈ interior (s + t)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<VAR>v : E<VAR>hv : v ∈ s<VAR>w : E<VAR>hw : w ∈ t<VAR>y : E<VAR>hy : y ∈ t<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hx : v ∈ s<VAR>h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y<GOAL>a • v + b • v + (a • w + b • y) ∈ interior (s + t)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<VAR>v : E<VAR>hv : v ∈ s<VAR>w : E<VAR>hw : w ∈ t<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ t<VAR>h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hvx : v ≠ x<GOAL>a • v + b • x + (a • w + b • y) ∈ interior (s + t)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : Sieve X<VAR>h : J.Covers S f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>J.Covers S (g ≫ f)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : Sieve X<VAR>h : Sieve.pullback f S ∈ J.sieves Y<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>Sieve.pullback (g ≫ f) S ∈ J.sieves Z
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.17758, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<VAR>z : IsZero h.left.H<GOAL>S.op.Exact
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C a * X + C b).natDegree = 1
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<GOAL>∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<VAR>g_ne_0 : g ≠ 0<GOAL>∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<VAR>g_ne_0 : g ≠ 0<GOAL>∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<VAR>g_ne_0 : g ≠ 0<VAR>g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f<GOAL>∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<VAR>g_ne_0 : g ≠ 0<VAR>g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f<VAR>algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)<GOAL>∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<VAR>g_ne_0 : g ≠ 0<VAR>g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f<VAR>algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)<VAR>this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype<GOAL>∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>f : R[X]<VAR>hf : f.Monic<VAR>g : K[X]<VAR>hg : g ∣ map (algebraMap R K) f<VAR>g_ne_0 : g ≠ 0<VAR>g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f<VAR>algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)<VAR>this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype<VAR>H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹<GOAL>∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
<VAR>u v m n✝ : ℤ<VAR>n : ℕ<GOAL>Even (m ^ n) ↔ Even m ∧ n ≠ 0
<VAR>u v m n✝ : ℤ<VAR>n : ℕ<VAR>ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0<GOAL>Even m → ¬n = 0 → Even m
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : α<VAR>hx : x ∈ s<VAR>this : ↑⟨x, ⋯⟩ ∈ s<GOAL>(Trans.trans (Trans.trans (Set.union ⋯).symm (Set.ofEq ⋯)) (Set.univ α)).symm x = Sum.inl ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n<GOAL>2⁻¹ < 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>z : S<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<VAR>p : R[X]<VAR>p_ne_zero : p ≠ 0<VAR>px : (aeval z) p = 0<VAR>a : R := p.leadingCoeff<GOAL>∃ x y, y ≠ 0 ∧ z * (algebraMap R S) y = ↑x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>z : S<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<VAR>p : R[X]<VAR>p_ne_zero : p ≠ 0<VAR>px : (aeval z) p = 0<VAR>a : R := p.leadingCoeff<VAR>a_ne_zero : a ≠ 0<GOAL>∃ x y, y ≠ 0 ∧ z * (algebraMap R S) y = ↑x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>z : S<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<VAR>p : R[X]<VAR>p_ne_zero : p ≠ 0<VAR>px : (aeval z) p = 0<VAR>a : R := p.leadingCoeff<VAR>a_ne_zero : a ≠ 0<VAR>x_integral : IsIntegral R (z * (algebraMap R S) a)<GOAL>∃ x y, y ≠ 0 ∧ z * (algebraMap R S) y = ↑x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<GOAL>∃ p, p ∈ factors x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<VAR>p' : α<VAR>hp' : Irreducible p'<VAR>hp'x : p' ∣ x<GOAL>∃ p, p ∈ factors x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<VAR>p' : α<VAR>hp' : Irreducible p'<VAR>hp'x : p' ∣ x<VAR>p : α<VAR>hp : p ∈ factors x<VAR>right✝ : p' ~ᵤ p<GOAL>∃ p, p ∈ factors x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>H : ∀ (n : β), IsPreconnected (s n)<VAR>K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty<VAR>i✝ j i : β<VAR>x✝ : i ∈ Ico j i✝<GOAL>(s (succ i) ∩ s i).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>H : ∀ (n : β), IsPreconnected (s n)<VAR>K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty<VAR>i✝ j i : β<VAR>x✝ : i ∈ Ico j i✝<GOAL>(s i ∩ s (succ i)).Nonempty
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<GOAL>(∀ (j : J), IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)) ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<GOAL>∀ (a : J), IsPullback (c'.ι.app a) ((α' ≫ α).app a) f (c.ι.app a) ↔ IsPullback (c'.ι.app a) (α'.app a) f (((Cocones.precompose α).obj c).ι.app a)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>j : J<GOAL>IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j) ↔ IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>j : J<GOAL>IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j) ↔ IsPullback (c'.ι.app j) (α'.app j) f (α.app j ≫ c.ι.app j)