mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Format.Modifier
Std.Time.Modifier.V.injEq : ∀ (presentation presentation_1 : Std.Time.ZoneId),
  (Std.Time.Modifier.V presentation = Std.Time.Modifier.V presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The canonical function `M → N → M ⊗ N`.  -/
TensorProduct.«term_⊗ₜ[_]_» : Lean.TrailingParserDescr
-- Init.Data.Vector.Lemmas
Vector.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β} {g : β → γ} {as : Vector α n},
  Vector.map g (Vector.map f as) = Vector.map (g ∘ f) as
-- Batteries.Data.ByteArray
ByteArray.getElem_eq_data_getElem : ∀ {i : ℕ} (a : ByteArray) (h : i < a.size), a[i] = a.data[i]
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.Hom.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : CategoryTheory.Join C D → CategoryTheory.Join C D → Sort u_5) (x y : C)
  (h_1 : (x y : C) → motive (CategoryTheory.Join.left x) (CategoryTheory.Join.left y))
  (h_2 : (x y : D) → motive (CategoryTheory.Join.right x) (CategoryTheory.Join.right y))
  (h_3 : (a : C) → (a_1 : D) → motive (CategoryTheory.Join.left a) (CategoryTheory.Join.right a_1))
  (h_4 : (a : D) → (a_1 : C) → motive (CategoryTheory.Join.right a) (CategoryTheory.Join.left a_1)),
  (match CategoryTheory.Join.left x, CategoryTheory.Join.left y with
    | CategoryTheory.Join.left x, CategoryTheory.Join.left y => h_1 x y
    | CategoryTheory.Join.right x, CategoryTheory.Join.right y => h_2 x y
    | CategoryTheory.Join.left a, CategoryTheory.Join.right a_1 => h_3 a a_1
    | CategoryTheory.Join.right a, CategoryTheory.Join.left a_1 => h_4 a a_1) =
    h_1 x y
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.mkAntiquot.formatter' : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.End
AddAut.addConj_symm_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (AddEquiv.symm (AddAut.addConj g)) h = -g + h + g
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y Y' Z Z' : C} [inst_2 : CategoryTheory.ExactPairing Y Y']
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) (g : Z ⟶ Z'),
  (CategoryTheory.tensorRightHomEquiv X Y Y' Z') (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.tensorRightHomEquiv X Y Y' Z) f)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Y')
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (E : L.LeftExtension F) (c : C),
  (CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso G F L E c).hom.hom =
    CategoryTheory.CategoryStruct.id (G.obj (E.right.obj c))
-- Mathlib.MeasureTheory.Measure.AddContent
/-- An `addContent C` on a `SetSemiring C` is sub-additive.  -/
MeasureTheory.addContent_sUnion_le_sum : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] [inst_1 : PartialOrder G]
  [CanonicallyOrderedAdd G] {m : MeasureTheory.AddContent G C},
  MeasureTheory.IsSetSemiring C → ∀ (J : Finset (Set α)), ↑J ⊆ C → ⋃₀ ↑J ∈ C → m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure], IsUnifLocDoublingMeasure μ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mk.injEq : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (s : ↑P.II) (rank_s : f.rank s = i) (s_1 : ↑P.II) (rank_s_1 : f.rank s_1 = i),
  ({ s := s, rank_s := rank_s } = { s := s_1, rank_s := rank_s_1 }) = (s = s_1)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Inversion `x ↦ x⁻¹` as an `IsometryEquiv`.  -/
IsometryEquiv.inv : (G : Type v) →
  [inst : Group G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricSMul G G] → [IsIsometricSMul Gᵐᵒᵖ G] → G ≃ᵢ G
-- Mathlib.Order.Interval.Set.UnorderedInterval
MonotoneOn.mapsTo_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  MonotoneOn f (Set.uIcc a b) → Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
-- Lean.Elab.Tactic.Induction
/-- Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
```
Return `some inductionAlts'` if one of the alternatives has multiple LHSs or no RHS.
In the new `inductionAlts'` all alternatives have a single LHS.

Remark: the `RHS` of alternatives with multi LHSs is copied.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.expandInductionAlts? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
sigPos_le_finrank : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M), sigPos Q ≤ Module.finrank R M
-- Mathlib.Data.Stream.Init
Stream'.get_append_right : ∀ {α : Type u} (n : ℕ) (x : List α) (a : Stream' α), (x ++ₛ a).get (x.length + n) = a.get n
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Creates an `ExprInfo` using the current context.  -/
Lean.Meta.RefinedDiscrTree.mkExprInfo : Lean.Expr → List Lean.FVarId → Lean.MetaM Lean.Meta.RefinedDiscrTree.ExprInfo
-- Mathlib.Order.Antisymmetrization
Antisymmetrization.prodEquiv_apply_mk : ∀ (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst_1 : Preorder β] {ab : α × β},
  (Antisymmetrization.prodEquiv α β) ⟦ab⟧ = (⟦ab.1⟧, ⟦ab.2⟧)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {k k' : α} {fallback : β k'},
  (↑m).WF →
    ∀ {f : Option (β k) → Option (β k)},
      (m.alter k f).getD k' fallback =
        if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_hom_inv_id' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.inv f)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id V))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id V))
-- Mathlib.Algebra.Group.Pi.Basic
Subsingleton.pi_single_eq : ∀ {I : Type u} {α : Type u_4} [inst : DecidableEq I] [Subsingleton I] [inst_2 : Zero α] (i : I) (x : α),
  Pi.single i x = fun x_1 => x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflects_limits_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), Subsingleton (CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
-- Mathlib.Order.Minimal
minimal_mem_image_monotone : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) → Minimal (fun x => x ∈ s) x → Minimal (fun x => x ∈ f '' s) (f x)
-- Batteries.Data.Nat.Bisect
Nat.avg_le_right : ∀ {a b : ℕ}, a ≤ b → a.avg b ≤ b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_diff_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.zpow_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ℤ), (f ^ n).toGerm = f.toGerm ^ n
-- Mathlib.Data.Finset.Disjoint
Finset.singleton_disjUnion : ∀ {α : Type u_2} (a : α) (t : Finset α) (h : Disjoint {a} t), {a}.disjUnion t h = Finset.cons a t ⋯
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminormAux.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))),
  PiTensorProduct.projectiveSeminormAux p = (List.map (fun p => ‖p.1‖ * ∏ i, ‖p.2 i‖) (FreeAddMonoid.toList p)).sum
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Go through rest of type, alpha renaming and setting options along the spine.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallParamsWithSignature.processSpine : Lean.PrettyPrinter.Delaborator.OptionsPerPos →
  Lean.SubExpr → Lean.MetaM (Lean.PrettyPrinter.Delaborator.OptionsPerPos × Lean.Expr)
-- Init.Core
/-- Constructs a dependent pair.

Using this constructor in a context in which the type is not known usually requires a type
ascription to determine `β`. This is because the desired relationship between the two values can't
generally be determined automatically.
 -/
Sigma.mk : {α : Type u} → {β : α → Type v} → (fst : α) → β fst → Sigma β
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Finite.measurableSet_sUnion : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)}, s.Finite → (∀ t ∈ s, MeasurableSet t) → MeasurableSet (⋃₀ s)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Cylinders are open when `A` is discrete.  -/
SymbolicDynamics.FullShift.isOpen_cylinder : ∀ {A : Type u_1} {G : Type u_2} [inst : TopologicalSpace A] [DiscreteTopology A] (U : Finset G) (x : G → A),
  IsOpen (SymbolicDynamics.FullShift.cylinder U x)
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.desc_toCocone_desc_app : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  (c : CategoryTheory.Limits.Cocone F) [inst_1 : DecidableEq J] {A : Type w} [inst_2 : AddCommGroup A]
  (f : AddCommGrpCat.Colimits.Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c) (x : AddCommGrpCat.Colimits.Quot F),
  (CategoryTheory.ConcreteCategory.hom (hc.desc (AddCommGrpCat.Colimits.toCocone F f)))
      ((AddCommGrpCat.Colimits.Quot.desc F c) x) =
    f x
-- Mathlib.FieldTheory.Fixed
FixedPoints.instIsInvariantSubfieldSubfield : ∀ (M : Type u) [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F],
  IsInvariantSubfield M (FixedPoints.subfield M F)
-- Mathlib.Algebra.Category.Grp.Shrink
/-- The natural transformation `GrpCat.shrinkFunctor.{w} F ⟶ GrpCat.shrinkFunctor.{w} G`
induces by a natural transformation `τ : F ⟶ G` between `w`-small functors to monoids.  -/
GrpCat.shrinkFunctorMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C GrpCat} →
      (F ⟶ G) →
        [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] →
          [inst_2 : ∀ (X : C), Small.{w, w'} ↑(G.obj X)] →
            GrpCat.shrinkFunctor.{w, w', v, u} F ⟶ GrpCat.shrinkFunctor.{w, w', v, u} G
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec.addMonoidHomLeft_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] (v : n → α)
  (M : Matrix m n α) (a : m), (Matrix.mulVec.addMonoidHomLeft v) M a = M.mulVec v a
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.neg_empty : ∀ {α : Type u_1} [inst : Neg α] (v : Fin 0 → α), -v = ![]
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- The children of the root of a W tree  -/
PFunctor.W.children : {P : PFunctor.{uA, uB}} → (x : P.W) → P.B x.head → P.W
-- Init.Data.Int.DivMod.Lemmas
Int.neg_add_bmod_self : ∀ (a : ℕ) (b : ℤ), (-↑a + b).bmod a = b.bmod a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_union_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s t : Set α},
  MeasureTheory.AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔
    MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ∧ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNNNorm_mul : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalNormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R]
  [Nontrivial R], ‖ContinuousLinearMap.mul 𝕜 R‖₊ = 1
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.step_append : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] {it₁ : Std.Iter β}
  {it₂ : Std.Iter β},
  (it₁.append it₂).step =
    match it₁.step with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => Std.PlausibleIterStep.yield (it₁'.append it₂) out ⋯
    | ⟨Std.IterStep.skip it₁', h⟩ => Std.PlausibleIterStep.skip (it₁'.append it₂) ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.appendSnd α₁ it₂) ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Ordered.distinctKeys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Ord α] [Std.LawfulBEqOrd α]
  {l : Std.DTreeMap.Internal.Impl α β}, l.Ordered → Std.Internal.List.DistinctKeys l.toListModel
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coeAddMonoidHom_injective`. -/
ContDiffMapSupportedIn.coeHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], Function.Injective ⇑(FunLike.coeAddMonoidHom F α β)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
isAddCyclic_right_of_prod : ∀ (M : Type u_4) (N : Type u_5) [inst : AddGroup M] [inst_1 : AddGroup N] [cyc : IsAddCyclic (M × N)], IsAddCyclic N
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
neighborhood of `x`.  -/
HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero : ∀ {𝕜 : 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}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFiniteFPowerSeriesAt f pf x 0 → f =ᶠ[nhds x] 0
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.image.ι_comp_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  {Z : C} (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) g = 0 ↔
    CategoryTheory.CategoryStruct.comp f g = 0
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Trivialization.memTrivializationAtlas_continuousAlternatingMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂],
  MemTrivializationAtlas (Bundle.Trivialization.continuousAlternatingMap 𝕜 ι e₁ e₂)
-- Mathlib.CategoryTheory.InducedCategory
/-- The underlying morphism.  -/
CategoryTheory.InducedCategory.Hom.hom : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → {X Y : CategoryTheory.InducedCategory D F} → X.Hom Y → (F X ⟶ F Y)
-- Init.Data.BitVec.Lemmas
BitVec.ult_iff_lt : ∀ {w : ℕ} {x y : BitVec w}, x.ult y = true ↔ x < y
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_left.inj : ∀ {B : Type u} {inst : Quiver B} {a b c : CategoryTheory.FreeBicategory B} {f : a ⟶ b} {g h : b ⟶ c}
  {η η_1 : CategoryTheory.FreeBicategory.Hom₂ g h},
  CategoryTheory.FreeBicategory.Hom₂.whisker_left f η = CategoryTheory.FreeBicategory.Hom₂.whisker_left f η_1 → η = η_1
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_map : ∀ {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] (a : CategoryTheory.Functor (C × D) E) (k : D) {X Y : C}
  (f : X ⟶ Y),
  ((CategoryTheory.Functor.curryingFlipEquiv.symm a).obj k).map f =
    a.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id k))
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  Matrix.mulVecLin 1 = LinearMap.id
-- Mathlib.Tactic.Translate.GuessName
/-- We need to fix a few abbreviations after applying `nameDict`, i.e. replacing `ZeroLE` by `Nonneg`.
This dictionary contains these fixes.
The input should contain entries that is in `lowerCamelCase` (e.g. `ltzero`; the initial sequence
of capital letters should be lower-cased) and the output should be in `UpperCamelCase`
(e.g. `LTZero`).
When applying the dictionary, we lower-case the output if the input was also given in lower-case.
 -/
Mathlib.Tactic.GuessName.GuessNameData.abbreviationDict : Mathlib.Tactic.GuessName.GuessNameData → Std.HashMap String String
-- Mathlib.Data.WSeq.Defs
_private.Mathlib.Data.WSeq.Defs.0.Stream'.WSeq.length.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) →
    (x : Option (Stream'.Seq1 (Option α))) →
      (Unit → motive none) →
        ((s' : Stream'.Seq (Option α)) → motive (some (none, s'))) →
          ((val : α) → (s' : Stream'.Seq (Option α)) → motive (some (some val, s'))) → motive x
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderCoproductsFunctorMonomorphismsOfHasCoproductsOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u'') [inst_1 : CategoryTheory.Category.{v'', u''} J]
  [CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u', v, u} (CategoryTheory.MorphismProperty.monomorphisms C)]
  [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u', max u'' v, max (max (max u u'') v) v''}
    (CategoryTheory.MorphismProperty.monomorphisms (CategoryTheory.Functor J C))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insert_equiv_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α} {v : β k}, (↑(m₁.insert k v)).Equiv ↑(m₂.insert k v)
-- Init.Data.SInt.Lemmas
Int16.ofNat_int8ToNatClampNeg : ∀ (x : Int8), 0 ≤ x → Int16.ofNat x.toNatClampNeg = x.toInt16
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add : ∀ {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) (x y : K),
  { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm (x + y)) } =
    { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x) } +
      { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm y) }
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofIntLE : ∀ {n : ℤ} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt), (ISize.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.cliqueFree : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ {n : ℕ}, 3 ≤ n → G.CliqueFree n
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.coe_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), ↑(a - b) = ↑a - ↑b
-- Mathlib.CategoryTheory.Presentable.Presheaf
CategoryTheory.Presheaf.instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [inst_3 : CategoryTheory.Limits.HasCoproducts A]
  (κ : Cardinal.{w}) [inst_4 : Fact κ.IsRegular] (X : C) (M : A) [CategoryTheory.IsCardinalPresentable M κ],
  CategoryTheory.IsCardinalPresentable (CategoryTheory.Presheaf.freeYoneda X M) κ
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.rightUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.LaxTrans.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.mkProof.goUnfold : Lean.Name → Lean.MVarId → Lean.MetaM Unit
-- Mathlib.RingTheory.Smooth.Locus
Algebra.isOpen_smoothLocus : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A], IsOpen (Algebra.smoothLocus R A)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow f = 0
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Inc.mono : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β}, H ≤ G → H.Inc e x → G.Inc e x
-- Init.Core
Pi.instSubsingleton : ∀ {α : Sort u} {β : α → Sort v} [∀ (a : α), Subsingleton (β a)], Subsingleton ((a : α) → β a)
-- Init.Data.UInt.Basic
/-- Converts a `Fin UInt16.size` into the corresponding `UInt16`.  -/
UInt16.ofFin : Fin UInt16.size → UInt16