mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Inseparable
GeneralizingMap_iff_stableUnderGeneralization_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  GeneralizingMap f ↔ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- The nonnegative part of a continuous compactly supported `ℝ`-valued function as a
continuous compactly supported `ℝ≥0`-valued function.  -/
CompactlySupportedContinuousMap.nnrealPart : {α : Type u_2} →
  [inst : TopologicalSpace α] → CompactlySupportedContinuousMap α ℝ → CompactlySupportedContinuousMap α NNReal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.sumNodes_eq_eval_iterate_derivative : ∀ {n k : ℕ},
  k ≤ n →
    ∀ (x : ℝ) {P : Polynomial ℝ},
      P.degree ≤ ↑n →
        Polynomial.Chebyshev.sumNodes n (Polynomial.Chebyshev.iterateDerivativeC✝ n k x) P =
          Polynomial.eval x ((⇑Polynomial.derivative)^[k] P)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_inv_iff_mul_lt_one : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, a < b⁻¹ ↔ a * b < 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_get?_eq_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α}, (t.get? a).isSome = t.contains a
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.addHaar.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G],
  MeasureTheory.Measure.addHaar =
    MeasureTheory.Measure.addHaarMeasure (Classical.arbitrary (TopologicalSpace.PositiveCompacts G))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSubtypeWalkLengthLT : {V : Type u} →
  (G : SimpleGraph V) → [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype { p // p.length < n }
-- Mathlib.RingTheory.FilteredAlgebra.Basic
/-- A convenience constructor for `IsModuleFiltration` when the index is the integers.  -/
IsModuleFiltration.mk_int : ∀ {R : Type u_3} {M : Type u_4} {σ : Type u_5} {σM : Type u_6} [inst : Preorder σ] [inst_1 : Semiring R]
  [inst_2 : SetLike σ R] [inst_3 : Preorder σM] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : SetLike σM M]
  (F : ℤ → σ) (mono : Monotone F) [inst_7 : SetLike.GradedMonoid F] (F' : ℤ → σM),
  Monotone F' → ∀ [SetLike.GradedSMul F F'], IsModuleFiltration F (fun n => F (n - 1)) F' fun n => F' (n - 1)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  {Z : HomologicalComplex D (ComplexShape.up ℤ)} (h : (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))).X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.mappingCone.descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) h) =
    CategoryTheory.CategoryStruct.comp
      ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.descShortComplex S)) h
-- Mathlib.Tactic.NormNum.Core
/-- Environment extensions for `norm_num` declarations  -/
Mathlib.Meta.NormNum.normNumExt : Lean.ScopedEnvExtension Mathlib.Meta.NormNum.Entry (Mathlib.Meta.NormNum.Entry × Mathlib.Meta.NormNum.NormNumExt)
  Mathlib.Meta.NormNum.NormNums
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_add : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (I J : FractionalIdeal S P) (g : P →ₐ[R] P'),
  FractionalIdeal.map g (I + J) = FractionalIdeal.map g I + FractionalIdeal.map g J
-- Lean.Structure
/-- Gets the name of the auxiliary definition that would have the inherited default value for the structure field if it exists.
 -/
Lean.mkInheritedDefaultFnOfProjFn : Lean.Name → Lean.Name
-- Lean.Parser.Types
Lean.Parser.InputContext.mk'.sizeOf_spec : ∀ (inputString fileName : String) (fileMap : Lean.FileMap) (endPos : String.Pos.Raw)
  (endPos_valid : autoParam (endPos ≤ inputString.rawEndPos) Lean.Parser.InputContext.endPos_valid._autoParam),
  sizeOf
      { inputString := inputString, fileName := fileName, fileMap := fileMap, endPos := endPos,
        endPos_valid := endPos_valid } =
    1 + sizeOf inputString + sizeOf fileName + sizeOf fileMap + sizeOf endPos + sizeOf endPos_valid
-- Mathlib.Order.Hom.Basic
/-- `OrderHom.dual` as an order isomorphism.  -/
OrderHom.dualIso : (α : Type u_8) → (β : Type u_9) → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) ≃o (αᵒᵈ →o βᵒᵈ)ᵒᵈ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsGreatest.norm_cfc : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [Nontrivial A] (f : 𝕜 → 𝕜) (a : A),
  autoParam (ContinuousOn f (spectrum 𝕜 a)) IsGreatest.norm_cfc._auto_1 →
    autoParam (p a) IsGreatest.norm_cfc._auto_3 → IsGreatest ((fun x => ‖f x‖) '' spectrum 𝕜 a) ‖cfc f a‖
-- Init.Control.Basic
ToBool.mk : {α : Type u} → (α → Bool) → ToBool α
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.functoriality_full`. -/
CategoryTheory.Limits.Cones.functoriality_full : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful], (CategoryTheory.Limits.Cone.functoriality F G).Full
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β},
  k' ∈ Std.ExtDTreeMap.Const.alter t k f ↔
    if cmp k k' = Ordering.eq then (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true else k' ∈ t
-- Mathlib.Order.CompleteLattice.Defs
le_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, (∀ b ∈ s, a ≤ b) → a ≤ sInf s
-- Mathlib.LinearAlgebra.Dimension.Localization
nonempty_oreSet_of_strongRankCondition : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R] [StrongRankCondition R],
  Nonempty (OreLocalization.OreSet (nonZeroDivisors R))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.ctorAlt.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {info : Lean.Compiler.LCNF.CtorInfo} {code : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_3}
  {info_1 : Lean.Compiler.LCNF.CtorInfo} {code_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_3},
  Lean.Compiler.LCNF.Alt.ctorAlt info code h = Lean.Compiler.LCNF.Alt.ctorAlt info_1 code_1 h_1 →
    info = info_1 ∧ code = code_1
-- Init.Data.Nat.Lemmas
Nat.mul_self_lt_mul_self : ∀ {m n : ℕ}, m < n → m * m < n * n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.allM_filter : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → Bool}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.IterM.filter f it) =
    Std.IterM.allM (fun x => if f x = true then p x else pure { down := true }) it
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_rio_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.contains (t.maxKeyD fallback) = true
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
/-- If we have the additional hypothesis `∀ᵐ x ∂μ, p x (fun n ↦ f n x)`, this is a measurable set
whose complement has measure 0 such that for all `x ∈ aeSeqSet`, `f i x` is equal to
`(hf i).mk (f i) x` for all `i` and we have the pointwise property `p x (fun n ↦ f n x)`.  -/
aeSeqSet : {ι : Sort u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] →
          {f : ι → α → β} →
            {μ : MeasureTheory.Measure α} → (∀ (i : ι), AEMeasurable (f i) μ) → (α → (ι → β) → Prop) → Set α
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit.range : Lean.Elab.InlayHintTextEdit → Lean.Syntax.Range
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_inv_of_le_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → a ≤ b⁻¹ → b ≤ a⁻¹
-- Mathlib.GroupTheory.Perm.Fin
support_finRotate_of_le : ∀ {n : ℕ}, 2 ≤ n → (finRotate n).support = Finset.univ
-- Mathlib.Algebra.Group.Action.Defs
IsCancelVAdd.right_cancel' : ∀ {G : Type u_9} {P : Type u_10} {inst : VAdd G P} [self : IsCancelVAdd G P] (a b : G) (c : P), a +ᵥ c = b +ᵥ c → a = b
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.eq_2 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α) (cb : Computation β),
  Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b ∈ cb, R a b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.FG.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] (p : SubAddAction R M),
  p.FG = ∃ s, s.Finite ∧ p = SubAddAction.closure R s
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ max a b → Set.Ioc a b ∪ Set.Ioi c = Set.Ioi (min a c)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.D₃.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄)
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄],
  HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j'
-- Mathlib.Order.Hom.Lattice
InfHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar.eq_1 : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [inst_5 : IsAbelianGalois ℚ K],
  IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R =
    IsGalois.intermediateFieldEquivSubgroup.trans
      ((IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R).dual.trans
        (OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm)
-- Batteries.Tactic.Lint.Frontend
/-- Formats a linter warning as `#check` command with comment.  -/
Batteries.Tactic.Lint.printWarning : Lean.Name → Lean.MessageData → optParam Bool false → optParam System.FilePath default → Lean.CoreM Lean.MessageData
-- Init.Data.String.Iterate
/-- Folds a function over a string from the right, accumulating a value starting with `init`. The
accumulated value is combined with each character in reverse order, using `f`.

Examples:

* `"coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2`

* `"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3`

* `"coffee tea water".foldr (fun c s => s.push c) "" = "retaw aet eeffoc"`
 -/
String.foldr : {α : Type u} → (Char → α → α) → α → String → α
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.isEmpty = true → ∀ {fallback : α}, (t.insert k).minD fallback = k
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- A graph is 2-edge-connected iff it has no bridge.  -/
SimpleGraph.isEdgeConnected_two : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsEdgeConnected 2 ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Preconnected
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.id.sizeOf_spec : ∀ (a : Mathlib.Tactic.Widget.StringDiagram.IdNode),
  sizeOf (Mathlib.Tactic.Widget.StringDiagram.Node.id a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(X ◁ coprod.inl) : X ⊗ Y ⟶ X ⊗ (Y ⨿ Z)` and
`(∂L X Y Z).inv :  X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`
is equal to the left coprojection `coprod.inl : X ⊗ Y ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`.  -/
CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C]
  {X Y Z Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_toNNReal : ∀ {a : ENNReal}, a ≠ ⊤ → Filter.Tendsto ENNReal.toNNReal (nhds a) (nhds a.toNNReal)
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_toInt : ∀ (x : Int8), Int8.ofIntLE x.toInt ⋯ ⋯ = x
-- Mathlib.Analysis.Convex.StrictCombination
StrictConvex.sum_mem_interior : ∀ {R : Type u_1} {V : Type u_2} {ι : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup V] [inst_5 : Module R V] {s : Set V} {t : Finset ι} {w : ι → R}
  {z : ι → V},
  StrictConvex R s →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        ∀ {i j : ι},
          i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → ∑ k ∈ t, w k • z k ∈ interior s
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
PiToModule.fromEnd_injective : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M), Submodule.span R (Set.range b) = ⊤ → Function.Injective ⇑(PiToModule.fromEnd R b)
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Function.const α b` as a bundled continuous function of `b`.  -/
ContinuousMap.constPi : (α : Type u_1) → {β : Type u_2} → [inst : TopologicalSpace β] → C(β, α → β)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.coprod.isCountablyGenerated : ∀ {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated],
  (la.coprod lb).IsCountablyGenerated
-- Mathlib.Data.Finset.Basic
Equiv.Finset.union.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (h : Disjoint s t),
  Equiv.Finset.union s t h = Equiv.Finset.union s t h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_4 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (op : Std.Tactic.BVDecide.BVUnOp)
  (expr : Std.Tactic.BVDecide.BVExpr w) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.un op expr with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_4 w op expr
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesLimit₂.isoObjConePointsOfIsLimit` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit_hom_comp_π : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone K₂} (hc₂ : CategoryTheory.Limits.IsLimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsLimit c₃) (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).hom
      (c₃.π.app j) =
    CategoryTheory.CategoryStruct.comp ((G.map (c₁.π.app j.1)).app c₂.pt) ((G.obj (K₁.obj j.1)).map (c₂.π.app j.2))
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hasForgetToMonCat.eq_1 : CommMonCat.hasForgetToMonCat =
  {
    forget₂ :=
      { obj := fun R => MonCat.of ↑R, map := fun {X Y} f => MonCat.ofHom (CommMonCat.Hom.hom f),
        map_id := CommMonCat.hasForgetToMonCat._proof_1, map_comp := @CommMonCat.hasForgetToMonCat._proof_2 },
    forget_comp := CommMonCat.hasForgetToMonCat._proof_4 }
-- Init.Data.Range.Basic
Std.Legacy.Range.start : Std.Legacy.Range → ℕ
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.instIterator : {α : Type w} → {f : α → α} → Std.Iterator (Std.Iterators.Types.RepeatIterator α f) Id α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {h' : a ∈ m.erase k}, (m.erase k).get a h' = m.get a ⋯
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α ENNReal), f.lintegral 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isMaximalIndepSet_compl : ∀ {α : Type u_3} {G : SimpleGraph α} (s : Finset α), Maximal Gᶜ.IsIndepSet ↑s ↔ Maximal G.IsClique ↑s
-- Mathlib.Logic.Function.Basic
Function.injective_surjInv : ∀ {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f), Function.Injective (Function.surjInv h)
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgHom.includeRight_apply : ∀ {ι : Type u_1} {R : Type u_2} (S : Type u_3) {A : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Semiring A] [inst_5 : Algebra R A]
  {𝒜 : ι → Submodule R A} [inst_6 : GradedAlgebra 𝒜] [inst_7 : Algebra R S] (x : A),
  (GradedAlgHom.includeRight S 𝒜) x = 1 ⊗ₜ[R] x
-- Lean.Meta.LazyDiscrTree
/-- Merge two discrimination trees.  -/
Lean.Meta.LazyDiscrTree.PreDiscrTree.append : {α : Type} →
  Lean.Meta.LazyDiscrTree.PreDiscrTree α →
    Lean.Meta.LazyDiscrTree.PreDiscrTree α → Lean.Meta.LazyDiscrTree.PreDiscrTree α
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_assoc : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) {g g' : CategoryTheory.FreeBicategory.Hom b c}
  (η : CategoryTheory.FreeBicategory.Hom₂ g g') (h : CategoryTheory.FreeBicategory.Hom c d),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.add_right : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {n : ℕ},
  p.IsMonicOfDegree n → q.natDegree < n → (p + q).IsMonicOfDegree n