ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : m '' s ∈ f<GOAL>sᶜ ∉ comap m f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : m '' s ∈ f<VAR>t : Set β<VAR>ht : t ∈ f<VAR>hts : m ⁻¹' t ⊆ sᶜ<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : m '' s ∈ f<VAR>t : Set β<VAR>ht : t ∈ f<VAR>hts : m ⁻¹' t ⊆ sᶜ<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxt : m x ∈ t<GOAL>False
<VAR>n : ℕ+<GOAL>1 + n.natPred = ↑n
<VAR>m n k : ℕ<GOAL>(m * n).lcm (k * n) = m.lcm k * n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : A ⟶ S.cycles<VAR>h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles<GOAL>f₁ = f₂
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>inst✝¹ : Finite α<VAR>X : α → CompHausLike P<VAR>inst✝ : HasExplicitFiniteCoproduct X<VAR>a : α<VAR>x y : (forget (CompHausLike P)).obj (X a)<VAR>hxy : (ι X a) x = (ι X a) y<GOAL>x = y
<VAR>α β✝ γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>β : Type u<VAR>p : Poly (Option α ⊕ β)<VAR>pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : {v | ∃ x, x ::ₒ v ∈ S} v<VAR>x : ℕ<VAR>hx : x ::ₒ v ∈ S<VAR>t : β → ℕ<VAR>ht : p (x ::ₒ v ⊗ t) = 0<GOAL>(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ x ::ₒ t) = 0
<VAR>α β✝ γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>β : Type u<VAR>p : Poly (Option α ⊕ β)<VAR>pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : {v | ∃ x, x ::ₒ v ∈ S} v<VAR>x : ℕ<VAR>hx : x ::ₒ v ∈ S<VAR>t : β → ℕ<VAR>ht : p (x ::ₒ v ⊗ t) = 0<GOAL>p ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
<VAR>α β✝ γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>β : Type u<VAR>p : Poly (Option α ⊕ β)<VAR>pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : {v | ∃ x, x ::ₒ v ∈ S} v<VAR>x : ℕ<VAR>hx : x ::ₒ v ∈ S<VAR>t : β → ℕ<VAR>ht : p (x ::ₒ v ⊗ t) = 0<GOAL>p (x ::ₒ v ⊗ t) = 0
<VAR>α β✝ γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>β : Type u<VAR>p : Poly (Option α ⊕ β)<VAR>pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0<VAR>t : Option β → ℕ<VAR>ht : (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0<GOAL>p (t none ::ₒ v ⊗ t ∘ some) = 0
<VAR>α β✝ γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>β : Type u<VAR>p : Poly (Option α ⊕ β)<VAR>pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0<VAR>t : Option β → ℕ<VAR>ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0<GOAL>p (t none ::ₒ v ⊗ t ∘ some) = 0
<VAR>x : ℝ<VAR>h : x < -1<GOAL>2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π
<VAR>x : ℝ<VAR>h : x < -1<GOAL>arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - x ^ 2)) - π
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ a ∈ l, p a<VAR>hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b<VAR>h : l.Nodup<GOAL>(List.pmap f l H).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ a ∈ l, p a<VAR>hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b<VAR>h : l.Nodup<GOAL>(map (fun x => f ↑x ⋯) l.attach).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>a : α<VAR>hs✝ : s.Finite<VAR>ht✝ : t.Finite<VAR>inst✝ : DecidableEq α<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>h : (s ∆ t).Finite<VAR>a✝ : α<GOAL>a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∆ ht.toFinset
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<VAR>hp : ¬map i p = 0<GOAL>(map i p).natDegree = Multiset.card (map i p).roots
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<VAR>hp : ¬map i p = 0<VAR>q : L[X]<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<GOAL>(map i p).natDegree = Multiset.card (map i p).roots
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hp : ¬map i p = 0<VAR>q : L[X]<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<GOAL>(map i p).natDegree = Multiset.card (map i p).roots
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<GOAL>(map i p).natDegree = Multiset.card (map i p).roots
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<VAR>hq : q ≠ 0<GOAL>(map i p).natDegree = Multiset.card (map i p).roots
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<VAR>hq : q ≠ 0<GOAL>q.natDegree = 0
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<VAR>hq : q ≠ 0<VAR>h : ¬q.natDegree = 0<GOAL>False
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<VAR>hq : q ≠ 0<VAR>h : ¬q.natDegree = 0<VAR>h' : (map (RingHom.id L) q).natDegree ≠ 0<GOAL>False
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<VAR>hq : q ≠ 0<VAR>h : ¬q.natDegree = 0<VAR>h' : (map (RingHom.id L) q).natDegree ≠ 0<VAR>this : (map (RingHom.id L) q).roots ≠ 0<GOAL>False
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>q : L[X]<VAR>hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0<VAR>hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)<VAR>he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p<VAR>hd : Multiset.card (map i p).roots + q.natDegree = (map i p).natDegree<VAR>hr : q.roots = 0<VAR>hq : q ≠ 0<VAR>h : ¬q.natDegree = 0<VAR>h' : (map (RingHom.id L) q).natDegree ≠ 0<GOAL>map (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q) ≠ 0
<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'<GOAL>map f I ⊔ map f f.ker = map f I
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>(l.rotate n).head? = l[n]?
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>h : M ≅[L] N<GOAL>M ⊨ T ↔ N ⊨ T
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : Disjoint a b<GOAL>(a ⊔ b) \ a = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg : CauchySeq fun n => ∑ i ∈ range n, g i<VAR>hf : ∀ (i : ℕ), ‖f i‖ ≤ g i<GOAL>CauchySeq fun n => ∑ i ∈ range n, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg : CauchySeq fun n => ∑ i ∈ range n, g i<VAR>hf : ∀ (i : ℕ), ‖f i‖ ≤ g i<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i<VAR>hf : ∀ (i : ℕ), ‖f i‖ ≤ g i<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hg : ∀ n ≥ N, dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i<VAR>hf : ∀ (i : ℕ), ‖f i‖ ≤ g i<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N n : ℕ<VAR>hn : n ≥ N<VAR>hg : dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε<GOAL>dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i<VAR>hf : ∀ (i : ℕ), ‖f i‖ ≤ g i<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N n : ℕ<VAR>hn : n ≥ N<VAR>hg : ‖∑ k ∈ Ico N n, g k‖ < ε<GOAL>‖∑ k ∈ Ico N n, f k‖ < ε
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>f g : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>ContMDiffAt I 𝓘(𝕜, E) n (↑I) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E) (↑I x)) ∘ ↑I ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (range ↑I) (↑I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>↑I ∘ ↑I.symm =ᶠ[nhdsWithin (↑I x) (range ↑I)] id
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>(↑I ∘ ↑I.symm) (↑I x) = id (↑I x)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>X : CostructuredArrow S T<GOAL>(eqToHom ⋯).left = eqToHom ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>h_nonneg : 0 ≤ᶠ[ae μ] f<GOAL>∫⁻ (x : α), ↑‖f x‖₊ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>h_nonneg : 0 ≤ᶠ[ae μ] f<GOAL>(fun a => ↑‖f a‖₊) =ᶠ[ae μ] fun a => ENNReal.ofReal (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>h_nonneg : 0 ≤ᶠ[ae μ] f<VAR>x : α<VAR>hx : 0 x ≤ f x<GOAL>↑‖f x‖₊ = ENNReal.ofReal (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h₁ : s ≤ᶠ[ae μ] t<VAR>h₂ : μ t ≤ μ s<VAR>hsm : MeasurableSet s<VAR>ht : μ t ≠ ⊤<GOAL>s =ᶠ[ae μ] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h₁ : s ≤ᶠ[ae μ] t<VAR>h₂ : μ t ≤ μ s<VAR>hsm : MeasurableSet s<VAR>ht : μ t ≠ ⊤<GOAL>μ (t \ s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h₁ : s ≤ᶠ[ae μ] t<VAR>hsm : MeasurableSet s<VAR>ht : μ t ≠ ⊤<VAR>h₂ : μ t = μ s<GOAL>μ (t \ s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h₁ : s ≤ᶠ[ae μ] t<VAR>hsm : MeasurableSet s<VAR>h₂ : μ t = μ s<VAR>ht : μ s ≠ ⊤<GOAL>μ (t \ s) = 0
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a✝ : Nontrivial A<VAR>a : A<GOAL>‖(gelfandTransform ℂ A) a‖ = ‖a‖
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a✝ : Nontrivial A<VAR>a : A<VAR>this : spectralRadius ℂ ((gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)<GOAL>‖(gelfandTransform ℂ A) a‖ = ‖a‖
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a✝ : Nontrivial A<VAR>a : A<VAR>this : ↑‖star ((gelfandTransform ℂ A) a) * (gelfandTransform ℂ A) a‖₊ = ↑‖star a * a‖₊<GOAL>‖(gelfandTransform ℂ A) a‖ = ‖a‖
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedCommRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a✝ : Nontrivial A<VAR>a : A<VAR>this : ‖(gelfandTransform ℂ A) a‖₊ ^ 2 = ‖a‖₊ ^ 2<GOAL>‖(gelfandTransform ℂ A) a‖ = ‖a‖
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n<VAR>x : ℤ_[p]<GOAL>x.appr (n + 1) < p ^ (n + 1)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n<VAR>x : ℤ_[p]<GOAL>(if h : x - ↑(x.appr n) = 0 then x.appr n else x.appr n + p ^ n * (toZMod ↑(unitCoeff ⋯) * 0 ^ match (x - ↑(x.appr n)).valuation - ↑n with | Int.ofNat m => m | Int.negSucc m => m.succ).val) < p ^ (n + 1)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n<VAR>x : ℤ_[p]<VAR>hp : p ^ n < p ^ (n + 1)<GOAL>(if h : x - ↑(x.appr n) = 0 then x.appr n else x.appr n + p ^ n * (toZMod ↑(unitCoeff ⋯) * 0 ^ match (x - ↑(x.appr n)).valuation - ↑n with | Int.ofNat m => m | Int.negSucc m => m.succ).val) < p ^ (n + 1)
<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₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁<GOAL>∃ e', e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right
<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₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁<VAR>φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ e.hom.left e.hom.right ⋯<GOAL>∃ e', e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right
<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₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁<VAR>φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ e.hom.left e.hom.right ⋯<VAR>this✝ : IsIso φ.hom₁<VAR>this : IsIso φ.hom₂<GOAL>∃ e', e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right
<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₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁<VAR>φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ e.hom.left e.hom.right ⋯<VAR>this✝¹ : IsIso φ.hom₁<VAR>this✝ : IsIso φ.hom₂<VAR>this : IsIso φ.hom₃<GOAL>∃ e', e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right
<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₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁<VAR>φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ e.hom.left e.hom.right ⋯<VAR>this✝² : IsIso φ.hom₁<VAR>this✝¹ : IsIso φ.hom₂<VAR>this✝ : IsIso φ.hom₃<VAR>this : IsIso φ<GOAL>∃ e', e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right