mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
analytic at `x`.  -/
AnalyticAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E},
  AnalyticAt 𝕜 g (f x) → AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (g ∘ f) x
-- Mathlib.LinearAlgebra.Determinant
/-- Multiplying a map by a scalar `c` multiplies its determinant by `c ^ dim M`.  -/
LinearMap.det_smul : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] [Module.Free A M]
  (c : A) (f : M →ₗ[A] M), LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f
-- Mathlib.Data.Fin.Basic
Fin.cast_injective : ∀ {k l : ℕ} (h : k = l), Function.Injective (Fin.cast h)
-- Init.Data.List.Nat.Range
List.range'_eq_singleton_iff : ∀ {s n a : ℕ}, List.range' s n = [a] ↔ s = a ∧ n = 1
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_sub_one : ∀ (r : ENNReal), ⌊r - 1⌋ₑ = ⌊r⌋ₑ - 1
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_eq_map_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H K : AddSubgroup G},
  AddSubgroup.map f H = AddSubgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalars_apply : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B) (x : A), (AlgEquiv.restrictScalars R f) x = f x
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A}
  (φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T))
  (hφ :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
        CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) =
          φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x))
      _auto_52✝)
  (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.presheafFiberDesc φ hφ) = φ X x
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The underlying object of the base category.  -/
CategoryTheory.Cokleisli.of : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {U : CategoryTheory.Comonad C} → CategoryTheory.Cokleisli U → C
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_id : ∀ {α : Type u_1}, Quiver.SingleObj.toPrefunctor id = 𝟭q (Quiver.SingleObj α)
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under the modulo operation.  -/
Dioph.«term_D%_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RocSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.Order.Basic
PartialOrder.ext : ∀ {α : Type u_2} {A B : PartialOrder α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B
-- Mathlib.Algebra.Category.Ring.Basic
/-- Typecheck a `RingHom` as a morphism in `CommSemiRingCat`.  -/
CommSemiRingCat.ofHom : {R S : Type u} →
  [inst : CommSemiring R] → [inst_1 : CommSemiring S] → (R →+* S) → (CommSemiRingCat.of R ⟶ CommSemiRingCat.of S)
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.matchesSimpTheorem? : Aesop.RuleFilter → Option Lean.Name
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.of_measure_zero : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε], μ s = 0 → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Topology.Sets.Opens
/-- The point `x` belongs to every `U : TopologicalSpace.OpenNhdsOf x`.  -/
TopologicalSpace.OpenNhdsOf.mem' : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} (self : TopologicalSpace.OpenNhdsOf x), x ∈ self.carrier
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxInv.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S], IsLocalization.Away.auxInv✝ S r = IsLocalization.Away.auxInv✝ S r
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.add_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (x y z : M), (B (x + y)) z = (B x) z + (B y) z
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.not_differentiableAt_inv_log_zero : ¬DifferentiableAt ℝ (fun x => (Real.log x)⁻¹) 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ext_iff : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} {inst : LinearOrder ι} {f : P.RankFunction ι} {i : ι}
  {x y : f.Cell i}, x = y ↔ x.s = y.s
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.cancel_left : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃}
  {g g' : M₁ →ₛₗ[σ₁₂] M₂}, Function.Injective ⇑f → (f ∘ₛₗ g = f ∘ₛₗ g' ↔ g = g')
-- Lean.Parser.Syntax
Lean.Parser.Command.elab.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.mk.inj : ∀ {p : Int.Internal.Linear.Poly} {h : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof} {p_1 : Int.Internal.Linear.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof}, { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_neg_right`. -/
Asymptotics.IsBigOWith.neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith c l f g' → Asymptotics.IsBigOWith c l f fun x => -g' x
-- Mathlib.Geometry.Manifold.Submersion
/-- A `C^n` submersion at `x` is `C^n` at `x`.  -/
Manifold.IsSubmersionAtOfComplement.contMDiffAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M}, Manifold.IsSubmersionAtOfComplement F I J n f x → ContMDiffAt I J n f x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
derivWithin_sinh : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.sinh (f x)) s x = Real.cosh (f x) * derivWithin f s x
-- Lean.Meta.Tactic.Contradiction
/-- Try to close the current goal by looking for a proof of `False` nested in a `False.Elim` application in the target.
Return `true` iff the goal has been closed.
 -/
_private.Lean.Meta.Tactic.Contradiction.0.Lean.Meta.nestedFalseElim : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Tactic.NormNum.Result
/-- The element is equal to the coercion of the natural number.  -/
Mathlib.Meta.NormNum.IsNat.out : ∀ {α : Type u} [inst : AddMonoidWithOne α] {a : α} {n : ℕ}, Mathlib.Meta.NormNum.IsNat a n → a = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsTerminal.comp_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsTerminal Z) {X Y : C}
  (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (t.from Y) = t.from X
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- **Alias** of `CategoryTheory.Limits.ImageMap.mk.injEq`. -/
CategoryTheory.Limits.ImageMap.mk.injEq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
  (map_ι :
    autoParam
      (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam)
  (map_1 : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
  (map_ι_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp map_1 (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam),
  ({ map := map, map_ι := map_ι } = { map := map_1, map_ι := map_ι_1 }) = (map = map_1)
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : NatCast F] (n : ℕ), Differentiable 𝕜 ↑n
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.ListBlank.modifyNth.match_1.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (motive : ℕ → Turing.ListBlank Γ → Sort u_2) (L : Turing.ListBlank Γ)
  (h_1 : (L : Turing.ListBlank Γ) → motive 0 L) (h_2 : (n : ℕ) → (L : Turing.ListBlank Γ) → motive n.succ L),
  (match 0, L with
    | 0, L => h_1 L
    | n.succ, L => h_2 n L) =
    h_1 L
-- Mathlib.Order.Preorder.Chain
isChain_preimage_subtypeVal : ∀ {α : Type u_1} {r : α → α → Prop} (s t : Set α),
  IsChain (fun x1 x2 => r ↑x1 ↑x2) (Subtype.val ⁻¹' t) ↔ IsChain r (s ∩ t)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insertIfNew_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).size ≤ t.size + 1
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `g * q = r` for some power series `q` and some polynomial `r` whose degree is `< n`,
then `q` and `r` are all zero. This implies the uniqueness of Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassDivisorAt I →
    ∀ [IsHausdorff I A] {q : PowerSeries A} {r : Polynomial A},
      r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat → g * q = ↑r → q = 0 ∧ r = 0
-- Mathlib.Combinatorics.Matroid.Dual
/-- The dual of a matroid; the bases are the complements (w.r.t. `M.E`) of the bases of `M`.  -/
Matroid.dual : {α : Type u_1} → Matroid α → Matroid α
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_eq_ofIntTruncate : ∀ {x : ℤ} {h₁ : Int8.minValue.toInt ≤ x} {h₂ : x ≤ Int8.maxValue.toInt}, Int8.ofIntLE x h₁ h₂ = Int8.ofIntClamp x
-- Mathlib.Topology.Compactification.StoneCech
/-- The extension of a function `α → γ` to a function `Ultrafilter α → γ`.
When `γ` is a compact Hausdorff space it will be continuous.  -/
Ultrafilter.extend : {α : Type u} → {γ : Type u_1} → [TopologicalSpace γ] → (α → γ) → Ultrafilter α → γ
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongEpi.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q} [CategoryTheory.Epi f],
  (∀ (X Y : C) (z : X ⟶ Y),
      CategoryTheory.Mono z → ∀ (u : P ⟶ X) (v : Q ⟶ Y) (sq : CategoryTheory.CommSq u f z v), sq.HasLift) →
    CategoryTheory.StrongEpi f
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_eq_self_iff : ∀ (i : Lean.Grind.IntInterval), i.nonEmpty = true → ∀ (x : ℤ), i.wrap x = x ↔ x ∈ i
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- An inductively defined relation on `Pre R M` used to force the initial algebra structure on
the associated quotient.
 -/
TensorAlgebra.Rel : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → FreeAlgebra R M → FreeAlgebra R M → Prop
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- Reinterpret `Additive G ≃+o H` as `G ≃*o Multiplicative H`.  -/
OrderAddMonoidIso.toMultiplicativeRight : {G : Type u_1} →
  {H : Type u_2} →
    [inst : CommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : AddCommMonoid H] → [inst_3 : PartialOrder H] → (Additive G ≃+o H) ≃ (G ≃*o Multiplicative H)
-- Mathlib.Order.Category.PartOrd
PartOrd.hom_ext : ∀ {X Y : PartOrd} {f g : X ⟶ Y}, PartOrd.Hom.hom f = PartOrd.Hom.hom g → f = g
-- Lean.Data.JsonRpc
_private.Lean.Data.JsonRpc.0.Lean.JsonRpc.messageMetaDataParser : String → Std.Internal.Parsec.String.Parser Lean.JsonRpc.MessageMetaData
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedTZifV1 : Inhabited Std.Time.TimeZone.TZif.TZifV1
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₃ =
    n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.orbitRel_le_snd : ∀ (G : Type u_1) (α : Type u_2) (β : Type u_3) [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MulAction G β],
  MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (MulAction.orbitRel G β)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.coreflective' : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful]
  [inst_5 : ∀ (F : CategoryTheory.Functor C H), L.HasPointwiseLeftKanExtension F],
  CategoryTheory.IsIso (L.lanAdjunction H).unit
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The complete graph on `n` vertices has `n.choose 2` edges.  -/
SimpleGraph.card_edgeFinset_top_eq_card_choose_two : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.edgeFinset.card = (Fintype.card V).choose 2
-- Init.Data.Int.Lemmas
Int.negSucc_mul_negSucc : ∀ (m n : ℕ), Int.negSucc m * Int.negSucc n = ↑m.succ * ↑n.succ
-- Mathlib.Order.Basic
/-- **Alias** of `eq_or_lt_of_le'`. -/
LE.le.eq_or_lt' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → a = b ∨ b < a
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- A tensorial operation on sections of a vector bundle respects zero (since it respects scalar
multiplication).  -/
TensorialAt.zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} [VectorBundle 𝕜 F V], TensorialAt I F Φ x → Φ 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.sup_edge_of_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V}, G.Adj s t → G ⊔ SimpleGraph.edge s t = G
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_mul_natCast : ∀ (o : Ordinal.{u_1}), ⨆ n, o * ↑n = o * Ordinal.omega0
-- Std.Sync.Channel
/-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed.  -/
Std.Channel.Sync.instForInOfInhabitedOfMonadOfMonadLiftTBaseIO : {α : Type} → {m : Type → Type u_1} → [Inhabited α] → [Monad m] → [MonadLiftT BaseIO m] → ForIn m (Std.Channel.Sync α) α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelEpiComp_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Epi f] [inst_3 : CategoryTheory.Limits.HasCokernel g],
  (CategoryTheory.Limits.cokernelEpiComp f g).inv =
    CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)) ⋯
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.iInter₂ : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {ι : Sort u_7} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set X},
  (∀ (i : ι) (j : κ i), Convexity.IsConvexSet R (s i j)) → Convexity.IsConvexSet R (⋂ i, ⋂ j, s i j)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- Given bilinear forms `B₁, B₂` where `B₂` is nondegenerate, `symmCompOfNondegenerate`
is the linear map `B₂ ∘ B₁`.  -/
LinearMap.BilinForm.symmCompOfNondegenerate : {V : Type u_5} →
  {K : Type u_6} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] →
            LinearMap.BilinForm K V → (B₂ : LinearMap.BilinForm K V) → B₂.Nondegenerate → V →ₗ[K] V
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.le_def : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {v : Valuation R Γ₀}
  {a b : WithVal v}, a ≤ b ↔ v a.ofVal ≤ v b.ofVal
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_comp_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y Z : CategoryTheory.Bicategory.InducedBicategory C F} (u : X.Hom Y) (v : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp u v).hom = CategoryTheory.CategoryStruct.comp u.hom v.hom
-- Mathlib.Algebra.Algebra.Prod
/-- Product of algebra isomorphisms.  -/
AlgEquiv.prodCongr : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_5} →
      {T : Type u_6} →
        {A : Type u_7} →
          {B : Type u_8} →
            [inst_1 : Semiring A] →
              [inst_2 : Semiring B] →
                [inst_3 : Semiring S] →
                  [inst_4 : Semiring T] →
                    [inst_5 : Algebra R S] →
                      [inst_6 : Algebra R T] →
                        [inst_7 : Algebra R A] →
                          [inst_8 : Algebra R B] → (S ≃ₐ[R] A) → (T ≃ₐ[R] B) → (S × T) ≃ₐ[R] A × B
-- Mathlib.Algebra.MonoidAlgebra.Lift
/-- `liftNC` as a `RingHom`, for when `f x` and `g y` commute  -/
MonoidAlgebra.liftNCRingHom : {k : Type u₁} →
  {G : Type u₂} →
    {R : Type u_2} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : Semiring R] →
            (f : k →+* R) → (g : G →* R) → (∀ (x : k) (y : G), Commute (f x) (g y)) → MonoidAlgebra k G →+* R
-- Mathlib.GroupTheory.Exponent
/-- The exponent of product of two additive monoids is the
`lcm` of the exponents of the individual additive monoids.  -/
AddMonoid.exponent_prod : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : AddMonoid M₁] [inst_1 : AddMonoid M₂],
  AddMonoid.exponent (M₁ × M₂) = lcm (AddMonoid.exponent M₁) (AddMonoid.exponent M₂)
-- Init.Data.Int.Order
Int.le_min : ∀ {a b c : ℤ}, a ≤ min b c ↔ a ≤ b ∧ a ≤ c
-- Init.Data.Vector.Monadic
Vector.forIn'_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs ys : Vector α n} (w : xs = ys)
  {b b' : β},
  b = b' →
    ∀ {f : (a' : α) → a' ∈ xs → β → m (ForInStep β)} {g : (a' : α) → a' ∈ ys → β → m (ForInStep β)},
      (∀ (a : α) (m_1 : a ∈ ys) (b : β), f a ⋯ b = g a m_1 b) → forIn' xs b f = forIn' ys b' g
-- Mathlib.Data.Multiset.Bind
Multiset.mem_bind : ∀ {α : Type u_1} {β : Type v} {b : β} {s : Multiset α} {f : α → Multiset β}, b ∈ s.bind f ↔ ∃ a ∈ s, b ∈ f a
-- Mathlib.Analysis.Normed.Group.Basic
pow_mem_closedBall : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ},
  a ∈ Metric.closedBall b r → a ^ n ∈ Metric.closedBall (b ^ n) (n • r)
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the pair `(t.contains k, t.insert k v)`.  -/
Std.DTreeMap.Internal.Impl.containsThenInsert : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      (k : α) →
        β k →
          (t : Std.DTreeMap.Internal.Impl α β) →
            t.Balanced → Bool × Std.DTreeMap.Internal.Impl.SizedBalancedTree α β t.size (t.size + 1)
-- Lean.Meta.LazyDiscrTree
/-- Create a discriminator tree for current module declarations.  -/
Lean.Meta.LazyDiscrTree.createModuleDiscrTree : {α : Type} →
  (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
    Lean.CoreM (Lean.Meta.LazyDiscrTree α)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg.injEq : ∀ (a a_1 : Lean.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg a =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg a_1) =
    (a = a_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.eq = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.eq = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.eq with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_2 ⋯
-- Batteries.Recycling.RBTree.Basic
RBTree.RBColor.black.sizeOf_spec : sizeOf RBTree.RBColor.black = 1