mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying lean expression of a 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.e : Mathlib.Tactic.BicategoryLike.Mor₁ → Lean.Expr
-- Mathlib.Topology.Instances.Real.Lemmas
Real.uniformContinuous_inv : ∀ (s : Set ℝ) {r : ℝ}, 0 < r → (∀ x ∈ s, r ≤ |x|) → UniformContinuous fun p => (↑p)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Our normalization procedure works by first defining a functor `F C ⥤ (N C ⥤ N C)` (which turns
out to be very easy), and then obtain a functor `F C ⥤ N C` by plugging in the normal object
`𝟙_ C`.  -/
CategoryTheory.FreeMonoidalCategory.normalize : (C : Type u) →
  CategoryTheory.Functor (CategoryTheory.FreeMonoidalCategory C)
    (CategoryTheory.Functor ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
      ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C))
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.isTheorem : Array Lean.Elab.DefView → Bool
-- Mathlib.RepresentationTheory.Intertwining
/-- Composition of two `Equiv`.  -/
Representation.Equiv.trans : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : Semiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          {ρ : Representation A G V} →
                            {σ : Representation A G W} → {τ : Representation A G U} → ρ.Equiv σ → σ.Equiv τ → ρ.Equiv τ
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.lpo : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask.mk.inj : ∀ {task : Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json))} {cancel : IO Unit}
  {task_1 : Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json))} {cancel_1 : IO Unit},
  { task := task, cancel := cancel } = { task := task_1, cancel := cancel_1 } → task = task_1 ∧ cancel = cancel_1
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.instFinCategoryOfFintypeOfDecidableEq : {ι : Type v} → [Fintype ι] → [DecidableEq ι] → CategoryTheory.FinCategory (CategoryTheory.Pairwise ι)
-- Mathlib.Analysis.Convex.Topology
Real.convex_iff_isPreconnected : ∀ {s : Set ℝ}, Convex ℝ s ↔ IsPreconnected s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic.0.Real.sqrtTwoAddSeries.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- A cocone on `F` with cocone point `X` is the same as an element of `lim Hom(F·, X)`,
naturally in `X`.  -/
CategoryTheory.Limits.yonedaCompLimIsoCocones : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.yoneda.comp
              (((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim) ≅
            F.cocones
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindMap'.eq_1 : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {A B : Rep.{max u w, u, v} k G} (f : A ⟶ B),
  Rep.coindMap' φ f =
    Rep.ofHom
      (let __spread.0 := CategoryTheory.Linear.rightComp k (Rep.res φ (Rep.leftRegular k H)) f;
      { toLinearMap := __spread.0, isIntertwining' := ⋯ })
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.ae_mem_finset_iff : ∀ {α : Type u_4} {mα : MeasurableSpace α} [MeasurableSingletonClass α] {μ : MeasureTheory.Measure α} {s : Finset α},
  (∀ᵐ (a : α) ∂μ, a ∈ s) ↔ μ = ∑ a ∈ s, μ {a} • MeasureTheory.Measure.dirac a
-- Mathlib.Logic.Function.Basic
instDecidableUncurryOfFstSnd_mathlib : {α : Type u_3} →
  {β : Type u_4} → {r : α → β → Prop} → {x : α × β} → [Decidable (r x.1 x.2)] → Decidable (Function.uncurry r x)
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurveAt_comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ dt : ℝ},
  IsMIntegralCurveAt (γ ∘ fun x => x - dt) v (t₀ + dt) ↔ IsMIntegralCurveAt γ v t₀
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} {hc : k' ∈ t.alter k f},
  (t.alter k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ⋯ ((f (t.get? k)).get ⋯) else t.get k' ⋯
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Universal property of Hausdorffification: any linear map to a Hausdorff module extends to a
unique map from the Hausdorffification.  -/
Hausdorffification.lift : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_5} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → [h : IsHausdorff I N] → (M →ₗ[R] N) → Hausdorffification I M →ₗ[R] N
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instAddCommMonoid : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → AddCommMonoid (FreeAlgebra R X)
-- Mathlib.Data.Finset.Powerset
Finset.powerset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α),
  (insert a s).powerset = s.powerset ∪ Finset.image (insert a) s.powerset
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {iter : Std.DTreeMap.Internal.Zipper α β} {upper : α}
  {iter_1 : Std.DTreeMap.Internal.Zipper α β} {upper_1 : α},
  { iter := iter, upper := upper } = { iter := iter_1, upper := upper_1 } → iter = iter_1 ∧ upper = upper_1
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toSeminormedAddCommGroup.eq_1 : ∀ {E : Type u_5} [inst : NormedAddCommGroup E],
  NormedAddCommGroup.toSeminormedAddCommGroup =
    { toNorm := inst.toNorm, toAddCommGroup := inst.toAddCommGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.Algebra.Lie.Basic
LieHom.comp_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L₃]
  [inst_6 : LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁), (f.comp g) x = f (g x)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_rco_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m...n).toList.getD i fallback = fallback
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.comp_id : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  (f : X →ₑ[φ] Y), f.comp (AddActionHom.id M) = f
-- Std.Do.SPred.SPred
Std.Do.SPred.exists_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {α : Sort u_1} {P : α → Std.Do.SPred (σ :: σs)},
  Std.Do.SPred.exists P s = spred(∃ a, P a s)
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.inter : ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
  IsLowerSet D → DirSupInaccOn D s → DirSupInaccOn D t → DirSupInaccOn D (s ∩ t)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_rotateL : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} {rk : α} {rv : β rk}
  {rl rr : Std.DTreeMap.Internal.Impl α β},
  rl.Balanced →
    (Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr).size =
      (Std.DTreeMap.Internal.Impl.bin k v l (Std.DTreeMap.Internal.Impl.bin rk rv rl rr)).size
-- Mathlib.Order.Partition.Finpartition
/-- Changes the type of a finpartition to an equal one.  -/
Finpartition.copy : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → {a b : α} → Finpartition a → a = b → Finpartition b
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go.match_1.eq_2 : ∀ {β : Type u_2} {α : Type u_1} (motive : List α → β → List β → Sort u_3) (x : α) (xs : List α) (last : β)
  (acc : List β) (h_1 : (last : β) → (acc : List β) → motive [] last acc)
  (h_2 : (x : α) → (xs : List α) → (last : β) → (acc : List β) → motive (x :: xs) last acc),
  (match x :: xs, last, acc with
    | [], last, acc => h_1 last acc
    | x :: xs, last, acc => h_2 x xs last acc) =
    h_2 x xs last acc
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toList_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.reverse.toList = t.toList.reverse
-- Mathlib.Data.Num.Prime
/-- Returns the smallest prime factor of `n ≠ 1`.  -/
Num.minFac : Num → PosNum
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle_intCast : ∀ {N : ℕ} [inst : NeZero N] (j : ℤ), ZMod.toAddCircle ↑j = ↑(↑j / ↑N)
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- The continued fraction `GenContFract.of v` terminates if and only if `v ∈ ℚ`.  -/
GenContFract.terminates_iff_rat : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] (v : K),
  (GenContFract.of v).Terminates ↔ ∃ q, v = ↑q
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.alter m k f) k' =
    if (k == k') = true then f (Std.DHashMap.Const.get? m k) else Std.DHashMap.Const.get? m k'
-- Mathlib.Tactic.Simproc.Factors
/-- Given a natural number `n`, returns `(l, ⊢ Nat.primeFactorsList n = l)`.  -/
Mathlib.Meta.Simproc.evalPrimeFactorsList : {en enl : Q(ℕ)} →
  Q(Mathlib.Meta.NormNum.IsNat «$en» «$enl») → Lean.MetaM ((l : Q(List ℕ)) × Q(«$en».primeFactorsList = «$l»))
-- Batteries.Data.Float.Lemmas
Float.Model.Format.mantissaBits.eq_1 : ∀ (spec : Float.Model.Format), spec.mantissaBits = 1 + spec.mantissaBitsWithoutImplicit
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_ciSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ (x : α), BddAbove (Set.range fun i => f i x)) →
    (∀ (i : ι), LowerSemicontinuous (f i)) → LowerSemicontinuous fun x' => ⨆ i, f i x'
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_one : ∀ {p : ℝ}, ENNReal.ofReal p < 1 ↔ p < 1
-- Batteries.Data.Fin.Lemmas
Fin.findRev?_eq_some_iff : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, Fin.findRev? p = some i ↔ p i = true ∧ ∀ (j : Fin n), i < j → p j = false
-- Mathlib.Order.Filter.Pointwise
Filter.instZSMul.eq_1 : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : Add α] [inst_2 : Neg α],
  Filter.instZSMul = { smul := fun n s => zsmulRec nsmulRec n s }
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_biUnion_left : ∀ {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq α] (s : Finset ι)
  (t : Finset α) (f : ι → Finset α), G.interedges (s.biUnion f) t = s.biUnion fun a => G.interedges (f a) t
-- Mathlib.Algebra.Lie.Subalgebra
/-- Given two nested Lie subalgebras `K ⊆ K'`, the inclusion `K ↪ K'` is a morphism of Lie
algebras.  -/
LieSubalgebra.inclusion : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → {K K' : LieSubalgebra R L} → K ≤ K' → ↥K →ₗ⁅R⁆ ↥K'
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value is positive definitive  -/
AbsoluteValue.eq_zero' : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (self : AbsoluteValue R S) (x : R), self.toFun x = 0 ↔ x = 0
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- **Alias** of `AntilipschitzWith.domRestrict`. -/
AntilipschitzWith.restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (s : Set α), AntilipschitzWith K (s.domRestrict f)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_map : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {f : K →+* L} {s : Subfield K} {y : L},
  y ∈ Subfield.map f s ↔ ∃ x ∈ s, f x = y
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ F).app X =
    F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α} [inst_4 : Inhabited β],
  (List.map Prod.fst l).contains k = false → Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.ofList l) k = default
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot : ∀ {R : Type u} [inst : CommRing R], PrimeSpectrum.isIdempotentElemEquivClopens.symm ⊥ = ⟨0, ⋯⟩
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.add_leftNegEquiv_symm : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S),
  ↑x + ↑((S.leftNegEquiv hS).symm x) = 0
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natCast : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n m : ℕ),
  Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [inst_1 : K.HasPullbacks] [P.IsStableUnderBaseChange],
  (∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y),
      (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) →
    P.IsLocalAtTarget K
-- Mathlib.Order.OrderIsoNat
/-- The **monotone chain condition**: a preorder is co-well-founded iff every increasing sequence
contains two non-increasing indices.

See `wellFoundedGT_iff_monotone_chain_condition` for a stronger version on partial orders.  -/
wellFoundedGT_iff_monotone_chain_condition' : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_zsmul_le : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (z : ℤ), ‖z • x‖ ≤ ‖x‖
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_def : ∀ (x : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ x =
    match x with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => insert Q (Finset.univ.biUnion fun s => Turing.PartrecToTM2.trStmts₁ (q s))
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:q.copy => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:q.succ => insert Q (insert (Turing.PartrecToTM2.unrev q) (Turing.PartrecToTM2.trStmts₁ q))
    | Q@h:(q₁.pred q₂) =>
      insert Q
        (Turing.PartrecToTM2.trStmts₁ q₁ ∪ insert (Turing.PartrecToTM2.unrev q₂) (Turing.PartrecToTM2.trStmts₁ q₂))
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => {Q}
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (x y : E),
      ((ProbabilityTheory.covarianceBilin μ) x) y =
        ∫ (z : E), inner ℝ x (z - ∫ (x : E), id x ∂μ) * inner ℝ y (z - ∫ (x : E), id x ∂μ) ∂μ
-- Mathlib.Topology.Inseparable
SeparationQuotient.mk_eq_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X},
  SeparationQuotient.mk x = SeparationQuotient.mk y ↔ Inseparable x y
-- Init.Data.Option.Lemmas
Option.filter_some_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α}, p a = true → Option.filter p (some a) = some a
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.not_boundaryGE_next : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  {j k : ι}, c.Rel j k → ¬e.BoundaryGE k
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- The dual cone of a set `s` is the cone consisting of all points `y` such that for all points
`x ∈ s` we have `0 ≤ ⟪x, y⟫`.  -/
ProperCone.innerDual : {E : Type u_2} →
  [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → [CompleteSpace E] → Set E → ProperCone ℝ E
-- Mathlib.Order.IsNormal
InitialSeg.isNormal : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : α ≤i β), Order.IsNormal ⇑f
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- `LeftPreLieRings` are examples of `LieAdmissibleRings` by the commutativity assumption on the
associator.  -/
LeftPreLieRing.instLieAdmissibleRing : {L : Type u_2} → [LeftPreLieRing L] → LieAdmissibleRing L
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMax!.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf) →
    (∀ (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')
          (Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (Std.DTreeMap.Internal.Impl.insertMax! k v r'))) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β), motive t (Std.DTreeMap.Internal.Impl.insertMax! k v t)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.vcomp_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C),
  (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_cexp_neg_sum_mul_add : ∀ {ι : Type u_2} [inst : Fintype ι] {b : ι → ℂ},
  (∀ (i : ι), 0 < (b i).re) →
    ∀ (c : ι → ℂ),
      ∫ (v : ι → ℝ), Complex.exp (-∑ i, b i * ↑(v i) ^ 2 + ∑ i, c i * ↑(v i)) =
        ∏ i, (↑Real.pi / b i) ^ (1 / 2) * Complex.exp (c i ^ 2 / (4 * b i))
-- Mathlib.Topology.Homotopy.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousMap.Homotopy.Simps.apply : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → f₀.Homotopy f₁ → ↑unitInterval × X → Y
-- Lean.Meta.Sym.InstantiateS
/-- Similar to `instantiateRevS`, but beta-reduces nested applications whose function becomes a lambda
after substitution.

For example, if `e` contains a subterm `#0 a` and we apply the substitution `#0 := fun x => x + 1`,
then `instantiateRevBetaS` produces `a + 1` instead of `(fun x => x + 1) a`.

This is useful when applying theorems. For example, when applying `Exists.intro`:
```
Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
```
to a goal of the form `∃ x : Nat, p x ∧ q x`, we create metavariables `?w` and `?h`.
With `instantiateRevBetaS`, the type of `?h` becomes `p ?w ∧ q ?w` instead of
`(fun x => p x ∧ q x) ?w`.
 -/
Lean.Meta.Sym.instantiateRevBetaS : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.reindex_smul : ∀ {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k]
  [inst_2 : Module k V] [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G k V] (a : G)
  (b : AffineBasis ι k V) (e : ι ≃ ι'), (a • b).reindex e = a • b.reindex e
-- Lean.Elab.Tactic.Location
Lean.Elab.Tactic.Location.targets.sizeOf_spec : ∀ (hypotheses : Array Lean.Syntax) (type : Bool),
  sizeOf (Lean.Elab.Tactic.Location.targets hypotheses type) = 1 + sizeOf hypotheses + sizeOf type
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_ordProj_of_dvd : ∀ {n p : ℕ}, n ≠ 0 → Nat.Prime p → p ∣ n → p ∣ p ^ n.factorization p
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_toSubfield : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ↑S.toSubfield = ↑S
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_compl₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.Integrable f μ → ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.false.injEq : ∀ (p p_1 : Lean.Expr), (Nat.EqResult.false✝ p = Nat.EqResult.false✝ p_1) = (p = p_1)
-- Mathlib.Analysis.Normed.Group.Bounded
IsCompact.exists_bound_of_continuousOn : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {s : Set α},
  IsCompact s → ∀ {f : α → E}, ContinuousOn f s → ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_eq_shiftLeft_mod : ∀ (a b : UInt32), a <<< b = a <<< (b % 32)
-- Lean.Expr
/-- `mkConst declName us` return `.const declName us`.  -/
Lean.mkConst : Lean.Name → optParam (List Lean.Level) [] → Lean.Expr
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- Every ring is Lie-admissible.
See note [reducible non-instances].  -/
Ring.instLieAdmissibleRing : {L : Type u_2} → [Ring L] → LieAdmissibleRing L
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.ofMul_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Additive.ofMul a ≤ Additive.ofMul b ↔ a ≤ b
-- Mathlib.CategoryTheory.Types.Set
Set.functorToTypes_map : ∀ {X : Type u} {S T : Set X} (f : S ⟶ T),
  Set.functorToTypes.map f =
    TypeCat.ofHom fun x =>
      match x with
      | ⟨x, hx⟩ => ⟨x, ⋯⟩
-- Mathlib.Algebra.Group.Hom.Defs
/-- The underlying function  -/
OneHom.toFun : {M : Type u_10} → {N : Type u_11} → [inst : One M] → [inst_1 : One N] → OneHom M N → M → N
-- Mathlib.Data.NNRat.Defs
NNRat.le_def : ∀ {p q : ℚ≥0}, p ≤ q ↔ p.num * q.den ≤ q.num * p.den