ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>κ.rnDeriv η a x = ⊤ ↔ (a, x) ∈ κ.mutuallySingularSet η
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (tanh ↑x) = tanh ↑x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>f : Multiset (α →₀ M)<VAR>h : α → M → N<VAR>h₀ : ∀ (a : α), h a 0 = 0<VAR>h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂<VAR>a : α →₀ M<VAR>s : Multiset (α →₀ M)<VAR>ih : s.sum.sum h = (Multiset.map (fun g => g.sum h) s).sum<GOAL>(a ::ₘ s).sum.sum h = (Multiset.map (fun g => g.sum h) (a ::ₘ s)).sum
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : Seq α<GOAL>(cons a s).head = some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<VAR>hr : 0 < ↑r<GOAL>dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁹ : SeminormedAddCommGroup V<VAR>inst✝⁸ : PseudoMetricSpace P<VAR>inst✝⁷ : NormedAddTorsor V P<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : MetricSpace Q<VAR>inst✝⁴ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : Invertible 2<VAR>p₁ p₂ p₃ p₄ : P<GOAL>dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁹ : SeminormedAddCommGroup V<VAR>inst✝⁸ : PseudoMetricSpace P<VAR>inst✝⁷ : NormedAddTorsor V P<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : MetricSpace Q<VAR>inst✝⁴ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : Invertible 2<VAR>p₁ p₂ p₃ p₄ : P<GOAL>‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁹ : SeminormedAddCommGroup V<VAR>inst✝⁸ : PseudoMetricSpace P<VAR>inst✝⁷ : NormedAddTorsor V P<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : MetricSpace Q<VAR>inst✝⁴ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : Invertible 2<VAR>p₁ p₂ p₃ p₄ : P<GOAL>‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / ‖2‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>f : α → β<VAR>s : Set β<VAR>l : Filter α<VAR>t : Set β<GOAL>t ∈ map f (l ⊓ 𝓟 (f ⁻¹' s)) ↔ t ∈ map f l ⊓ 𝓟 s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra F[X] S<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Algebra F S<VAR>inst✝ : IsScalarTower F F[X] S<VAR>b : Basis ι F[X] S<VAR>f : S<VAR>hf : f ≠ 0<VAR>this : Fintype ι<GOAL>FiniteDimensional.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra F[X] S<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Algebra F S<VAR>inst✝ : IsScalarTower F F[X] S<VAR>b : Basis ι F[X] S<VAR>f : S<VAR>hf : f ≠ 0<VAR>this : Fintype ι<VAR>h : ¬span {f} = ⊥<GOAL>FiniteDimensional.finrank F (S ⧸ span {f}) = ((Algebra.norm F[X]) f).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra F[X] S<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Algebra F S<VAR>inst✝ : IsScalarTower F F[X] S<VAR>b : Basis ι F[X] S<VAR>f : S<VAR>hf : f ≠ 0<VAR>this : Fintype ι<VAR>h : ¬span {f} = ⊥<GOAL>FiniteDimensional.finrank F (S ⧸ span {f}) = (∏ i : ι, smithCoeffs b (span {f}) ⋯ i).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra F[X] S<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Algebra F S<VAR>inst✝ : IsScalarTower F F[X] S<VAR>b : Basis ι F[X] S<VAR>f : S<VAR>hf : f ≠ 0<VAR>this : Fintype ι<VAR>h : ¬span {f} = ⊥<GOAL>∑ i : ι, FiniteDimensional.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = ∑ i : ι, (smithCoeffs b (span {f}) h i).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra F[X] S<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Algebra F S<VAR>inst✝ : IsScalarTower F F[X] S<VAR>b : Basis ι F[X] S<VAR>f : S<VAR>hf : f ≠ 0<VAR>this : Fintype ι<VAR>h : ¬span {f} = ⊥<VAR>i : ι<GOAL>FiniteDimensional.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = (smithCoeffs b (span {f}) h i).natDegree
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>h : ∃ x, ‖x‖ ≠ 0<VAR>x : V<VAR>hx : ‖x‖ ≠ 0<GOAL>1 ≤ ‖id V‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>h : ∃ x, ‖x‖ ≠ 0<VAR>x : V<VAR>hx : ‖x‖ ≠ 0<VAR>this : ‖(id V) x‖ / ‖x‖ ≤ ‖id V‖<GOAL>1 ≤ ‖id V‖
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I : Ideal R<VAR>hI : I.IsRadical<GOAL>IsIrreducible (zeroLocus ↑I) ↔ I.IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I : Ideal R<VAR>hI : I.IsRadical<GOAL>(zeroLocus ↑I).Nonempty ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I : Ideal R<VAR>hI : I.IsRadical<GOAL>(zeroLocus ↑I).Nonempty ↔ I ≠ ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I : Ideal R<VAR>hI : I.IsRadical<GOAL>IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>s s' : σ<VAR>n n' : ℕ<GOAL>coeff (Finsupp.single s' n') (X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁷ : Countable ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : OrderTopology ι<VAR>inst✝⁴ : FirstCountableTopology ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>N : ι<VAR>hτbdd : ∀ (x : Ω), τ x ≤ N<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Adapted f u<VAR>n : ι<GOAL>MeasurableSet {ω | (fun x => hitting u s (τ x) N x) ω ≤ n}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁷ : Countable ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : OrderTopology ι<VAR>inst✝⁴ : FirstCountableTopology ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>N : ι<VAR>hτbdd : ∀ (x : Ω), τ x ≤ N<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Adapted f u<VAR>n : ι<VAR>h₁ : {x | hitting u s (τ x) N x ≤ n} = (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪ ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}<GOAL>MeasurableSet {ω | (fun x => hitting u s (τ x) N x) ω ≤ n}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁷ : Countable ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : OrderTopology ι<VAR>inst✝⁴ : FirstCountableTopology ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>N : ι<VAR>hτbdd : ∀ (x : Ω), τ x ≤ N<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Adapted f u<VAR>n : ι<VAR>h₁ : {x | hitting u s (τ x) N x ≤ n} = (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪ ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}<VAR>h₂ : ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅<GOAL>MeasurableSet {ω | (fun x => hitting u s (τ x) N x) ω ≤ n}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝⁸ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝⁷ : Countable ι<VAR>inst✝⁶ : TopologicalSpace ι<VAR>inst✝⁵ : OrderTopology ι<VAR>inst✝⁴ : FirstCountableTopology ι<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>f : Filtration ι m<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>N : ι<VAR>hτbdd : ∀ (x : Ω), τ x ≤ N<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Adapted f u<VAR>n : ι<VAR>h₁ : {x | hitting u s (τ x) N x ≤ n} = (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪ ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}<VAR>h₂ : ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅<GOAL>MeasurableSet (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n})
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>x ∈ selfAdjoint R ↔ star x = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>x ∈ (selfAdjoint R).carrier ↔ star x = x
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<GOAL>IsConnected (StructuredArrow d F)
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<VAR>this : Nonempty (StructuredArrow d F)<GOAL>IsConnected (StructuredArrow d F)
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<VAR>this : Nonempty (StructuredArrow d F)<GOAL>∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<VAR>this : Nonempty (StructuredArrow d F)<VAR>X₁ : C<VAR>f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁<VAR>X₂ : C<VAR>f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂<VAR>y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁<VAR>y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂<GOAL>Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ } { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<VAR>this : Nonempty (StructuredArrow d F)<VAR>X₁ : C<VAR>f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁<VAR>X₂ : C<VAR>f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂<VAR>y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁<VAR>y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂<VAR>e : y₁ = y₂<GOAL>Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ } { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<VAR>this : Nonempty (StructuredArrow d F)<VAR>X₁ : C<VAR>f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁<VAR>X₂ : C<VAR>f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂<VAR>y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁<VAR>y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂<VAR>e : y₁ = y₂<VAR>t : EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) ⟨X₁, f₁⟩ ⟨X₂, f₂⟩<GOAL>Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ } { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
<VAR>C : Type v<VAR>inst✝¹ : Category.{v, v} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v, u₁} D<VAR>F : C ⥤ D<VAR>I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}<VAR>d : D<VAR>this : Nonempty (StructuredArrow d F)<VAR>X₁ : C<VAR>f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁<VAR>X₂ : C<VAR>f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂<VAR>t : EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) ⟨X₁, f₁⟩ ⟨X₂, f₂⟩<GOAL>Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ } { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<GOAL>IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)))
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<GOAL>↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)) = mk R S M
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>s : S<VAR>x : M<GOAL>s • 1 ⊗ₜ[R] x = s ⊗ₜ[R] x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>s : S<VAR>x : M<GOAL>(s • 1) ⊗ₜ[R] x = s ⊗ₜ[R] x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>s : S<VAR>x : M<GOAL>s • 1 = s
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<VAR>p : Submodule R₁ M₁<VAR>x✝¹ x✝ : ↥p<GOAL>((B.domRestrict₁₂ p p) x✝¹) x✝ = 0 → ((B.domRestrict₁₂ p p) x✝) x✝¹ = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<VAR>p : Submodule R₁ M₁<VAR>x✝¹ x✝ : ↥p<GOAL>(B ↑x✝¹) ↑x✝ = 0 → (B ↑x✝) ↑x✝¹ = 0
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝⁴ : SmallCategory J<VAR>inst✝³ : FinCategory J<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>f : ι → α<GOAL>Finset.univ.inf (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.inf f
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝⁴ : SmallCategory J<VAR>inst✝³ : FinCategory J<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>f : ι → α<GOAL>Finset.univ.inf f = Fintype.elems.inf f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝¹ : Applicative m<VAR>inst✝ : LawfulApplicative m<VAR>x : m α<VAR>h : ∀ (a : α), p a<GOAL>Subtype.val <$> (fun a => ⟨a, ⋯⟩) <$> x = x
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>a : α<VAR>v : Vector3 α n<GOAL>insert a v fz = a :: v
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<GOAL>(∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<GOAL>(¬∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔ ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<GOAL>(∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔ ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>h : (↑P).Normal<VAR>this : Unique (Sylow p G)<GOAL>(↑P).Characteristic
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>h : (↑P).Normal<VAR>this : Unique (Sylow p G)<GOAL>∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom ↑P = ↑P
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>h : (↑P).Normal<VAR>this : Unique (Sylow p G)<VAR>Φ : G ≃* G<GOAL>Φ • P = P
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<VAR>H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2<GOAL>a₁.y ≤ a.y
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<VAR>H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2<GOAL>a₁.x ≤ a.x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>l' : Type u_5<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>o' : Type u_8<VAR>m'' : Type u_9<VAR>n'' : Type u_10<VAR>R : Type u_11<VAR>A : Type u_12<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : Module R A<VAR>e₁ : m ≃ m'<VAR>e₂ : n ≃ n'<VAR>e₁' : m' ≃ m''<VAR>e₂' : n' ≃ n''<GOAL>⇑(reindexLinearEquiv R A e₁' e₂') ∘ ⇑(reindexLinearEquiv R A e₁ e₂) = ⇑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>l' : Type u_5<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>o' : Type u_8<VAR>m'' : Type u_9<VAR>n'' : Type u_10<VAR>R : Type u_11<VAR>A : Type u_12<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : Module R A<VAR>e₁ : m ≃ m'<VAR>e₂ : n ≃ n'<VAR>e₁' : m' ≃ m''<VAR>e₂' : n' ≃ n''<GOAL>⇑(reindexLinearEquiv R A e₁' e₂') ∘ ⇑(reindexLinearEquiv R A e₁ e₂) = ⇑(reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂')
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<GOAL>Metric.closedBall 0 r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<GOAL>∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b ≤ r₁ * r₂