ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k m : ℕ<VAR>hm : n ≤ k + m<GOAL>∑ s : { s // s.card = m }, p.changeOriginSeriesTerm k m ↑s ⋯ = 0
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>i : ι<GOAL>(e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
<VAR>α : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>1 < 2
<VAR>α : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>1 < 1 + 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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>inst✝² : Mul β<VAR>inst✝¹ : MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_indep : iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>IndepFun (f i * f j) (f k) κ μ
<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>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>inst✝² : Mul β<VAR>inst✝¹ : MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_indep : iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<VAR>this : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ<GOAL>IndepFun (f i * f j) (f k) κ μ
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>toDFinsupp {a} = DFinsupp.single a 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (g * a)<VAR>h_inv : ∀ (a : G), P a → P (g⁻¹ * a)<VAR>n : ℤ<GOAL>P (g ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (g * a)<VAR>h_inv : ∀ (a : G), P a → P (g⁻¹ * a)<GOAL>P (g ^ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (g * a)<VAR>h_inv : ∀ (a : G), P a → P (g⁻¹ * a)<VAR>n : ℕ<VAR>ih : P (g ^ ↑n)<GOAL>P (g ^ (↑n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (g * a)<VAR>h_inv : ∀ (a : G), P a → P (g⁻¹ * a)<VAR>n : ℕ<VAR>ih : P (g ^ (-↑n))<GOAL>P (g ^ (-↑n - 1))
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>f : E → G<VAR>hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<VAR>K : ℝ≥0<VAR>hK : ‖f' x‖₊ < K<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>f : E → G<VAR>hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<VAR>K : ℝ≥0<VAR>hK : ‖f' x‖₊ < K<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ∩ s ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>f : E → G<VAR>hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<VAR>K : ℝ≥0<VAR>hK : ‖f' x‖₊ < K<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : s ∩ ball x ε ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f✝ g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>f : E → G<VAR>hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<VAR>K : ℝ≥0<VAR>hK : ‖f' x‖₊ < K<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : s ∩ ball x ε ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}<GOAL>LipschitzOnWith K f (s ∩ ball x ε)
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ := Fintype.card σ<GOAL>(-1) ^ (k + 1) * ∑ a ∈ antidiagonal k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<GOAL>basisDivisor x y ≠ 0 ↔ x ≠ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c✝ d b a c : α<GOAL>b - a - c = b - (a + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c✝ d b a c : α<GOAL>b - a - c ≤ b - (a + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c✝ d b a c : α<GOAL>b - (a + c) ≤ b - a - c
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>i✝ : m<VAR>j✝ : o<GOAL>(M * -N) i✝ j✝ = (-(M * N)) i✝ j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s s₁ s₂ : Finset α<VAR>h : s₁ ⊆ s₂<GOAL>map f s₁ ⊆ map f s₂
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(addOppositeEquiv.symm x).leadingCoeff = AddOpposite.op (AddOpposite.unop x).leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>AddOpposite.unop (addOppositeEquiv.symm x).leadingCoeff = AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ ψ : R⟦X⟧<GOAL>(coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ ψ : R⟦X⟧<GOAL>∑ p ∈ antidiagonal (single () n), (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ = ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ ψ : R⟦X⟧<GOAL>∑ x ∈ antidiagonal n, (MvPowerSeries.coeff R (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).1) φ * (MvPowerSeries.coeff R (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).2) ψ = ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<GOAL>(↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<VAR>hr : r < 0<GOAL>(↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<VAR>h✝ : 0 ≤ r<GOAL>(↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<GOAL>(extensionOfMax i f).domain = ⊤
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<GOAL>y ∈ (extensionOfMax i f).domain
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<GOAL>∃ y_1 ∈ (extensionOfMax i f).domain, ∃ z ∈ Submodule.span R {?y}, y_1 + z = y
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<GOAL>N
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<GOAL>r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<VAR>this : {r | ¬IsUnit r} ⊆ spectrum R ↑a<GOAL>r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<VAR>this : {r | ¬IsUnit r} ⊆ spectrum R ↑a<GOAL>r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<VAR>this : {r | ¬IsUnit r} ⊆ spectrum R ↑a<VAR>hr : IsUnit r<GOAL>¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • ↑a))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a : A<GOAL>IsQuasiregular ↑a ↔ IsQuasiregular a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a : A<VAR>ha : IsQuasiregular ↑a<GOAL>IsQuasiregular a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a : A<VAR>ha : ∃ y, y + ↑a + ↑a * y = 0 ∧ ↑a + y + y * ↑a = 0<GOAL>∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a y : A<VAR>hy₁ : ↑y + ↑a + ↑a * ↑y = 0<VAR>hy₂ : ↑a + ↑y + ↑y * ↑a = 0<GOAL>∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>(((𝓤 α).lift' gen).lift' fun s => s ○ s) = (𝓤 α).lift' fun s => gen s ○ gen s
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>Monotone gen
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>Monotone fun s => s ○ s
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>((𝓤 α).lift' fun s => gen (s ○ s)) = ((𝓤 α).lift' fun s => s ○ s).lift' gen
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>hτ : IsStoppingTime ℱ τ<VAR>h_countable : (Set.range τ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f|↑ℱ i]
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>hτ : IsStoppingTime ℱ τ<VAR>h_countable : (Set.range τ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<VAR>t : Set Ω<GOAL>MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>s : Opens α<GOAL>CompleteLattice.IsCompactElement s ↔ IsCompact ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>s : Opens α<GOAL>(∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) ↔ ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<GOAL>s.Subsingleton
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>U : Set X<VAR>hUo : IsOpen U<VAR>hU : Xor' (x ∈ U) (y ∈ U)<GOAL>False
<VAR>X✝ : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>U : Set X<VAR>hUo : IsOpen U<VAR>hU : Xor' (x ∈ U) (y ∈ U)<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<GOAL>False
<VAR>X✝ : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>U : Set X<VAR>hUo : IsOpen U<VAR>hU : Xor' (x ∈ U) (y ∈ U)<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<VAR>this : s ∩ U = s<GOAL>False
<VAR>n✝ p : ℕ<VAR>pp : Prime p<VAR>m n : ℕ<VAR>hn : p = m * n<GOAL>m = 1 ∨ m = p
<VAR>n✝ p : ℕ<VAR>pp : Prime p<VAR>m n : ℕ<VAR>hn : p = m * n<VAR>this : IsUnit m ∨ IsUnit n<GOAL>m = 1 ∨ m = p
<VAR>n✝ p : ℕ<VAR>pp : Prime p<VAR>m n : ℕ<VAR>hn : p = m * n<VAR>this : m = 1 ∨ n = 1<GOAL>m = 1 ∨ m = p
<VAR>n✝ p : ℕ<VAR>pp : Prime p<VAR>m n : ℕ<VAR>hn : p = m * n<VAR>this : m = 1 ∨ n = 1<GOAL>n = 1 → m = p
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>m : ℕ<VAR>hn : p = m * 1<VAR>this : m = 1 ∨ 1 = 1<GOAL>m = p
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0<VAR>hs' : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (completedCosZeta a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0<VAR>hs' : s ≠ 1 ∨ a ≠ 0<GOAL>s / 2 ≠ 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0<VAR>hs' : s ≠ 1 ∨ a ≠ 0<GOAL>s / 2 ≠ ↑(hurwitzEvenFEPair a).symm.k ∨ (hurwitzEvenFEPair a).symm.g₀ = 0
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>x : β<VAR>hxs : x ∈ s<VAR>hx : f x ∈ lowerBounds (f '' s)<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i : ι<VAR>m : M i<VAR>w : Word M<VAR>hmw : w.fstIdx ≠ some i<VAR>h1 : m ≠ 1<GOAL>∀ l ∈ ⟨i, m⟩ :: w.toList, l.snd ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i : ι<VAR>m : M i<VAR>w : Word M<VAR>hmw : w.fstIdx ≠ some i<VAR>h1 : m ≠ 1<GOAL>∀ (l : (i : ι) × M i), l = ⟨i, m⟩ ∨ l ∈ w.toList → l.snd ≠ 1
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSpace Ω'<VAR>f : Ω → Ω'<VAR>f_mble : Measurable f<VAR>ν₁ ν₂ : FiniteMeasure Ω<VAR>s : Set Ω'<VAR>s_mble : MeasurableSet s<GOAL>↑((ν₁ + ν₂).map f) s = ↑(ν₁.map f + ν₂.map f) s
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Finite α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Finite β<VAR>f : Perm α<VAR>e : α ≃ β<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hs : ∀ (x : α), x ∈ s<VAR>ht : ∀ (x : β), x ∈ t<GOAL>signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Finite α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Finite β<VAR>f : Perm α<VAR>e : α ≃ β<VAR>t : List β<VAR>s : List α<VAR>hs : ∀ (x : α), x ∈ ⟦s⟧<VAR>ht : ∀ (x : β), x ∈ ⟦t⟧<GOAL>signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Finite α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Finite β<VAR>f : Perm α<VAR>e : α ≃ β<VAR>t : List β<VAR>s : List α<VAR>hs : ∀ (x : α), x ∈ ⟦s⟧<VAR>ht : ∀ (x : β), x ∈ ⟦t⟧<GOAL>signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Finite α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Finite β<VAR>f : Perm α<VAR>e : α ≃ β<VAR>t : List β<VAR>s : List α<VAR>hs : ∀ (x : α), x ∈ ⟦s⟧<VAR>ht : ∀ (x : β), x ∈ ⟦t⟧<VAR>n : ℕ<VAR>e' : β ≃ Fin n<GOAL>signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Finite α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Finite β<VAR>f : Perm α<VAR>e : α ≃ β<VAR>t : List β<VAR>s : List α<VAR>hs : ∀ (x : α), x ∈ ⟦s⟧<VAR>ht : ∀ (x : β), x ∈ ⟦t⟧<VAR>n : ℕ<VAR>e' : β ≃ Fin n<GOAL>signAux ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') = signAux (((e.trans e').symm.trans f).trans (e.trans e'))
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Ring R'<VAR>f g : R⟦X⟧<VAR>f' g' : R'⟦X⟧<VAR>S : Type u_3<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Module R S<VAR>r : R<VAR>x : S⟦X⟧<VAR>x✝ : ℤ<GOAL>((ofPowerSeries ℤ S) (r • x)).coeff x✝ = (r • (ofPowerSeries ℤ S) x).coeff x✝
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>(filter (fun p => p.card = s.card / P.parts.card) P.parts).card = P.parts.card - s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>(filter (fun p => p.card = s.card / P.parts.card) P.parts).card = (filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).card + (filter (fun a => ¬a.card = s.card / P.parts.card + 1) P.parts).card - s.card % P.parts.card
<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>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype m<VAR>A : Matrix m m R<VAR>e₁ e₂ : n ≃ m<GOAL>(A.submatrix ⇑e₁ ⇑e₂).rank = A.rank
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>l : Filter α<GOAL>(∀ ε > 0, ∀ᶠ (x : α) in l, dist (f x) 1 < ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.57069, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯).Exact