mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
Lean.Parser.Term.inaccessible.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Subtype.OrderExtra
instOrdSubtype : {α : Type u} → [Ord α] → {P : α → Prop} → Ord (Subtype P)
-- Mathlib.Order.Monotone.Monovary
monovaryOn_univ : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  MonovaryOn f g Set.univ ↔ Monovary f g
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mkCLM_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] (a : M),
  (SeparationQuotient.mkCLM R M) a = SeparationQuotient.mk a
-- Mathlib.Data.Matrix.Mul
dotProduct_add : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (u v w : m → α),
  u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instEpiπTruncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], CategoryTheory.Epi (K.πTruncGE e)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.mk.inj : ∀ {R : Type u} {A : Type v} {B : Type w} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra R A} {inst_4 : Algebra R B} {toRingHom : A →+* B}
  {commutes' : ∀ (r : R), (↑↑toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r} {toRingHom_1 : A →+* B}
  {commutes'_1 : ∀ (r : R), (↑↑toRingHom_1).toFun ((algebraMap R A) r) = (algebraMap R B) r},
  { toRingHom := toRingHom, commutes' := commutes' } = { toRingHom := toRingHom_1, commutes' := commutes'_1 } →
    toRingHom = toRingHom_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_1.splitter : (motive : Std.Tactic.BVDecide.BVBinPred → Sort u_1) →
  (op : Std.Tactic.BVDecide.BVBinPred) →
    (Unit → motive Std.Tactic.BVDecide.BVBinPred.eq) → (Unit → motive Std.Tactic.BVDecide.BVBinPred.ult) → motive op
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- An equivalent expression of `IsProperSemilinearSet` in terms of `Finset` instead of
`Set.Finite`.  -/
isProperSemilinearSet_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M},
  IsProperSemilinearSet s ↔ ∃ S, (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ ↑S
-- Std.Data.Iterators.Lemmas.Consumers.Set
_private.Std.Data.Iterators.Lemmas.Consumers.Set.0.Std.Iter.toTreeSet.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] (it : Std.Iter β)
  (cmp : β → β → Ordering), it.toTreeSet cmp = (it.toIterM.toTreeSet cmp).run
-- Mathlib.LinearAlgebra.Ray
/-- `someVector` is nonzero.  -/
Module.Ray.someVector_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : Module.Ray R M), x.someVector ≠ 0
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.isLocalization_ofField : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K], IsLocalization S ↥(Localization.subalgebra.ofField K S hS)
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- Global integral curves are unique.

If a continuously differentiable vector field `v` admits two global integral curves
`γ γ' : ℝ → M`, and `γ t₀ = γ' t₀` for some `t₀`, then `γ` and `γ'` are equal.  -/
isMIntegralCurve_eq_of_contMDiff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [T2Space M],
  (∀ (t : ℝ), I.IsInteriorPoint (γ t)) →
    (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) → IsMIntegralCurve γ v → IsMIntegralCurve γ' v → γ t₀ = γ' t₀ → γ = γ'
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_add : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f g : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I),
  BoxIntegral.integralSum (f + g) vol π = BoxIntegral.integralSum f vol π + BoxIntegral.integralSum g vol π
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainNonUnitalAlgHom.eq_1 : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Add M] [inst_4 : Add N] (f : M →ₙ+ N),
  AddMonoidAlgebra.mapDomainNonUnitalAlgHom R A f =
    { toFun := (AddMonoidAlgebra.mapDomainNonUnitalRingHom A f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.NumberTheory.SumTwoSquares
/-- The set of sums of two squares is closed under multiplication in any commutative ring.
See also `sq_add_sq_mul_sq_add_sq`.  -/
sq_add_sq_mul : ∀ {R : Type u_1} [inst : CommRing R] {a b x y u v : R},
  a = x ^ 2 + y ^ 2 → b = u ^ 2 + v ^ 2 → ∃ r s, a * b = r ^ 2 + s ^ 2
-- Mathlib.Order.Concept
intentClosure_isClosed : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set β),
  (intentClosure r).IsClosed x = (upperPolar r (lowerPolar r x) = x)
-- Mathlib.Topology.Instances.NNReal.Lemmas
tendsto_real_toNNReal : ∀ {α : Type u_2} {f : Filter α} {m : α → ℝ} {x : ℝ},
  Filter.Tendsto m f (nhds x) → Filter.Tendsto (fun a => (m a).toNNReal) f (nhds x.toNNReal)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.comp_inl_add_comp_inr : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (L : M₁ × M₂ →L[R] M₃) (v : M₁ × M₂),
  (L ∘SL ContinuousLinearMap.inl R M₁ M₂) v.1 + (L ∘SL ContinuousLinearMap.inr R M₁ M₂) v.2 = L v
-- Init.Core
UInt8.ofBitVec.injEq : ∀ (toBitVec toBitVec_1 : BitVec 8), ({ toBitVec := toBitVec } = { toBitVec := toBitVec_1 }) = (toBitVec = toBitVec_1)
-- Mathlib.Logic.Basic
not_iff : ∀ {a b : Prop}, ¬(a ↔ b) ↔ (¬a ↔ b)
-- Plausible.Testable
/-- Increase the number of shrinking steps in a test result.
 -/
Plausible.Testable.addShrinks : {p : Prop} → ℕ → Plausible.TestResult p → Plausible.TestResult p
-- Mathlib.Logic.Relation
Acc.of_downward_closed : ∀ {α : Type u_1} {β : Type u_2} {rβ : β → β → Prop} (f : α → β),
  (∀ {a : α} {b : β}, rβ b (f a) → ∃ c, f c = b) → ∀ (a : α), Acc (InvImage rβ f) a → Acc rβ (f a)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : SizeOf C] (r : S.X₂ ⟶ S.X₁) (s : S.X₃ ⟶ S.X₂)
  (f_r :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam)
  (s_g :
    autoParam (CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam)
  (id :
    autoParam
      (CategoryTheory.CategoryStruct.comp r S.f + CategoryTheory.CategoryStruct.comp S.g s =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam),
  sizeOf { r := r, s := s, f_r := f_r, s_g := s_g, id := id } =
    1 + sizeOf r + sizeOf s + sizeOf f_r + sizeOf s_g + sizeOf id
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.replicate.inj : ∀ {w w' n : ℕ} {expr : Std.Tactic.BVDecide.BVExpr w} {h : w' = w * n} {w_1 n_1 : ℕ}
  {expr_1 : Std.Tactic.BVDecide.BVExpr w_1} {h_1 : w' = w_1 * n_1},
  Std.Tactic.BVDecide.BVExpr.replicate n expr h = Std.Tactic.BVDecide.BVExpr.replicate n_1 expr_1 h_1 →
    w = w_1 ∧ n = n_1 ∧ expr ≍ expr_1
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_eq_measure_smaller_of_between_null_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ (s₃ \ s₁) = 0 → μ s₁ = μ s₂
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (v : Int.Internal.Linear.Var)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match Int.Internal.Linear.Expr.var v with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_2 v
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_injective : ∀ {R : Type u_2} [inst : NonAssocRing R], Function.Injective Subring.unop
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_prod_of_mem : ∀ {α : Type u_2} [inst : CommMonoid α] {m : Multiset α} {a : α},
  a ∈ m → ∀ [inst_1 : Preorder α] [CanonicallyOrderedMul α], a ≤ m.prod
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContDiffWithinAtProp.eq_1 : ∀ {𝕜 : 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) {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') (n : WithTop ℕ∞) (f : H → H') (s : Set H) (x : H),
  ContDiffWithinAtProp I I' n f s x = ContDiffWithinAt 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
-- Lean.SubExpr
/-- A subexpression of the type of one of the hypotheses.  -/
Lean.SubExpr.GoalLocation.hypType : Lean.FVarId → Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre F E) (CategoryTheory.Limits.colimit.desc F c) =
    CategoryTheory.Limits.colimit.desc (E.comp F) (CategoryTheory.Limits.Cocone.whisker E c)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.  -/
OrderMonoidIso.symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) (x : α), e.symm (e x) = x
-- Mathlib.GroupTheory.Perm.ConjAct
Equiv.Perm.conj_smul_range_ofSubtype : ∀ {α : Type u_1} [inst : DecidableEq α] [Finite α] (g : Equiv.Perm α) (s : Finset α),
  ConjAct.toConjAct g • Equiv.Perm.ofSubtype.range = Equiv.Perm.ofSubtype.range
-- Std.Time.Date.Unit.Week
Std.Time.Week.instNegOffset : Neg Std.Time.Week.Offset
-- Mathlib.Data.List.Nodup
List.Nodup.erase_getElem : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α},
  l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
-- Lean.Meta.MethodSpecs
/-- Name of the implementation function  -/
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.name : Lean.MethodSpecTheorem✝ → Lean.Name
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termπ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `sUnion`).  -/
MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set (Set α)},
  S.Countable → ⋃₀ S = Set.univ → (μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : MulOneClass α] →
          [inst_3 : MulOneClass β] → (toMonoidHom : α →* β) → Monotone (↑toMonoidHom).toFun → α →*o β
-- Mathlib.Topology.Category.TopCat.EffectiveEpi
Topology.IsQuotientMap.liftEquiv.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} (hf : Topology.IsQuotientMap ⇑f), hf.liftEquiv = hf.liftEquiv
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.eq_mul_weierstrassDiv_add_weierstrassMod : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A) {g : PowerSeries A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    ∀ [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], f = g * (f /ʷ g) + ↑(f %ʷ g)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.card_interedges_finpartition_right : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {t : Finset β}
  [inst_1 : DecidableEq β] (s : Finset α) (P : Finpartition t),
  (Rel.interedges r s t).card = ∑ b ∈ P.parts, (Rel.interedges r s b).card
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.bind_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C)
  {S : CategoryTheory.Sieve X} {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → CategoryTheory.Sieve Y},
  S ∈ J X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : S.arrows f), R H ∈ J Y) → CategoryTheory.Sieve.bind S.arrows R ∈ J X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastShiftRightConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.two_le_chromaticNumber_iff_ne_bot : ∀ {V : Type u} {G : SimpleGraph V}, 2 ≤ G.chromaticNumber ↔ G ≠ ⊥
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.resolution_complex : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g),
  (Rep.FiniteCyclicGroup.resolution k g hg).complex =
    (Rep.FiniteCyclicGroup.chainComplexFunctor k g).obj (Rep.leftRegular k G)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearEquivAt_apply' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e]
  (x : Bundle.TotalSpace F E) (hx : x ∈ e.source),
  (Bundle.Trivialization.continuousLinearEquivAt R e x.proj ⋯) x.snd = (↑e x).2
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLEMap_comp_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'] [inst_6 : CategoryTheory.Limits.HasZeroObject C]
  {Z : HomologicalComplex C c'} (h : M.truncLE e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLEMap (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLEMap φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLEMap φ' e) h)
-- Mathlib.Data.Part
Part.ofOption_dom : ∀ {α : Type u_4} (o : Option α), (↑o).Dom ↔ o.isSome = true
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (a : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a))
      (d.transitionMap hij) =
    CategoryTheory.CategoryStruct.comp ((d.trans hij).app a) ((d.cocone j).ι.app a)
-- Mathlib.Algebra.Central.End
LinearEquiv.conjAlgEquiv_ext_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : CommSemiring S] [inst_5 : Module S M] [inst_6 : SMulCommClass R S M]
  [inst_7 : Algebra S R] [inst_8 : IsScalarTower S R M] {M₂ : Type u_4} [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] [inst_11 : Module S M₂] [inst_12 : SMulCommClass R S M₂] [inst_13 : IsScalarTower S R M₂]
  [Algebra.IsCentral S R] {f g : M ≃ₗ[R] M₂},
  LinearEquiv.conjAlgEquiv S f = LinearEquiv.conjAlgEquiv S g ↔ ∃ α, ⇑f = α • ⇑g
-- Std.Http.Data.Status
Std.Http.instReprStatus : Repr Std.Http.Status
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- An additive free group basis for `G` over `ι` is associated to a map `ι → G` recording the
images of the generators.  -/
FreeAddGroupBasis.instFunLike : {ι : Type u_1} → {G : Type u_3} → [inst : AddGroup G] → FunLike (FreeAddGroupBasis ι G) ι G
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_of_not_fg : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  ¬p.FG → p.spanFinrank = 0
-- Aesop.Forward.SlotIndex
Aesop.instBEqSlotIndex.beq : Aesop.SlotIndex → Aesop.SlotIndex → Bool
-- Mathlib.Data.Finset.NAry
Finset.image_subset_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {a : α}, a ∈ s → Finset.image (fun b => f a b) t ⊆ Finset.image₂ f s t
-- Init.Data.String.Lemmas.FindPos
String.posLT_eq_posLE : ∀ {s : String} {p : String.Pos.Raw} {h : 0 < p}, s.posLT p h = s.posLE p.dec
-- Mathlib.GroupTheory.Transfer
Subgroup.transferFunction_apply : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G) (q : G ⧸ H),
  H.transferFunction g q =
    g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) q).fst)
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- The chosen structural isomorphism between to 1-morphisms.  -/
CategoryTheory.BicategoricalCoherence.iso : {B : Type u} →
  {inst : CategoryTheory.Bicategory B} →
    {a b : B} → {f g : a ⟶ b} → [self : CategoryTheory.BicategoricalCoherence f g] → f ≅ g
-- Mathlib.SetTheory.Ordinal.Notation
/-- The `oadd` pseudo-constructor for `NONote`  -/
NONote.oadd : (e : NONote) → ℕ+ → (a : NONote) → a.below e → NONote
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- A special case of `CategoryTheory.Limits.cokernel.map_desc` adapted to `explicitCokernel`.  -/
SemiNormedGrp.ExplicitCoker.map_desc : ∀ {A B C D B' D' : SemiNormedGrp} {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D}
  {h : CategoryTheory.CategoryStruct.comp fab fbd = CategoryTheory.CategoryStruct.comp fac fcd} {fbb' : B ⟶ B'}
  {fdd' : D ⟶ D'} {condb : CategoryTheory.CategoryStruct.comp fab fbb' = 0}
  {condd : CategoryTheory.CategoryStruct.comp fcd fdd' = 0} {g : B' ⟶ D'},
  CategoryTheory.CategoryStruct.comp fbb' g = CategoryTheory.CategoryStruct.comp fbd fdd' →
    CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelDesc condb) g =
      CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernel.map h)
        (SemiNormedGrp.explicitCokernelDesc condd)
-- Lean.Util.Diff
Lean.Diff.Action.insert.sizeOf_spec : sizeOf Lean.Diff.Action.insert = 1
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.mk.inj : ∀ {zonesPaths zonesPaths_1 : Array System.FilePath},
  { zonesPaths := zonesPaths } = { zonesPaths := zonesPaths_1 } → zonesPaths = zonesPaths_1
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (A : CategoryTheory.Mon C) → Inhabited (Bimod A A)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.equivLike_neg_eq_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), EquivLike.inv f = ⇑f.symm
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mul_helper : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {a₁ b₁ a₂ b₂ a₃ b₃ a₄ b₄ k₁ k₂ : α},
  a₁ + b₃ + k₁ = b₁ + a₃ + k₁ →
    a₂ + b₄ + k₂ = b₂ + a₄ + k₂ →
      ∃ k, a₁ * a₂ + b₁ * b₂ + (a₃ * b₄ + b₃ * a₄) + k = a₁ * b₂ + b₁ * a₂ + (a₃ * a₄ + b₃ * b₄) + k
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.radical_mul_divRadical : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {a : E}, UniqueFactorizationMonoid.radical a * EuclideanDomain.divRadical a = a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.code : Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.Code
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State.postponed : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State → Array (Lean.Expr × Lean.Expr)
-- Std.Http.Protocol.H1.Message
/-- Returns a copy of the message head with the headers replaced.
 -/
Std.Http.Protocol.H1.Message.Head.setHeaders : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Message.Head dir → Std.Http.Headers → Std.Http.Protocol.H1.Message.Head dir
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.hasOfPostcompProperty_monomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange], P.HasOfPostcompProperty (CategoryTheory.MorphismProperty.monomorphisms C)