ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<VAR>a : K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hgI : a * g j ∉ ↑(RingHom.ker (algebraMap R S))<VAR>g'' : (i : ι) → i ∈ s → R<VAR>hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i<VAR>this : (a : Prop) → Decidable a := Classical.propDecidable<VAR>g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0<VAR>hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i<GOAL>∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<VAR>a : K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hgI✝ : a * g j ∉ ↑(RingHom.ker (algebraMap R S))<VAR>g'' : (i : ι) → i ∈ s → R<VAR>hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i<VAR>this : (a : Prop) → Decidable a := Classical.propDecidable<VAR>g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0<VAR>hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i<VAR>hgI : (algebraMap R S) (g' j) ≠ 0<GOAL>∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<VAR>a : K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hgI✝ : a * g j ∉ ↑(RingHom.ker (algebraMap R S))<VAR>g'' : (i : ι) → i ∈ s → R<VAR>hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i<VAR>this : (a : Prop) → Decidable a := Classical.propDecidable<VAR>g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0<VAR>hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i<VAR>hgI : (algebraMap R S) (g' j) ≠ 0<GOAL>∑ i ∈ s, (fun i => (algebraMap R S) (g' i)) i • (⇑f' ∘ b) i = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq✝ : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<VAR>a : K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hgI✝ : a * g j ∉ ↑(RingHom.ker (algebraMap R S))<VAR>g'' : (i : ι) → i ∈ s → R<VAR>hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i<VAR>this : (a : Prop) → Decidable a := Classical.propDecidable<VAR>g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0<VAR>hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i<VAR>hgI : (algebraMap R S) (g' j) ≠ 0<VAR>eq : f (∑ i ∈ s, g' i • b i) = 0<GOAL>∑ i ∈ s, (fun i => (algebraMap R S) (g' i)) i • (⇑f' ∘ b) i = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>inst✝⁶ : SMul M α<VAR>inst✝⁵ : SMul M β✝<VAR>inst✝⁴ : SMul N α<VAR>inst✝³ : SMul N β✝<VAR>a✝ : M<VAR>x : α × β✝<VAR>β : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid β<VAR>inst✝ : DistribMulAction M β<VAR>a : M<VAR>b : α<GOAL>a • (b, 0) = (a • b, 0)
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>k : arctan x⁻¹ + arctan y⁻¹ = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y<GOAL>(x + y) / (1 - x * y) = -((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y<GOAL>(x + y) / (1 - x * y) = (-x + -y) / (x * y - 1)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hne : Even n ∧ ¬Odd n<GOAL>a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hn✝ : n ≠ 0<VAR>hn : Odd n ∧ ¬Even n<GOAL>a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>p : X → Prop<GOAL>(∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>p : X → Prop<GOAL>(¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>f = 0 ↔ ↑f = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>μ : Ordinal.{u}<GOAL>P I μ
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>μ o : Ordinal.{u}<VAR>h : P I o<VAR>ho : Order.succ o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<GOAL>LinearIndependent ℤ (eval C)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>μ o : Ordinal.{u}<VAR>h : P I o<VAR>ho : Order.succ o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho' : o < Ordinal.type fun x x_1 => x < x_1<GOAL>LinearIndependent ℤ (eval C)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>μ o : Ordinal.{u}<VAR>h : P I o<VAR>ho : Order.succ o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho' : o < Ordinal.type fun x x_1 => x < x_1<GOAL>LinearIndependent ℤ (SumEval C ho')
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>μ o : Ordinal.{u}<VAR>h : P I o<VAR>ho : Order.succ o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho' : o < Ordinal.type fun x x_1 => x < x_1<GOAL>LinearIndependent (ι := ↑(GoodProducts (π C fun x => ord I x < o))) ℤ (eval (π C fun x => ord I x < o))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>μ o : Ordinal.{u}<VAR>h : P I o<VAR>ho : Order.succ o ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho' : o < Ordinal.type fun x x_1 => x < x_1<GOAL>LinearIndependent (ι := ↑(MaxProducts C ho')) ℤ (⇑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho')) ⋯).g ∘ SumEval C ho' ∘ Sum.inr)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝ : AddCommMonoid E<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>y : Ω<GOAL>stoppedValue u τ y = (∑ i ∈ s, {ω | τ ω = i}.indicator (u i)) y
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝ : AddCommMonoid E<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>y : Ω<GOAL>u (τ y) y = ∑ i ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s, u i y
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝ : AddCommMonoid E<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>y : Ω<GOAL>Finset.filter (fun i => y ∈ {ω | τ ω = i}) s = {τ y}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝ : AddCommMonoid E<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>y : Ω<VAR>ω : ι<GOAL>ω ∈ Finset.filter (fun i => y ∈ {ω | τ ω = i}) s ↔ ω ∈ {τ y}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝ : AddCommMonoid E<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>y : Ω<VAR>ω : ι<GOAL>ω ∈ s ∧ τ y = ω ↔ ω = τ y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>hausdorffDist s t = 0 ↔ s = t
<VAR>n m : ℕ<GOAL>n ≤ n.dist m + m
<VAR>n m : ℕ<GOAL>n ≤ m.dist n + m
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Nonempty β<VAR>a b : α<GOAL>const β a ≤ const β b ↔ a ≤ b
<VAR>n : ℕ<VAR>h : 0 + 2 ≤ n<GOAL>(n - (0 + 1)) ^ (0 + 2) < n.descFactorial (0 + 2)
<VAR>n : ℕ<VAR>h : 0 + 2 ≤ n<GOAL>(n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
<VAR>n k : ℕ<VAR>h : k + 1 + 2 ≤ n<GOAL>(n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)
<VAR>n k : ℕ<VAR>h : k + 1 + 2 ≤ n<GOAL>(n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
<VAR>n k : ℕ<VAR>h : k + 1 + 2 ≤ n<GOAL>(n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
<VAR>n k : ℕ<VAR>h : k + 1 + 2 ≤ n<GOAL>(n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
<VAR>n k : ℕ<VAR>h : k + 1 + 2 ≤ n<GOAL>(n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
<VAR>μ : YoungDiagram<VAR>x : ℕ<VAR>hx : x ∈ μ.rowLens<GOAL>0 < x
<VAR>μ : YoungDiagram<VAR>x : ℕ<VAR>hx : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x<GOAL>0 < x
<VAR>μ : YoungDiagram<VAR>i : ℕ<VAR>hi : i ∈ List.range (μ.colLen 0)<GOAL>0 < μ.rowLen i
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>(isoRestrict f).inv ≫ f = Y.ofRestrict ⋯
<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>b + m • p - (toIocDiv hp a b + m) • p ∈ Set.Ioc a (a + p)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r : X<VAR>s t : ↥S<GOAL>(↑s /ₒ t) • (r /ₒ s) = r /ₒ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h₁ : Continuous f<VAR>h₂ : Injective f<VAR>h₃ : IsClosedMap f<GOAL>ClosedEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h₁ : Continuous f<VAR>h₂ : Injective f<VAR>h₃ : IsClosedMap f<GOAL>inst✝² = induced f inst✝¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h₁ : Continuous f<VAR>h₂ : Injective f<VAR>h₃ : IsClosedMap f<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpen s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h₁ : Continuous f<VAR>h₂ : Injective f<VAR>h₃ : IsClosedMap f<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>f ⁻¹' (f '' sᶜ)ᶜ = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hmono : Monotone f<VAR>x : X<GOAL>IntegrableAtFilter f (𝓝 x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hmono : Monotone f<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<GOAL>IntegrableAtFilter f (𝓝 x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hmono : Monotone f<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<VAR>a b : X<VAR>xab : x ∈ Icc a b<VAR>hab : Icc a b ∈ 𝓝 x<VAR>abU : Icc a b ⊆ U<GOAL>IntegrableAtFilter f (𝓝 x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hmono : Monotone f<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<VAR>a b : X<VAR>xab : x ∈ Icc a b<VAR>hab : Icc a b ∈ 𝓝 x<VAR>abU : Icc a b ⊆ U<VAR>ab : a ≤ b<GOAL>IntegrableAtFilter f (𝓝 x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹² : MeasurableSpace X<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace Y<VAR>inst✝⁹ : TopologicalSpace Y<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder E<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : OrderTopology E<VAR>inst✝¹ : SecondCountableTopology E<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hmono : Monotone f<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<VAR>a b : X<VAR>xab : x ∈ Icc a b<VAR>hab : Icc a b ∈ 𝓝 x<VAR>abU : Icc a b ⊆ U<VAR>ab : a ≤ b<GOAL>IntegrableOn f (Icc a b) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : CommGroup α<VAR>inst✝² : CommGroup β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s t u : Finset α<VAR>a✝ : α<VAR>d : ℕ<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<GOAL>Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : CommGroup α<VAR>inst✝² : CommGroup β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s t u : Finset α<VAR>a✝ : α<VAR>d : ℕ<VAR>a : α<VAR>ha : a ∈ s<GOAL>∏ a_1 ∈ s, a_1 ^ Pi.single a 1 a_1 = a
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp 2 β<GOAL>dist x y = √(∑ x_1 : ι, dist (x x_1) (y x_1) ^ 2)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f✝ f g : β → α<VAR>hs : ∃ x ∈ s, f x ≠ 0<VAR>hg : ∀ b ∈ s, f b = s.gcd f * g b<GOAL>s.gcd f * s.gcd g = s.gcd f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f✝ f g : β → α<VAR>hs : ∃ x ∈ s, f x ≠ 0<VAR>hg : ∀ b ∈ s, f b = s.gcd f * g b<GOAL>¬s.gcd f = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f✝ f g : β → α<VAR>hg : ∀ b ∈ s, f b = s.gcd f * g b<VAR>hs : s.gcd f = 0<GOAL>∀ x ∈ s, f x = 0
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : Z → X<VAR>z : Z<VAR>e : Trivialization F proj<VAR>he : proj z ∈ e.baseSet<VAR>hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)<GOAL>ContinuousAt f z
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : Z → X<VAR>z : Z<VAR>e : Trivialization F proj<VAR>he : proj z ∈ e.baseSet<VAR>hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)<VAR>hez : z ∈ e.symm.target<GOAL>ContinuousAt f z
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>(aleph (succ o)).IsRegular
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>(succ (aleph o)).IsRegular
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : ProperSpace E<VAR>inst✝² : ProperSpace F<VAR>f : 𝓕<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : CocompactMapClass 𝓕 E F<VAR>ε : ℝ<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : ProperSpace E<VAR>inst✝² : ProperSpace F<VAR>f : 𝓕<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : CocompactMapClass 𝓕 E F<VAR>ε : ℝ<VAR>h : Tendsto (⇑f) (cocompact E) (cocompact F)<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : ProperSpace E<VAR>inst✝² : ProperSpace F<VAR>f : 𝓕<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : CocompactMapClass 𝓕 E F<VAR>ε : ℝ<VAR>h : ∀ s ∈ cocompact F, ⇑f ⁻¹' s ∈ cocompact E<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : ProperSpace E<VAR>inst✝² : ProperSpace F<VAR>f : 𝓕<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : CocompactMapClass 𝓕 E F<VAR>ε : ℝ<VAR>h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : ProperSpace E<VAR>inst✝² : ProperSpace F<VAR>f : 𝓕<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : CocompactMapClass 𝓕 E F<VAR>ε : ℝ<VAR>h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E<VAR>r : ℝ<VAR>hr : (closedBall 0 r)ᶜ ⊆ ⇑f ⁻¹' (closedBall 0 ε)ᶜ<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : ProperSpace E<VAR>inst✝² : ProperSpace F<VAR>f : 𝓕<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : CocompactMapClass 𝓕 E F<VAR>ε : ℝ<VAR>h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E<VAR>r : ℝ<VAR>hr : (closedBall 0 r)ᶜ ⊆ ⇑f ⁻¹' (closedBall 0 ε)ᶜ<GOAL>∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j✝ : n<VAR>b : n → α<VAR>c✝ : m → α<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m n α<VAR>j : n<VAR>c : m → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.updateColumn j c).submatrix ⇑e ⇑f = (A.updateColumn (f (f.symm j)) fun i => c (e (e.symm i))).submatrix ⇑e ⇑f
<VAR>a b m n✝ p✝ n p k : ℕ<VAR>hn : n ≠ 0<VAR>h : n.factorization = single p k<GOAL>n = p ^ k