ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<GOAL>supported M R (s ∩ t) = supported M R s ⊓ supported M R t
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<GOAL>supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>s₁ s₂ : Sphere P<VAR>p : P<VAR>hs₁ : p ∈ s₁<VAR>hs₂ : p ∈ s₂<VAR>h : s₁.center = s₂.center<GOAL>s₁.radius = s₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>s₁ s₂ : Sphere P<VAR>p : P<VAR>hs₁ : dist p s₁.center = s₁.radius<VAR>hs₂ : dist p s₂.center = s₂.radius<VAR>h : s₁.center = s₂.center<GOAL>s₁.radius = s₂.radius
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>h : ¬a = 0<VAR>x : α<VAR>hx : x ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)<GOAL>normalize x = x
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>h : ¬a = 0<VAR>y : α<VAR>left✝ : y ∈ Classical.choose ⋯<VAR>hx : normalize y ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)<GOAL>normalize (normalize y) = normalize y
<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>hr : r ≠ 0<VAR>x : ↑(sphere 1 r)<GOAL>‖↑x‖ ≠ 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>U V : Opens ↑X<VAR>s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)<GOAL>F.interUnionPullbackConeLift U V s ≫ F.val.map (homOfLE ⋯).op = s.snd
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>U V : Opens ↑X<VAR>s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)<GOAL>⋯.some.lift { pt := s.pt, π := { app := fun X_1 => Opposite.casesOn X_1 fun unop => Pairwise.casesOn unop (fun a => ULift.casesOn a fun down => WalkingPair.casesOn down s.fst s.snd) fun a a_1 => ULift.casesOn a fun down => WalkingPair.casesOn down (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op), naturality := ⋯ } } ≫ F.val.map (eqToHom ⋯).op ≫ F.val.map (homOfLE ⋯).op = s.snd
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>U V : Opens ↑X<VAR>s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)<GOAL>⋯.some.lift { pt := s.pt, π := { app := fun X_1 => Pairwise.rec (fun a => WalkingPair.rec s.fst s.snd a.down) (fun a a_1 => WalkingPair.rec (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op) a.down) (unop X_1), naturality := ⋯ } } ≫ F.val.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) = s.snd
<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>h : e.toBasis.orientation ≠ f.toBasis.orientation<GOAL>e.toBasis.det ⇑f = -1
<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>h : e.toBasis.det ⇑f ≠ -1<GOAL>e.toBasis.orientation = f.toBasis.orientation
<VAR>k : ℕ<VAR>h : ¬k = 0<GOAL>(primitiveRoots k ℂ).card = φ k
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : CommRing L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hζ : IsPrimitiveRoot ζ 2<VAR>inst✝ : IsDomain L<GOAL>(Algebra.norm K) ζ = (-1) ^ FiniteDimensional.finrank K L
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>f' : ℕ → α → ℝ := fun i a => -f i a<VAR>F' : α → ℝ := fun a => -F a<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f' i a) atTop (𝓝 (F' a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>f' : ℕ → α → ℝ := fun i a => -f i a<VAR>F' : α → ℝ := fun a => -F a<GOAL>Tendsto (fun i => ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>f' : ℕ → α → ℝ := fun i a => -f i a<VAR>F' : α → ℝ := fun a => -F a<GOAL>∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>f' : ℕ → α → ℝ := fun i a => -f i a<VAR>F' : α → ℝ := fun a => -F a<GOAL>∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁ b₂ b₃ c₁ c₂ : R<VAR>ea eb : ℕ<VAR>x : R<GOAL>x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module (MvPolynomial σ R) A<VAR>inst✝ : IsScalarTower R (MvPolynomial σ R) A<VAR>D : MvPolynomial σ R →ₗ[R] A<VAR>h₁ : D 1 = 0<VAR>H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)<GOAL>∀ (p q : MvPolynomial σ R), D (p * q) = p • D q + q • D p
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module (MvPolynomial σ R) A<VAR>inst✝ : IsScalarTower R (MvPolynomial σ R) A<VAR>D : MvPolynomial σ R →ₗ[R] A<VAR>h₁ : D 1 = 0<VAR>H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)<VAR>hC : ∀ (r : R), D (C r) = 0<GOAL>∀ (p q : MvPolynomial σ R), D (p * q) = p • D q + q • D p
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module (MvPolynomial σ R) A<VAR>inst✝ : IsScalarTower R (MvPolynomial σ R) A<VAR>D : MvPolynomial σ R →ₗ[R] A<VAR>h₁ : D 1 = 0<VAR>H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)<VAR>hC : ∀ (r : R), D (C r) = 0<VAR>this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p<VAR>p q : MvPolynomial σ R<GOAL>D (p * q) = p • D q + q • D p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ C<VAR>V V₀ V₁ V₂ : Coalgebra F✝<VAR>f✝ : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<VAR>F G : C ⥤ C<VAR>α : F ⟶ G<VAR>X✝ Y✝ : Coalgebra F<VAR>f : X✝ ⟶ Y✝<GOAL>((fun V => { V := V.V, str := V.str ≫ α.app V.V }) X✝).str ≫ G.map f.f = f.f ≫ ((fun V => { V := V.V, str := V.str ≫ α.app V.V }) Y✝).str
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>v : E<GOAL>(adjoint (adjoint A)) v = A v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>v : E<VAR>w : F<GOAL>⟪w, (adjoint (adjoint A)) v⟫_𝕜 = ⟪w, A v⟫_𝕜
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m n : ℕ<GOAL>0 ^ (n + 1) ≤ 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m n : ℕ<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace ℝ F<VAR>inst✝¹¹ : NormedAddCommGroup F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T'✝ T'' : Set α → E →L[ℝ] F<VAR>C✝ C'✝ C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT) f ≤ (setToL1 hT') f
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<VAR>r : g = h<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<VAR>r : (g x) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = (h x) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩)<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<VAR>r : (g x) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩)<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<VAR>r : fromCoset ⟨x • ↑⟨↑(MonoidHom.range f), ⋯⟩, ⋯⟩ = (((Equiv.symm τ).trans (↑g x)).trans τ) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩)<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<VAR>r : fromCoset ⟨x • Set.range ⇑f, ⋯⟩ = τ ((↑g x) ((Equiv.symm τ) (fromCoset ⟨Set.range ⇑f, ⋯⟩)))<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∉ MonoidHom.range f<VAR>r : fromCoset ⟨x • Set.range ⇑f, ⋯⟩ = fromCoset ⟨↑(MonoidHom.range f), ⋯⟩<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>T : Triangle C<GOAL>(1 • (CategoryTheory.shiftFunctor C 0).map T.mor₃ ≫ (shiftFunctorComm C 1 0).hom.app T.obj₁) ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorZero C ℤ).hom.app T.obj₁) = (CategoryTheory.shiftFunctorZero C ℤ).hom.app T.obj₃ ≫ T.mor₃
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>x : E<GOAL>√(1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>x : E<GOAL>1 + ‖x‖ ^ 2 ≤ (1 + ‖x‖) ^ 2
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>n : ℤ<GOAL>WithTop.map (fun x => ↑x) ⋯.order - ↑(Exists.choose hf) = ↑n ↔ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>n : ℤ<VAR>h : ⋯.order = ⊤<GOAL>WithTop.map (fun x => ↑x) ⋯.order - ↑(Exists.choose hf) = ↑n ↔ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>n : ℤ<VAR>h : ¬⋯.order = ⊤<GOAL>WithTop.map (fun x => ↑x) ⋯.order - ↑(Exists.choose hf) = ↑n ↔ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q✝ R✝ : Prop<VAR>inst✝² : Decidable P<VAR>inst✝¹ : Decidable Q✝<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<VAR>Q : P → Prop<VAR>R : ¬P → Prop<VAR>inst✝ : Decidable P<GOAL>dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
<VAR>a b c : ℕ<GOAL>range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
<VAR>a b c : ℕ<GOAL>Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a)) (Ico 0 b)
<VAR>a b c : ℕ<GOAL>image (⇑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)
<VAR>a b c x : ℕ<GOAL>x ∈ image (⇑(addLeftEmbedding a)) (Ico 0 b) ↔ x ∈ Ico a (a + b)
<VAR>a b c x : ℕ<GOAL>(∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b
<VAR>α : Type u_1<VAR>inst✝³ : NormedLatticeAddCommGroup α<VAR>G : Type u_2<VAR>inst✝² : OrderedAddCommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousSub G<VAR>h : IsClosed {x | 0 ≤ x}<GOAL>IsClosed {p | p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>inst✝³ : NormedLatticeAddCommGroup α<VAR>G : Type u_2<VAR>inst✝² : OrderedAddCommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousSub G<VAR>h : IsClosed {x | 0 ≤ x}<VAR>this : {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}<GOAL>IsClosed {p | p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>inst✝³ : NormedLatticeAddCommGroup α<VAR>G : Type u_2<VAR>inst✝² : OrderedAddCommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousSub G<VAR>h : IsClosed {x | 0 ≤ x}<VAR>this : {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}<GOAL>IsClosed ((fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x})
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A : Matrix m n R<GOAL>(A * Aᴴ).PosSemidef
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>inst✝ : Monoid M<VAR>x : ↥(IsUnit.submonoid M)<GOAL>(fun x => ⟨↑x, ⋯⟩) ((fun x => IsUnit.unit ⋯) x) = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>inst✝ : Monoid M<VAR>x y : Mˣ<GOAL>{ toFun := fun x => ⟨↑x, ⋯⟩, invFun := fun x => IsUnit.unit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x * y) = { toFun := fun x => ⟨↑x, ⋯⟩, invFun := fun x => IsUnit.unit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x * { toFun := fun x => ⟨↑x, ⋯⟩, invFun := fun x => IsUnit.unit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>inst✝ : Monoid M<VAR>x y : Mˣ<GOAL>⟨↑x * ↑y, ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>f : Arrow C<GOAL>data.i.app f ≫ data.p.app f = f.hom
<VAR>num den : Int<GOAL>num /. -den = -num /. den
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<GOAL>UniformContinuous Subtype.val
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ 0<GOAL>UniformContinuous Subtype.val
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ 0<GOAL>∀ (i : α), UniformContinuous fun x => ↑x i
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ 0<VAR>i : α<GOAL>UniformContinuous fun x => ↑x i
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ 0<VAR>i : α<GOAL>∀ (i_1 : ℝ), 0 < i_1 → ∃ j, 0 < j ∧ ∀ (x y : ↥(lp E p)), (x, y) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.1 - p.2‖ < i_1}
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ 0<VAR>i : α<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>f g : ↥(lp E p)<VAR>hfg : ‖f - g‖ < ε<GOAL>(↑f i, ↑g i) ∈ {p | ‖p.1 - p.2‖ < ε}
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ 0<VAR>i : α<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>f g : ↥(lp E p)<VAR>hfg : ‖f - g‖ < ε<VAR>this : ‖↑f i - ↑g i‖ ≤ ‖f - g‖<GOAL>(↑f i, ↑g i) ∈ {p | ‖p.1 - p.2‖ < ε}
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>x✝ y : M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : Ray R M<GOAL>x ≠ -x
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>x✝ y : M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>rayOfNeZero R x hx ≠ -rayOfNeZero R x hx
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>x✝ y : M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>¬SameRay R x (-x)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x✝ : α<GOAL>x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t : Multiset α<VAR>a✝ b : α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ≤ a ::ₘ s.erase a
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t : Multiset α<VAR>a✝ b : α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ≤ a ::ₘ s
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>∃ C, 0 < C ∧ AntilipschitzWith C ⇑(continuousLinearMapOfBilin B)
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>C : ℝ<VAR>C_pos : 0 < C<VAR>below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖<GOAL>∃ C, 0 < C ∧ AntilipschitzWith C ⇑(continuousLinearMapOfBilin B)
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>C : ℝ<VAR>C_pos : 0 < C<VAR>below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖<GOAL>AntilipschitzWith C⁻¹.toNNReal ⇑(continuousLinearMapOfBilin B)
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>C : ℝ<VAR>C_pos : 0 < C<VAR>below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖<GOAL>∀ (x : V), ‖x‖ ≤ ↑C⁻¹.toNNReal * ‖(continuousLinearMapOfBilin B) x‖
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>C : ℝ<VAR>C_pos : 0 < C<VAR>below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖<GOAL>∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ ‖(continuousLinearMapOfBilin B) x‖
<VAR>β : Sort ?u.112935<VAR>α : Sort ?u.112940<VAR>P : β → Sort w<VAR>e✝ : α ≃ β<VAR>ι'' : Sort u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>π : ι'' → Type u_1<VAR>e : ι ⊕ ι' ≃ ι''<VAR>f : (i : ι) → π (e (inl i))<VAR>g : (i : ι') → π (e (inr i))<VAR>i : ι<GOAL>(piCongrLeft π e) ((sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (inl i)) = f i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>hs : s.Nonempty<GOAL>s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>hs : s.Nonempty<GOAL>¬s = ∅