mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, t.contains a = false → t.get! a = default
-- Init.Data.String.Lemmas.Basic
String.Slice.slice_eq_self_iff : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, s.slice p₁ p₂ h = s ↔ p₁ = s.startPos ∧ p₂ = s.endPos
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_surjective : ∀ {α : Type u_1} [inst : DecidableEq α] [Nonempty α], Function.Surjective FreeAddGroup.norm
-- Mathlib.Order.SymmDiff
sdiff_symmDiff' : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), c \ symmDiff a b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_eq_closure_inter_affineSpan : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 s = closure s ∩ ↑(affineSpan 𝕜 s)
-- Mathlib.CategoryTheory.CatCommSq
/-- A variant of `vComp` where both squares can be explicitly provided.  -/
CategoryTheory.CatCommSq.vComp' : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₅ : Type u_5} →
          {C₆ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆] →
                        {L₁ : CategoryTheory.Functor C₁ C₂} →
                          {L₂ : CategoryTheory.Functor C₂ C₃} →
                            {H₁ : CategoryTheory.Functor C₁ C₄} →
                              {H₂ : CategoryTheory.Functor C₂ C₅} →
                                {H₃ : CategoryTheory.Functor C₃ C₆} →
                                  {R₁ : CategoryTheory.Functor C₄ C₅} →
                                    {R₂ : CategoryTheory.Functor C₅ C₆} →
                                      CategoryTheory.CatCommSq H₁ L₁ R₁ H₂ →
                                        CategoryTheory.CatCommSq H₂ L₂ R₂ H₃ →
                                          CategoryTheory.CatCommSq H₁ (L₁.comp L₂) (R₁.comp R₂) H₃
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- Up to a measurable equivalence, `projectiveFamily I` is the centered multivariate Gaussian
with covariance matrix `covMatrix I`.  -/
ProbabilityTheory.BrownianReal.measurePreserving_toLp_projectiveFamily : ∀ (I : Finset NNReal),
  MeasureTheory.MeasurePreserving (WithLp.toLp 2) (ProbabilityTheory.BrownianReal.projectiveFamily I)
    (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.minKey? = some (t.minKeyD fallback)
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_mul_unit_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z)
-- Mathlib.Algebra.Notation.Defs
div_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Div α] (a : α) (b : P → α) (c : ¬P → α),
  (a / if h : P then b h else c h) = if h : P then a / b h else a / c h
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.instLocallyFiniteSumSumOfDecidableEq : {V : Type u_3} →
  {W : Type u_5} →
    {G : SimpleGraph V} →
      {H : SimpleGraph W} →
        [DecidableEq V] → [DecidableEq W] → [G.LocallyFinite] → [H.LocallyFinite] → (G ⊕g H).LocallyFinite
-- Lean.DocString.Syntax
/-- A named reference to a URL defined elsewhere. Use parentheses to write the URL here.  -/
Lean.Doc.Syntax.ref : Lean.ParserDescr
-- Mathlib.NumberTheory.Dioph
Poly.proj_apply : ∀ {α : Type u_1} (i : α) (x : α → ℕ), (Poly.proj i) x = ↑(x i)
-- Lean.LocalContext
Lean.LocalContext.mk.injEq : ∀ (fvarIdToDecl : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl)
  (decls : Lean.PersistentArray (Option Lean.LocalDecl)) (auxDeclToFullName : Lean.FVarIdMap Lean.Name)
  (fvarIdToDecl_1 : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl)
  (decls_1 : Lean.PersistentArray (Option Lean.LocalDecl)) (auxDeclToFullName_1 : Lean.FVarIdMap Lean.Name),
  ({ fvarIdToDecl := fvarIdToDecl, decls := decls, auxDeclToFullName := auxDeclToFullName } =
      { fvarIdToDecl := fvarIdToDecl_1, decls := decls_1, auxDeclToFullName := auxDeclToFullName_1 }) =
    (fvarIdToDecl = fvarIdToDecl_1 ∧ decls = decls_1 ∧ auxDeclToFullName = auxDeclToFullName_1)
-- Mathlib.Data.Sigma.Basic
Sigma.instInhabitedSigma : {α : Type u_1} → {β : α → Type u_4} → [inst : Inhabited α] → [Inhabited (β default)] → Inhabited (Sigma β)
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` is connected, any functor `F : J ⥤ Discrete α` is isomorphic to
the constant functor with value `F.obj j` (for any choice of `j`).
 -/
CategoryTheory.isoConstant : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    [CategoryTheory.IsPreconnected J] →
      {α : Type u₂} →
        (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) →
          (j : J) → F ≅ (CategoryTheory.Functor.const J).obj (F.obj j)
-- Mathlib.Algebra.RingQuot
RingQuot.instAddCommMonoid : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → AddCommMonoid (RingQuot r)
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankLeOne.exists_val_lt : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_4} [inst_1 : DivisionRing K]
  (v : Valuation K Γ₀) [inst_2 : v.RankLeOne],
  Subsingleton (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ ∨
    ∀ {γ : NNReal}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (Valuation.RankLeOne.hom' v) (v.restrict x) < γ
-- Mathlib.LinearAlgebra.Complex.Module
StarModule.complexToReal : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Star E] [inst_2 : Module ℂ E] [StarModule ℂ E], StarModule ℝ E
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), (BoundedLatticeHom.id β).comp f = f
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAtFilter_sub_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter (fun x => f x - c) f' L ↔ HasDerivAtFilter f f' L
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_one_right : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime x 1
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (ℱ : TopCat.Presheaf C X) (x : ↑X), (TopCat.Presheaf.stalkFunctor C x).obj ℱ = ℱ.stalk x
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift_compr₂ : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] {f : M →ₗ[R] N →ₗ[R] P}
  (g : P →ₗ[R] Q), TensorProduct.lift (f.compr₂ g) = g ∘ₗ TensorProduct.lift f
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.inv_mem_Ico_iff : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a c d : α},
  a⁻¹ ∈ Set.Ico c d ↔ a ∈ Set.Ioc d⁻¹ c⁻¹
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.neg_pi_div_two_eq_arcsin : ∀ {x : ℝ}, -(Real.pi / 2) = Real.arcsin x ↔ x ≤ -1
-- Init.Data.Vector.Lemmas
Vector.findRev?_eq_find?_reverse : ∀ {α : Type} {n : ℕ} {f : α → Bool} {xs : Vector α n}, Vector.findRev? f xs = Vector.find? f xs.reverse
-- Mathlib.Algebra.Expr
/-- Produce a `Mul` instance for `Q($α)` such that `x * y : Q($α)` is `q($x * $y)`.  -/
Expr.instMul : {u : Lean.Level} → (α : Q(Type u)) → Q(Mul «$α») → Mul Q(«$α»)
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_toFormula_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n}, T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ
-- Mathlib.Data.Finset.Defs
Finset.Subset.antisymm_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.penultimate_cons_of_not_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  ¬p.Nil → (SimpleGraph.Walk.cons h p).penultimate = p.penultimate
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side.  -/
InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.cos (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖x‖
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.homMk_hom_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X}
  (f : ↑Y → ↑Z) (hf : Topology.ContinuousGeneratedBy X f) (a : ↑Y), (ContinuousGeneratedByCat.homMk f hf).hom a = f a
-- Mathlib.Data.Matrix.Basic
Matrix.piAddEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} [inst : (i : ι) → Add (β i)]
  (f : Matrix m n ((i : ι) → β i)) (i : ι), Matrix.piAddEquiv f i = f.map fun x => x i
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.factorsThrough_conductor : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.FactorsThrough χ.conductor
-- Mathlib.Control.ULift
/-- Embedding of pure values.  -/
ULift.pure : {α : Type u} → α → ULift.{u_1, u} α
-- Batteries.Recycling.RBTree.Basic
/-- Asserts that `p` holds on every element of the tree.  -/
RBTree.RBNode.All : {α : Type u_1} → (α → Prop) → RBTree.RBNode α → Prop
-- Lean.Widget.UserWidget
Lean.Widget.instToJsonUserWidgetDefinition : Lean.ToJson Lean.Widget.UserWidgetDefinition
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
SpectrumRestricts.smul_of_nonneg : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A},
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : ℝ}, 0 ≤ r → SpectrumRestricts (r • a) ⇑ContinuousMap.realToNNReal
-- Mathlib.Analysis.Analytic.Basic
analyticOn_univ : ∀ {𝕜 : 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},
  AnalyticOn 𝕜 f Set.univ ↔ AnalyticOnNhd 𝕜 f Set.univ
-- Mathlib.Logic.Hydra
Relation.cutExpand_singleton : ∀ {α : Type u_1} {r : α → α → Prop} {s : Multiset α} {x : α}, (∀ x' ∈ s, r x' x) → Relation.CutExpand r s {x}
-- Std.Data.TreeSet.Raw.Basic
/-- Partitions a tree set into two tree sets based on a predicate.  -/
Std.TreeSet.Raw.partition : {α : Type u} →
  {cmp : α → α → Ordering} → (α → Bool) → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp × Std.TreeSet.Raw α cmp
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The addition rule.  -/
Projectivization.Subspace.mem_add' : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (self : Projectivization.Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
  Projectivization.mk K v hv ∈ self.carrier →
    Projectivization.mk K w hw ∈ self.carrier → Projectivization.mk K (v + w) hvw ∈ self.carrier
-- Mathlib.Topology.MetricSpace.IsometricSMul
diam_smul : ∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X),
  Metric.diam (c • s) = Metric.diam s
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F),
  ↑(AddSubmonoid.comap f S) = ⇑f ⁻¹' ↑S
-- Init.Data.UInt.Lemmas
UInt8.toUInt8_toUInt64 : ∀ (n : UInt8), n.toUInt64.toUInt8 = n
-- Aesop.Tree.Data
Aesop.NormalizationState.normal : Lean.MVarId →
  Lean.Meta.SavedState → Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)) → Aesop.NormalizationState
-- Mathlib.Algebra.Ring.Pi
instRingHomSurjectiveForallEvalRingHom : ∀ {I : Type u} (f : I → Type u_1) [inst : (i : I) → Semiring (f i)] (i : I), RingHomSurjective (Pi.evalRingHom f i)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.congr : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : LE E],
  MeasureTheory.Supermartingale f ℱ μ →
    MeasureTheory.StronglyAdapted ℱ g → (∀ (t : ι), f t =ᵐ[μ] g t) → MeasureTheory.Supermartingale g ℱ μ
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.single.eq_1 : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι),
  HomologicalComplex.single V c j =
    { obj := fun A => { X := fun i => if i = j then A else 0, d := fun x x_1 => 0, shape := ⋯, d_comp_d' := ⋯ },
      map := fun {X Y} f =>
        {
          f := fun i =>
            if h : i = j then
              CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
            else 0,
          comm' := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_4 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (op : Std.Tactic.BVDecide.BVUnOp)
  (expr : Std.Tactic.BVDecide.BVExpr w) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.un op expr with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_4 w op expr
-- Init.Data.String.Basic
String.Pos.sliceFrom.congr_simp : ∀ {s : String} (p₀ pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : p₀ ≤ pos), p₀.sliceFrom pos h = p₀.sliceFrom pos_1 ⋯
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNNNorm_lsmul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E],
  ‖ContinuousLinearMap.lsmul 𝕜 R‖₊ ≤ 1
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coe_neg`. -/
ContDiffMapSupportedIn.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprLocalTimeType : Repr Std.Time.TimeZone.TZif.LocalTimeType
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.ext : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {f g : A →ₜ+ B}, (∀ (x : A), f x = g x) → f = g
-- Aesop.Search.Queue.Class
Aesop.Queue : Type → Type
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in a string, starting
from the end of the slice and traversing towards the start. If there is no match `none` is
returned.

This function is generic over all currently supported patterns except
`String`/`String.Slice`.

Examples:

* `("coffee tea water".toSlice.revFind? Char.isWhitespace).map (·.get!) == some ' '`

* `"tea".toSlice.revFind? (fun (c : Char) => c == 'X') == none`
 -/
String.revFind? : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        (s : String) → (pattern : ρ) → [String.Slice.Pattern.ToBackwardSearcher pattern σ] → Option s.Pos
-- Mathlib.Analysis.Complex.AbelLimit
Complex.stolzCone.eq_1 : ∀ (s : ℝ), Complex.stolzCone s = {z | |z.im| < s * (1 - z.re)}
-- Mathlib.Algebra.Lie.Basic
LieHom.mk : {R : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing L'] →
              [inst_4 : LieAlgebra R L'] →
                (toLinearMap : L →ₗ[R] L') →
                  (∀ {x y : L}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆) → L →ₗ⁅R⁆ L'
-- Mathlib.Lean.Meta.Basic
/-- Checks that `e` is a function (i.e. that its type is a `.forallE` after `instantiateMVars` and
`whnf`). If not, coerces `e` to a function or fails with a descriptive error.  -/
Lean.Meta.ensureIsFunction : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Complex.ReImTopology
TendstoUniformlyOn.re : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} {K : Set α},
  TendstoUniformlyOn f g p K → TendstoUniformlyOn (fun n x => (f n x).re) (fun y => (g y).re) p K
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Init.Grind.ToInt
Lean.Grind.instInhabitedIntInterval : Inhabited Lean.Grind.IntInterval
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk'_comp_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], (QuotientAddGroup.mk' N).comp N.subtype = 0
-- Init.Meta.Defs
Lean.instQuoteTermMkStr1 : Lean.Quote Lean.Term
-- Init.Data.String.Basic
String.Slice.Pos.get.congr_simp : ∀ {s : String.Slice} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos), pos.get h = pos_1.get ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfcₙ_lt : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : ℝ},
  (∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ < c) → ‖cfcₙ f a‖ < c
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.nhds_one_hasBasis : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M},
  (nhds 1).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.surjective_mk : ∀ (X : Type u_1) [inst : TopologicalSpace X], Function.Surjective T2Quotient.mk
-- Lean.Server.References
Lean.Server.References.MatchedDefinition.mk.inj : ∀ {α : Type} {mod : Lean.Name} {modUri : Lean.Lsp.DocumentUri} {ident : α} {range : Lean.Lsp.Range} {mod_1 : Lean.Name}
  {modUri_1 : Lean.Lsp.DocumentUri} {ident_1 : α} {range_1 : Lean.Lsp.Range},
  { mod := mod, modUri := modUri, ident := ident, range := range } =
      { mod := mod_1, modUri := modUri_1, ident := ident_1, range := range_1 } →
    mod = mod_1 ∧ modUri = modUri_1 ∧ ident = ident_1 ∧ range = range_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => Real.sinh (f x)) x
-- Init.Prelude
instInhabitedUSize : Inhabited USize
-- Mathlib.Algebra.Group.Defs
ZPow.toPow.eq_1 : ∀ {M : Type u_2} [inst : ZPow M], ZPow.toPow = { pow := fun x n => ZPow.zpow n x }
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.mk.inj : ∀ {optionsPerPos : Lean.PrettyPrinter.Delaborator.OptionsPerPos} {currNamespace : Lean.Name}
  {openDecls : List Lean.OpenDecl} {inPattern : Bool} {subExpr : Lean.SubExpr} {depth lctxInitIndices : ℕ}
  {optionsPerPos_1 : Lean.PrettyPrinter.Delaborator.OptionsPerPos} {currNamespace_1 : Lean.Name}
  {openDecls_1 : List Lean.OpenDecl} {inPattern_1 : Bool} {subExpr_1 : Lean.SubExpr} {depth_1 lctxInitIndices_1 : ℕ},
  { optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls, inPattern := inPattern,
        subExpr := subExpr, depth := depth, lctxInitIndices := lctxInitIndices } =
      { optionsPerPos := optionsPerPos_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        inPattern := inPattern_1, subExpr := subExpr_1, depth := depth_1, lctxInitIndices := lctxInitIndices_1 } →
    optionsPerPos = optionsPerPos_1 ∧
      currNamespace = currNamespace_1 ∧
        openDecls = openDecls_1 ∧
          inPattern = inPattern_1 ∧ subExpr = subExpr_1 ∧ depth = depth_1 ∧ lctxInitIndices = lctxInitIndices_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.incompatible_of_reducedToEmpty : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty →
    Std.Tactic.BVDecide.LRAT.Internal.Incompatible (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) c assignment
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.isConstant.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (decl : Std.Sat.AIG.Decl α) →
      (Unit → motive Std.Sat.AIG.Decl.false) →
        ((x : Std.Sat.AIG.Decl α) → (x = Std.Sat.AIG.Decl.false → False) → motive x) → motive decl