mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Indicator
Set.indicator_compl_add_self : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f : α → M), sᶜ.indicator f + s.indicator f = f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_of_measurable_on_compl_countable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  {f : α → β} (s : Set α), s.Countable → Measurable (sᶜ.domRestrict f) → Measurable f
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNeg_addPos : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  assignment.addPosAssignment.hasNegAssignment = assignment.hasNegAssignment
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_iUnion : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {ι : Sort u_4}
  {s : ι → Set E}, B.polar (⋃ i, s i) = ⋂ i, B.polar (s i)
-- Init.Data.SInt.Lemmas
Int32.ofNat_le_iff_le : ∀ {a b : ℕ}, a < 2 ^ 31 → b < 2 ^ 31 → (Int32.ofNat a ≤ Int32.ofNat b ↔ a ≤ b)
-- Mathlib.ModelTheory.Definability
/-- A 1-dimensional version of `Definable`, for `Set M`.  -/
Set.Definable₁ : {M : Type w} → Set M → (L : FirstOrder.Language) → [L.Structure M] → Set M → Prop
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
OrderIso.withZeroUnits_apply : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] (n : WithZero αˣ),
  OrderIso.withZeroUnits n = WithZero.recZeroCoe 0 Units.val n
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
integer parts of the stream of integer and fractional parts.
 -/
GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {ifp_succ_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n →
    (GenContFract.of v).s.get? n = some { a := 1, b := ↑ifp_succ_n.b }
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeOrder.liftRight : {𝕆 : Type u_1} →
  {α : Type u_3} →
    {β : Type u_4} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [GradeOrder 𝕆 β] → (f : α → β) → StrictMono f → (∀ (a b : α), a ⋖ b → f a ⋖ f b) → GradeOrder 𝕆 α
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.ker_fst : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'], (AddMonoidHom.fst G G').ker = ⊥.prod ⊤
-- Init.Data.Bool
Bool.instLE : LE Bool
-- Init.Data.UInt.Lemmas
USize.toNat_add : ∀ (a b : USize), (a + b).toNat = (a.toNat + b.toNat) % 2 ^ System.Platform.numBits
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If `E : C ≌ D` and `E' : D ≌ F` are equivalences whose inverse functors are compatible with shifts,
so is `(E.trans E').inverse`.
 -/
CategoryTheory.Equivalence.CommShift.instCommShiftInverseTrans : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [E.inverse.CommShift A] →
                    {F : Type u_4} →
                      [inst_6 : CategoryTheory.Category.{v_3, u_4} F] →
                        [inst_7 : CategoryTheory.HasShift F A] →
                          {E' : D ≌ F} → [E'.inverse.CommShift A] → (E.trans E').inverse.CommShift A
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_zero_eqOn : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A], Set.EqOn (fun a => a ^ 0) (fun x => 1) (Set.Ici 0)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_iInf : ∀ {ι : Type u_1} [Finite ι] (u : ι → ℕ → ENNReal), ExpGrowth.expGrowthInf (⨅ i, u i) = ⨅ i, ExpGrowth.expGrowthInf (u i)
-- Mathlib.Data.Multiset.Basic
Multiset.toList_zero : ∀ {α : Type u_1}, Multiset.toList 0 = []
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_of_add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {k : ι}, P.root k = P.root j + P.root i → RootPairing.chainTopCoeff i j = RootPairing.chainTopCoeff i k + 1
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
/-- The integral of `f (R⁻¹ • x)` with respect to an additive Haar measure is a multiple of the
integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
thanks to the convention that a non-integrable function has integral zero.  -/
MeasureTheory.Measure.integral_comp_inv_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] (f : E → F) (R : ℝ),
  ∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ Module.finrank ℝ E| • ∫ (x : E), f x ∂μ
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_fderiv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E},
  fderiv 𝕜 (⇑iso ∘ f) = fun x => ↑↑iso ∘SL fderiv 𝕜 f x
-- Plausible.Testable
Plausible.Not.printableProp : {x : Prop} → [Plausible.PrintableProp x] → Plausible.PrintableProp ¬x
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instMulAction : {M : Type u_2} →
  {N : Type u_4} →
    {ι : Type u_6} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : TopologicalSpace N] →
              {R' : Type u_7} →
                {A : Type u_9} →
                  [inst_4 : Monoid R'] →
                    [inst_5 : Semiring A] →
                      [inst_6 : Module A M] →
                        [inst_7 : Module A N] →
                          [inst_8 : DistribMulAction R' N] →
                            [ContinuousConstSMul R' N] → [SMulCommClass A R' N] → MulAction R' (M [⋀^ι]→L[A] N)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The coprojection from a value of the functor to the colimit object.  -/
CategoryTheory.Limits.colimit.ι : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] → (j : J) → F.obj j ⟶ CategoryTheory.Limits.colimit F
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {obj : Type u₂}
  {category : autoParam (CategoryTheory.Category.{v₂, u₂} obj) CategoryTheory.BasedCategory.category._autoParam}
  {p : CategoryTheory.Functor obj 𝒮} {obj_1 : Type u₂}
  {category_1 : autoParam (CategoryTheory.Category.{v₂, u₂} obj_1) CategoryTheory.BasedCategory.category._autoParam}
  {p_1 : CategoryTheory.Functor obj_1 𝒮},
  { obj := obj, category := category, p := p } = { obj := obj_1, category := category_1, p := p_1 } →
    obj = obj_1 ∧ category ≍ category_1 ∧ p ≍ p_1
-- Mathlib.Combinatorics.Quiver.Covering
/-- In a quiver with involutive inverses, the star and costar at every vertex are equivalent.
This map is induced by `Quiver.reverse`.  -/
Quiver.starEquivCostar : {U : Type u_1} → [inst : Quiver U] → [Quiver.HasInvolutiveReverse U] → (u : U) → Quiver.Star u ≃ Quiver.Costar u
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {f : A →+* B},
  Ideal.map f I ≤ J → (∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)) → hI.IsDPMorphism hJ f
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
AlgebraicTopology.singularChainComplexFunctorAdjunction_unit_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (n : ℕ) (R : C),
  (AlgebraicTopology.singularChainComplexFunctorAdjunction C n).unit.app R =
    CategoryTheory.Limits.Sigma.ι (fun x => R)
      ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplexToTop.app { len := n }).app (Opposite.op { len := n })))
        (SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id { len := n })))
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `h.Ω₀` is the subobject of `Ω` which corresponds to the identity `𝟙 Ω`,
given `h : SubobjectRepresentableBy Ω`.  -/
CategoryTheory.SubobjectRepresentableBy.Ω₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} → CategoryTheory.SubobjectRepresentableBy Ω → CategoryTheory.Subobject Ω
-- Init.Data.List.Lex
List.cons_lt_cons_iff : ∀ {α : Type u_1} [inst : LT α] {a b : α} {l₁ l₂ : List α}, a :: l₁ < b :: l₂ ↔ a < b ∨ a = b ∧ l₁ < l₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.mk : Lean.Grind.CommRing.Var → ℕ → Lean.Grind.CommRing.Power
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_inj : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i = toZ i0 j ↔ i = j
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The p-adic valuation of `n` is less than or equal to its logarithm w.r.t. `p`.  -/
padicValNat_le_nat_log : ∀ {p : ℕ} (n : ℕ), padicValNat p n ≤ Nat.log p n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_insertIfNew_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  k ∈ t.insertIfNew k v
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_at_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.eval₂ f 1 p = f (Polynomial.eval 1 p)
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.exists_retraction_subtype_of_isClosed : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)},
  IsClosed s → s.Nonempty → ∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Function.Surjective f ∧ Continuous f
-- Lean.MetavarContext
/-- A monad with a stateful metavariable context, defining `getMCtx` and `modifyMCtx`.  -/
Lean.MonadMCtx : (Type → Type) → Type
-- Mathlib.Data.List.MinMax
List.argmin_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {a : α},
  List.argmin f [a] = some a
-- Mathlib.Analysis.Normed.Group.AddTorsor
instIsTopologicalAddTorsor_1 : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P], IsTopologicalAddTorsor P
-- Mathlib.Algebra.Ring.CentroidHom
_private.Mathlib.Algebra.Ring.CentroidHom.0.CentroidHom.termL : Lean.ParserDescr
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The valuation on the completion agrees with the global valuation on elements of the
integer ring.  -/
IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  Valued.v ↑r = (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑r
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.seq.inj : ∀ {action : Lean.Syntax} {k : Lean.Elab.Term.Do.Code} {action_1 : Lean.Syntax} {k_1 : Lean.Elab.Term.Do.Code},
  Lean.Elab.Term.Do.Code.seq action k = Lean.Elab.Term.Do.Code.seq action_1 k_1 → action = action_1 ∧ k = k_1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupCohomology.cocycles₂ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 2)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₂ f φ) h)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_pi_single`.  -/
Fintype.sum_pi_single : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : ι → Type u_6} [inst_2 : (i : ι) → AddCommMonoid (M i)]
  (i : ι) (f : (i : ι) → M i), ∑ j, Pi.single j (f j) i = f i
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} (x : 𝕜),
  f x ≠ 0 →
    g x ≠ 0 →
      DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → logDeriv (fun z => f z / g z) x = logDeriv f x - logDeriv g x
-- Mathlib.CategoryTheory.Sigma.Basic
/-- Assemble an `I`-indexed family of functors into a functor between the sigma types.
 -/
CategoryTheory.Sigma.Functor.sigma : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₁} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₁, u₁} (D i)] →
          ((i : I) → CategoryTheory.Functor (C i) (D i)) → CategoryTheory.Functor ((i : I) × C i) ((i : I) × D i)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_univ : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} (n m : ι),
  MeasureTheory.hittingBtwn u Set.univ n m = fun x => min n m
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.ext_iff : ∀ {x y : Std.Time.Timestamp}, x = y ↔ x.val = y.val
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `f : ι → Set X` is a locally finite covering of a σ-compact topological space by nonempty
sets, then the index type `ι` is encodable.  -/
LocallyFinite.encodable : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [SigmaCompactSpace X] →
      {ι : Type u_4} → {f : ι → Set X} → LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Encodable ι
-- Init.Data.List.Count
List.IsInfix.countP_le : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₁ <:+: l₂ → List.countP p l₁ ≤ List.countP p l₂
-- Lean.Parser.Term.Doc
Lean.Parser.Term.Doc.RecommendedSpelling.mk.injEq : ∀ («notation» recommendedSpelling : String) (additionalInformation? : Option String)
  (notation_1 recommendedSpelling_1 : String) (additionalInformation?_1 : Option String),
  ({ «notation» := «notation», recommendedSpelling := recommendedSpelling,
        additionalInformation? := additionalInformation? } =
      { «notation» := notation_1, recommendedSpelling := recommendedSpelling_1,
        additionalInformation? := additionalInformation?_1 }) =
    («notation» = notation_1 ∧
      recommendedSpelling = recommendedSpelling_1 ∧ additionalInformation? = additionalInformation?_1)
-- Mathlib.Order.Lattice
lt_sup_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < max b c ↔ a < b ∨ a < c
-- Mathlib.Algebra.Ring.NonZeroDivisors
dvd_cancel_right_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] {r x y : R}, r ∈ nonZeroDivisors R → (x * r ∣ y * r ↔ x ∣ y)
-- Mathlib.Order.Minimal
Set.exists_insert_of_not_maximal : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s) → P s → ¬Maximal P s → ∃ x ∉ s, P (insert x s)
-- Mathlib.Data.ZMod.QuotientRing
Int.quotientSpanEquivZMod_comp_Quotient_mk : ∀ (n : ℤ), (↑n.quotientSpanEquivZMod).comp (Ideal.Quotient.mk (Ideal.span {n})) = Int.castRingHom (ZMod n.natAbs)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf : ∀ {G : Type u_1} [inst : Group G] {x y : G} [inst_1 : DecidableEq G],
  IsOfFinOrder x → (y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x)))
-- Init.Data.Option.Monadic
Option.forM_join : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] [LawfulMonad m] (o : Option (Option α))
  (f : α → m PUnit.{u_1 + 1}), forM o.join f = forM o fun x => forM x f
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
_private.Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv.0.coe_auxIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] [inst_4 : NormedAddCommGroup W]
  [inst_5 : InnerProductSpace 𝕜 W] [inst_6 : CompleteSpace W] (e : V ≃L[𝕜] W) {α α' : 𝕜} (hα : α ≠ 0)
  (hα2 : α' * α' = α⁻¹) (he : ContinuousLinearMap.adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V)
  (he' : ↑e ∘SL ContinuousLinearMap.adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W) (hαa : (starRingEnd 𝕜) α' = α'),
  ↑↑(auxIsometry✝ e hα hα2 he he' hαa) = α' • ↑e
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instCommRingHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → CommRing (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.of_le_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E]
  {A' : IntermediateField F E}, A.LinearDisjoint L → A' ≤ A → A'.LinearDisjoint L
-- Mathlib.Analysis.SpecificLimits.Normed
isUnit_one_sub_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] {x : R}, ‖x‖ < 1 → IsUnit (1 - x)
-- Lean.Parser.Do
Lean.Parser.Term.termTry.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_smul_right_of_tower : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N)
  [inst_5 : CommSemiring S] [inst_6 : Algebra S R] [inst_7 : Module S M] [IsScalarTower S R M] [inst_9 : Module S N]
  [IsScalarTower S R N] (a : S) (x y : M), QuadraticMap.polar (⇑Q) x (a • y) = a • QuadraticMap.polar (⇑Q) x y
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_cexp_mul_of_re_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    MeasureTheory.Integrable (fun ω => Complex.exp (z * ↑(X ω))) μ
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y},
  e.IsImage s t → e.IsImage s' t' → e.IsImage (s ∩ s') (t ∩ t')
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_sup'_eq_sup'_comp`. -/
Finset.comp_sup'_eq_sup'_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup γ] {s : Finset β}
  (H : s.Nonempty) {f : β → α} (g : α → γ), (∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g (s.sup' H f) = s.sup' H (g ∘ f)
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_comp_add_const_eq_meromorphicOrderAt`

---

`meromorphicOrderAt` is invariant under translation.  -/
meromorphicOrderAt_fun_comp_add_const_eq_meromorphicOrderAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E},
  meromorphicOrderAt (fun x => f (x + c)) x = meromorphicOrderAt f (x + c)
-- Mathlib.Algebra.Category.Grp.Zero
GrpCat.subsingleton_of_isZero : ∀ {G : GrpCat}, CategoryTheory.Limits.IsZero G → Subsingleton ↑G
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ X₄ : C} (f₁₂ : X₁ ⟶ X₂) (f₁₃ : X₁ ⟶ X₃)
  (f₂₄ : X₂ ⟶ X₄) (f₃₄ : X₃ ⟶ X₄)
  (fac : CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄)
  (X₁_1 X₂_1 X₃_1 X₄_1 : C) (f₁₂_1 : X₁_1 ⟶ X₂_1) (f₁₃_1 : X₁_1 ⟶ X₃_1) (f₂₄_1 : X₂_1 ⟶ X₄_1) (f₃₄_1 : X₃_1 ⟶ X₄_1)
  (fac_1 : CategoryTheory.CategoryStruct.comp f₁₂_1 f₂₄_1 = CategoryTheory.CategoryStruct.comp f₁₃_1 f₃₄_1),
  ({ X₁ := X₁, X₂ := X₂, X₃ := X₃, X₄ := X₄, f₁₂ := f₁₂, f₁₃ := f₁₃, f₂₄ := f₂₄, f₃₄ := f₃₄, fac := fac } =
      { X₁ := X₁_1, X₂ := X₂_1, X₃ := X₃_1, X₄ := X₄_1, f₁₂ := f₁₂_1, f₁₃ := f₁₃_1, f₂₄ := f₂₄_1, f₃₄ := f₃₄_1,
        fac := fac_1 }) =
    (X₁ = X₁_1 ∧ X₂ = X₂_1 ∧ X₃ = X₃_1 ∧ X₄ = X₄_1 ∧ f₁₂ ≍ f₁₂_1 ∧ f₁₃ ≍ f₁₃_1 ∧ f₂₄ ≍ f₂₄_1 ∧ f₃₄ ≍ f₃₄_1)
-- Lean.Widget.UserWidget
/-- Sourcetext of the JS module to run.  -/
Lean.Widget.WidgetSource.sourcetext : Lean.Widget.WidgetSource → String
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Filter.Tendsto.arcsin_nhdsLE : ∀ {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ},
  Filter.Tendsto f l (nhdsWithin x (Set.Iic x)) →
    Filter.Tendsto (fun x => Real.arcsin (f x)) l (nhdsWithin (Real.arcsin x) (Set.Iic (Real.arcsin x)))
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.mk : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            (toFun : E → F) →
              ContDiff ℝ (↑⊤) toFun →
                (∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C) → SchwartzMap E F
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Config.mk.sizeOf_spec : ∀ (verbose enforceUnfoldReducible enforceFoldProjs : Bool),
  sizeOf
      { verbose := verbose, enforceUnfoldReducible := enforceUnfoldReducible, enforceFoldProjs := enforceFoldProjs } =
    1 + sizeOf verbose + sizeOf enforceUnfoldReducible + sizeOf enforceFoldProjs
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalPreprocessor.toPreprocessorBase : Mathlib.Tactic.Linarith.GlobalPreprocessor → Mathlib.Tactic.Linarith.PreprocessorBase
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- There are distinct indices smaller than the successor of the domain's cardinality
yielding the same value  -/
OrdinalApprox.exists_gfpApprox_eq_gfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  ∃ a < (Order.succ (Cardinal.mk α)).ord,
    ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.gfpApprox f x a = OrdinalApprox.gfpApprox f x b
-- Mathlib.Order.Preorder.Finite
Set.finite_isBot : ∀ (α : Type u_2) [inst : PartialOrder α], {a | IsBot a}.Finite
-- Init.Data.Vector.Lemmas
Vector.contains_eq_true_of_mem : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {a : α} {as : Vector α n}, a ∈ as → as.contains a = true
-- Mathlib.Data.List.Basic
List.map_leftInverse_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
  Function.LeftInverse (List.map f) (List.map g) ↔ Function.LeftInverse f g