mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `Comma L R₁ ⥤ Comma L R₃` induced by the composition of the natural transformations
`r : R₁ ⟶ R₂` and `r' : R₂ ⟶ R₃` is naturally isomorphic to the composition of the functors
induced by these natural transformations.  -/
CategoryTheory.Comma.mapRightComp : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              {R₁ R₂ L₃ : CategoryTheory.Functor B T} →
                (r : R₂ ⟶ R₁) →
                  (r' : L₃ ⟶ R₂) →
                    CategoryTheory.Comma.mapRight L (CategoryTheory.CategoryStruct.comp r' r) ≅
                      (CategoryTheory.Comma.mapRight L r').comp (CategoryTheory.Comma.mapRight L r)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The affine span of any two distinct points of a collinear set of points equals the affine
span of the whole set.  -/
Collinear.affineSpan_eq_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P},
  Collinear k s → ∀ {p₁ p₂ : P}, p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → line[k, p₁, p₂] = affineSpan k s
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.zero_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.Hom.τ₃ 0 = 0
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `Set.Finite.absorbs_biInter`. -/
Absorbs.biInter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α] {t : Set α}
  {ι : Type u_3} {I : Set ι}, I.Finite → ∀ {s : ι → Set α}, (∀ i ∈ I, Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ i ∈ I, s i) t
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
Submodule.dualCoannihilator_map_linearEquiv_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : N ≃ₗ[R] Module.Dual R M) (p : Submodule R M),
  (Submodule.map (↑e).flip p).dualCoannihilator = Submodule.map (↑e.symm) p.dualAnnihilator
-- Aesop.Util.UnionFind
_private.Aesop.Util.UnionFind.0.Aesop.UnionFind.findRepUnsafe : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → USize → Aesop.UnionFind α → USize × Aesop.UnionFind α
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce_reduceStep : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m},
  ↑A 1 0 ≠ 0 → FixedDetMatrices.reduce (FixedDetMatrices.reduceStep A) = FixedDetMatrices.reduce A
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nonneg_of_mem_Icc : ∀ {x : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → 0 ≤ Real.cos x
-- Mathlib.Logic.Equiv.Defs
Equiv.bijectiveEquiv_symm_apply_coe : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (a : α), ↑(Equiv.bijectiveEquiv.symm f) a = f a
-- Mathlib.CategoryTheory.Action.Concrete
Action.FintypeCat.toEndHom_apply : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : N.Normal] (g h : G),
  (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.toEndHom N) g).hom) ⟦h⟧ = ⟦h * g⁻¹⟧
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {s : Set α} (hs : MeasurableSet s)
  (f g : MeasureTheory.SimpleFunc α β) (a : α),
  (MeasureTheory.SimpleFunc.piecewise s hs f g) a = if a ∈ s then f a else g a
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- The ordering on group topologies on the group `γ`. `t ≤ s` if every set open in `s`
is also open in `t` (`t` is finer than `s`).  -/
AddGroupTopology.instPartialOrder : {α : Type u} → [inst : AddGroup α] → PartialOrder (AddGroupTopology α)
-- Mathlib.RingTheory.Nilpotent.Basic
neg_one_pow_ne_zero : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R] (n : ℕ), (-1) ^ n ≠ 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f : β → α}, UniformContinuous f → UniformContinuous fun x => (f x)⁻¹
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.toContinuousMap_injective : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Function.Injective ContinuousMonoidHom.toContinuousMap
-- Mathlib.Order.Std
/-- Arguments for `Preorder.ofStd`; see that function for details.  -/
Preorder.OfStdArgs : Type u_1 → Type u_1
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instDecidableEq : {m : Type u_1} →
  {n : Type u_2} → {A : Type u_5} → [DecidableEq A] → [Fintype m] → [Fintype n] → DecidableEq (CStarMatrix m n A)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonpos_iff : ∀ {b x : ℝ}, 1 < b → 0 < x → (Real.logb b x ≤ 0 ↔ x ≤ 1)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  (CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad t).hom = t
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeft_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.mapLeft R l).map f).left = f.left
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.instInhabitedPreDefinition.default : Lean.Elab.PreDefinition
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inclusion_comp_embedding : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S T : CategoryTheory.Subgroupoid C} (h : S ≤ T),
  (CategoryTheory.Subgroupoid.inclusion h).comp T.hom = S.hom
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Specialize.forall : ∀ {α : Sort u_1} {σs : List (Type u_2)} {ψ : α → Std.Do.SPred σs} {P : Std.Do.SPred σs} (a : α),
  (P ∧ ∀ x, ψ x) ⊢ₛ P ∧ ψ a
-- Mathlib.Algebra.Group.Action.Defs
/-- Like `Add.toVAdd`, but adds on the right.

See also `AddMonoid.toOppositeAddAction`.  -/
Add.toVAddAddOpposite : (α : Type u_9) → [Add α] → VAdd αᵃᵒᵖ α
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`.  -/
ContDiffWithinAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} (x : E),
  ContDiffWithinAt 𝕜 n g t (f x) → ContDiffWithinAt 𝕜 n f s x → Set.MapsTo f s t → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffOn_finsetSum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (fun x => ∑ i ∈ t, f i x) s
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.skipWhile.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((nextCurr : s.Pos) → motive (some nextCurr)) → (Unit → motive none) → motive x
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_comp_of_eq : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {g : M' → M''} {x : M} {y : M'},
  MDiffAt g y → MDiffAt f x → f x = y → mfderiv% (g ∘ f) x = mfderiv% g (f x) ∘SL mfderiv% f x
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance_idem : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f : ι → G),
  Fintype.balance (Fintype.balance f) = Fintype.balance f
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- `n`-times continuously differentiable diffeomorphism between `M` and `M'` with respect to `I`
and `I'`, denoted as `M ≃ₘ^n⟮I, I'⟯ M'` (in the `Manifold` namespace).  -/
Manifold.«term_≃ₘ^_⟮_,_⟯_» : Lean.TrailingParserDescr
-- Lean.Elab.DeprecatedSyntax
Lean.Elab.SyntaxDeprecationEntry.mk : Lean.SyntaxNodeKind → Option String → Option String → Lean.Elab.SyntaxDeprecationEntry
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.ofOLeanEntry : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → σ → α → Lean.ImportM β
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- **Alias** of the reverse direction of `ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection`. -/
ContinuousLinearMap.LinearMap.IsSymmetricProjection.isStarProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], (↑T).IsSymmetricProjection → IsStarProjection T
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filter! f t) k =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.hom_comp : ∀ {A B C : ProfiniteAddGrp.{u}} (f : A ⟶ B) (g : B ⟶ C),
  ProfiniteAddGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (ProfiniteAddGrp.Hom.hom g).comp (ProfiniteAddGrp.Hom.hom f)
-- Mathlib.Algebra.Group.Prod
AddEquiv.coe_prodComm : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N], ⇑AddEquiv.prodComm = Prod.swap
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.ref : Lean.Elab.Term.MutualClosure.LetRecClosure → Lean.Syntax
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The inverse map for the equivalence `SpecialLinearGroup.centerEquivRootsOfUnity`.  -/
SpecialLinearGroup.centerEquivRootsOfUnity_invFun : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          [Module.Free R V] →
            [Module.Finite R V] →
              ↥(rootsOfUnity (max (Module.finrank R V) 1) R) → ↥(Subgroup.center (SpecialLinearGroup R V))
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousOn_toNNReal : ContinuousOn ENNReal.toNNReal {a | a ≠ ⊤}
-- Mathlib.CategoryTheory.Equivalence
/-- If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`.  -/
CategoryTheory.Equivalence.congrRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (C ≌ D) → (CategoryTheory.Functor E C ≌ CategoryTheory.Functor E D)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.mk.inj : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.DTreeMap._auto_1}
  {inner : Std.DTreeMap.Internal.Impl α β} {wf : inner.WF} {inner_1 : Std.DTreeMap.Internal.Impl α β}
  {wf_1 : inner_1.WF}, { inner := inner, wf := wf } = { inner := inner_1, wf := wf_1 } → inner = inner_1
-- Mathlib.Data.List.PeriodicityLemma
/-- `HasPeriod w p`, means that the list `w` has the period `p`,
which can be seen in two equivalent ways:
· The list `w` starts again after the prefix of length `p`. That is, `w` overlaps with itself
  with offset `p`.
· The element of `w` at index `i` is the same as the element at index `i + p`, for all `i`
The definition is given in terms of the self-overlap.
 -/
List.HasPeriod : {α : Type u_1} → List α → ℕ → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.epi : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs : CategoryTheory.Limits.IsColimit s), CategoryTheory.Epi s.π
-- Lean.Meta.Tactic.Grind.ReflCmp
_private.Lean.Meta.Tactic.Grind.ReflCmp.0.Lean.Meta.Grind.getReflCmpThm?.go? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → γ a} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.map f t) = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.Combinatorics.Additive.Dissociation
MulEquiv.mulDissociated_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : CommGroup β] {s : Set α} (e : β ≃* α),
  MulDissociated (⇑e ⁻¹' s) ↔ MulDissociated s
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_mapDomain_apply_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {τ : Type u_3} (d : σ →₀ ℕ) (f : σ → τ),
  (MvPowerSeries.monomial (Finsupp.mapDomain f d)) 1 = d.prod fun s e => MvPowerSeries.X (f s) ^ e
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.inv_op_smul_set_distrib : ∀ {α : Type u_2} [inst : Group α] (a : α) (s : Set α), (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Context.mk : Mathlib.Tactic.DepRewrite.Config →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr →
        Array (Lean.FVarId × Lean.Expr) →
          Std.HashSet Lean.FVarId → Lean.HeadIndex → ℕ → Mathlib.Tactic.DepRewrite.Context
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.fst_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2], AffineMap.fst.linear = LinearMap.fst k V1 V2
-- Mathlib.Algebra.Torsor.Defs
/-- Torsor subtraction and addition with the same element cancels out.  -/
AddTorsor.vsub_vadd' : ∀ {G : outParam (Type u_1)} {P : Type u_2} {inst : AddGroup G} [self : AddTorsor G P] (p₁ p₂ : P), (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
-- Mathlib.Probability.Kernel.Composition.MeasureComp
ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure α),
  π {true} ≠ 0 → ν.AbsolutelyContinuous (π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν))
-- Mathlib.Geometry.Euclidean.Incenter
/-- A weaker version of `touchpoint_mem_affineSpan`.  -/
Affine.Simplex.touchpoint_mem_affineSpan_simplex : ∀ {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 : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  (i : Fin (n + 1)), s.touchpoint signs i ∈ affineSpan ℝ (Set.range s.points)
-- Lean.Environment
_private.Lean.Environment.0.Lean.RealizationContext.mk.inj : ∀ {env : NonScalar} {opts : Lean.Options} {realizeMapRef : IO.Ref (Lean.NameMap NonScalar)} {env_1 : NonScalar}
  {opts_1 : Lean.Options} {realizeMapRef_1 : IO.Ref (Lean.NameMap NonScalar)},
  { env := env, opts := opts, realizeMapRef := realizeMapRef } =
      { env := env_1, opts := opts_1, realizeMapRef := realizeMapRef_1 } →
    env = env_1 ∧ opts = opts_1 ∧ realizeMapRef = realizeMapRef_1
-- Mathlib.Topology.Compactness.Lindelof
Finset.isLindelof_biUnion : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (s : Finset ι) {f : ι → Set X},
  (∀ i ∈ s, IsLindelof (f i)) → IsLindelof (⋃ i ∈ s, f i)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A subset `p : α → Prop` of the type closed under `ωSup` induces an
`OmegaCompletePartialOrder` on the subtype `{a : α // p a}`.  -/
OmegaCompletePartialOrder.subtype : {α : Type u_6} →
  [inst : OmegaCompletePartialOrder α] →
    (p : α → Prop) →
      (∀ (c : OmegaCompletePartialOrder.Chain α), (∀ i ∈ c, p i) → p (OmegaCompletePartialOrder.ωSup c)) →
        OmegaCompletePartialOrder (Subtype p)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeWhile_eq_takeWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.takeWhile pat = s.toSlice.takeWhile pat
-- Mathlib.Algebra.Group.Action.Option
Option.instIsCentralVAdd : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α], IsCentralVAdd M (Option α)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffAdd I n G] {f g : M → G} {s : Set M} {x : M},
  ContMDiffWithinAt I' I n f s x → ContMDiffWithinAt I' I n g s x → ContMDiffWithinAt I' I n (f + g) s x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instSMul : {𝕜 : Type u_2} →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : NormedField 𝕜] → [inst_5 : NormedSpace 𝕜 F] → [SMulCommClass ℝ 𝕜 F] → SMul 𝕜 (SchwartzMap E F)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instIsScalarTower_1 : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_1} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : NonUnitalSeminormedRing β] [inst_3 : Zero 𝕜] [inst_4 : SMul 𝕜 β] [inst_5 : IsBoundedSMul 𝕜 β]
  [IsScalarTower 𝕜 β β], IsScalarTower 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
RingHom.map_det : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type w}
  [inst_3 : CommRing S] (f : R →+* S) (M : Matrix n n R), f M.det = (f.mapMatrix M).det
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.DHashMap.Raw.Const.ofList l).isEmpty = l.isEmpty
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instIsRankLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], ValuativeRel.IsRankLeOne K
-- Mathlib.Order.Monotone.Basic
antitone_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Antitone f
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_swap : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {x y : α}, x ≠ y → Equiv.Perm.sign (Equiv.swap x y) = -1
-- Mathlib.Analysis.Complex.LocallyUniformLimit
/-- A circle integral which coincides with `deriv f z` whenever one can apply the Cauchy formula for
the derivative. It is useful in the proof that locally uniform limits of holomorphic functions are
holomorphic, because it depends continuously on `f` for the uniform topology.  -/
Complex.cderiv : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → ℝ → (ℂ → E) → ℂ → E
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.getD : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → [Std.LawfulEqCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → β a → β a
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.letDeclArgHasBinders : Lean.Syntax → Bool
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Flipping arguments gives a continuous linear equivalence between
`G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'` and `ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')`  -/
ContinuousLinearMap.flipMultilinearEquiv : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (G : Type wG) →
        (G' : Type wG') →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : SeminormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : SeminormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        [Fintype ι] →
                          (G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') ≃L[𝕜] ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, P.part a = ∅ ↔ a ∉ s
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.coe_graph : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (f : G →+ H), ↑f.graph = {x | f x.1 = x.2}
-- Mathlib.Order.Hom.Lattice
InfHom.coe_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : Bot β], ⇑⊥ = ⊥
-- Std.Do.WP.Monad
Std.Do.WPMonad.toLawfulMonad : ∀ {m : Type u → Type v} {ps : outParam Std.Do.PostShape} {inst : Monad m} [self : Std.Do.WPMonad m ps], LawfulMonad m
-- Init.GetElem
/-- Internal implementation of `as[i]?`. Do not use directly.  -/
List.get?Internal : {α : Type u_1} → List α → ℕ → Option α
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddMonoid.enorm_zero : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ESeminormedAddMonoid E], ‖0‖ₑ = 0