ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset = (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s).toFinset
<VAR>α✝ : Type u<VAR>m n o✝ : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>α : Type u_4<VAR>o : ℕ<VAR>ho : o = m + n<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin o<GOAL>vecAppend ho u v i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
<VAR>α✝ : Type u<VAR>m n o✝ : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>α : Type u_4<VAR>o : ℕ<VAR>ho : o = m + n<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin o<GOAL>(if hi : ↑(Fin.cast ho i) < m then ⋯ ▸ u ((Fin.cast ho i).castLT hi) else ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
<VAR>α✝ : Type u<VAR>m n o✝ : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>α : Type u_4<VAR>o : ℕ<VAR>ho : o = m + n<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin o<VAR>hi : ¬↑(Fin.cast ho i) < m<GOAL>⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩
<VAR>α✝ : Type u<VAR>m n o✝ : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>α : Type u_4<VAR>o : ℕ<VAR>ho : o = m + n<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin o<VAR>hi : ¬↑(Fin.cast ho i) < m<GOAL>v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : MulActionWithZero 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<VAR>x✝ : α<GOAL>‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>(minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>(minpoly A x).degree = ↑1 ↔ x ∈ (algebraMap A B).range
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t K : Set X<VAR>hs : s.Infinite<VAR>hK : IsCompact K<VAR>hsub : s ⊆ K<VAR>x : X<VAR>hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)<GOAL>x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>h : 0 ≈ 1<VAR>this✝ : (1 - 0).LimZero<VAR>this : LimZero 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>r s : R<VAR>m : M<VAR>n : N<GOAL>(r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LE α<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ a * b<GOAL>1 * b ≤ a * b
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>Function.Surjective ⇑(S.transitionMap n)
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>Function.Surjective (⇑(S.transitionMap n) ∘ ⇑(S.proj (n + 1)))
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<VAR>m : ℕ := Nat.find S_nonempty<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<VAR>m : ℕ := Nat.find S_nonempty<VAR>m_mem : m ∈ S<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<VAR>m : ℕ := Nat.find S_nonempty<VAR>s0 : ℤ × ℤ × ℤ<VAR>hs0 : Fermat42 s0.1 s0.2.1 s0.2.2<VAR>hs1 : m = s0.2.2.natAbs<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<VAR>m : ℕ := Nat.find S_nonempty<VAR>s0 : ℤ × ℤ × ℤ<VAR>hs0 : Fermat42 s0.1 s0.2.1 s0.2.2<VAR>hs1 : m = s0.2.2.natAbs<GOAL>∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<VAR>m : ℕ := Nat.find S_nonempty<VAR>s0 : ℤ × ℤ × ℤ<VAR>hs0 : Fermat42 s0.1 s0.2.1 s0.2.2<VAR>hs1 : m = s0.2.2.natAbs<VAR>a1 b1 c1 : ℤ<VAR>h1 : Fermat42 a1 b1 c1<GOAL>m ≤ c1.natAbs
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}<VAR>S_nonempty : S.Nonempty<VAR>m : ℕ := Nat.find S_nonempty<VAR>s0 : ℤ × ℤ × ℤ<VAR>hs0 : Fermat42 s0.1 s0.2.1 s0.2.2<VAR>hs1 : m = s0.2.2.natAbs<VAR>a1 b1 c1 : ℤ<VAR>h1 : Fermat42 a1 b1 c1<GOAL>c1.natAbs ∈ S
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s<GOAL>ContDiffOn 𝕜 none f s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s<VAR>n : ℕ<GOAL>ContDiffOn 𝕜 (some n) f s
<VAR>n m : ℕ<VAR>a : Fin (n + 1)<VAR>h₁ : a ≠ 0<VAR>h₂ : a ≠ last n<GOAL>a.pred h₁ < a.castPred h₂
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>f : E →ₗ[ℝ] E := r • 1<GOAL>map (⇑f) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>f : E →ₗ[ℝ] E := r • 1<VAR>hf : LinearMap.det f ≠ 0<GOAL>map (⇑f) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
<VAR>ι : Type u_1<VAR>M✝ : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>M : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>f : Box ι → M<GOAL>∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G✝ : Type u_7<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Monoid N<VAR>inst✝² : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>L : List ι<VAR>f : ι → M<VAR>G : Type u_8<VAR>inst✝¹ : FunLike G M N<VAR>inst✝ : MonoidHomClass G M N<VAR>g : G<GOAL>(map (⇑g ∘ f) L).prod = g (map f L).prod
<VAR>α : Type u_1<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>s : Multiset α<VAR>a : α<VAR>t : Multiset α<VAR>hst : s < t<VAR>hts : t < a ::ₘ s<GOAL>card t < succ (card s)
<VAR>M : Type ?u.3475<VAR>inst✝ : Monoid M<VAR>u : (↥(Submonoid.center M))ˣ<VAR>r : Mˣ<GOAL>↑(r * (Units.map (Submonoid.center M).subtype) u) = ↑((Units.map (Submonoid.center M).subtype) u * r)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<GOAL>edgeDensity r s ∅ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : CompleteSpace α<VAR>i : γ → β<VAR>hf : Multipliable f<VAR>hi : Injective i<GOAL>Multipliable (f ∘ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : Preorder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>ha : IsLUB s a<VAR>hb : Tendsto f (𝓝[s] a) (𝓝 b)<VAR>x : α<VAR>hx : x ∈ s<GOAL>f x ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : Preorder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>hb : Tendsto f (𝓝[s] a) (𝓝 b)<VAR>x : α<VAR>hx : x ∈ s<VAR>ha : IsLUB (s ∩ Ici x) a<GOAL>f x ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : Preorder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>hb : Tendsto f (𝓝[s] a) (𝓝 b)<VAR>x : α<VAR>hx : x ∈ s<VAR>ha : IsLUB (s ∩ Ici x) a<VAR>this : (𝓝[s ∩ Ici x] a).NeBot<GOAL>f x ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : Preorder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>hb : Tendsto f (𝓝[s] a) (𝓝 b)<VAR>x : α<VAR>hx : x ∈ s<VAR>ha : IsLUB (s ∩ Ici x) a<VAR>this : (𝓝[s ∩ Ici x] a).NeBot<GOAL>∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>q : Submodule R M := ⨆ i ∈ s, p i<VAR>p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)<GOAL>IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>q : Submodule R M := ⨆ i ∈ s, p i<VAR>p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)<VAR>hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype<GOAL>IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>q : Submodule R M := ⨆ i ∈ s, p i<VAR>p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)<VAR>hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype<VAR>hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)<GOAL>IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>q : Submodule R M := ⨆ i ∈ s, p i<VAR>p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)<VAR>hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype<VAR>hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)<VAR>hp₂ : ⨆ i ∈ s, p' i = ⊤<GOAL>IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝¹ : Reflective i<VAR>A : C<VAR>inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)<VAR>η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit<GOAL>A ∈ i.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝¹ : Reflective i<VAR>A : C<VAR>inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)<VAR>η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit<VAR>this : IsIso (η.app (i.obj ((reflector i).obj A)))<GOAL>A ∈ i.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝¹ : Reflective i<VAR>A : C<VAR>inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)<VAR>η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit<VAR>this✝ : IsIso (η.app (i.obj ((reflector i).obj A)))<VAR>this : Epi (η.app A)<GOAL>A ∈ i.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝¹ : Reflective i<VAR>A : C<VAR>inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)<VAR>η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit<VAR>this✝¹ : IsIso (η.app (i.obj ((reflector i).obj A)))<VAR>this✝ : Epi (η.app A)<VAR>this : IsIso (η.app A)<GOAL>A ∈ i.essImage
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<GOAL>exp 𝕂 (-A) = (exp 𝕂 A)⁻¹
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<GOAL>exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<VAR>this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing<VAR>this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing<VAR>this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra<GOAL>exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>zero : T.mor₃ = 0<GOAL>∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>zero : T.mor₃ = 0<VAR>this : Epi T.mor₂<GOAL>∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>zero : T.mor₃ = 0<VAR>this✝ : Epi T.mor₂<VAR>this : IsSplitEpi T.mor₂<GOAL>∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>zero : T.mor₃ = 0<VAR>this✝ : Epi T.mor₂<VAR>this : IsSplitEpi T.mor₂<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁<GOAL>∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>zero : T.mor₃ = 0<VAR>this✝ : Epi T.mor₂<VAR>this : IsSplitEpi T.mor₂<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁<VAR>d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯<GOAL>∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
<VAR>a b : ℝ<VAR>n : ℕ<VAR>C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b<VAR>h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)<GOAL>∫ (x : ℝ) in a..b, sin x ^ (n + 2) = (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b<VAR>h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x<GOAL>∫ (x : ℝ) in a..b, sin x ^ (n + 2) = (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b<VAR>h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x<GOAL>∫ (x : ℝ) in a..b, sin x ^ (n + 2) = (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b<VAR>h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x<VAR>H : ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x = sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x<GOAL>∫ (x : ℝ) in a..b, sin x ^ (n + 2) = (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b<VAR>h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x<GOAL>IntervalIntegrable (fun x => ↑(n + 1) * cos x * sin x ^ n) MeasureTheory.volume a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b<VAR>h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x<GOAL>IntervalIntegrable sin MeasureTheory.volume a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>s : Stream' α<GOAL>↑(l ++ₛ s) = (↑l).append ↑s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>L✝ : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L✝.IsLocalization W<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>L : C ⥤ D<VAR>hL : W.IsInvertedBy L<GOAL>(inv (L.map φ.s)).op ≫ (L.map φ.f).op = inv (L.map φ.s).op ≫ (L.map φ.f).op
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a b : R<VAR>h : Rel r a b<GOAL>Rel r (-a) (-b)
<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 α<GOAL>IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>w₁ : Word G<VAR>h₁ : H<VAR>hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i<VAR>w₂ : Word G<VAR>h₂ : H<VAR>hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i<VAR>h : CoprodI.of ((φ i) h₁) • w₁ = CoprodI.of ((φ i) h₂) • w₂<GOAL>{ toWord := w₁, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }