mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.mvfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {x : M} {f : M → E'},
  MDiffAt[s] f x →
    d[s] f x =
      fderivWithin 𝕜 (writtenInExtChartAt I (modelWithCornersSelf 𝕜 E') x f)
        (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.linearMap_eq_zero_iff_of_eq_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_8}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {V : Submodule R M} (f : ↥V →ₗ[R] N) {S : Set M}
  (hV : V = Submodule.span R S), f = 0 ↔ ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = 0
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.WeaklyConnectedComponent.instInhabited : {V : Type u_1} → [inst : Quiver V] → [Inhabited V] → Inhabited (Quiver.WeaklyConnectedComponent V)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin
/-- `0` is an initial object in `Fin n` when `n ≠ 0`.  -/
Fin.isInitialZero : (n : ℕ) → [inst : NeZero n] → CategoryTheory.Limits.IsInitial 0
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
ULift.nndist_eq : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β), nndist x y = nndist x.down y.down
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry : Type → Type
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.degMatrix.eq_1 : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : AddMonoidWithOne R],
  SimpleGraph.degMatrix R G = Matrix.diagonal fun x => ↑(G.degree x)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_add_sum_eq_sum_zipWith_add_sum_drop : ∀ {M : Type u_4} [inst : AddCommMonoid M] (l l' : List M),
  l.sum + l'.sum =
    (List.zipWith (fun x1 x2 => x1 + x2) l l').sum + (List.drop l'.length l).sum + (List.drop l.length l').sum
-- Init.Data.SInt.Lemmas
ISize.ofInt_bitVecToInt : ∀ (n : BitVec System.Platform.numBits), ISize.ofInt n.toInt = ISize.ofBitVec n
-- Init.Data.Vector.Lemmas
Vector.contains_iff : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {a : α} {as : Vector α n}, as.contains a = true ↔ a ∈ as
-- Mathlib.GroupTheory.Perm.List
List.formPerm_pow_apply_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α),
  l.Nodup → ∀ (n i : ℕ) (h : i < l.length), (l.formPerm ^ n) l[i] = l[(i + n) % l.length]
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.join.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 α) → Sort u_2) →
    (x : Option (Stream'.Seq1 α)) → (Unit → motive none) → ((s' : Stream'.Seq1 α) → motive (some s')) → motive x
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.instCategoryFunctorsInverting : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (D : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          CategoryTheory.Category.{max u v_1, max (max (max u_1 v_1) u) v} (W.FunctorsInverting D)
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.mk : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) →
  Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty) →
    String → Array (Lean.Doc.Inline Lean.ElabInline) → Lean.VersoModuleDocs.DocFrame✝
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp k ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minEntryD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.minEntryD fallback = t₂.minEntryD fallback
-- Init.Data.List.Lemmas
List.length_eq_of_beq : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α}, (l₁ == l₂) = true → l₁.length = l₂.length
-- Mathlib.Analysis.LocallyConvex.AbsConvex
IsOpen.absConvexHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [ZeroLEOneClass 𝕜] [inst_5 : TopologicalSpace E] [ContinuousConstSMul 𝕜 E]
  [IsTopologicalAddGroup E] {s : Set E}, IsOpen s → 0 ∈ s → IsOpen ((absConvexHull 𝕜) s)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_inter_self`. -/
Set.diff_inter_self : ∀ {α : Type u_1} {a b : Set α}, b \ a ∩ a = ∅
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image_image2_distrib_left`.  -/
Set.image2_image_left_comm : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} {f : α' → β → γ}
  {g : α → α'} {f' : α → β → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f (g a) b = g' (f' a b)) → Set.image2 f (g '' s) t = g' '' Set.image2 f' s t
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.immediate.sizeOf_spec : ∀ (names : Array Lean.Name), sizeOf (Aesop.Frontend.BuilderOption.immediate names) = 1 + sizeOf names
-- Mathlib.Probability.IdentDistrib
/-- If `X` and `Y` are independent and `(X, Y)` and `(X', Y')` are identically distributed,
then `X'` and `Y'` are independent.  -/
ProbabilityTheory.indepFun_of_identDistrib_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ] {μ : MeasureTheory.Measure γ} {μ' : MeasureTheory.Measure δ}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'] {X : γ → α} {X' : δ → α} {Y : γ → β}
  {Y' : δ → β},
  ProbabilityTheory.IndepFun X Y μ →
    ProbabilityTheory.IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ' →
      ProbabilityTheory.IndepFun X' Y' μ'
-- Mathlib.Algebra.Order.Group.Basic
zpow_right_inj : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α},
  1 < a → ∀ {m n : ℤ}, a ^ m = a ^ n ↔ m = n
-- Init.PropLemmas
forall_and : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.one_le_mulConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G}, A.Nonempty → B.Nonempty → 1 ≤ A.mulConst B
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_natural_right : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map g))
      (CategoryTheory.Localization.Monoidal.μ L W ε X Y₂).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X Y₁).hom
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_comp_ofList : ∀ {α : Type u_1}, ⇑FreeMonoid.toList ∘ ⇑FreeMonoid.ofList = id
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformContinuousOn.tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {x : α} [inst_1 : UniformSpace α]
  [inst_2 : UniformSpace γ] {U : Set α},
  U ∈ nhds x → ∀ {F : α → β → γ}, UniformContinuousOn (↿F) (U ×ˢ Set.univ) → TendstoUniformly F (F x) (nhds x)
-- Mathlib.Analysis.Seminorm
/-- A seminorm is convex. Also see `convexOn_norm`.  -/
Seminorm.convexOn : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul ℝ 𝕜] [NormSMulClass ℝ 𝕜]
  [inst_4 : Module 𝕜 E] [inst_5 : SMul ℝ E] [IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E), ConvexOn ℝ Set.univ ⇑p
-- Aesop.Builder.Default
Aesop.RuleBuilder.default : Aesop.RuleBuilder
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
/-- Auxiliary definition for `SSet.isColimitCoconeN`.  -/
_private.Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit.0.SSet.isColimitCoconeN.desc : {X : SSet} → (s : CategoryTheory.Limits.Cocone X.functorN) → X ⟶ s.pt
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.trivializationAt_proj_fst : ∀ {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] {x : Bundle.TotalSpace F E}, (↑(trivializationAt F E x.proj) x).1 = x.proj
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.const_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl ((fun x => c) + f) s
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_cons : ∀ {m n : ℕ}, m < n → (m<...=n).toList = (m + 1) :: ((m + 1)<...=n).toList
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Init.Data.SInt.Bitwise
Int16.ofBitVec_and : ∀ (a b : BitVec 16), Int16.ofBitVec (a &&& b) = Int16.ofBitVec a &&& Int16.ofBitVec b
-- Mathlib.Data.Fin.SuccPred
/-- Given a fixed pivot `p : Fin (n + 1)`, `p.succAbove` is injective.  -/
Fin.succAbove_right_inj : ∀ {n : ℕ} {p : Fin (n + 1)} {i j : Fin n}, p.succAbove i = p.succAbove j ↔ i = j
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n'), CochainComplex.HomComplex.Cochain.leftShift 0 a n' hn' = 0
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (-f) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The composition of two linear changes of variables given by matrix multiplication.  -/
WeierstrassCurve.VariableChange.mul_def : ∀ {R : Type u} [inst : CommRing R] (C C' : WeierstrassCurve.VariableChange R),
  C * C' =
    { u := C.u * C'.u, r := C.r * ↑C'.u ^ 2 + C'.r, s := ↑C'.u * C.s + C'.s,
      t := C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t }
-- Mathlib.Data.Ordmap.Invariants
Ordnode.any_iff_exists : ∀ {α : Type u_1} {P : α → Prop} {t : Ordnode α}, Ordnode.Any P t ↔ ∃ x, Ordnode.Emem x t ∧ P x
-- Mathlib.Topology.WithTopology
WithTopology.instLT : {X : Type u_1} → (t : TopologicalSpace X) → [LT X] → LT (WithTopology X t)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec.eq_1 : ∀ {β : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (f : β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × β)) (b : β),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec f b =
    Stream'.Seq.corec
      (fun a =>
        Option.map
          (fun x =>
            match x with
            | (exp, coef, next) => ((exp, coef), next))
          (f a))
      b
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.span_invSubmonoid : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], Submodule.span R ↑(IsLocalization.invSubmonoid M S) = ⊤
-- Mathlib.Order.Heyting.Basic
PUnit.top_eq : ⊤ = PUnit.unit
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.conjugator.singleton : ∀ {α : Type u} [inst : DecidableEq α] {a : α × Bool}, FreeGroup.reduceCyclically.conjugator [a] = []
-- Mathlib.Algebra.Order.Module.Rat
LinearOrderedField.toPosSMulStrictMono_rat : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α], PosSMulStrictMono ℚ α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, a ∈ m.insert k ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.reindex_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (e : ι ≃ E.I₀), (E.reindex e).I₀ = ι
-- Mathlib.Topology.Algebra.MulAction
/-- If an additive action is central, then its right action is continuous when its
left action is.  -/
ContinuousVAdd.op : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X] [inst_4 : VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X], ContinuousVAdd Mᵃᵒᵖ X
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.isConstant_of_isIso_counit_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (F : CategoryTheory.Sheaf J D) [inst_3 : CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D CategoryTheory.Limits.terminalIsTerminal).counit.app F)],
  CategoryTheory.Sheaf.IsConstant J F
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point lies in the Monge planes.  -/
Affine.Simplex.mongePoint_mem_mongePlane : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)},
  s.mongePoint ∈ s.mongePlane i₁ i₂
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.trans_le : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
  {c : ℝ} {f : α → E} {g : α → F} {k : α → G} {l : Filter α},
  Asymptotics.IsBigOWith c l f g → (∀ (x : α), ‖g x‖ ≤ ‖k x‖) → 0 ≤ c → Asymptotics.IsBigOWith c l f k
-- Lean.Elab.Tactic.Simp
/-- If `zetaDelta := false`, create a `FVarId` set with all local let declarations in the `simp` argument list.  -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabSimpArgs.toZetaDeltaSet : Lean.Syntax → Lean.Meta.Simp.Context → Lean.Elab.Tactic.TacticM Lean.FVarIdSet
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (fallback fallback_1 : β),
          fallback = fallback_1 →
            Std.ExtDHashMap.Const.getD m a fallback = Std.ExtDHashMap.Const.getD m_1 a_1 fallback_1
-- Mathlib.Order.Defs.Unbundled
IsEquiv.toSymm : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsEquiv α r], Std.Symm r
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Given a family of topological spaces `X i`, we say that a topological space is
`X`-generated (`IsGeneratedBy X Y`) when the topology on `Y` is the `X`-generated
topology, i.e. when the identity is a homeomorphism
`WithGeneratedByTopology X Y ≃ₜ Y` (see `IsGeneratedBy.homeomorph`).  -/
Topology.IsGeneratedBy : {ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → (Y : Type v) → [tY : TopologicalSpace Y] → Prop
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- **Slutsky's theorem** for a continuous function: if `X n` converges in distribution to `Z`,
`Y n` converges in probability to a constant `c`, and `g` is a continuous function, then
`g (X n, Y n)` converges in distribution to `g (Z, c)`.  -/
MeasureTheory.TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'}
  {μ' : MeasureTheory.Measure Ω'} [inst : MeasureTheory.IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''}
  {μ'' : MeasureTheory.Measure Ω''} [inst_1 : MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E}
  {Z : Ω' → E} {l : Filter ι} [inst_2 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_4 : BorelSpace E]
  {E' : Type u_6} {F : Type u_7} {mE' : MeasurableSpace E'} [inst_5 : SeminormedAddCommGroup E']
  [SecondCountableTopology E'] [BorelSpace E'] [inst_8 : TopologicalSpace F] [inst_9 : MeasurableSpace F]
  [inst_10 : BorelSpace F] {g : E × E' → F},
  Continuous g →
    ∀ [l.IsCountablyGenerated] {X : ι → Ω'' → E} {Y : ι → Ω'' → E'} {c : E'},
      MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ' →
        (MeasureTheory.TendstoInMeasure μ'' Y l fun x => c) →
          (∀ (i : ι), AEMeasurable (Y i) μ'') →
            MeasureTheory.TendstoInDistribution (fun n ω => g (X n ω, Y n ω)) l (fun ω => g (Z ω, c)) (fun x => μ'') μ'
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_zero : ∀ {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X] [inst_1 : Zero Y]
  [inst_2 : SMulZeroClass N Y], ⇑0 = 0
-- Mathlib.Order.Preorder.Chain
IsChain.image_embedding : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β],
  IsChain (fun x1 x2 => x1 ≤ x2) s → ∀ (φ : α ↪o β), IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_zero_of_not_linearIndependent_cols : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] [IsDomain R]
  {A : Matrix m m R}, (¬LinearIndependent R fun i => A.transpose i) → A.det = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_k.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon_k k m p =
    Bool.rec
      (Bool.rec
        (Lean.Grind.CommRing.Poly.rec
          (fun k' =>
            Bool.rec (Lean.Grind.CommRing.Poly.add (k.mul k') m (Lean.Grind.CommRing.Poly.num 0))
              (Lean.Grind.CommRing.Poly.num 0) (k'.beq' 0))
          (fun k' m' x ih => Lean.Grind.CommRing.Poly.add (k.mul k') (m.mul_k m') ih) p)
        (Lean.Grind.CommRing.Poly.mulConst_k k p) (m.beq' Lean.Grind.CommRing.Mon.unit))
      (Lean.Grind.CommRing.Poly.num 0) (k.beq' 0)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isSuccLimit_of_isPrincipal_mul`. -/
Ordinal.isSuccLimit_of_principal_mul : ∀ {o : Ordinal.{u}}, 2 < o → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o → Order.IsSuccLimit o
-- Init.Data.Option.Basic
Option.instBEq : {α : Type u_1} → [BEq α] → BEq (Option α)
-- Mathlib.Order.RelSeries
/-- Let `r` be a relation on `α`, a relation series of `r` of length `n` is a series
`a_0, a_1, ..., a_n` such that `r a_i a_{i+1}` for all `i < n`
 -/
RelSeries : {α : Type u_1} → SetRel α α → Type u_1
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂ : CategoryTheory.Nerve.nerveFunctor₂.Full
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Category structure on the oplax natural transformations between OplaxFunctors.

Note that this a scoped instance in the `Oplax.OplaxTrans` namespace.  -/
CategoryTheory.Oplax.OplaxTrans.homCategory : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.kernel.condition_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier (CategoryTheory.Limits.kernel f)),
  (CategoryTheory.ConcreteCategory.hom f) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) x) =
    (CategoryTheory.ConcreteCategory.hom 0) x
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.OfSurjective.dpow_def : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  {f : A →+* B} {J : Ideal B} (hf : Function.Surjective ⇑f) (hIJ : J = Ideal.map f I)
  (hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)) {n : ℕ} {x : B},
  (DividedPowers.Quotient.OfSurjective.dividedPowers hI hf hIJ hIf).dpow n x =
    DividedPowers.Quotient.OfSurjective.dpow hI f n x
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_3 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.read q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_3 q