mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `differentiable_finCons` where the derivative variables are free on the RHS
instead.  -/
differentiable_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  (Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The bit that we take out of the BitVec variable by getLsb.
 -/
Std.Tactic.BVDecide.BVBit.idx : (self : Std.Tactic.BVDecide.BVBit) → Fin self.w
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.fromAddMonoid_of : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ] (i : ι) (f : γ →+ β i),
  DirectSum.fromAddMonoid ((DirectSum.of (fun i => γ →+ β i) i) f) = (DirectSum.of β i).comp f
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.instNontrivial : ∀ {n : ℕ}, Nontrivial (QuaternionGroup n)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Icc₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] (a b : G₀) {c : G₀},
  0 < c → (fun x => c * x) ⁻¹' Set.Icc a b = Set.Icc (a / c) (b / c)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.eq_toIterM_iter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (it : Std.Iter ((a : α) × β a)),
  it.toIterM = { internalState := it.internalState }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_zero_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom f
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.findMin.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α → Sort u_2) (r : ℕ)
  (a : α) (c : Batteries.BinomialHeap.Imp.HeapNode α) (s : Batteries.BinomialHeap.Imp.Heap α)
  (res : Batteries.BinomialHeap.Imp.FindMin α)
  (h_1 : (res : Batteries.BinomialHeap.Imp.FindMin α) → motive Batteries.BinomialHeap.Imp.Heap.nil res)
  (h_2 :
    (r : ℕ) →
      (a : α) →
        (c : Batteries.BinomialHeap.Imp.HeapNode α) →
          (s : Batteries.BinomialHeap.Imp.Heap α) →
            (res : Batteries.BinomialHeap.Imp.FindMin α) → motive (Batteries.BinomialHeap.Imp.Heap.cons r a c s) res),
  (match Batteries.BinomialHeap.Imp.Heap.cons r a c s, res with
    | Batteries.BinomialHeap.Imp.Heap.nil, res => h_1 res
    | Batteries.BinomialHeap.Imp.Heap.cons r a c s, res => h_2 r a c s res) =
    h_2 r a c s res
-- Mathlib.Order.CompleteBooleanAlgebra
iSup₂_disjoint_iff : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Frame α] {a : α} {f : (i : ι) → κ i → α},
  Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isBigO_re_sub_re : ∀ {z : ℂ}, (fun w => w.re - z.re) =O[nhds z] fun w => w - z
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceTo_lt_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  String.Slice.Pos.ofSliceTo p < q ↔ ∀ (h : q ≤ p₀), p < p₀.sliceTo q h
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.zero_eq_map_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [inst : Zero β], 0 = WithBot.map f v ↔ ∃ x, v = ↑x ∧ f x = 0
-- Init.Prelude
/-- Multiplication of natural numbers, usually accessed via the `*` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
 -/
Nat.mul : ℕ → ℕ → ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonWorkspaceSymbolParams.toJson : Lean.Lsp.WorkspaceSymbolParams → Lean.Json
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.sum_range_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [ContinuousAdd M] {f : ℕ → M} {k : ℕ},
  HasSum (fun n => f (n + k)) m → HasSum f (∑ i ∈ Finset.range k, f i + m)
-- Mathlib.Data.ZMod.Basic
ZMod.mul_val_inv : ∀ {m n : ℕ}, m.Coprime n → ↑m * ↑(↑m)⁻¹.val = 1
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulReflectLE_iff_mulPosReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α],
  PosMulReflectLE α ↔ MulPosReflectLE α
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The inclusion `X ⊗ T ⟶ S.unionProd T` as simplicial sets.  -/
SSet.Subcomplex.unionProd.ι₁ : {X Y : SSet} →
  (S : X.Subcomplex) →
    (T : Y.Subcomplex) → CategoryTheory.MonoidalCategoryStruct.tensorObj X T.toSSet ⟶ (S.unionProd T).toSSet
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_def : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α}, -s = Finset.image (fun x => -x) s
-- Mathlib.Algebra.Torsor.Defs
/-- Dividing by the result of multiplying with a group element produces the same result
as dividing the points and dividing by that group element.  -/
sdiv_smul_eq_sdiv_div : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ p₂ : P) (g : G), p₁ /ₛ g • p₂ = (p₁ /ₛ p₂) / g
-- Lean.Meta.Sym.ProofInstInfo
/-- Returns information about the type signature of `declName`. It contains information about which arguments
are proofs or instances. Returns `none` if no arguments are proofs or instances.
 -/
Lean.Meta.Sym.getProofInstInfo? : Lean.Name → Lean.Meta.Sym.SymM (Option Lean.Meta.Sym.ProofInstInfo)
-- Mathlib.Topology.List
List.continuousAt_length : ∀ {α : Type u_1} [inst : TopologicalSpace α] (l : List α), ContinuousAt List.length l
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- A continuous function on a compact space automatically has compact support.  -/
CompactlySupportedContinuousMap.continuousMapEquiv : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] → [CompactSpace α] → C(α, β) ≃ CompactlySupportedContinuousMap α β
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Context.mk.inj : ∀ {cfg : Mathlib.Tactic.DepRewrite.Config} {p x h : Lean.Expr} {Δ : Array (Lean.FVarId × Lean.Expr)}
  {δ : Std.HashSet Lean.FVarId} {pHeadIdx : Lean.HeadIndex} {pNumArgs : ℕ} {cfg_1 : Mathlib.Tactic.DepRewrite.Config}
  {p_1 x_1 h_1 : Lean.Expr} {Δ_1 : Array (Lean.FVarId × Lean.Expr)} {δ_1 : Std.HashSet Lean.FVarId}
  {pHeadIdx_1 : Lean.HeadIndex} {pNumArgs_1 : ℕ},
  { cfg := cfg, p := p, x := x, h := h, Δ := Δ, δ := δ, pHeadIdx := pHeadIdx, pNumArgs := pNumArgs } =
      { cfg := cfg_1, p := p_1, x := x_1, h := h_1, Δ := Δ_1, δ := δ_1, pHeadIdx := pHeadIdx_1,
        pNumArgs := pNumArgs_1 } →
    cfg = cfg_1 ∧ p = p_1 ∧ x = x_1 ∧ h = h_1 ∧ Δ = Δ_1 ∧ δ = δ_1 ∧ pHeadIdx = pHeadIdx_1 ∧ pNumArgs = pNumArgs_1
-- Mathlib.Topology.Constructible
IsRetrocompact.singleton : ∀ {X : Type u_2} [inst : TopologicalSpace X] {a : X}, IsRetrocompact {a}
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.zero : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x : M}, x ≡ 0 [SMOD U] ↔ x ∈ U
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.tensorObj.instTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {M N : C} →
          [CategoryTheory.AddMonObj M] →
            [CategoryTheory.AddMonObj N] →
              CategoryTheory.AddMonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
-- 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 (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) 2 μ →
    MeasureTheory.MemLp (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) 2 ν →
      ProbabilityTheory.variance (⇑L) (μ.prod ν) =
        ProbabilityTheory.variance (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ +
          ProbabilityTheory.variance (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRciSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRciSlice._auto_1) →
    Std.Rci.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RciSlice α)
-- Mathlib.Order.Cover
Set.covBy_iff_exists_insert : ∀ {α : Type u_1} {s t : Set α}, s ⋖ t ↔ ∃ a ∉ s, insert a s = t
-- Init.Data.List.Lemmas
List.head_append_of_ne_nil : ∀ {α : Type u_1} {l' l : List α} {w₁ : l ++ l' ≠ []} (w₂ : l ≠ []), (l ++ l').head w₁ = l.head w₂
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instNormedCommGroup : {E : Type u_2} → [inst : SeminormedCommGroup E] → NormedCommGroup (SeparationQuotient E)
-- Mathlib.Data.W.Constructions
WType.Natα.succ.sizeOf_spec : sizeOf WType.Natα.succ = 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
mem_unitary_of_spectrum_subset_unitary : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [ContinuousFunctionalCalculus ℂ A IsStarNormal] {u : A} [IsStarNormal u], spectrum ℂ u ⊆ ↑(unitary ℂ) → u ∈ unitary A
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algHom_ext'_iff : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] {f g : TrivSqZeroExt R M →ₐ[S] A},
  f = g ↔
    f.comp (TrivSqZeroExt.inlAlgHom S R M) = g.comp (TrivSqZeroExt.inlAlgHom S R M) ∧
      f.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M) = g.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ GrpCat MonCat)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_iSup_of_directed : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_1} [Nonempty ι] {S : ι → NonUnitalSubring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app._auto_1)
  {Z : Cᵒᵖ}
  (h :
    (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj X) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).hom.app (Opposite.unop X)).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app
          (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X))))
        h)
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_var_cert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (x y : Int.Internal.Linear.Var),
  Int.Internal.Linear.norm_eq_var_cert lhs rhs x y =
    (lhs.sub rhs).norm.beq'
      (Int.Internal.Linear.Poly.add 1 x (Int.Internal.Linear.Poly.add (-1) y (Int.Internal.Linear.Poly.num 0)))
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.subsingleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}, Subsingleton (CategoryTheory.Limits.IsLimit t)
-- Mathlib.Topology.Algebra.ClopenNhdofOne
ProfiniteGrp.exist_openNormalAddSubgroup_sub_open_nhds_of_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] {U : Set G}, IsOpen U → 0 ∈ U → ∃ H, ↑H ⊆ U
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.BlockMem.coe_top : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a : X), ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasDetector.hasCodetector_of_hasDetector_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasDetector Cᵒᵖ],
  CategoryTheory.HasCodetector C
-- Init.Data.List.Lemmas
List.filterMap_replicate : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {a : α} {f : α → Option β},
  List.filterMap f (List.replicate n a) =
    match f a with
    | none => []
    | some b => List.replicate n b
-- Init.SizeOf
Lean.Macro.Methods.mk.sizeOf_spec : ∀ (expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)) (getCurrNamespace : Lean.MacroM Lean.Name)
  (hasDecl : Lean.Name → Lean.MacroM Bool) (resolveNamespace : Lean.Name → Lean.MacroM (List Lean.Name))
  (resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))),
  sizeOf
      { expandMacro? := expandMacro?, getCurrNamespace := getCurrNamespace, hasDecl := hasDecl,
        resolveNamespace := resolveNamespace, resolveGlobalName := resolveGlobalName } =
    1
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_30 : HAdd Std.Time.Day.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.drain_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m],
  (Std.IterM.empty m β).drain = pure PUnit.unit
-- Mathlib.Condensed.Discrete.Colimit
Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : Profinite) [Finite ↑X.toTop], CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ↑X.toTop) F
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableVAdd₂ M X] {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f +ᵥ g) μ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred.eq_def : ∀ {α : Type u_1} (p : α → Bool) (x : List α),
  Turing.PartrecToTM2.splitAtPred p x =
    match x with
    | [] => ([], none, [])
    | a :: as =>
      bif p a then ([], some a, as)
      else
        match Turing.PartrecToTM2.splitAtPred p as with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)
-- Mathlib.Analysis.InnerProductSpace.Defs
PreInnerProductSpace.Core.mk.injEq : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (toInner : Inner 𝕜 F)
  (conj_inner_symm : ∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y)
  (re_inner_nonneg : ∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x))
  (add_left : ∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z)
  (smul_left : ∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y) (toInner_1 : Inner 𝕜 F)
  (conj_inner_symm_1 : ∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y)
  (re_inner_nonneg_1 : ∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x))
  (add_left_1 : ∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z)
  (smul_left_1 : ∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y),
  ({ toInner := toInner, conj_inner_symm := conj_inner_symm, re_inner_nonneg := re_inner_nonneg, add_left := add_left,
        smul_left := smul_left } =
      { toInner := toInner_1, conj_inner_symm := conj_inner_symm_1, re_inner_nonneg := re_inner_nonneg_1,
        add_left := add_left_1, smul_left := smul_left_1 }) =
    (toInner = toInner_1)
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkAtomCached.match_1.eq_2 : ∀ {α : Type} (decls : Array (Std.Sat.AIG.Decl α)) (decl : Std.Sat.AIG.Decl α)
  (motive : Option (Std.Sat.AIG.CacheHit decls decl) → Sort u_1)
  (h_1 : (hit : Std.Sat.AIG.CacheHit decls decl) → motive (some hit)) (h_2 : Unit → motive none),
  (match none with
    | some hit => h_1 hit
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- If there is an absolute upper bound on the size of an independent set, then matroids
can be defined using an 'augmentation' axiom similar to the standard definition of
finite matroids for independent sets.  -/
IndepMatroid.ofBddAugment : {α : Type u_1} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
            (∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) → (∀ (I : Set α), Indep I → I ⊆ E) → IndepMatroid α
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Productive.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM m β → Std.IterM.TerminationMeasures.Productive α m
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.le_re_herglotzRieszKernel_aux : ∀ (θ φ r R : ℝ),
  0 < r →
    r < R →
      (R - r) / (R + r) ≤
        ((↑R * Complex.exp (↑θ * Complex.I) + ↑r * Complex.exp (↑φ * Complex.I)) /
            (↑R * Complex.exp (↑θ * Complex.I) - ↑r * Complex.exp (↑φ * Complex.I))).re
-- Init.Internal.Order.Basic
Lean.Order.CompleteLattice.mk : {α : Sort u} →
  [toPartialOrder : Lean.Order.PartialOrder α] →
    (∀ (c : α → Prop), Exists (Lean.Order.is_sup c)) → Lean.Order.CompleteLattice α
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nat_nhds_top : Filter.Tendsto (fun n => ↑n) Filter.atTop (nhds ⊤)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldr_eq_foldr_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → δ → δ} {init : δ},
  Std.ExtDTreeMap.foldr f init t = List.foldr (fun a b => f a.fst a.snd b) init t.toList
-- Mathlib.Topology.Order.OrderClosed
instOrderClosedTopologyForall : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → TopologicalSpace (α i)]
  [∀ (i : ι), OrderClosedTopology (α i)], OrderClosedTopology ((i : ι) → α i)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.nnnorm_smul_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)), ‖c • f‖₊ = ‖f‖₊
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.map_ι_comp_inv_sigmaComparison_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)] (j : J) {Z : D}
  (h : (∐ fun b => G.obj (f b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.ι f j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.sigmaComparison G f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => G.obj (f x)) j) h
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.IsCardinalAccessible.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {κ : Cardinal.{w}} [inst_2 : Fact κ.IsRegular],
  autoParam
      (∀ (J : Type w) [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ],
        CategoryTheory.Limits.PreservesColimitsOfShape J F)
      CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShape._autoParam →
    F.IsCardinalAccessible κ
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
qrSign.eq_1 : ∀ (m n : ℕ), qrSign m n = jacobiSym (ZMod.χ₄ ↑m) n
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (A : Type u) →
                                    [inst_9 : TopologicalSpace A] →
                                      [inst_10 : ChartedSpace H A] →
                                        [inst_11 : AddCommGroup A] →
                                          [LieAddGroup I (↑⊤) A] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              AddCommGroup ((smoothSheaf IM I M A).presheaf.obj U)
-- Init.Data.String.Termination
String.Slice.Pos.eq_prev_of_prev?_eq_some : ∀ {s : String.Slice} {p q : s.Pos} (h : p.prev? = some q), q = p.prev ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G), ↑K.toAddSubmonoid = ↑K
-- Mathlib.Analysis.Calculus.DiffContOnCl
diffContOnCl_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  DiffContOnCl 𝕜 f Set.univ ↔ Differentiable 𝕜 f
-- Mathlib.Algebra.Group.Defs
LeftCancelSemigroup.toSemigroup : {G : Type u} → [self : LeftCancelSemigroup G] → Semigroup G
-- Std.Http.Data.URI.Encoding
List.toByteArray.loop.eq_1 : ∀ (x : ByteArray), List.toByteArray.loop [] x = x
-- Lean.Elab.PreDefinition.WF.PackMutual
Lean.Elab.WF.preDefsFromUnaryNonRec : Lean.Elab.FixedParamPerms →
  Lean.Meta.ArgsPacker →
    Array Lean.Elab.PreDefinition → Lean.Elab.PreDefinition → Lean.MetaM (Array Lean.Elab.PreDefinition)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_equiv_eq_comap_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N) (K : AddSubsemigroup M),
  AddSubsemigroup.map (↑f) K = AddSubsemigroup.comap (↑f.symm) K