ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0<VAR>hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤<GOAL>(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0<VAR>hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤<GOAL>(∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) = (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0<VAR>hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>a : α<GOAL>(g a ^ (p - 1)) ^ q = g a ^ p
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<GOAL>∀ {a b : Submodule R M}, { toFun := restrictScalars S, inj' := ⋯ } a ≤ { toFun := restrictScalars S, inj' := ⋯ } b ↔ a ≤ b
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖(toDualContinuousMultilinearMap F) x‖ ≤ projectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯‖ ≤ projectiveSeminorm x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a : α<VAR>s : Set α<GOAL>(insert a s).ncard ≤ s.ncard + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a : α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(insert a s).ncard ≤ s.ncard + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a : α<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>(insert a s).ncard ≤ s.ncard + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a : α<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>0 ≤ s.ncard + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.next (l.prev x hx) ⋯ = x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>hn : n < l.length<VAR>hx : l.nthLe n hn ∈ l<GOAL>l.next (l.prev (l.nthLe n hn) hx) ⋯ = l.nthLe n hn
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>hn : n < l.length<VAR>hx : l.nthLe n hn ∈ l<GOAL>l.nthLe ((n + (l.length - 1) + 1) % l.length) ⋯ = l.nthLe n hn
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0<VAR>hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0<VAR>hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_top : ¬∫⁻ (a : α), g a ^ q ∂μ = ⊤<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>ts : Set (TopologicalSpace E)<VAR>h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E<VAR>this : TopologicalSpace E := sInf ts<GOAL>LocallyConvexSpace 𝕜 E
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>ts : Set (TopologicalSpace E)<VAR>h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E<VAR>this : TopologicalSpace E := sInf ts<VAR>x : E<GOAL>(𝓝 x).HasBasis ((fun x If => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) x) ((fun x If => ⋂ i ∈ If.1, If.2 i) x)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>ts : Set (TopologicalSpace E)<VAR>h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E<VAR>this : TopologicalSpace E := sInf ts<VAR>x : E<GOAL>(⨅ i, 𝓝 x).HasBasis ((fun x If => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) x) ((fun x If => ⋂ i ∈ If.1, If.2 i) x)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Ioc a b ↔ x ∈ Ioc (r • a) (r • b)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y, (a < y ∧ y ≤ b) ∧ r * y = x) ↔ r * a < x ∧ x ≤ r * b
<VAR>m n a b c d : ℤ<VAR>h₁ : c ≡ d [ZMOD n]<VAR>h₂ : a + c ≡ b + d [ZMOD n]<GOAL>a ≡ b [ZMOD n]
<VAR>m n a b c d : ℤ<VAR>h₁ : c ≡ d [ZMOD n]<VAR>h₂ : c + a ≡ d + b [ZMOD n]<GOAL>a ≡ b [ZMOD n]
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>x : B<VAR>hx : adjoin K {(algebraMap B L) x} = ⊤<GOAL>(aeval x) (derivative (minpoly A x)) ∈ differentIdeal A B
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>x : B<VAR>hx : adjoin K {(algebraMap B L) x} = ⊤<GOAL>Ideal.span {(aeval x) (derivative (minpoly A x))} ≤ differentIdeal A B
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>x : B<VAR>hx : adjoin K {(algebraMap B L) x} = ⊤<GOAL>conductor A x * differentIdeal A B ≤ differentIdeal A B
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<GOAL>𝓝[≥] a = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<GOAL>((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<GOAL>(⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Disjoint (f i) (f j)<GOAL>{i, j}.SupIndep f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Disjoint (f i) (f j)<GOAL>∀ i_1 ∈ {i, j}, Disjoint (f i_1) (({i, j}.erase i_1).sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Disjoint (f i) (f j)<VAR>k : ι<VAR>hk : k ∈ {i, j}<GOAL>Disjoint (f k) (({i, j}.erase k).sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Disjoint (f i) (f j)<VAR>k : ι<VAR>hk : k = i ∨ k = j<GOAL>Disjoint (f k) (({i, j}.erase k).sup f)
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>f : SmallHom W₁ X Y<GOAL>(SmallHom.equiv W₂ L₂) (Φ.smallHomMap f) = e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) f) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<GOAL>(SmallHom.equiv W₂ L₂) (Φ.smallHomMap ((SmallHom.equiv W₁ W₁.Q).symm g)) = e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) ((SmallHom.equiv W₁ W₁.Q).symm g)) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<GOAL>(SmallHom.equiv W₂ L₂) ((SmallHom.equiv W₂ W₂.Q).symm ((((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr ((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y)) ((Φ.localizedFunctor W₁.Q W₂.Q).map g))) = e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) ((SmallHom.equiv W₁ W₁.Q).symm g)) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<GOAL>(SmallHom.equiv W₂ L₂) ((SmallHom.equiv W₂ W₂.Q).symm ((((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr ((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y)) ((Φ.localizedFunctor W₁.Q W₂.Q).map g))) = e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) ((SmallHom.equiv W₁ W₁.Q).symm g)) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<GOAL>α₂.inv.app (Φ.functor.obj X) ≫ E₂.map ((((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr ((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y)) ((Φ.localizedFunctor W₁.Q W₂.Q).map g)) ≫ α₂.hom.app (Φ.functor.obj Y) = e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>γ : G' ⋙ E₂ ≅ E₁ ⋙ G := liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G) ((W₁.Q.associator G' E₂).symm ≪≫ isoWhiskerRight β.symm E₂ ≪≫ Φ.functor.associator W₂.Q E₂ ≪≫ isoWhiskerLeft Φ.functor α₂ ≪≫ e ≪≫ isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)<GOAL>α₂.inv.app (Φ.functor.obj X) ≫ E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor.obj Y) = e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>γ : G' ⋙ E₂ ≅ E₁ ⋙ G := liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G) ((W₁.Q.associator G' E₂).symm ≪≫ isoWhiskerRight β.symm E₂ ≪≫ Φ.functor.associator W₂.Q E₂ ≪≫ isoWhiskerLeft Φ.functor α₂ ≪≫ e ≪≫ isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)<VAR>hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) = E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)<GOAL>α₂.inv.app (Φ.functor.obj X) ≫ E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor.obj Y) = e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>γ : G' ⋙ E₂ ≅ E₁ ⋙ G := liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G) ((W₁.Q.associator G' E₂).symm ≪≫ isoWhiskerRight β.symm E₂ ≪≫ Φ.functor.associator W₂.Q E₂ ≪≫ isoWhiskerLeft Φ.functor α₂ ≪≫ e ≪≫ isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)<VAR>hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) = E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)<GOAL>α₂.inv.app (Φ.functor.obj X) ≫ E₂.map (β.hom.app X) ≫ E₂.map (G'.map g) ≫ E₂.map (β.inv.app Y) ≫ α₂.hom.app (Φ.functor.obj Y) = e.hom.app X ≫ G.map (α₁.inv.app X) ≫ G.map (E₁.map g) ≫ G.map (α₁.hom.app Y) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>γ : G' ⋙ E₂ ≅ E₁ ⋙ G := liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G) ((W₁.Q.associator G' E₂).symm ≪≫ isoWhiskerRight β.symm E₂ ≪≫ Φ.functor.associator W₂.Q E₂ ≪≫ isoWhiskerLeft Φ.functor α₂ ≪≫ e ≪≫ isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)<VAR>hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) = E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)<GOAL>α₂.inv.app (Φ.functor.obj X) ≫ E₂.map (β.hom.app X) ≫ E₂.map (G'.map g) ≫ E₂.map (β.inv.app Y) ≫ α₂.hom.app (Φ.functor.obj Y) = e.hom.app X ≫ G.map (α₁.inv.app X) ≫ (γ.inv.app (W₁.Q.obj X) ≫ (G' ⋙ E₂).map g ≫ γ.hom.app (W₁.Q.obj Y)) ≫ G.map (α₁.hom.app Y) ≫ e.inv.app Y
<VAR>C₁ : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>W : ?m.28304<VAR>X Y Z : C₁<VAR>inst✝¹ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : D₁ ⥤ D₂<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G<VAR>g : W₁.Q.obj X ⟶ W₁.Q.obj Y<VAR>G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q<VAR>β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'<VAR>E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor<VAR>α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor<VAR>α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>γ : G' ⋙ E₂ ≅ E₁ ⋙ G := liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G) ((W₁.Q.associator G' E₂).symm ≪≫ isoWhiskerRight β.symm E₂ ≪≫ Φ.functor.associator W₂.Q E₂ ≪≫ isoWhiskerLeft Φ.functor α₂ ≪≫ e ≪≫ isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)<VAR>hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) = E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)<GOAL>γ.hom.app (W₁.Q.obj X) ≫ G.map (α₁.hom.app X) ≫ e.inv.app X ≫ α₂.inv.app (Φ.functor.obj X) ≫ E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor.obj Y) = E₂.map (G'.map g) ≫ γ.hom.app (W₁.Q.obj Y) ≫ G.map (α₁.hom.app Y) ≫ e.inv.app Y
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>h : l.Nodup<VAR>i : ℕ<VAR>hi : i < l.length<VAR>j : ℕ<VAR>hj : j < l.length<GOAL>l[i] = l[j] ↔ i = j
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>h : l.Nodup<VAR>i : ℕ<VAR>hi : i < l.length<VAR>j : ℕ<VAR>hj : j < l.length<VAR>this : l.get ⟨i, hi⟩ = l.get ⟨j, hj⟩ ↔ ⟨i, hi⟩ = ⟨j, hj⟩<GOAL>l[i] = l[j] ↔ i = j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι✝ : Sort u_6<VAR>s✝ t u : Set α<VAR>ι : Sort u_7<VAR>m : ι → MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s