ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>x : α<VAR>s : Set α<VAR>xs : x ∈ s<VAR>hs : IsOpen s<VAR>v : Set α<VAR>xv : x ∈ v<VAR>hv : IsOpen v<VAR>μv : μ v < ⊤<GOAL>∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, x ∈ v ∧ v ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>x : α<VAR>s : Set α<VAR>xs : x ∈ s<VAR>hs : IsOpen s<VAR>v : Set α<VAR>xv : x ∈ v<VAR>hv : IsOpen v<VAR>μv : μ v < ⊤<GOAL>μ (v ∩ s) ≤ μ v
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : ℕ → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : ℕ → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝⁴ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F✝ : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F✝<VAR>inst✝³ : HasMulticoequalizer D.diagram<VAR>inst✝² : PreservesColimit D.diagram.multispan F✝<VAR>F : C ⥤ Type v<VAR>inst✝¹ : PreservesColimit D.diagram.multispan F<VAR>inst✝ : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>x : F.obj D.glued<VAR>e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F<GOAL>∃ i y, F.map (D.ι i) y = x
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝⁴ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F✝ : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F✝<VAR>inst✝³ : HasMulticoequalizer D.diagram<VAR>inst✝² : PreservesColimit D.diagram.multispan F✝<VAR>F : C ⥤ Type v<VAR>inst✝¹ : PreservesColimit D.diagram.multispan F<VAR>inst✝ : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>x : F.obj D.glued<VAR>e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F<VAR>i : (D.mapGlueData F).J<VAR>y : (D.mapGlueData F).U i<VAR>eq : (D.mapGlueData F).ι i y = e.hom x<GOAL>∃ i y, F.map (D.ι i) y = x
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝⁴ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F✝ : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F✝<VAR>inst✝³ : HasMulticoequalizer D.diagram<VAR>inst✝² : PreservesColimit D.diagram.multispan F✝<VAR>F : C ⥤ Type v<VAR>inst✝¹ : PreservesColimit D.diagram.multispan F<VAR>inst✝ : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>x : F.obj D.glued<VAR>e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F<VAR>i : (D.mapGlueData F).J<VAR>y : (D.mapGlueData F).U i<VAR>eq : ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x<GOAL>∃ i y, F.map (D.ι i) y = x
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝⁴ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F✝ : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F✝<VAR>inst✝³ : HasMulticoequalizer D.diagram<VAR>inst✝² : PreservesColimit D.diagram.multispan F✝<VAR>F : C ⥤ Type v<VAR>inst✝¹ : PreservesColimit D.diagram.multispan F<VAR>inst✝ : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>x : F.obj D.glued<VAR>e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F<VAR>i : (D.mapGlueData F).J<VAR>y : (D.mapGlueData F).U i<VAR>eq : F.map (D.ι i) y = 𝟙 (F.obj D.glued) x<GOAL>∃ i y, F.map (D.ι i) y = x
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>x y : X<GOAL>↑(d x y) ≤ 2 * dist x y
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>x y : X<GOAL>d x y ≤ ⨅ i, 2 * (zipWith d (x :: i) (i ++ [y])).sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>x y : X<VAR>l : List X<GOAL>d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>x y : X<VAR>l : List X<VAR>hd₀_trans : Transitive fun x y => d x y = 0<GOAL>d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>x y : X<VAR>l : List X<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<GOAL>d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>n : ℕ<VAR>ihn : ∀ m < n, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>x y : X<VAR>l : List X<VAR>hn : l.length = n<GOAL>d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<GOAL>d x y ≤ 2 * L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y = 0<GOAL>d x y ≤ 2 * L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y ≠ 0<GOAL>d x y ≤ 2 * L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y ≠ 0<VAR>s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}<VAR>hs₀ : 0 ∈ s<VAR>hsne : s.Nonempty<GOAL>∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y ≠ 0<VAR>s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}<VAR>hs₀ : 0 ∈ s<VAR>hsne : s.Nonempty<VAR>M : ℕ<VAR>hMl : M ≤ l.length<VAR>hMs : IsGreatest s M<GOAL>∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y ≠ 0<VAR>s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}<VAR>hs₀ : 0 ∈ s<VAR>hsne : s.Nonempty<VAR>M : ℕ<VAR>hMl : M ≤ l.length<VAR>hMs : IsGreatest s M<VAR>hM_lt : M < L.length<GOAL>∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y ≠ 0<VAR>s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}<VAR>hs₀ : 0 ∈ s<VAR>hsne : s.Nonempty<VAR>M : ℕ<VAR>hMl : M ≤ l.length<VAR>hMs : IsGreatest s M<VAR>hM_lt : M < L.length<VAR>hM_ltx : M < (x :: l).length<GOAL>∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))<VAR>hd₀_trans : Transitive fun x y => d x y = 0<VAR>this : IsTrans X fun x y => d x y = 0<VAR>x y : X<VAR>l : List X<VAR>ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum<VAR>L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])<VAR>hL_len : L.length = l.length + 1<VAR>hd₀ : d x y ≠ 0<VAR>s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}<VAR>hs₀ : 0 ∈ s<VAR>hsne : s.Nonempty<VAR>M : ℕ<VAR>hMl : M ≤ l.length<VAR>hMs : IsGreatest s M<VAR>hM_lt : M < L.length<VAR>hM_ltx : M < (x :: l).length<VAR>hM_lty : M < (l ++ [y]).length<GOAL>∃ z z', d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedAddCommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTopology γ<VAR>inst✝ : ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x<GOAL>UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedAddCommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTopology γ<VAR>inst✝ : ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x<GOAL>UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) univ x
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>ham : m = 0 → a = true<VAR>hbn : n = 0 → b = true<GOAL>(if bit a m = 0 then if f false true = true then bit b n else 0 else if bit b n = 0 then if f true false = true then bit a m else 0 else let n' := bit a m / 2; let m' := bit b n / 2; let b₁ := bit a m % 2 = 1; let b₂ := bit b n % 2 = 1; let r := bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) = bit (f a b) (bitwise f m n)
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>ham : bit a m ≠ 0<VAR>hbn : bit b n ≠ 0<GOAL>(if bit a m = 0 then if f false true = true then bit b n else 0 else if bit b n = 0 then if f true false = true then bit a m else 0 else let n' := bit a m / 2; let m' := bit b n / 2; let b₁ := bit a m % 2 = 1; let b₂ := bit b n % 2 = 1; let r := bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) = bit (f a b) (bitwise f m n)
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>ham : bit a m ≠ 0<VAR>hbn : bit b n ≠ 0<GOAL>(if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) = bit (f a b) (bitwise f m n)
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>ham : bit a m ≠ 0<VAR>hbn : bit b n ≠ 0<GOAL>(if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) = (if f a b = true then fun x => x + x + 1 else fun x => x + x) (bitwise f m n)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<GOAL>map f (cyclotomic n R) = cyclotomic n S
<VAR>n : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<GOAL>map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂<GOAL>IsPreconnected J
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂<GOAL>∀ (j₁ j₂ : J), Zigzag j₁ j₂
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂<VAR>j₁ j₂ : J<VAR>l : List J<VAR>hl₁ : List.Chain Zag j₁ l<VAR>hl₂ : (j₁ :: l).getLast ⋯ = j₂<GOAL>Zigzag j₁ j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>hs : s.Nontrivial<GOAL>∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<GOAL>(interpolate ∅ v) r = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x y z a b : α<VAR>c : ↑(Ioo (a ⊓ b) a)<GOAL>a ⊓ (↑c ⊔ b) = ↑c
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x y z a b : α<VAR>c : ↑(Ioo b (a ⊔ b))<GOAL>a ⊓ ↑c ⊔ b = ↑c
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>i : X ≅ Y<VAR>e : ↑(F.obj X) ≃ ↑(F.obj Y)<GOAL>Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a x✝¹ x✝ : α<GOAL>x✝¹ ⊔ x✝ = a → x✝¹ = a ∨ x✝ = a
<VAR>a b c d m n : ℤ<VAR>ha : 0 < a<VAR>hab : a ∣ c - b<GOAL>a + b ≤ c ↔ b < c
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<GOAL>∃ Q_1 NQ_1 PQ, Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<GOAL>∃ Q_1 NQ_1 PQ, Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<GOAL>∃ Q_1 NQ_1 PQ, Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<GOAL>((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP = ((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<GOAL>(((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n = (((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<GOAL>↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) = ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<VAR>hgn : ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding) ((PM.comp NP).equivRange n) = (g.toEmbedding.comp (PM.comp NP).toHom.range.subtype) ((PM.comp NP).equivRange n)<GOAL>↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) = ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<VAR>hgn : QM (NQ n) = g (PM (NP n))<GOAL>↑((((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n) = ↑((((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n)
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<VAR>hgn : QM (NQ n) = g (PM (NP n))<GOAL>↑((Substructure.inclusion ⋯) ((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n))) = ↑((Substructure.inclusion ⋯) (QM.equivRange (NQ n)))
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<VAR>hgn : QM (NQ n) = g (PM (NP n))<GOAL>↑(Set.inclusion ⋯ ((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n))) = ↑(Set.inclusion ⋯ (QM.equivRange (NQ n)))
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<VAR>hgn : QM (NQ n) = g (PM (NP n))<GOAL>↑((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n)) = g (PM (NP n))