mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Do.Basic
/-- Return true if we should not lift nested action `(← …)` out of syntax nodes with the given kind.  -/
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.liftNestedActionDelimiter : Lean.SyntaxNodeKind → Bool
-- Mathlib.Algebra.Group.Action.Prod
Prod.vaddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] [inst_2 : VAdd N α]
  [inst_3 : VAdd N β] [VAddCommClass M N α] [VAddCommClass M N β], VAddCommClass M N (α × β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharTwoJEqZeroNF_iff : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R), W.IsCharTwoJEqZeroNF ↔ W.a₁ = 0 ∧ W.a₂ = 0
-- Mathlib.ModelTheory.Order
FirstOrder.Language.OrderedStructure.relMap_leSymb : ∀ {L : FirstOrder.Language} {M : Type w'} {inst : L.IsOrdered} {inst_1 : LE M} {inst_2 : L.Structure M}
  [self : L.OrderedStructure M] (x : Fin 2 → M),
  FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb x ↔ x 0 ≤ x 1
-- Mathlib.Algebra.Group.Shrink
Shrink.instInv : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Inv α] → Inv (Shrink.{v, u_2} α)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_nhds_of_im_pos : ∀ {z : ℂ}, 0 < z.im → Complex.arg =ᶠ[nhds z] fun x => Real.arccos (x.re / ‖x‖)
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.ι_map_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G) (j : J) {Z : C} (h : CategoryTheory.Limits.chosenCoend G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.map f) h) =
    CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op j)).app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι G j) h)
-- Init.GrindInstances.ToInt
Lean.Grind.instMulUInt64UintOfNatNat : Lean.Grind.ToInt.Mul UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
AddGroup.card_nsmul_eq_card_nsmul_card_univ : ∀ {G : Type u_5} [inst : AddGroup G] [inst_1 : Fintype G] (S : Set G)
  [inst_2 : (k : ℕ) → DecidablePred fun x => x ∈ k • S] (k : ℕ),
  Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₄ : UInt8 → UInt8 → UInt8 → UInt8 → Option Char
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
ENat.instMeasurableSpace : MeasurableSpace ℕ∞
-- Init.Omega.Constraint
Lean.Omega.Constraint.combine.eq_1 : ∀ (x y : Lean.Omega.Constraint),
  x.combine y =
    { lowerBound := Option.merge max x.lowerBound y.lowerBound,
      upperBound := Option.merge min x.upperBound y.upperBound }
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
/-- Construct the type of the cast of the given `CastKind`.  -/
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.mkRel : Lean.Expr → Lean.Expr → Mathlib.Tactic.Translate.CastKind✝ → Lean.MetaM Lean.Expr
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
/-- Local notation for a covariant derivative on a vector bundle acting on a vector field and a
section.  -/
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.CovariantDerivative.«term∇__» : Lean.ParserDescr
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.tendsto_atBot_diagonal : ∀ {α : Type u_3} [inst : Preorder α], Filter.Tendsto (fun a => (a, a)) Filter.atBot Filter.atBot
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Continuity from below: the measure of the union of a sequence of (not necessarily measurable)
sets is the limit of the measures of the partial unions.  -/
MeasureTheory.ProbabilityMeasure.tendsto_measure_iUnion_accumulate : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} [inst_1 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {f : ι → Set Ω},
  Filter.Tendsto (fun i => μ (Set.accumulate f i)) Filter.atTop (nhds (μ (⋃ i, f i)))
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The image of the normalizer is equal to the normalizer of the image of an
isomorphism.  -/
AddSubgroup.map_equiv_normalizer_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (f : G ≃+ N),
  AddSubgroup.map f.toAddMonoidHom (AddSubgroup.normalizer ↑H) =
    AddSubgroup.normalizer ↑(AddSubgroup.map f.toAddMonoidHom H)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.pushout.inr f g) g' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f (CategoryTheory.CategoryStruct.comp g g'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g')
        h)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_prod_map : ∀ {ι : Type u_2} {κ : Type u_3} {M : Type u_5} [inst : CommMonoid M] (m : Multiset ι) (n : Multiset κ) {f : ι → κ → M},
  (Multiset.map (fun a => (Multiset.map (fun b => f a b) n).prod) m).prod =
    (Multiset.map (fun b => (Multiset.map (fun a => f a b) m).prod) n).prod
-- Mathlib.RingTheory.Ideal.Operations
Submodule.span_smul_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R)
  (N : Submodule R M), Ideal.span s • N = s • N
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.eq_1 : ∀ (α : Type u), FreeGroup α = Quot FreeGroup.Red.Step
-- Mathlib.Topology.Spectral.Hom
SpectralMap.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : SpectralMap β γ} {f₁ f₂ : SpectralMap α β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_def : ∀ {α : Type u_1} {ε : Type u_4} [inst : ENorm ε] {x : MeasurableSpace α} (f : α → ε) (μ : MeasureTheory.Measure α),
  MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The closed unit ball in a valued ring is open.  -/
Valued.isOpen_integer : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  IsOpen ↑Valued.v.integer
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.unsortedEigenvalues.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T T_1 : E →ₗ[𝕜] E} (e_T : T = T_1) [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n) (i i_1 : Fin n),
  i = i_1 → LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn i = LinearMap.IsSymmetric.unsortedEigenvalues✝ ⋯ hn i_1
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.isEmpty.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β), m.isEmpty = (m.size == 0)
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_apply : ∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (a : CategoryTheory.Limits.colimit J),
  (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J) a =
    Quot.lift (fun p => ⟦p.snd⟧) ⋯ ((CategoryTheory.Limits.Types.colimitEquivColimitType J) a)
-- Mathlib.Topology.ClusterPt
clusterPt_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F ↔ ∀ s ∈ nhds x, ∃ᶠ (y : X) in F, y ∈ s
-- Init.Data.List.Perm
List.Perm.isEmpty_eq : ∀ {α : Type u_1} {l l' : List α}, l.Perm l' → l.isEmpty = l'.isEmpty
-- Mathlib.FieldTheory.CardinalEmb
/-- Extend `succEquiv` from `ι` to `WithTop ι`.  -/
Field.Emb.Cardinal.equivSucc : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [inst_3 : Algebra.IsAlgebraic F E] →
              (i : WithTop (Module.rank F E).ord.ToType) →
                (↥(Field.Emb.Cardinal.filtration (Order.succ i)) →ₐ[F] AlgebraicClosure E) ≃
                  (↥(Field.Emb.Cardinal.filtration i) →ₐ[F] AlgebraicClosure E) × Field.Emb.Cardinal.factor i
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
/-- The cokernel of the map `∐ fun (_ : α) ↦ R ⟶ ∐ fun (_ : β) ↦ R` induced
by a map `f : α → β` identifies to the coproduct of copies of `R`
indexed by the complement of the range of `f`.  -/
CategoryTheory.Limits.isColimitSigmaConstCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (R : C) →
        {α : Type u_1} →
          {β : Type u_2} →
            (f : α → β) →
              [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R] →
                [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] →
                  [inst_4 : CategoryTheory.Limits.HasCoproduct fun x => R] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.sigmaConstCokernelCofork R f)
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_one_mul : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → Metric.closedBall 1 δ * s = Metric.cthickening δ s
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.not_reachable_sum_inl_inr : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (v : V) (w : W),
  ¬(G ⊕g H).Reachable (Sum.inl v) (Sum.inr w)
-- Init.Data.List.Basic
List.length_nil : ∀ {α : Type u}, [].length = 0
-- ProofWidgets.Data.Html
/-- A `component h e props children` represents `<Foo {...props}>{...children}</Foo>`,
where `Foo : Component Props` is some component such that `h = hash Foo.javascript`,
`e = Foo.«export»`, and `props` will produce a JSON-encoded value of type `Props`.  -/
ProofWidgets.Html.component : UInt64 → String → ProofWidgets.LazyEncodable Lean.Json → Array ProofWidgets.Html → ProofWidgets.Html
-- Mathlib.Data.Countable.Basic
WithBot.instCountable : ∀ {α : Type u} [Countable α], Countable (WithBot α)
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Zeroes out coefficients of a `HahnSeries` at indices not less than `c`.  -/
HahnSeries.truncLT : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : Zero R] → [inst_1 : PartialOrder Γ] → [DecidableLT Γ] → Γ → ZeroHom (HahnSeries Γ R) (HahnSeries Γ R)
-- Mathlib.Data.Setoid.Partition
/-- Distinct elements of a set of sets partitioning α are disjoint.  -/
Setoid.eqv_classes_disjoint : ∀ {α : Type u_1} {c : Set (Set α)}, (∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) → c.PairwiseDisjoint id
-- Mathlib.Data.Nat.Choose.Central
Nat.two_le_centralBinom : ∀ (n : ℕ), 0 < n → 2 ≤ n.centralBinom
-- Mathlib.Data.Matrix.Basic
Matrix.piLinearEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} (R : Type u_16) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → Module R (β i)] (a : Matrix m n ((i : ι) → β i)) (i : ι),
  (Matrix.piLinearEquiv R) a i = Matrix.piAddEquiv.toFun a i
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_one_right_eq_nil : ∀ {m : ℕ}, (m<...1).toList = []
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm3c : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.not_limZero_of_pos : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f : CauSeq α abs},
  f.Pos → ¬f.LimZero
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_injective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
  Function.Injective f → Function.Injective (Finsupp.mapDomain f)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- `tensorLeftHomEquiv` commutes with tensoring on the right  -/
CategoryTheory.tensorLeftHomEquiv_tensor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z Z' : C} [inst_2 : CategoryTheory.ExactPairing Y Y']
  (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) (g : X' ⟶ Z'),
  (CategoryTheory.tensorLeftHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj X X') Y Y'
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Z Z')).symm
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
        (CategoryTheory.MonoidalCategoryStruct.associator Y Z Z').hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y' X X').inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm f) g)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_unitInv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f f' : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f' ↔
    f = f'
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller₀.congr_simp : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] (I : Ideal R) [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R], Perfection.teichmuller₀ p I = Perfection.teichmuller₀ p I
-- Init.Notation
Lean.guardMsgsSpec : Lean.ParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, ¬cmp k (t.maxKey ⋯) = Ordering.eq → (t.erase k).maxKey he = t.maxKey ⋯
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ENNReal},
  HasFiniteFPowerSeriesOnBall f p x n r → HasFPowerSeriesOnBall f p x r
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_comap_comap_eq_relfinrank_of_surjective : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : L →+* E),
  Function.Surjective ⇑f → (Subfield.comap f A).relfinrank (Subfield.comap f B) = A.relfinrank B
-- Init.Data.Order.Ord
/-- The corresponding lemma for `LawfulEqCmp` is `LawfulEqCmp.compare_eq_iff_eq`  -/
Std.LawfulEqOrd.compare_eq_iff_eq : ∀ {α : Type u} [inst : Ord α] [Std.LawfulEqOrd α] {a b : α}, compare a b = Ordering.eq ↔ a = b
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.mk.inj : ∀ {X : Type u_1} {R : Type u_2} {inst : Zero R} {inst_1 : Add R} {inst_2 : LE R} {toFun : X → X → R}
  {refl' : ∀ (x : X), toFun x x = 0} {symm' : ∀ (x y : X), toFun x y = toFun y x}
  {triangle' : ∀ (x y z : X), toFun x z ≤ toFun x y + toFun y z} {toFun_1 : X → X → R}
  {refl'_1 : ∀ (x : X), toFun_1 x x = 0} {symm'_1 : ∀ (x y : X), toFun_1 x y = toFun_1 y x}
  {triangle'_1 : ∀ (x y z : X), toFun_1 x z ≤ toFun_1 x y + toFun_1 y z},
  { toFun := toFun, refl' := refl', symm' := symm', triangle' := triangle' } =
      { toFun := toFun_1, refl' := refl'_1, symm' := symm'_1, triangle' := triangle'_1 } →
    toFun = toFun_1
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.mk : Lean.Name →
  Aesop.BuilderName →
    Aesop.ScopeName → Aesop.RuleTacDescr → Aesop.IndexingMode → Option Aesop.RulePattern → Aesop.CoreRuleBuilderOutput
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.ext : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {i : ι} {x y : Monoid.CoprodI.Word.Pair M i},
  x.head = y.head → x.tail = y.tail → x = y
-- Mathlib.Algebra.GroupWithZero.Associated
/-- `Associates.mk` as a `MonoidHom`.  -/
Associates.mkMonoidHom : {M : Type u_1} → [inst : CommMonoid M] → M →* Associates M
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_dual_prod : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν]
  {L : StrongDual ℝ (E × F)},
  MeasureTheory.MemLp id 2 μ →
    MeasureTheory.MemLp id 2 ν →
      ProbabilityTheory.variance (⇑L) (μ.prod ν) =
        ProbabilityTheory.variance (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ +
          ProbabilityTheory.variance (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ico_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ico a b)), Subtype.val '' Set.Iic c = Set.Icc a ↑c
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I), (P.toCostructuredArrow.obj X).hom = P.cocone.ι.app X
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.equivalenceOfIsInitial_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.Under.equivalenceOfIsInitial hX).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (({ obj := fun Y => CategoryTheory.Under.mk (hX.to Y), map := fun {X_1 Y} f => CategoryTheory.Under.homMk f ⋯,
                    map_id := ⋯, map_comp := ⋯ }.comp
                (CategoryTheory.Under.forget X)).obj
            x))
      ⋯
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonPartialResultParams.toJson : Lean.Lsp.PartialResultParams → Lean.Json
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- Given a topology on a ring `R` and an ideal `J`, `IsAdic J` means the topology is the
`J`-adic one.  -/
IsAdic : {R : Type u_1} → [inst : CommRing R] → [H : TopologicalSpace R] → Ideal R → Prop
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- A version of `Matrix.charpoly_mul_comm` for rectangular matrices.
See also `Matrix.charpoly_mul_comm_of_le` which has just `(A * B).charpoly` as the LHS.
 -/
Matrix.charpoly_mul_comm' : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (A : Matrix m n R) (B : Matrix n m R),
  Polynomial.X ^ Fintype.card n * (A * B).charpoly = Polynomial.X ^ Fintype.card m * (B * A).charpoly
-- Mathlib.Analysis.Analytic.Constructions
/-- `AnalyticOnNhd.comp` for functions on product spaces  -/
AnalyticOnNhd.comp₂ : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H]
  {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E},
  AnalyticOnNhd 𝕜 h s →
    AnalyticOnNhd 𝕜 f t → AnalyticOnNhd 𝕜 g t → (∀ x ∈ t, (f x, g x) ∈ s) → AnalyticOnNhd 𝕜 (fun x => h (f x, g x)) t
-- Mathlib.Algebra.Homology.Augment
ChainComplex.truncate_map_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {X Y : ChainComplex V ℕ} (f : X ⟶ Y) (i : ℕ), (ChainComplex.truncate.map f).f i = f.f (i + 1)
-- Init.Data.BitVec.Lemmas
BitVec.sdiv_zero : ∀ {n : ℕ} {x : BitVec n}, x.sdiv 0#n = 0#n
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- Composition of `π` with `f` and with `g` agree  -/
CategoryTheory.IsSplitCoequalizer.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π),
  CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.cone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) →
            [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] →
              (X : C) → (F.obj (Opposite.op 0)).obj.obj (Opposite.op X) → CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a Haar measure under right multiplication is again a Haar measure.  -/
MeasureTheory.Measure.isHaarMeasure_map_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [IsTopologicalGroup G] (g : G),
  (MeasureTheory.Measure.map (fun x => x * g) μ).IsHaarMeasure
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound_of_K_ne_0 : ∀ {δ K ε : ℝ}, K ≠ 0 → gronwallBound δ K ε = fun x => δ * Real.exp (K * x) + ε / K * (Real.exp (K * x) - 1)
-- Mathlib.Analysis.Normed.Order.UpperLower
upperClosure_interior_subset : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] (s : Set α),
  ↑(upperClosure (interior s)) ⊆ interior ↑(upperClosure s)
-- Mathlib.Algebra.Ring.WithZero
WithZero.instSemiring : {α : Type u_1} → [Semiring α] → Semiring (WithZero α)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal_mkQ_single_smul : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R) (x y : S),
  ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | r • x => y) = r • (KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => y
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- the right adjoint  -/
CategoryTheory.Bicategory.Adj.Hom.r : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → CategoryTheory.Bicategory.Adj.Hom a b → (b ⟶ a)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zipWith_nil_right : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Stream'.Seq α},
  Stream'.Seq.zipWith f s Stream'.Seq.nil = Stream'.Seq.nil
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The difference of two weighted homogeneous polynomials of degree `n` is weighted homogeneous
of weighted degree `n`.  -/
MvPolynomial.IsWeightedHomogeneous.sub : ∀ {M : Type u_2} {σ : Type u_3} [inst : AddCommMonoid M] {n : M} {R : Type u_4} [inst_1 : CommRing R] {w : σ → M}
  {φ ψ : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w φ n →
    MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ - ψ) n
-- Mathlib.Order.UpperLower.Relative
instSetLikeRelUpperSet : {α : Type u_1} → {P : α → Prop} → [inst : LE α] → SetLike (RelUpperSet P) α