ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>v : ℕ<VAR>hv : v ≠ 1<VAR>hr : CharP R v<VAR>h : ↑1 = 0<GOAL>v = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ U ∈ 𝓝 x, U ∩ s = {x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : SMul R M<VAR>inst✝² : SMul R S<VAR>inst✝¹ : MulAction S M<VAR>inst✝ : IsScalarTower R S M<VAR>h : a • s = 1<GOAL>IsSMulRegular M 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => r * f x) l atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<GOAL>∀ᶠ (a : α) in l, b ≤ r * f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<VAR>n : ℕ<VAR>hn : 1 ≤ n • r<GOAL>∀ᶠ (a : α) in l, b ≤ r * f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<VAR>n : ℕ<VAR>hn : 1 ≤ r * ↑n<GOAL>∀ᶠ (a : α) in l, b ≤ r * f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>b : R<VAR>n : ℕ<VAR>hn : 1 ≤ r * ↑n<VAR>x : α<VAR>hx : ↑n * max b 0 ≤ f x<GOAL>b ≤ r * f x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.L₁'.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.L₀'.X₂<VAR>hp : π₁ ≫ x₃ = p ≫ S.L₀'.g<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>hπ₂ : Epi π₂<VAR>x₁ : A₂ ⟶ (ShortComplex.mk S.v₁₂.τ₁ S.v₂₃.τ₁ ⋯).X₁<VAR>hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ (ShortComplex.mk S.v₁₂.τ₁ S.v₂₃.τ₁ ⋯).f<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>hπ₂ : Epi π₂<VAR>x₁ : A₂ ⟶ S.L₁.X₁<VAR>hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁<VAR>x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f<VAR>x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>hπ₂ : Epi π₂<VAR>x₁ : A₂ ⟶ S.L₁.X₁<VAR>hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁<VAR>x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f<VAR>x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃<VAR>hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>hπ₂ : Epi π₂<VAR>x₁ : A₂ ⟶ S.L₁.X₁<VAR>hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁<VAR>x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f<VAR>x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃<VAR>hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0<VAR>k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>hπ₂ : Epi π₂<VAR>x₁ : A₂ ⟶ S.L₁.X₁<VAR>hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁<VAR>x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f<VAR>x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃<VAR>hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0<VAR>k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'<VAR>hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A₀ : C<VAR>x₃ : A₀ ⟶ S.L₀.X₃<VAR>hx₃ : x₃ ≫ S.δ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A₀<VAR>hπ₁ : Epi π₁<VAR>p : A₁ ⟶ S.P<VAR>hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<VAR>hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>hπ₂ : Epi π₂<VAR>x₁ : A₂ ⟶ S.L₁.X₁<VAR>hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁<VAR>x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f<VAR>x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃<VAR>hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0<VAR>k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'<VAR>hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'<VAR>hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>inst✝ : Algebra R S<VAR>f : τ → S<VAR>g : σ → MvPolynomial τ R<VAR>i✝ : σ<GOAL>((aeval f).comp (bind₁ g)) (X i✝) = (aeval fun i => (aeval f) (g i)) (X i✝)
<VAR>q✝ a b c p q : ℚ<GOAL>p = q ↔ p.num * ↑q.den = q.num * ↑p.den
<VAR>q✝ a b c p q : ℚ<GOAL>p.num /. ↑p.den = q.num /. ↑q.den ↔ p.num * ↑q.den = q.num * ↑p.den
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>logDeriv f x = 0
<VAR>step s n : Nat<GOAL>range' s (n + 1) step = range' s n step ++ [s + step * n]
<VAR>step s n : Nat<GOAL>range' s (1 + n) step = range' s n step ++ [s + step * n]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>a⁻¹ < b ↔ 1 < b * a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>1 / a < b ↔ 1 < b * a
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<GOAL>(boundedBy m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (t n)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g : G<GOAL>x * of' k G g %ᵒᶠ g = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g g' : G<GOAL>(x * of' k G g %ᵒᶠ g) g' = 0 g'
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g g' : G<GOAL>(x * of' k G g %ᵒᶠ g) g' = 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<GOAL>ContDiffOn ℝ ⊤ (uncurry y) (Ioo 0 1 ×ˢ univ)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>hs : IsOpen (Ioo 0 1)<GOAL>ContDiffOn ℝ ⊤ (uncurry y) (Ioo 0 1 ×ˢ univ)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>hs : IsOpen (Ioo 0 1)<VAR>hk : IsCompact (closedBall 0 1)<GOAL>ContDiffOn ℝ ⊤ (uncurry y) (Ioo 0 1 ×ˢ univ)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>hs : IsOpen (Ioo 0 1)<VAR>hk : IsCompact (closedBall 0 1)<GOAL>∀ (p : ℝ) (x : E), p ∈ Ioo 0 1 → x ∉ closedBall 0 1 → w p x = 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>hs : IsOpen (Ioo 0 1)<VAR>hk : IsCompact (closedBall 0 1)<GOAL>LocallyIntegrable φ μ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>hs : IsOpen (Ioo 0 1)<VAR>hk : IsCompact (closedBall 0 1)<GOAL>ContDiffOn ℝ ⊤ (↿w) (Ioo 0 1 ×ˢ univ)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃
<VAR>f✝ f : StieltjesFunction<GOAL>{x | leftLim (↑f) x ≠ ↑f x}.Countable
<VAR>f✝ f : StieltjesFunction<GOAL>{x | leftLim (↑f) x ≠ ↑f x} ⊆ {x | ¬ContinuousAt (↑f) x}
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<VAR>hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}<VAR>h'x : ContinuousAt (↑f) x<GOAL>leftLim (↑f) x = ↑f x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<GOAL>∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<VAR>hUo : ∀ (i : ι), IsOpen (U i)<GOAL>∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>u : Set ι<VAR>hucount : u.Countable<VAR>husub : s ⊆ ⋃ i ∈ u, U i<GOAL>∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>u : Set ι<VAR>hucount : u.Countable<VAR>husub : s ⊆ ⋃ i ∈ u, U i<GOAL>s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>u : Set ι<VAR>hucount : u.Countable<VAR>husub : Disjoint (⋃ i ∈ u, U i)ᶜ s<GOAL>s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>U : ι → Set X := tᶜ<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>u : Set ι<VAR>hucount : u.Countable<VAR>husub : Disjoint (⋂ i ∈ u, t i) s<GOAL>s ∩ ⋂ i ∈ u, t i = ∅
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>x y : ℕ → α<VAR>h : res x = res y<VAR>n : ℕ<GOAL>x n = y n
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>x y : ℕ → α<VAR>h : res x = res y<VAR>n : ℕ<GOAL>res x n.succ = res y n.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>f' : β ≃ γ<VAR>f'' : γ ≃ δ<GOAL>(e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace G<VAR>inst✝ : μ.InnerRegular<VAR>E : Set G<VAR>hE : MeasurableSet E<VAR>hEpos : 0 < μ E<VAR>K : Set G<VAR>hKE : K ⊆ E<VAR>hK : IsCompact K<VAR>K_closed : IsClosed K<VAR>hKpos : 0 < μ K<GOAL>E / E ∈ 𝓝 1
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace G<VAR>inst✝ : μ.InnerRegular<VAR>E : Set G<VAR>hE : MeasurableSet E<VAR>hEpos : 0 < μ E<VAR>K : Set G<VAR>hKE : K ⊆ E<VAR>hK : IsCompact K<VAR>K_closed : IsClosed K<VAR>hKpos : 0 < μ K<VAR>g : G<VAR>hg : μ (g • K \ K) < μ K<GOAL>g ∈ E / E
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace G<VAR>inst✝ : μ.InnerRegular<VAR>E : Set G<VAR>hE : MeasurableSet E<VAR>hEpos : 0 < μ E<VAR>K : Set G<VAR>hKE : K ⊆ E<VAR>hK : IsCompact K<VAR>K_closed : IsClosed K<VAR>hKpos : 0 < μ K<VAR>g : G<VAR>hg : μ (g • K \ K) < μ K<VAR>this : ¬Disjoint (g • K) K<GOAL>g ∈ E / E
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace G<VAR>inst✝ : μ.InnerRegular<VAR>E : Set G<VAR>hE : MeasurableSet E<VAR>hEpos : 0 < μ E<VAR>K : Set G<VAR>hKE : K ⊆ E<VAR>hK : IsCompact K<VAR>K_closed : IsClosed K<VAR>hKpos : 0 < μ K<VAR>g : G<VAR>hg : μ (g • K \ K) < μ K<VAR>this : ¬Disjoint (g • K) K<VAR>x : G<VAR>hxK : x ∈ K<VAR>hgxK : (fun x => g • x) x ∈ K<GOAL>g ∈ E / E
<VAR>R : Type u_1<VAR>inst✝ : Zero R<VAR>n : R<GOAL>¬NeZero n ↔ n = 0
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<GOAL>LinearIndependent R (Sum.elim (fun x => ↑(f x)) g)
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<GOAL>Disjoint (span R (range fun x => ↑(f x))) (span R (range g))
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<VAR>x : M<VAR>h₁ : x ∈ span R (range fun x => ↑(f x))<VAR>h₂ : x ∈ span R (range g)<GOAL>x = 0
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<VAR>x : M<VAR>h₁ : x ∈ span R (range fun x => ↑(f x))<VAR>h₂ : x ∈ span R (range g)<VAR>this : x ∈ M'<GOAL>x = 0
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<VAR>c : ι₂ →₀ R<VAR>h₁ : (c.sum fun i a => a • g i) ∈ span R (range fun x => ↑(f x))<VAR>h₂ : (c.sum fun i a => a • g i) ∈ span R (range g)<VAR>this : (c.sum fun i a => a • g i) ∈ M'<GOAL>(c.sum fun i a => a • g i) = 0
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<VAR>c : ι₂ →₀ R<VAR>h₁ : (c.sum fun i a => a • g i) ∈ span R (range fun x => ↑(f x))<VAR>h₂ : (c.sum fun i a => a • g i) ∈ span R (range g)<VAR>this : (c.sum fun a b => b • Submodule.Quotient.mk (g a)) = 0<GOAL>(c.sum fun i a => a • g i) = 0
<VAR>M : Type u_1<VAR>inst✝ : DivisionMonoid M<VAR>a b c d : M<VAR>hbd : Commute b d<VAR>hb : IsUnit b<VAR>hd : IsUnit d<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<GOAL>(-A).det = (-1) ^ Fintype.card n * A.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>inst✝¹ : f₁.NeBot<VAR>inst✝ : g₁.NeBot<GOAL>f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>inst✝¹ : f₁.NeBot<VAR>inst✝ : g₁.NeBot<VAR>h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂<GOAL>f₁ = f₂ ∧ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>inst✝¹ : f₁.NeBot<VAR>inst✝ : g₁.NeBot<VAR>h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂<VAR>hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂<GOAL>f₁ = f₂ ∧ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>inst✝¹ : f₁.NeBot<VAR>inst✝ : g₁.NeBot<VAR>h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂<VAR>hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂<VAR>this : f₂.NeBot<GOAL>f₁ = f₂ ∧ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>inst✝¹ : f₁.NeBot<VAR>inst✝ : g₁.NeBot<VAR>h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂<VAR>hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂<VAR>this✝ : f₂.NeBot<VAR>this : g₂.NeBot<GOAL>f₁ = f₂ ∧ g₁ = g₂
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<GOAL>∃ n > 0, (↑n)⁻¹ * a < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>n : ℕ<VAR>npos : n > 0<VAR>hn : a < ↑n * b<GOAL>∃ n > 0, (↑n)⁻¹ * a < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>n : ℕ<VAR>npos : n > 0<VAR>hn : a < ↑n * b<GOAL>(↑n)⁻¹ * a < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>n : ℕ<VAR>npos : n > 0<VAR>hn : a < ↑n * b<GOAL>a / ↑n < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>o : α → Option β<VAR>f : α → σ<VAR>g : α → β → σ<VAR>ho : Computable o<VAR>hf : Computable f<VAR>hg : Computable₂ g<VAR>a : α<GOAL>(Nat.casesOn (encode (o a)) (Option.some (f a)) fun n => Option.map (g a) (decode n)) = Option.some (Option.casesOn (o a) (f a) (g a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>ContinuousWithinAt f s (x.1, x.2) ↔ ContinuousWithinAt (fun x_1 => f (x_1, (x.1, x.2).2)) {a | (a, (x.1, x.2).2) ∈ s} (x.1, x.2).1