ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>this : Epi S.g<GOAL>((opcyclesFunctor C c i).mapShortComplex.obj S).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>((cyclesFunctor C c j).mapShortComplex.obj S).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>this : Mono S.f<GOAL>((cyclesFunctor C c j).mapShortComplex.obj S).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>Epi ((opcyclesFunctor C c i).mapShortComplex.obj S).g
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>this : Epi S.g<GOAL>Epi ((opcyclesFunctor C c i).mapShortComplex.obj S).g
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>Mono ((cyclesFunctor C c j).mapShortComplex.obj S).f
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>this : Mono S.f<GOAL>Mono ((cyclesFunctor C c j).mapShortComplex.obj S).f
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>wittAdd p 0 = X (0, 0) + X (1, 0)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>(map (Int.castRingHom ℚ)) (wittAdd p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) + X (1, 0))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<GOAL>ContinuousWithinAt φ B x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<GOAL>∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<GOAL>φ ⁻¹' V' ∈ 𝓝[B] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<GOAL>φ ⁻¹' V' ∈ 𝓝[B] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<GOAL>∀ y ∈ V ∩ B, φ y ∈ V'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<VAR>y : X<VAR>hyV : y ∈ V<VAR>hyB : y ∈ B<GOAL>φ y ∈ V'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<VAR>y : X<VAR>hyV : y ∈ V<VAR>hyB : y ∈ B<VAR>this : (𝓝[A] y).NeBot<GOAL>φ y ∈ V'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<VAR>y : X<VAR>hyV : y ∈ V<VAR>hyB : y ∈ B<VAR>this : (𝓝[A] y).NeBot<VAR>limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))<GOAL>φ y ∈ V'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<VAR>y : X<VAR>hyV : y ∈ V<VAR>hyB : y ∈ B<VAR>this : (𝓝[A] y).NeBot<VAR>limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))<VAR>hVy : V ∈ 𝓝 y<GOAL>φ y ∈ V'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<VAR>φ : X → Y := extendFrom A f<VAR>x : X<VAR>x_in : x ∈ B<VAR>V' : Set Y<VAR>V'_in : V' ∈ 𝓝 (φ x)<VAR>V'_closed : IsClosed V'<VAR>V : Set X<VAR>V_in : V ∈ 𝓝 x<VAR>V_op : IsOpen V<VAR>hV : V ∩ A ⊆ f ⁻¹' V'<VAR>y : X<VAR>hyV : y ∈ V<VAR>hyB : y ∈ B<VAR>this✝ : (𝓝[A] y).NeBot<VAR>limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))<VAR>hVy : V ∈ 𝓝 y<VAR>this : V ∩ A ∈ 𝓝[A] y<GOAL>φ y ∈ V'
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
<VAR>a b : ℝ<VAR>n : ℕ<VAR>this : ∫ (x : ℝ) in a..b, x ^ 1 = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)<GOAL>∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>x : E<VAR>y : E'<GOAL>⟪f x, y⟫_𝕜 = ⟪x, f.symm y⟫_𝕜
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>n : ℕ<VAR>v : Fin n → V<GOAL>LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ (last n✝)<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.castSucc<VAR>i : Fin n✝<VAR>y✝ : α✝ i.castSucc<VAR>z : α✝ (last n✝)<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>y : α<VAR>ys : Fin m → α<GOAL>append xs (cons y ys) = append (snoc xs y) ys ∘ cast ⋯
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ (last n✝)<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.castSucc<VAR>i : Fin n✝<VAR>y✝ : α✝ i.castSucc<VAR>z : α✝ (last n✝)<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>y : α<VAR>ys : Fin m → α<GOAL>append xs (cons y ys) = (append xs (cons y ys) ∘ cast ⋯) ∘ cast ⋯
<VAR>m✝ n✝ a b c d m n : ℕ<VAR>hm1 : m % 2 = 1<VAR>hn1 : n % 2 = 1<VAR>hm0 : 0 < m<VAR>hn0 : 0 < n<GOAL>2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>ha : μ {a} ≠ ⊤<VAR>hb : μ {b} ≠ ⊤<GOAL>IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_4, u_1} C<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : hl₁.IsPreservedBy F<VAR>inst✝ : hl₂.IsPreservedBy F<VAR>γ : LeftHomologyMapData φ hl₁ hl₂<GOAL>F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>v : HeightOneSpectrum R<VAR>hv : v ∈ {v | v.maxPowDividing I ≠ 1}<VAR>h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>v : HeightOneSpectrum R<VAR>hv : v ∈ {v | v.maxPowDividing I ≠ 1}<VAR>h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0<VAR>hv' : v.maxPowDividing I = 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<GOAL>IsCauSeq abv (-f) ↔ IsCauSeq abv f
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : Field 𝕂<VAR>inst✝³ : Ring 𝔸<VAR>inst✝² : Algebra 𝕂 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<GOAL>exp 𝕂 0 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>_root_.Disjoint (s.erase a) t ↔ _root_.Disjoint s (t.erase a)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>x : ℝ<GOAL>HasDerivAt (fun y => ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) ((fourier (-n)) ↑x) x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>x : ℝ<GOAL>(fun y => ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) = fun x => (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>x : ℝ<GOAL>(fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : Y ⟶ X<GOAL>α.hom ≫ f = 𝟙 X ↔ f = α.inv
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)<VAR>this : StrictAntiOn f (Icc s t) → False<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>this : StrictAntiOn f (Icc s t) → False<VAR>hf_mono_st : StrictMonoOn f (Icc s t)<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>this : StrictAntiOn f (Icc s t) → False<VAR>hf_mono_st : StrictMonoOn f (Icc s t)<VAR>hsx : s ≤ x<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>this : StrictAntiOn f (Icc s t) → False<VAR>hf_mono_st : StrictMonoOn f (Icc s t)<VAR>hsx : s ≤ x<VAR>hyt : y ≤ t<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>hf_mono_st : StrictMonoOn f (Icc s t)<VAR>hsx : s ≤ x<VAR>hyt : y ≤ t<VAR>this : Icc x y ⊆ Icc s t<GOAL>f x < f y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>hf_mono : StrictMonoOn f (Icc a b)<VAR>x y : α<VAR>hxy : x < y<VAR>s : α := min a x<VAR>t : α := max b y<VAR>hsa : s ≤ a<VAR>hbt : b ≤ t<VAR>hst : s ≤ t<VAR>hf_mono_st : StrictMonoOn f (Icc s t)<VAR>hsx : s ≤ x<VAR>hyt : y ≤ t<VAR>this : StrictMonoOn f (Icc x y)<GOAL>f x < f y
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>inst✝³ : Category.{?u.42329, u_1} C₁<VAR>inst✝² : Category.{?u.42333, u_2} C₂<VAR>inst✝¹ : Category.{?u.42337, u_3} C₃<VAR>F : C₁ ⥤ C₂ ⥤ C₃<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>inst✝ : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>X₁ X₂ : GradedObject I C₁<VAR>φ : X₁ ⟶ X₂<VAR>Y₁ Y₂ : GradedObject J C₂<VAR>ψ : Y₁ ⟶ Y₂<GOAL>mapMap (((mapBifunctor F I J).map (𝟙 X₁)).app Y₁ ≫ ((mapBifunctor F I J).obj X₁).map ψ) p ≫ mapMap (((mapBifunctor F I J).map φ).app Y₂ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₂)) p = mapMap (((mapBifunctor F I J).map φ).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₁)) p ≫ mapMap (((mapBifunctor F I J).map (𝟙 X₂)).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map ψ) p
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>hc : c ≠ 0<GOAL>a / c * (c / b) = a / b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<VAR>i : ι<GOAL>(b.toBasis.repr x) i = b.repr x i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<VAR>i : ι<GOAL>b.repr.toLinearEquiv x i = b.repr x i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s✝ t : Set E<VAR>x : E<VAR>s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : y ∈ balancedCore 𝕜 s<GOAL>(fun x => a • x) y ∈ balancedCore 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s✝ t : Set E<VAR>x : E<VAR>s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t<GOAL>(fun x => a • x) y ∈ balancedCore 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s✝ t✝ : Set E<VAR>x : E<VAR>s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>t : Set E<VAR>ht1 : Balanced 𝕜 t<VAR>ht2 : t ⊆ s<VAR>hy : y ∈ t<GOAL>(fun x => a • x) y ∈ balancedCore 𝕜 s