mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_δ_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory D] [inst_4 : CategoryTheory.MonoidalCategory E]
  (L : CategoryTheory.Functor D E) [inst_5 : L.OplaxMonoidal] (F G : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ ((CategoryTheory.Functor.whiskeringRight C D E).obj L) F G).app X =
    CategoryTheory.Functor.OplaxMonoidal.δ L (F.obj X) (G.obj X)
-- Lean.Parser.Command
Lean.Parser.Command.structSimpleBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_rio' : ∀ {n k : ℕ}, List.map (fun x => k + x) (*...n).toList = (k...k + n).toList
-- Lean.EnvExtension
/-- Returns a function suitable for `SimplePersistentEnvExtensionDescr.replay?` that replays all new
entries onto the state using `addEntryFn`. `p` should filter out entries that have already been
added to the state by a prior replay of the same realizable constant.
 -/
Lean.SimplePersistentEnvExtension.replayOfFilter : {σ : Type u_1} → {α : Type u_2} → (σ → α → Bool) → (σ → α → σ) → List α → σ → σ → List α × σ
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_sup : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] {s t : ClosedSubmodule R N},
  ↑(s ⊔ t) = ↑(↑s ⊔ ↑t).closure
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commSemiring.inj : ∀ {id id_1 : ℕ},
  Lean.Meta.Sym.Arith.ClassifyResult.commSemiring id = Lean.Meta.Sym.Arith.ClassifyResult.commSemiring id_1 → id = id_1
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Parenthesizer
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.match_1.eq_1 : ∀ {n : ℕ} (motive : List (BitVec n) → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (x : BitVec n) → (rest : List (BitVec n)) → motive (x :: rest)),
  (match [] with
    | [] => h_1 ()
    | x :: rest => h_2 x rest) =
    h_1 ()
-- Mathlib.Order.Minimal
MinimalFor.le : ∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrder α] {i j : ι} {Q : ι → Prop} {f : ι → α},
  MinimalFor Q f i → Q j → f i ≤ f j
-- Mathlib.Algebra.Group.Defs
SubNegZeroMonoid.toSubNegMonoid : {G : Type u_2} → [self : SubNegZeroMonoid G] → SubNegMonoid G
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.of_bound : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α}
  (c : ℝ), (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → f =O[l] g
-- Mathlib.Data.Fin.Embedding
Fin.coe_castAddEmb : ∀ {n : ℕ} (m : ℕ), ⇑(Fin.castAddEmb m) = Fin.castAdd m
-- Mathlib.Tactic.DuplicateDecls
/-- Sort the hypotheses in `e` into a normalized order by sorting their types.
Also replace universe levels with a default value.

TODO: When there are multiple variables of the same type, their order will not be changed.
This is a limitation of the current approach.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.sortBinders : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_le_min?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km kme : α}
  (hkme : (t.erase k).min? = some kme), t.min?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.id_weightMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (x : M),
  (↑(RootPairing.Equiv.id P)).weightMap x = x
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.piIsoPi_inv_kernel_ι : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : CategoryTheory.Limits.HasProduct Z] (i : ι),
  CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) =
    ModuleCat.ofHom (LinearMap.proj i)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_prodMk₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (fun a => (f i a, f j a)) (f k) μ
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.isSuccPrelimit_type_lt : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [h : NoMaxOrder α],
  Order.IsSuccPrelimit (Ordinal.type fun x1 x2 => x1 < x2)
-- Mathlib.LinearAlgebra.Ray
/-- If vectors `v₁` and `v₂` are on the same ray, then for some nonnegative `a b`, `a + b = 1`, we
have `v₁ = a • (v₁ + v₂)` and `v₂ = b • (v₁ + v₂)`.  -/
SameRay.exists_eq_smul_add : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v₁ v₂ : M},
  SameRay R v₁ v₂ → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.PushoutCocone.isoMk t).inv.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.pointsWithCircumcenterIndexInhabited : (n : ℕ) → Inhabited (Affine.Simplex.PointsWithCircumcenterIndex n)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.iSup_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {ι : Sort u_3} (f : ι → I.Filtration M), (iSup f).N = ⨆ i, (f i).N
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_eq_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : Fintype ι],
  MeasureTheory.Measure.infinitePi μ = MeasureTheory.Measure.pi μ
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_le_mul_card_image : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ),
  (∀ b ∈ Finset.image f s, {a ∈ s | f a = b}.card ≤ n) → s.card ≤ n * (Finset.image f s).card
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelp : Lean.ToJson Lean.Lsp.SignatureHelp
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RocSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxcIterator α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RicSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxcIterator α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Init.Data.SInt.Lemmas
Int8.le_total : ∀ (a b : Int8), a ≤ b ∨ b ≤ a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles are translation invariant.  -/
EuclideanGeometry.angle_vsub_const : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ p : P),
  EuclideanGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = EuclideanGeometry.angle p₁ p₂ p₃
-- Batteries.Data.Array.Match
/-- Current longest matching prefix  -/
Array.Matcher.state : {α : Type u_1} → (self : Array.Matcher α) → Fin (self.table.size + 1)
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_mapFinIdx_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f g : (i : ℕ) → α → i < l.length → β},
  l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : ℕ) (h : i < l.length), f i l[i] h = g i l[i] h
-- Init.Data.Array.Monadic
/-- We can express a for loop over an array as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
 -/
Array.forIn_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  (f : α → β → m (ForInStep β)) (init : β),
  forIn xs init f =
    ForInStep.value <$>
      Array.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) xs
-- Mathlib.GroupTheory.Rank
Subgroup.rank_closure_finset_le_card : ∀ {G : Type u_1} [inst : Group G] (s : Finset G), Group.rank ↥(Subgroup.closure ↑s) ≤ s.card
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- The natural inclusion map from `PSL(n, R)` to `PGL(n, R)` induced by the inclusion
map from `SL(n, R)` to `GL(n, R)`.  -/
Matrix.ProjectiveSpecialLinearGroup.toPGL : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] → Matrix.ProjectiveSpecialLinearGroup n R →* Matrix.ProjGenLinGroup n R
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf_iff_le_normalizer_inf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, (H.subgroupOf K).Normal ↔ K ≤ Subgroup.normalizer ↑(H ⊓ K)
-- Mathlib.Topology.Algebra.Monoid
Prod.continuousMul : ∀ {M : Type u_3} {N : Type u_4} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M]
  [inst_3 : TopologicalSpace N] [inst_4 : Mul N] [ContinuousMul N], ContinuousMul (M × N)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesFunctor_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C],
  (CategoryTheory.ShortComplex.opcyclesFunctor C).Additive
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Composition of `CatCospanTransforms` is defined "componentwise".  -/
CategoryTheory.Limits.CatCospanTransform.comp : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {A'' : Type u₇} →
                                  {B'' : Type u₈} →
                                    {C'' : Type u₉} →
                                      [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] →
                                        [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] →
                                          [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] →
                                            {F'' : CategoryTheory.Functor A'' B''} →
                                              {G'' : CategoryTheory.Functor C'' B''} →
                                                CategoryTheory.Limits.CatCospanTransform F G F' G' →
                                                  CategoryTheory.Limits.CatCospanTransform F' G' F'' G'' →
                                                    CategoryTheory.Limits.CatCospanTransform F G F'' G''
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The recurrence relation for the indefinite version of the `Γ` function.  -/
Complex.partialGamma_add_one : ∀ {s : ℂ}, 0 < s.re → ∀ {X : ℝ}, 0 ≤ X → (s + 1).partialGamma X = s * s.partialGamma X - ↑(Real.exp (-X)) * ↑X ^ s
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.mk : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (Std.ExtDHashMap α fun x => β) → Std.ExtHashMap α β
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_const_iff : ∀ {β : Type u_2} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] [Infinite β]
  [T2Space G] (a : G), (Multipliable fun x => a) ↔ a = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Inhabited α],
  t.WF →
    ∀ {k fallback : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKeyD k fallback =
        if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else fallback
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.φ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject C}
  (s : X.Splitting) (f : X ⟶ Y) (n : ℕ),
  s.φ f n = CategoryTheory.CategoryStruct.comp (s.ι n) (f.app (Opposite.op { len := n }))
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.lift_map : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (F : V ⥤rq D) {v w : V} (f : v ⟶ w),
  (CategoryTheory.Cat.FreeRefl.lift F).map (CategoryTheory.Cat.FreeRefl.homMk f) = F.map f
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rco.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ}
  {m : Type u → Type w} [inst_8 : Monad m] {r : Std.Rco α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Rco.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_whiskerLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {L₁ L₂ : CategoryTheory.Functor B C} {R₁ R₂ : CategoryTheory.Functor C B} {L : CategoryTheory.Functor A B}
  {R : CategoryTheory.Functor B A} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj : L ⊣ R) (τ : L₂ ⟶ L₁),
  (CategoryTheory.conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ) =
    CategoryTheory.Functor.whiskerRight ((CategoryTheory.conjugateEquiv adj₁ adj₂) τ) R
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.comp_tendsto_lim : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {F : Polynomial ℤ_[p]} (ncs : CauSeq ℤ_[p] norm),
  Filter.Tendsto (fun i => Polynomial.eval (↑ncs i) F) Filter.atTop (nhds (Polynomial.eval ncs.lim F))
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varsToConstants.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} {γ : Type u_4} (motive : L.Term (γ ⊕ α) → Sort u_5) (l : ℕ)
  (f : L.Functions l) (ts : Fin l → L.Term (γ ⊕ α)) (h_1 : (a : α) → motive (FirstOrder.Language.var (Sum.inr a)))
  (h_2 : (c : γ) → motive (FirstOrder.Language.var (Sum.inl c)))
  (h_3 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term (γ ⊕ α)) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.func f ts with
    | FirstOrder.Language.var (Sum.inr a) => h_1 a
    | FirstOrder.Language.var (Sum.inl c) => h_2 c
    | FirstOrder.Language.func f ts => h_3 l f ts) =
    h_3 l f ts
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.Limits.IsZero.hasInjectiveDimensionLT_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.HasInjectiveDimensionLT X 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Mathlib.Topology.Separation.Basic
SeparationQuotient.instT0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], T0Space (SeparationQuotient X)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.symm_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.symm.toPartialEquiv = e.symm
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Subalgebra.eq_bot_of_finrank_one : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  {S : Subalgebra F E}, Module.finrank F ↥S = 1 → ∀ [Module.Free F ↥S], S = ⊥
-- Std.Data.DTreeMap.Raw.Iterator
Std.DTreeMap.Raw.keys.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp), t.keys = t.inner.keys
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforwardToOfIso_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C Y}
  {𝒢 : TopCat.Presheaf C X} (H₂ : ℱ ⟶ (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopCat.Presheaf.pushforwardToOfIso H₁ H₂).app U =
    CategoryTheory.CategoryStruct.comp
      (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U))))
      (𝒢.map (CategoryTheory.eqToHom ⋯))
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.IterM.step_append.match_1.eq_3 : ∀ {α₁ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an inner regular measure under map of a left additive action is again
inner regular  -/
MeasureTheory.innerRegular_map_vadd : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : AddMonoid α] [inst_4 : AddAction α G] [ContinuousConstVAdd α G] [μ.InnerRegular] (a : α),
  (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).InnerRegular
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.stx.inj : ∀ {val val_1 : Lean.Syntax}, Lean.Elab.Term.Arg.stx val = Lean.Elab.Term.Arg.stx val_1 → val = val_1
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.instMvPolynomialOfFinite : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_1}
  [Finite ι] [Algebra.FiniteType R S], Algebra.FiniteType R (MvPolynomial ι S)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.colorClasses_isPartition : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α), Setoid.IsPartition C.colorClasses
-- Mathlib.Algebra.Module.ULift
ULift.vadd_def : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (s : ULift.{u_1, u} R) (x : M), s +ᵥ x = s.down +ᵥ x
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.dropEnd_eq_sliceTo : ∀ {s : String.Slice} {n : ℕ}, s.dropEnd n = s.sliceTo (s.endPos.prevn n)
-- Mathlib.Tactic.CongrExclamation
/-- Try applying user-provided congruence lemmas. If any are applicable,
returns a list of new goals.

Tries a congruence lemma associated to the LHS and then, if that failed, the RHS.
 -/
Lean.MVarId.userCongr? : Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValue! : {α : Type u} → {β : Type v} → [BEq α] → [Inhabited β] → α → List ((_ : α) × β) → β
-- Init.Data.Array.Range
Array.zipIdx_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.zipIdx i = #[] ↔ xs = #[]
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_sum_of_subset : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedAdd M] {f : ι → M}
  {s t : Finset ι}, s ⊆ t → ∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
-- Lean.Meta.Sym.Arith.MonadCanon
Lean.Meta.Sym.Arith.MonadCanon.mk : {m : Type → Type} → (Lean.Expr → m Lean.Expr) → (Lean.Expr → m (Option Lean.Expr)) → Lean.Meta.Sym.Arith.MonadCanon m
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofNatMultiset.congr_simp : ∀ (v v_1 : Multiset ℕ) (e_v : v = v_1) (h : ∀ p ∈ v, Nat.Prime p),
  PrimeMultiset.ofNatMultiset v h = PrimeMultiset.ofNatMultiset v_1 ⋯
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_toEquiv_trans : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] {e₁₂ : A ≃ₐc[R] B}
  {e₂₃ : B ≃ₐc[R] C}, (↑e₁₂).trans ↑e₂₃ = ↑(e₁₂.trans e₂₃)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- This lemma follows from the preexisting `Unique` instance, but
it is often convenient to use it directly as `apply toUnit_unique` forcing
lean to do the necessary elaboration.
 -/
CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C]
  {X : C} (f g : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C), f = g
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOp_left_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
  {X_1 Y : SimplexCategoryᵒᵖ} (f : X_1 ⟶ Y), X.leftOp.left.map f = (X.right.map f.unop).unop
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instLocallyPathConnectedSpace : LocallyPathConnectedSpace UpperHalfPlane
-- Mathlib.Data.Seq.Computation
Computation.orElse.eq_1 : ∀ {α : Type u} (c₁ : Computation α) (c₂ : Unit → Computation α),
  c₁.orElse c₂ =
    Computation.corec
      (fun x =>
        match x with
        | (c₁, c₂) =>
          match c₁.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr c₁' =>
            match c₂.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr c₂' => Sum.inr (c₁', c₂'))
      (c₁, c₂ ())
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- The function `Real.arcosh` is real analytic.  -/
Real.analyticAt_arcosh : ∀ {x : ℝ}, x ∈ Set.Ioi 1 → AnalyticAt ℝ Real.arcosh x