ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<GOAL>l.reduceOption.length < l.length ↔ none ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<GOAL>(¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>head✝ : Option α<VAR>tail✝ : List (Option α)<VAR>tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝<GOAL>head✝.isSome = true → none ∈ tail✝ ↔ none = head✝ ∨ none ∈ tail✝
<VAR>num den n : ℕ<GOAL>mkRat (↑num) den ^ n = mkRat (↑num ^ n) (den ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<GOAL>Ioc a b ⊆ closure (interior (Ioc a b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<GOAL>Ioc a a ⊆ closure (interior (Ioc a a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>h : a ≠ b<GOAL>Ioc a b ⊆ closure (interior (Ioc a b))
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (sin ↑x) = sin ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e' : PartialEquiv α γ<VAR>x : α<VAR>he : x ∈ e.source<VAR>he' : x ∈ e'.source<GOAL>↑e x ∈ ↑e.symm.symm.symm ⁻¹' e'.source
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>d : Set (α × α)<VAR>hd : d ∈ 𝓤 α<GOAL>𝓤 α ≤ (𝓟 ∘ interior) d
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>d : Set (α × α)<VAR>hd : d ∈ 𝓤 α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>hs_comp : s ○ (s ○ s) ⊆ d<GOAL>𝓤 α ≤ (𝓟 ∘ interior) d
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>d : Set (α × α)<VAR>hd : d ∈ 𝓤 α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>t : Set (α × α)<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<VAR>ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}<GOAL>𝓤 α ≤ (𝓟 ∘ interior) d
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>d : Set (α × α)<VAR>hd : d ∈ 𝓤 α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>t : Set (α × α)<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<VAR>ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}<VAR>this : s ⊆ interior d<GOAL>𝓤 α ≤ (𝓟 ∘ interior) d
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>d : Set (α × α)<VAR>hd : d ∈ 𝓤 α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>t : Set (α × α)<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<VAR>ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}<VAR>this✝ : s ⊆ interior d<VAR>this : interior d ∈ 𝓤 α<GOAL>𝓤 α ≤ (𝓟 ∘ interior) d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>x z : R<VAR>hy : IsRadical (x * z)<VAR>h0 : x * z ≠ 0<GOAL>∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>x z : R<VAR>hy : IsRadical (x * z)<VAR>h0 : x * z ≠ 0<VAR>w : R<VAR>dvd : x ∣ w ^ 2<GOAL>x * z ∣ (w * z) ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>x z : R<VAR>hy : IsRadical (x * z)<VAR>h0 : x * z ≠ 0<VAR>w : R<VAR>dvd : x ∣ w ^ 2<GOAL>x * z ∣ w ^ 2 * (z * z)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>update f i '' Ico a b = Ico (update f i a) (update f i b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>hs : s.Nonempty<GOAL>IsLeast s (sInf s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>hs : s.Nonempty<GOAL>IsLeast s (argminOn id ⋯ s hs)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<GOAL>∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<GOAL>∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<GOAL>Disjoint (thickening (↑r / 2) s) (thickening (↑r / 2) t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<GOAL>thickening (↑r / 2) s ⊓ thickening (↑r / 2) t ≤ ⊥
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<VAR>z : α<VAR>hzs : z ∈ thickening (↑r / 2) s<VAR>hzt : z ∈ thickening (↑r / 2) t<GOAL>z ∈ ⊥
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<VAR>z : α<VAR>hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal (↑r / 2)<VAR>hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal (↑r / 2)<GOAL>z ∈ ⊥
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<VAR>z : α<VAR>hzs : ∃ z_1 ∈ s, edist z z_1 < ↑(r / 2)<VAR>hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)<GOAL>z ∈ ⊥
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y<VAR>z x : α<VAR>hx : x ∈ s<VAR>hzx : edist z x < ↑(r / 2)<VAR>y : α<VAR>hy : y ∈ t<VAR>hzy : edist z y < ↑(r / 2)<GOAL>edist x y ≤ ↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a b c : α<VAR>s : Finset α<VAR>hS : s.Nontrivial<GOAL>(s \ {c}).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a b c : α<VAR>s : Finset α<VAR>hS : s.Nontrivial<GOAL>¬(s = ∅ ∨ s = {c})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a b c : α<VAR>s : Finset α<VAR>hS : s.Nontrivial<GOAL>s ≠ ∅ ∧ s ≠ {c}
<VAR>n : ℕ<VAR>x✝ : ℤ<GOAL>x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}
<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>n e1 t1 k l : α<VAR>e2 : ℕ<VAR>h1 : n * e1 = t1<VAR>h2 : l * n ^ e2 = k<GOAL>k * e1 ^ e2 = l * t1 ^ e2
<VAR>n m l : ℕ<VAR>hml : m ≤ l<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>decide (k < l) = true
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<GOAL>cthickening δ (closure s) = cthickening δ s
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_9, u_1} C<VAR>inst✝⁸ : Category.{?u.48505, u_2} C₁<VAR>inst✝⁷ : Category.{?u.48509, u_3} C₂<VAR>inst✝⁶ : Category.{?u.48513, u_4} C₃<VAR>inst✝⁵ : Category.{u_10, u_5} D₁<VAR>inst✝⁴ : Category.{u_8, u_6} D₂<VAR>inst✝³ : Category.{?u.48525, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<GOAL>(homEquiv W L₁ L₂) (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>h : ¬FiniteDimensional K V<GOAL>finrank K (Module.Dual K V) = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>h : ¬FiniteDimensional K V<GOAL>∀ (s : Finset V), Basis (↑↑s) K V → False
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>h : ¬FiniteDimensional K V<GOAL>∀ (s : Finset (Module.Dual K V)), Basis (↑↑s) K (Module.Dual K V) → False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁵ : EquivLike F α β<VAR>inst✝⁴ : LE α<VAR>inst✝³ : OrderBot α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : OrderBot β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>this : BotHomClass F α β := OrderIsoClass.toBotHomClass<GOAL>f a = ⊥ ↔ a = ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c✝ a b c d : α<GOAL>max a b - max c d ≤ max (a - c) (b - d)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c✝ a b c d : α<GOAL>a ≤ max (a - c) (b - d) + max c d ∧ b ≤ max (a - c) (b - d) + max c d
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i : Fin n<VAR>y : α i.castSucc<VAR>z : α (last n)<GOAL>snoc p x i.castSucc = p i
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i : Fin n<VAR>y : α i.castSucc<VAR>z : α (last n)<GOAL>p (i.castSucc.castLT ⋯) = p i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : 0 < a + b<GOAL>f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : 0 < a + b<GOAL>a / (a + b) + b / (a + b) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>b : ℝ<VAR>hm : ‖m‖ ≤ b<GOAL>‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<GOAL>(emptyOn β).comap f = emptyOn α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)<GOAL>∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsClosed s<GOAL>MeasurableSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>h1 : s = ∅<GOAL>MeasurableSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsClosed s<VAR>h1 : s.Nonempty<GOAL>MeasurableSet (f ⁻¹' s)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>p : α → Prop<VAR>x✝ : DecidablePred p<VAR>h : ∀ i ∈ s, ¬p i<VAR>f : (i : α) → p i → β<VAR>g : (i : α) → ¬p i → β<GOAL>(∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x // x ∈ s }, g ↑i ⋯
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>s : Finset β<VAR>f : β → L.BoundedFormula α n<VAR>v : α → M<VAR>v' : Fin n → M<GOAL>(iInf s f).Realize v v' ↔ ∀ b ∈ s, (f b).Realize v v'
<VAR>a b c d m n : ℕ<VAR>p q : ℕ → Prop<VAR>n✝ : ℕ<GOAL>(m + n) % (n✝ + 1) = if n✝ + 1 ≤ m % (n✝ + 1) + n % (n✝ + 1) then m % (n✝ + 1) + n % (n✝ + 1) - (n✝ + 1) else m % (n✝ + 1) + n % (n✝ + 1)
<VAR>a b c d m n : ℕ<VAR>p q : ℕ → Prop<VAR>n✝ : ℕ<GOAL>(m % (n✝ + 1) + n % (n✝ + 1)) % (n✝ + 1) = if n✝ + 1 ≤ m % (n✝ + 1) + n % (n✝ + 1) then m % (n✝ + 1) + n % (n✝ + 1) - (n✝ + 1) else m % (n✝ + 1) + n % (n✝ + 1)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>w.im * (1 - rexp (-dist z w)) = dist ↑z ↑(w.center (dist z w)) - dist ↑w ↑(w.center (dist z w))
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) = w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ t : Set α<VAR>htm : MeasurableSet t<VAR>hst : s =ᶠ[ae μ] t<GOAL>∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ t : Set α<VAR>htm : MeasurableSet t<VAR>hst : s =ᶠ[ae μ] t<GOAL>t ∪ toMeasurable μ (s \ t) ⊇ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ t : Set α<VAR>htm : MeasurableSet t<VAR>hst : s =ᶠ[ae μ] t<GOAL>t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (s ∩ f ⁻¹' t) = f '' s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' s ∩ t ⊆ f '' (s ∩ f ⁻¹' t)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : MulHomClass F α α₂<VAR>f : F<VAR>x y : MonoidAlgebra β α<GOAL>mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : MulHomClass F α α₂<VAR>f : F<VAR>x y : MonoidAlgebra β α<GOAL>(sum x fun a b => sum y fun a_1 b_1 => Finsupp.single (f a * f a_1) (b * b_1)) = sum (mapDomain (⇑f) x) fun a₁ b₁ => sum (mapDomain (⇑f) y) fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : MulHomClass F α α₂<VAR>f : F<VAR>x y : MonoidAlgebra β α<GOAL>(sum x fun a b => sum y fun a_1 b_1 => Finsupp.single (f a * f a_1) (b * b_1)) = sum x fun a m => sum (mapDomain (⇑f) y) fun a₂ b₂ => single (f a * a₂) (m * b₂)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : MulHomClass F α α₂<VAR>f : F<VAR>x y : MonoidAlgebra β α<GOAL>∀ (b : α₂), (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b * a₂) (0 * b₂)) = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : MulHomClass F α α₂<VAR>f : F<VAR>x y : MonoidAlgebra β α<GOAL>∀ (b : α₂) (m₁ m₂ : β), (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b * a₂) ((m₁ + m₂) * b₂)) = (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b * a₂) (m₁ * b₂)) + sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b * a₂) (m₂ * b₂)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s✝ t : Set E<VAR>x✝ y x : E<VAR>s : Set E<GOAL>infEdist x⁻¹ s = infEdist x s⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>hne : a ≠ b<GOAL>{a, b} \ {b} = {a}
<VAR>α : Type u_1<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a ⩿ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>x : α<VAR>h : x ∉ xs<GOAL>(dlookup x (map Prod.toSigma (xs.zip ys))).getD x = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>x : α<VAR>h : x ∉ xs<GOAL>none.getD x = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>x : α<VAR>h : x ∉ xs<GOAL>x ∉ (map Prod.toSigma (xs.zip ys)).keys
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>x : α<VAR>h : x ∉ xs<GOAL>∀ (x_1 : α), (x, x_1) ∉ xs.zip ys
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>x : α<VAR>h : x ∉ xs<VAR>y : α<VAR>hy : (x, y) ∈ xs.zip ys<GOAL>False
<VAR>a b c : ℕ<VAR>h1 : a.pow b = c<GOAL>a.pow (2 * b) = c.mul c
<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✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>n : ℤ<GOAL>count K v (↑v.asIdeal ^ n) = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>𝓟 (Icc (⊤ - 1) (⊤ + 1)) ≤ 𝓝 ⊤
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>f : α → β<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∈ s<GOAL>f a ∣ ∏ i ∈ s, f i
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<GOAL>dualCoannihilator ⊤ = ⊥
<VAR>R : Type u_1<VAR>S : Type u_3<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>N₁ N₂ : Submodule R M<GOAL>(∀ x ∈ N₁, x ∈ B.flip.dualSubmodule N₂) ↔ ∀ x ∈ N₂, x ∈ B.dualSubmodule N₁