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>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>∀ (n : ℕ), F (x (n + k)) ≤ᶠ[ae μ] ?intro.refine_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>∫⁻ (a : α), ?intro.refine_1 a ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun n => F (x (n + k)) a) atTop (𝓝 (f a))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : s =ᶠ[ae (comap f μ)] t<GOAL>f '' s =ᶠ[ae μ] f '' t
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : (comap f μ) {a | ¬s a = t a} = 0<GOAL>μ {a | ¬(f '' s) a = (f '' t) a} = 0
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : (comap f μ) {a | ¬s a = t a} = 0<VAR>h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s<GOAL>μ {a | ¬(f '' s) a = (f '' t) a} = 0
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : (comap f μ) {a | ¬s a = t a} = 0<VAR>h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s<VAR>h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s<GOAL>μ {a | ¬(f '' s) a = (f '' t) a} = 0
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : (comap f μ) {a | ¬s a = t a} = 0<VAR>h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s<VAR>h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)<GOAL>μ {a | ¬(f '' s) a = (f '' t) a} = 0
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s t : Set α<VAR>hst : (comap f μ) (s \ t ∪ t \ s) = 0<VAR>h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s<VAR>h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)<GOAL>μ (f '' (s \ t ∪ t \ s)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → β<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>h_zero : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>Integrable (fun x => ‖f x‖ ^ p.toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<VAR>this : ContinuousOn f (Ioo b a) → Tendsto f (𝓝[>] b) (𝓝 lb) → ContinuousOn (extendFrom (Ioo b a) f) (Ico b a)<GOAL>ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<VAR>this : ContinuousOn f (⇑OrderDual.ofDual ⁻¹' Ioo a b) → Tendsto f (𝓝[⇑OrderDual.ofDual ⁻¹' Iio b] b) (𝓝 lb) → ContinuousOn (extendFrom (⇑OrderDual.ofDual ⁻¹' Ioo a b) f) (⇑OrderDual.ofDual ⁻¹' Ioc a b)<GOAL>ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<GOAL>fderiv 𝕜 (fun y => f y + c) x = fderiv 𝕜 f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : a = c + b<GOAL>c ≤ c + b - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>f : γ → β<VAR>x✝ : List α<GOAL>Forall₂ R x✝ (map f []) ↔ Forall₂ (fun a c => R a (f c)) x✝ []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>f : γ → β<VAR>x✝ : List α<VAR>b : γ<VAR>u : List γ<GOAL>Forall₂ R x✝ (map f (b :: u)) ↔ Forall₂ (fun a c => R a (f c)) x✝ (b :: u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : IsOpenMap f<VAR>s : Set β<VAR>t : Set ↑(f ⁻¹' s)<GOAL>IsOpen t → IsOpen (s.restrictPreimage f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : IsOpenMap f<VAR>s : Set β<VAR>t : Set ↑(f ⁻¹' s)<GOAL>∀ (u : Set α), IsOpen u → Subtype.val ⁻¹' u = t → ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<VAR>f' : { x // x ∈ s } → α<VAR>hf' : Function.Injective f'<VAR>hsf' : ∀ (x : { x // x ∈ s }), f' x ∈ t' x<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<VAR>f' : { x // x ∈ s } → α<VAR>hf' : Function.Injective f'<VAR>hsf' : ∀ (x : { x // x ∈ s }), f' x ∈ t' x<VAR>ι'' : Set ι := (↑s)ᶜ<VAR>t'' : ↑ι'' → Finset α := fun a'' => t ↑a'' \ s.biUnion t<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<VAR>f' : { x // x ∈ s } → α<VAR>hf' : Function.Injective f'<VAR>hsf' : ∀ (x : { x // x ∈ s }), f' x ∈ t' x<VAR>ι'' : Set ι := (↑s)ᶜ<VAR>t'' : ↑ι'' → Finset α := fun a'' => t ↑a'' \ s.biUnion t<VAR>card_ι''_le : Fintype.card ↑ι'' ≤ n<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<VAR>f' : { x // x ∈ s } → α<VAR>hf' : Function.Injective f'<VAR>hsf' : ∀ (x : { x // x ∈ s }), f' x ∈ t' x<VAR>ι'' : Set ι := (↑s)ᶜ<VAR>t'' : ↑ι'' → Finset α := fun a'' => t ↑a'' \ s.biUnion t<VAR>card_ι''_le : Fintype.card ↑ι'' ≤ n<VAR>f'' : ↑ι'' → α<VAR>hf'' : Function.Injective f''<VAR>hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<VAR>f' : { x // x ∈ s } → α<VAR>hf' : Function.Injective f'<VAR>hsf' : ∀ (x : { x // x ∈ s }), f' x ∈ t' x<VAR>ι'' : Set ι := (↑s)ᶜ<VAR>t'' : ↑ι'' → Finset α := fun a'' => t ↑a'' \ s.biUnion t<VAR>card_ι''_le : Fintype.card ↑ι'' ≤ n<VAR>f'' : ↑ι'' → α<VAR>hf'' : Function.Injective f''<VAR>hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x<VAR>f'_mem_biUnion : ∀ (x' : ι) (hx' : x' ∈ s), f' ⟨x', hx'⟩ ∈ s.biUnion t<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n.succ<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ univ<VAR>hus : s.card = (s.biUnion t).card<VAR>this : DecidableEq ι<VAR>card_ι'_le : Fintype.card { x // x ∈ s } ≤ n<VAR>t' : { x // x ∈ s } → Finset α := fun x' => t ↑x'<VAR>f' : { x // x ∈ s } → α<VAR>hf' : Function.Injective f'<VAR>hsf' : ∀ (x : { x // x ∈ s }), f' x ∈ t' x<VAR>ι'' : Set ι := (↑s)ᶜ<VAR>t'' : ↑ι'' → Finset α := fun a'' => t ↑a'' \ s.biUnion t<VAR>card_ι''_le : Fintype.card ↑ι'' ≤ n<VAR>f'' : ↑ι'' → α<VAR>hf'' : Function.Injective f''<VAR>hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x<VAR>f'_mem_biUnion : ∀ (x' : ι) (hx' : x' ∈ s), f' ⟨x', hx'⟩ ∈ s.biUnion t<VAR>f''_not_mem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : AddGroupWithOne R<VAR>h : s ⊆ t<GOAL>↑(t \ s).card = ↑t.card - ↑s.card
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F : C ⥤ D ⥤ E<VAR>X✝ Y✝ Z✝ : C × D<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun X => (F.obj X.1).obj X.2, map := fun {X Y} f => (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 }.map (f ≫ g) = { obj := fun X => (F.obj X.1).obj X.2, map := fun {X Y} f => (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 }.map f ≫ { obj := fun X => (F.obj X.1).obj X.2, map := fun {X Y} f => (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 }.map g
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F : C ⥤ D ⥤ E<VAR>X✝ Y✝ Z✝ : C × D<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>(F.map f.1).app X✝.2 ≫ (F.map g.1).app X✝.2 ≫ (F.obj Z✝.1).map f.2 ≫ (F.obj Z✝.1).map g.2 = (F.map f.1).app X✝.2 ≫ (F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2 ≫ (F.obj Z✝.1).map g.2
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F : C ⥤ D ⥤ E<VAR>X✝ Y✝ Z✝ : C × D<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>(F.map f.1).app X✝.2 ≫ ((F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2) ≫ (F.obj Z✝.1).map g.2 = (F.map f.1).app X✝.2 ≫ (F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2 ≫ (F.obj Z✝.1).map g.2
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>X✝ Y✝ : C ⥤ D ⥤ E<VAR>T : X✝ ⟶ Y✝<VAR>X Y : C × D<VAR>f : X ⟶ Y<GOAL>((fun F => { obj := fun X => (F.obj X.1).obj X.2, map := fun {X Y} f => (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2, map_id := ⋯, map_comp := ⋯ }) X✝).map f ≫ (fun X => (T.app X.1).app X.2) Y = (fun X => (T.app X.1).app X.2) X ≫ ((fun F => { obj := fun X => (F.obj X.1).obj X.2, map := fun {X Y} f => (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2, map_id := ⋯, map_comp := ⋯ }) Y✝).map f
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>X✝ Y✝ : C ⥤ D ⥤ E<VAR>T : X✝ ⟶ Y✝<VAR>X Y : C × D<VAR>f : X ⟶ Y<GOAL>(X✝.map f.1).app X.2 ≫ (X✝.obj Y.1).map f.2 ≫ (T.app Y.1).app Y.2 = (T.app X.1).app X.2 ≫ (Y✝.map f.1).app X.2 ≫ (Y✝.obj Y.1).map f.2
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>X✝ Y✝ : C ⥤ D ⥤ E<VAR>T : X✝ ⟶ Y✝<VAR>X Y : C × D<VAR>f : X ⟶ Y<GOAL>(X✝.map f.1).app X.2 ≫ (T.app Y.1).app X.2 ≫ (Y✝.obj Y.1).map f.2 = (T.app X.1).app X.2 ≫ (Y✝.map f.1).app X.2 ≫ (Y✝.obj Y.1).map f.2
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>X✝ Y✝ : C ⥤ D ⥤ E<VAR>T : X✝ ⟶ Y✝<VAR>X Y : C × D<VAR>f : X ⟶ Y<GOAL>((T.app X.1).app X.2 ≫ (Y✝.map f.1).app X.2) ≫ (Y✝.obj Y.1).map f.2 = (T.app X.1).app X.2 ≫ (Y✝.map f.1).app X.2 ≫ (Y✝.obj Y.1).map f.2
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : MonoidHomClass 𝓕 E F<VAR>f : 𝓕<GOAL>Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : MonoidHomClass 𝓕 E F<VAR>f : 𝓕<GOAL>(∀ (x y : E), ‖f (x / y)‖ = ‖x / y‖) ↔ ∀ (x : E), ‖f x‖ = ‖x‖
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>a : ℕ →o α<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>¬a n < a m ↔ a n = a m
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>a : ℕ →o α<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>¬(a n ≤ a m ∧ a n ≠ a m) ↔ a n = a m
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>h₃ : S₃.RightHomologyData<VAR>γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂<VAR>γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃<GOAL>rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp a (b - m • p) = toIocMod hp a b
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Finite α<VAR>f : α → β<GOAL>Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin (m * n) → α<VAR>i : Fin n<VAR>j : Fin m<GOAL>m * ↑i + m = m * (↑i + 1)
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin (m * n) → α<GOAL>ofFn f = (ofFn fun i => ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).join
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.22527, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c.symm<VAR>i j : ι<VAR>hij : ¬c.Rel i j<GOAL>(X.d j i).unop = 0
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.22527, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex Vᵒᵖ c.symm<VAR>x✝⁴ x✝³ x✝² : ι<VAR>x✝¹ : c.Rel x✝⁴ x✝³<VAR>x✝ : c.Rel x✝³ x✝²<GOAL>(fun i j => (X.d j i).unop) x✝⁴ x✝³ ≫ (fun i j => (X.d j i).unop) x✝³ x✝² = 0