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>inst✝⁵ : Countable ι✝<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>ι : Type u_5<VAR>inst✝² : PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁵ : Countable ι✝<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>ι : Type u_5<VAR>inst✝² : PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁵ : Countable ι✝<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>ι : Type u_5<VAR>inst✝² : PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>p : α → Prop<VAR>hb : p ⊥<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>p (s.sup f)
<VAR>n m p : ℕ<VAR>pp : Prime p<VAR>h : 1 = 1 ∨ m ≤ minFac 1<VAR>d : p ∣ 1<GOAL>m ≤ p
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ j₃ k₁ k₂ l : C<VAR>f₁ : j₁ ⟶ k₁<VAR>f₂ : j₂ ⟶ k₁<VAR>f₃ : j₂ ⟶ k₂<VAR>f₄ : j₃ ⟶ k₂<VAR>g₁ : j₁ ⟶ l<VAR>g₂ : j₃ ⟶ l<GOAL>∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ j₃ k₁ k₂ l : C<VAR>f₁ : j₁ ⟶ k₁<VAR>f₂ : j₂ ⟶ k₁<VAR>f₃ : j₂ ⟶ k₂<VAR>f₄ : j₃ ⟶ k₂<VAR>g₁ : j₁ ⟶ l<VAR>g₂ : j₃ ⟶ l<VAR>l' : C<VAR>k₁l : k₁ ⟶ l'<VAR>k₂l : k₂ ⟶ l'<VAR>hl : f₂ ≫ k₁l = f₃ ≫ k₂l<GOAL>∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ j₃ k₁ k₂ l : C<VAR>f₁ : j₁ ⟶ k₁<VAR>f₂ : j₂ ⟶ k₁<VAR>f₃ : j₂ ⟶ k₂<VAR>f₄ : j₃ ⟶ k₂<VAR>g₁ : j₁ ⟶ l<VAR>g₂ : j₃ ⟶ l<VAR>l' : C<VAR>k₁l : k₁ ⟶ l'<VAR>k₂l : k₂ ⟶ l'<VAR>hl : f₂ ≫ k₁l = f₃ ≫ k₂l<VAR>s : C<VAR>ls : l ⟶ s<VAR>l's : l' ⟶ s<VAR>hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's<VAR>hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's<GOAL>∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊥, ⊥)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < ↑x
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>r : ℝ<VAR>x✝ : EReal × EReal<VAR>h : x✝.1 < ↑0 ∧ x✝.2 < ↑r<GOAL>x✝.1 + x✝.2 < ↑r
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : SMulWithZero α β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t✝ t : Finset β<GOAL>0 • t ⊆ 0
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<VAR>w₁ : m ∈ b<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<VAR>w₁ : m ∈ b<VAR>w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<VAR>w₁ : m ∈ b<VAR>w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m<VAR>i₁ : (Finset.erase b m).card < Finset.card b<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<VAR>w₁ : m ∈ b<VAR>w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m<VAR>i₁ : (Finset.erase b m).card < Finset.card b<VAR>i₂ : 0 < (Finset.erase b m).card<GOAL>2 ≤ Finset.card b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ f✝ : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f (f p.leadingCoeff * x) (normalizeScaleRoots p) = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ f✝ : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<GOAL>∑ i ∈ Finset.range ((normalizeScaleRoots p).natDegree + 1), f ((normalizeScaleRoots p).coeff i) * (f p.leadingCoeff * x) ^ i = ∑ i ∈ Finset.range (p.natDegree + 1), f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff i) * x ^ i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ f✝ : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<GOAL>Finset.range ((normalizeScaleRoots p).natDegree + 1) = Finset.range (p.natDegree + 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ f✝ : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<GOAL>∀ x_1 ∈ Finset.range (p.natDegree + 1), f ((normalizeScaleRoots p).coeff x_1) * (f p.leadingCoeff * x) ^ x_1 = f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff x_1) * x ^ x_1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ f✝ : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<VAR>_hn : n ∈ Finset.range (p.natDegree + 1)<GOAL>f ((normalizeScaleRoots p).coeff n) * (f p.leadingCoeff * x) ^ n = f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ f✝ : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<VAR>_hn : n ∈ Finset.range (p.natDegree + 1)<GOAL>f (p.coeff n) * f p.leadingCoeff ^ (p.natDegree - 1) * x ^ n = f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>f : E →ᵃ[𝕜] F<VAR>hs : Convex 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 (f x) (⇑f '' s)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H✝ : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>x : S<VAR>this : Module S A := Module.compHom A f.toRingHom<GOAL>(pushoutDesc S' f g H) ((algebraMap S S') x) = f x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H✝ : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>x : S<VAR>this✝ : Module S A := Module.compHom A f.toRingHom<VAR>this : IsScalarTower R S A<GOAL>(pushoutDesc S' f g H) ((algebraMap S S') x) = f x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H✝ : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>x : S<VAR>this✝¹ : Module S A := Module.compHom A f.toRingHom<VAR>this✝ : IsScalarTower R S A<VAR>this : IsScalarTower S A A<GOAL>(pushoutDesc S' f g H) ((algebraMap S S') x) = f x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H✝ : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>x : S<VAR>this✝¹ : Module S A := Module.compHom A f.toRingHom<VAR>this✝ : IsScalarTower R S A<VAR>this : IsScalarTower S A A<GOAL>x • 1 = f x
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>inst✝ : DecidableEq V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).toSubgraph = c.toSubgraph
<VAR>n✝ n b : ℕ<VAR>l : List ℕ<GOAL>n * ofDigits b l = ofDigits b (List.map (fun x => n * x) l)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : Cardinal.{u_2}<VAR>hx : x < ℵ₀<GOAL>2 ^ x < ℵ₀
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>n : ℕ<VAR>hx : ↑n < ℵ₀<GOAL>2 ^ ↑n < ℵ₀
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hfs : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>t : Set α<VAR>htc : IsComplete t<VAR>htf : MapsTo f t t<VAR>hft : ContractingWith K (MapsTo.restrict f t t htf)<VAR>y : α<VAR>hyt : y ∈ t<VAR>hy : edist y (f y) ≠ ⊤<VAR>hxy : edist x y ≠ ⊤<GOAL>efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : MapsTo f s s<VAR>hfs : ContractingWith K (MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>t : Set α<VAR>htc : IsComplete t<VAR>htf : MapsTo f t t<VAR>hft : ContractingWith K (MapsTo.restrict f t t htf)<VAR>y : α<VAR>hyt : y ∈ t<VAR>hy : edist y (f y) ≠ ⊤<VAR>hxy : edist x y ≠ ⊤<VAR>h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤<GOAL>edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(lTensor M (Submodule.subtype I))
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s✝ t : Set ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hS : MeasurableSet S<GOAL>cylinder s S ∈ measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s✝ t : Set ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hS : MeasurableSet S<GOAL>∃ s_1 S_1, MeasurableSet S_1 ∧ cylinder s S = cylinder s_1 S_1
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < 2 ^ (n + 1)<GOAL>dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < 2 ^ (n + 1)<GOAL>dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < |2 ^ (n + 1)|<GOAL>dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < |2 ^ (n + 1)|<GOAL>dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)|
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < |2 ^ (n + 1)|<GOAL>|(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)| = |(f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0 - (f ^ 2 ^ n) ((f ^ 2 ^ n) 0)| / |2 ^ (n + 1)|
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>s t : Cocone F<VAR>h : IsColimit t<VAR>f f' g : t ⟶ s<GOAL>g.hom = (h.descCoconeMorphism s).hom
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>P : Type u_2<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>h : Projective R P<VAR>f : M →ₗ[R] N<VAR>g : P →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (g p)<GOAL>∃ h, f ∘ₗ h = g
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>P : Type u_2<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>h : Projective R P<VAR>f : M →ₗ[R] N<VAR>g : P →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (g p)<VAR>s : P →ₗ[R] P →₀ R<VAR>hs : Function.LeftInverse ⇑(Finsupp.total P P R id) ⇑s<GOAL>∃ h, f ∘ₗ h = g
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>P : Type u_2<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>h : Projective R P<VAR>f : M →ₗ[R] N<VAR>g : P →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (g p)<VAR>s : P →ₗ[R] P →₀ R<VAR>hs : Function.LeftInverse ⇑(Finsupp.total P P R id) ⇑s<GOAL>f ∘ₗ φ ∘ₗ s = g
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>P : Type u_2<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>h : Projective R P<VAR>f : M →ₗ[R] N<VAR>g : P →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (g p)<VAR>s : P →ₗ[R] P →₀ R<VAR>hs : Function.LeftInverse ⇑(Finsupp.total P P R id) ⇑s<VAR>p : P<GOAL>(f ∘ₗ φ ∘ₗ s) p = g ((Finsupp.total P P R id) (s p))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝ : Preorder α<VAR>s : NonemptyInterval α<VAR>a : α<GOAL>↑s = Interval.pure a ↔ s = pure a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>i : ℕ<GOAL>f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<GOAL>hitting u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>h : a ∈ s<VAR>hab : a * b ∈ s<GOAL>b ∈ s
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I✝ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I : LieIdeal R L<VAR>h₁ : Function.Injective ⇑f<VAR>h₂ : map f I = ⊥<GOAL>I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I✝ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I : LieIdeal R L<VAR>h₁ : comap f ⊥ = ⊥<VAR>h₂ : map f I = ⊥<GOAL>I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I✝ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I : LieIdeal R L<VAR>h₁ : comap f ⊥ = ⊥<VAR>h₂ : I ≤ ⊥<GOAL>I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I✝ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I : LieIdeal R L<VAR>h₁ : comap f ⊥ = ⊥<VAR>h₂ : I ≤ ⊥<GOAL>I ≤ ⊥
<VAR>n : ℕ<VAR>inst✝ : NeZero n<GOAL>Fintype.card (DihedralGroup n) = 2 * n
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M' G'<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ LiftPropWithinAt P (↑f ∘ g) s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M' G'<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>ContinuousWithinAt g s x → (P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt (↑f ∘ g) s x ∧ P ((↑f ∘ g) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x))