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>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : SemilatticeSup δ<VAR>inst✝ : OrderBot δ<VAR>g : γ → δ<GOAL>(image₂ f s t).sup g = s.sup fun x => t.sup fun x_1 => g (f x x_1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : SemilatticeSup δ<VAR>inst✝ : OrderBot δ<VAR>g : γ → δ<GOAL>(s.sup fun i => t.sup fun i' => (g ∘ uncurry f) (i, i')) = s.sup fun x => t.sup fun x_1 => g (f x x_1)
<VAR>f : ℂ → ℂ<VAR>c z : ℂ<VAR>R R₁ R₂ : ℝ<VAR>hd : DifferentiableOn ℂ f (ball 0 R)<VAR>h_maps : MapsTo f (ball 0 R) (ball 0 R)<VAR>h₀ : f 0 = 0<VAR>hz : abs z < R<GOAL>abs (f z) ≤ abs z
<VAR>f : ℂ → ℂ<VAR>c z : ℂ<VAR>R R₁ R₂ : ℝ<VAR>hd : DifferentiableOn ℂ f (ball 0 R)<VAR>h_maps : MapsTo f (ball 0 R) (ball 0 R)<VAR>h₀ : f 0 = 0<VAR>hz : z ∈ ball 0 R<GOAL>abs (f z) ≤ abs z
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<GOAL>deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<GOAL>deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<GOAL>deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<GOAL>deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<GOAL>deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<GOAL>deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<VAR>hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)<GOAL>deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<VAR>hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)<GOAL>-deriv f 1 = γ
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<VAR>hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)<VAR>derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)<GOAL>-deriv f 1 = γ
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<VAR>hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)<VAR>derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)<VAR>derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)<GOAL>-deriv f 1 = γ
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<VAR>hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)<VAR>derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)<VAR>derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)<GOAL>-deriv f 1 ≤ γ
<VAR>n : ℕ<VAR>f : ℝ → ℝ := log ∘ Gamma<VAR>hc : ConvexOn ℝ (Ioi 0) f<VAR>h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x<VAR>hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x<VAR>hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x<VAR>hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)<VAR>derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)<VAR>derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)<GOAL>γ ≤ -deriv f 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>h₁ : p % 2 = 1<GOAL>p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>h₁ : p % 8 % 2 = 1<GOAL>p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>h₁ : p % 8 % 2 = 1<VAR>h₂ : p % 8 < 8<GOAL>p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
<VAR>α : Type u<VAR>f : Filter α<VAR>s✝ t s : Set α<GOAL>s ∈ f ↔ s ∈ f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝³ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝ : IsNoetherian R M<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))<GOAL>(trace R M) f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝³ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝ : IsNoetherian R M<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))<VAR>hN : {i | N i ≠ ⊥}.Finite<GOAL>(trace R M) f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝³ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝ : IsNoetherian R M<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))<VAR>hN : {i | N i ≠ ⊥}.Finite<VAR>s : Finset ι := hN.toFinset<VAR>κ : ι → Type u_3 := fun i => Module.Free.ChooseBasisIndex R ↥(N i)<VAR>b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i) := fun i => Module.Free.chooseBasis R ↥(N ↑i)<GOAL>(trace R M) f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝ : IsNoetherian R M<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))<VAR>hN : {i | N i ≠ ⊥}.Finite<VAR>s : Finset ι := hN.toFinset<VAR>κ : ι → Type u_3 := fun i => Module.Free.ChooseBasisIndex R ↥(N i)<VAR>b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i) := fun i => Module.Free.chooseBasis R ↥(N ↑i)<VAR>h : IsInternal fun i => N ↑i<GOAL>(trace R M) f = 0
<VAR>ξ : ℝ<VAR>u v✝ : ℤ<VAR>hv : 2 ≤ v✝<VAR>v : ℕ<VAR>h : ContfracLegendre.Ass ξ u ↑v<GOAL>∃ n, ↑u / ↑v = ξ.convergent n
<VAR>v✝ : ℤ<VAR>hv : 2 ≤ v✝<VAR>v : ℕ<VAR>ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n<VAR>ξ : ℝ<VAR>u : ℤ<VAR>h : ContfracLegendre.Ass ξ u ↑v<GOAL>∃ n, ↑u / ↑v = ξ.convergent n
<VAR>v✝ : ℤ<VAR>hv : 2 ≤ v✝<VAR>v : ℕ<VAR>ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n<VAR>ξ : ℝ<VAR>u : ℤ<VAR>h : ContfracLegendre.Ass ξ u ↑v<VAR>ht : v < 1<GOAL>∃ n, ↑u / ↑v = ξ.convergent n
<VAR>v : ℤ<VAR>hv : 2 ≤ v<VAR>ξ : ℝ<VAR>u : ℤ<VAR>ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n<VAR>h : ContfracLegendre.Ass ξ u ↑1<GOAL>∃ n, ↑u / ↑1 = ξ.convergent n
<VAR>v✝ : ℤ<VAR>hv : 2 ≤ v✝<VAR>v : ℕ<VAR>ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n<VAR>ξ : ℝ<VAR>u : ℤ<VAR>h : ContfracLegendre.Ass ξ u ↑v<VAR>ht : 1 < v<GOAL>∃ n, ↑u / ↑v = ξ.convergent n
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>h : M ≃[L] N<VAR>f g : N ≃[L] P<VAR>hfg : (fun f => f.comp h) f = (fun f => f.comp h) g<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<GOAL>IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<GOAL>IntegrableAtFilter f (l ⊓ ae μ) μ → IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t✝ : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>t : Set α<VAR>ht : t ∈ l<VAR>u : Set α<VAR>hu : u ∈ ae μ<VAR>hf : IntegrableOn f (t ∩ u) μ<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t✝ : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>t : Set α<VAR>ht : t ∈ l<VAR>u : Set α<VAR>hu : u ∈ ae μ<VAR>hf : IntegrableOn f (t ∩ u) μ<GOAL>∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)<VAR>k : ZMod (minimalPeriod (fun x => g • x) (Quotient.out' q))<GOAL>↑((toEquiv ⋯) (g ^ k.cast • Quotient.out' q)) = g ^ k.cast * Quotient.out' (Quotient.out' q)
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<GOAL>IsLocalization M S ↔ IsLocalization (Submonoid.map h.toMonoidHom M) S
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<GOAL>IsLocalization (Submonoid.map h.toMonoidHom M) S → IsLocalization M S
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<GOAL>IsLocalization M S
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<GOAL>M = Submonoid.map h.symm.toMonoidHom (Submonoid.map h.toMonoidHom M)
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<GOAL>inst✝¹ = ((algebraMap P S).comp h.symm.symm.toRingHom).toAlgebra
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<GOAL>inst✝¹ = ((algebraMap R S).comp (h.symm.toRingHom.comp h.symm.symm.toRingHom)).toAlgebra
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<GOAL>inst✝¹ = (algebraMap R S).toAlgebra
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<GOAL>∀ (r : R), (algebraMap R S) r = (algebraMap R S) r
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>h : R ≃+* P<VAR>this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra<VAR>H : IsLocalization (Submonoid.map h.toMonoidHom M) S<VAR>r : R<GOAL>(algebraMap R S) r = (algebraMap R S) r
<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : SeparableSpace X<VAR>inst✝¹ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>inst✝ : DiscreteTopology ↑s<GOAL>#↑s < 𝔠
<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : SeparableSpace X<VAR>inst✝¹ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>inst✝ : DiscreteTopology ↑s<VAR>h : 𝔠 ≤ #↑s<GOAL>False
<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : SeparableSpace X<VAR>inst✝¹ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>inst✝ : DiscreteTopology ↑s<VAR>h : 𝔠 ≤ #↑s<VAR>t : Set X<VAR>htc : t.Countable<VAR>htd : Dense t<GOAL>False
<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : SeparableSpace X<VAR>inst✝¹ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>inst✝ : DiscreteTopology ↑s<VAR>h : 𝔠 ≤ #↑s<VAR>t : Set X<VAR>htc : t.Countable<VAR>htd : Dense t<VAR>this : Countable ↑t<GOAL>False
<VAR>X : Type u<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : SeparableSpace X<VAR>inst✝¹ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>inst✝ : DiscreteTopology ↑s<VAR>h : 𝔠 ≤ #↑s<VAR>t : Set X<VAR>htc : t.Countable<VAR>htd : Dense t<VAR>this : Countable ↑t<GOAL>2 ^ 𝔠 ≤ 𝔠
<VAR>u : ℤˣ<GOAL>u⁻¹ = u
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Set C<VAR>c : C<GOAL>c ∈ (full D).objs ↔ c ∈ D
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E'✝ : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'✝<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'✝<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>inst✝¹ : Fintype ι<VAR>E' : ι → Type u_18<VAR>inst✝ : (i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<GOAL>f =o[l] g' ↔ ∀ (i : ι), (fun x => f x i) =o[l] g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E'✝ : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'✝<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'✝<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>inst✝¹ : Fintype ι<VAR>E' : ι → Type u_18<VAR>inst✝ : (i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith c l (fun x => f x i) g') ↔ ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f x i) g'
<VAR>x✝ y x : ℝ<VAR>hx : 0 < cos x<GOAL>(√(1 + tan x ^ 2))⁻¹ = cos x
<VAR>n : Nat<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>p : α✝ → Bool<GOAL>findIdx? p (replicate n a) = if 0 < n ∧ p a = true then some 0 else none
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 0<GOAL>p.degree ≤ 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 0<VAR>this : p.degree ≤ 0<VAR>hc : p.coeff 0 = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : (C 0).degree = 0<VAR>this : p.degree ≤ 0<VAR>hc : p.coeff 0 = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>this : p.degree ≤ 0<VAR>hc : p.coeff 0 = 0<VAR>h : degree 0 = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 0<VAR>this : p.degree ≤ 0<VAR>hc : p.coeff 0 ≠ 0<GOAL>1 = p * C (p.coeff 0)⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 0<VAR>this : p.degree ≤ 0<VAR>hc : p.coeff 0 ≠ 0<GOAL>1 = C (p.coeff 0) * C (p.coeff 0)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>(∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x) ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P : Karoubi C<GOAL>(𝟙 P).f = (P.decompId_i ≫ P.decompId_p).f
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>t : Set Ω<VAR>h_indep : IndepSet t t μ<GOAL>μ t = 0 ∨ μ t = 1
<VAR>b u v w : Ordinal.{u_1}<VAR>hvb : v < b<VAR>hw : w < b ^ u<GOAL>b ^ u * v + w < b ^ succ u
<VAR>b u v w : Ordinal.{u_1}<VAR>hvb : v < b<VAR>hw : w < b ^ u<GOAL>b ^ succ u = b ^ u * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>f : α → β<VAR>hf : Injective f<VAR>inst✝ : Nonempty α<VAR>b : β<VAR>h : b ∈ Set.range f<GOAL>f ((Set.range f).restrict (invFun f) ⟨b, h⟩) = f (hf.invOfMemRange ⟨b, h⟩)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>S : Finset Λ<VAR>q₁ q₂ : Stmt₁<VAR>h : q₁ ∈ stmts₁ q₂<VAR>hs : SupportsStmt S q₂<GOAL>SupportsStmt S q₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι✝ : Sort uι<VAR>s t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>ι : Type u_6<VAR>inst✝¹ : Countable ι<VAR>inst✝ : Nonempty ι<VAR>t : ι → Set α<VAR>t_meas : ∀ (n : ι), MeasurableSet (t n)<VAR>g : ι → α → β<VAR>hg : ∀ (n : ι), Measurable (g n)<VAR>ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)<VAR>inhabited_h : Inhabited ι<VAR>g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val<VAR>ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩<GOAL>∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι✝ : Sort uι<VAR>s t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>ι : Type u_6<VAR>inst✝¹ : Countable ι<VAR>inst✝ : Nonempty ι<VAR>t : ι → Set α<VAR>t_meas : ∀ (n : ι), MeasurableSet (t n)<VAR>g : ι → α → β<VAR>hg : ∀ (n : ι), Measurable (g n)<VAR>ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)<VAR>inhabited_h : Inhabited ι<VAR>g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val<VAR>ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩<VAR>f : ↑(⋃ i, t i) → β := iUnionLift t g' ht' (⋃ i, t i) ⋯<GOAL>∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι✝ : Sort uι<VAR>s t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>ι : Type u_6<VAR>inst✝¹ : Countable ι<VAR>inst✝ : Nonempty ι<VAR>t : ι → Set α<VAR>t_meas : ∀ (n : ι), MeasurableSet (t n)<VAR>g : ι → α → β<VAR>hg : ∀ (n : ι), Measurable (g n)<VAR>ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)<VAR>inhabited_h : Inhabited ι<VAR>g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val<VAR>ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩<VAR>f : ↑(⋃ i, t i) → β := iUnionLift t g' ht' (⋃ i, t i) ⋯<VAR>hfm : Measurable f<GOAL>∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x y : α<VAR>r : ℝ<VAR>h : dist x y ≤ K * r<VAR>rpos : 0 < r<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<GOAL>closedBall y r ∈ (vitaliFamily μ K).setsAt x
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x y : α<VAR>r : ℝ<VAR>h : dist x y ≤ K * r<VAR>rpos : 0 < r<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<GOAL>(∃ r_1, closedBall y r ⊆ closedBall x r_1 ∧ μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)) ∨ ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)