mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Basic
/-- The text document's language identifier.  -/
Lean.Lsp.TextDocumentItem.languageId : Lean.Lsp.TextDocumentItem → String
-- Mathlib.NumberTheory.Divisors
/-- The factors of `n` are the prime divisors  -/
Nat.primeFactors_eq_to_filter_divisors_prime : ∀ (n : ℕ), n.primeFactors = {p ∈ n.divisors | Nat.Prime p}
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.inv_rpow : ∀ (x : NNReal) (y : ℝ), x⁻¹ ^ y = (x ^ y)⁻¹
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α},
  Std.DHashMap.Internal.Raw₀.Const.get!
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k =
    ()
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipSuffixWhile_eq_endPos_iff_or : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice},
  s.skipSuffixWhile pat = s.endPos ↔
    ¬String.Slice.Pattern.Model.RevMatchesAt pat s.endPos ∨
      String.Slice.Pattern.Model.IsLongestRevMatchAt pat s.endPos s.endPos
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : LowerSet α),
  ((LowerSet.map f) s).compl = (UpperSet.map f) s.compl
-- Batteries.Tactic.Lint.Basic
/-- Gets a linter by declaration name.  -/
Batteries.Tactic.Lint.getLinter : Lean.Name → Lean.Name → Lean.CoreM Batteries.Tactic.Lint.NamedLinter
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_X_pow_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
  0 < n → ∀ (a : R), (Polynomial.X ^ n - Polynomial.C a).roots.card ≤ n
-- Mathlib.Order.Heyting.Basic
PUnit.sup_eq : ∀ (a b : PUnit.{u + 1}), max a b = PUnit.unit
-- Init.Data.Dyadic.Basic
/-- Determine if a dyadic rational is less than or equal to another.  -/
Dyadic.ble : Dyadic → Dyadic → Bool
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_terminates_of_get?_terminates : ∀ {α : Type u} {s : Stream'.WSeq α} {n : ℕ}, (s.get? n).Terminates → s.head.Terminates
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.one_div_spanSingleton : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] (x : K),
  1 / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x⁻¹
-- Init.Data.Order.Classes
Std.LawfulOrderLeftLeaningMax.max_eq_right : ∀ {α : Type u} {inst : Max α} {inst_1 : LE α} [self : Std.LawfulOrderLeftLeaningMax α] (a b : α), ¬b ≤ a → a ⊔ b = b
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.refl_comp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N), (FirstOrder.Language.Embedding.refl L N).comp f = f
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.setModState : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Doc.ModuleDocstringState✝ → m Unit
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid is equal to the affine combination of the points with `centroidWeights`.  -/
Affine.Simplex.centroid_eq_affineCombination : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n),
  s.centroid = (Finset.affineCombination k Finset.univ s.points) (Finset.centroidWeights k Finset.univ)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (g : E →L[𝕜] F),
  ContinuousLinearMap.lTensor G g =
    ↑↑(TensorProduct.commIsometry 𝕜 F G) ∘SL ContinuousLinearMap.rTensor G g ∘SL ↑↑(TensorProduct.commIsometry 𝕜 G E)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.ofAdd_eq_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α] {a : α}, Multiplicative.ofAdd a = ⊥ ↔ a = ⊥
-- Mathlib.Data.Quot
Quot.instDecidableLiftOnOfDecidablePred_mathlib : {α : Sort u_1} →
  (r : α → α → Prop) →
    (q : Quot r) → (f : α → Prop) → (h : ∀ (a b : α), r a b → f a = f b) → [DecidablePred f] → Decidable (q.liftOn f h)
-- Mathlib.Data.Quot
Quot.lift_mk : ∀ {α : Sort u_1} {γ : Sort u_4} {r : α → α → Prop} (f : α → γ) (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) (a : α),
  Quot.lift f h (Quot.mk r a) = f a
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddCommMonoid.toESeminormedAddCommMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ENormedAddCommMonoid E] → ESeminormedAddCommMonoid E
-- Mathlib.Algebra.Group.AddChar
AddChar.sum_eq_ite : ∀ {A : Type u_1} {R : Type u_2} [inst : AddGroup A] [inst_1 : Fintype A] [inst_2 : CommSemiring R] [IsDomain R]
  (ψ : AddChar A R) [inst_4 : Decidable (ψ = 0)], ∑ a, ψ a = if ψ = 0 then ↑(Fintype.card A) else 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLTGE n).obj j).obj₂ = j
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q.mk.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (p : α × α),
  Lean.Grind.Ring.OfSemiring.Q.mk p = Quot.mk (Lean.Grind.Ring.OfSemiring.r α) p
-- Mathlib.Data.List.NatAntidiagonal
List.Nat.map_swap_antidiagonal : ∀ {n : ℕ}, List.map Prod.swap (List.Nat.antidiagonal n) = (List.Nat.antidiagonal n).reverse
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instZeroHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (G H : CategoryTheory.Grp C),
  G.instZeroHom H =
    {
      zero :=
        CategoryTheory.Grp.homMk
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit G.X)
            CategoryTheory.MonObj.one) }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
value `cos (n * θ)`.  -/
Polynomial.Chebyshev.T_complex_cos : ∀ (θ : ℂ) (n : ℤ), Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.T ℂ n) = Complex.cos (↑n * θ)
-- Mathlib.Topology.Germ
Filter.Eventually.germ_congr_set : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f g : X → Y} {A : Set X}
  {P : (x : X) → (nhds x).Germ Y → Prop},
  (∀ᶠ (x : X) in nhdsSet A, P x ↑f) → (∀ᶠ (z : X) in nhdsSet A, g z = f z) → ∀ᶠ (x : X) in nhdsSet A, P x ↑g
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instRightIdentityJoinBot : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l],
  Std.RightIdentity (fun x1 x2 => Lean.Order.join x1 x2) Lean.Order.bot
-- Init.Grind.Util
/-- Gadget for representing `a = b` in patterns for backward propagation.  -/
Lean.Grind.eqBwdPattern : {α : Sort u_1} → α → α → Prop
-- Init.Data.Order.Lemmas
Std.beq_iff_le_and_ge : ∀ {α : Type u} [inst : BEq α] [inst_1 : LE α] [Std.LawfulOrderBEq α] {a b : α}, (a == b) = true ↔ a ≤ b ∧ b ≤ a
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueAddEquiv_symm_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Unique m] [inst_1 : Unique n] [inst_2 : Add A] (a : A),
  Matrix.uniqueAddEquiv.symm a = Matrix.of fun x x_1 => a
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.eq_2 : ∀ (a b : ℤ), Lean.Grind.instBEqIntInterval.beq (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b) = (a == b)
-- Mathlib.Tactic.Linarith.Frontend
/-- `partitionByTypeIdx l` takes a list `l` of pairs `(h, i)` where `h` is a proof of a
comparison and `i` records the original position of `h`. The proofs are grouped by the
type of the variables appearing in the comparison, e.g. `(a : ℚ) < 1` and
`(b : ℤ) > c` will be separated. The resulting map associates each type with the
list of `(h, i)` pairs over that type.
 -/
Mathlib.Tactic.Linarith.partitionByTypeIdx : List (Lean.Expr × ℕ) → Lean.MetaM (Mathlib.Tactic.Linarith.ExprMultiMap (Lean.Expr × ℕ))
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_inv : ∀ {G : Type u_1} [inst : Group G] (g₁ g₂ : G), ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `CostructuredArrow S T ⥤ CostructuredArrow U V` that is deduced from
a natural transformation `F ⋙ U ⟶ S ⋙ G` and a morphism `G.obj T ⟶ V`  -/
CategoryTheory.CostructuredArrow.map₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {A : Type u₃} →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                {B : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                    {U : CategoryTheory.Functor A B} →
                      {V : B} →
                        {F : CategoryTheory.Functor C A} →
                          {G : CategoryTheory.Functor D B} →
                            (F.comp U ⟶ S.comp G) →
                              (G.obj T ⟶ V) →
                                CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T)
                                  (CategoryTheory.CostructuredArrow U V)
-- Mathlib.GroupTheory.Coprod.Basic
/-- Lift a pair of additive monoid homomorphisms `f : M →+ P`, `g : N →+ P`
to an additive monoid homomorphism `AddMonoid.Coprod M N →+ P`.

See also `AddMonoid.Coprod.clift` for a version that allows custom computational behavior
and works for an `AddZeroClass` codomain.  -/
AddMonoid.Coprod.lift : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] → [inst_2 : AddMonoid P] → (M →+ P) → (N →+ P) → AddMonoid.Coprod M N →+ P
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceδ_comp_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : A} (h_1 : (F.shift n₁).obj T.obj₂ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h)
          (CategoryTheory.CategoryStruct.comp ((F.shift n₁).map T.mor₁) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)),
  (match some c with
    | none => h_1 ()
    | some c => h_2 c) =
    h_2 c
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_le_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ} (x : E), 0 < D → ExistsContDiffBumpBase.y D x ≤ 1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.brecOn.go : {motive_1 : Aesop.Frontend.RuleExpr → Sort u} →
  {motive_2 : Array Aesop.Frontend.RuleExpr → Sort u} →
    {motive_3 : List Aesop.Frontend.RuleExpr → Sort u} →
      (t : Aesop.Frontend.RuleExpr) →
        ((t : Aesop.Frontend.RuleExpr) → t.below → motive_1 t) →
          ((t : Array Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_1 t → motive_2 t) →
            ((t : List Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_2 t → motive_3 t) →
              motive_1 t ×' t.below
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.decodeList.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (v : ℕ) (h_1 : Unit → motive 0) (h_2 : (v : ℕ) → motive v.succ),
  (match v.succ with
    | 0 => h_1 ()
    | v.succ => h_2 v) =
    h_2 v
-- Mathlib.Logic.Equiv.Finset
Denumerable.raise'Finset.eq_1 : ∀ (l : List ℕ) (n : ℕ), Denumerable.raise'Finset l n = { val := ↑(Denumerable.raise' l n), nodup := ⋯ }
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instVAdd : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → {G : Type u_6} → [VAdd M G] → VAdd M (l.Germ G)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.prod_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, f' =o[l] k' → g' =o[l] k' → (fun x => (f' x, g' x)) =o[l] k'
-- Mathlib.Topology.Defs.Filter
/-- A function between topological spaces is continuous at a point `x₀` within a subset `s`
if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`.  -/
ContinuousWithinAt : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Set X → X → Prop
-- Init.Data.UInt.Lemmas
UInt64.ofNat_uSizeToNat : ∀ (n : USize), UInt64.ofNat n.toNat = n.toUInt64
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.map_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
  (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
    (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m
-- Aesop.RuleTac.GoalDiff
_private.Aesop.RuleTac.GoalDiff.0.Aesop.hasUnknownFVar : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Fintype.EquivFin
_private.Mathlib.Data.Fintype.EquivFin.0.Infinite.natEmbeddingAux.eq_1 : ∀ (α : Type u_4) [inst : Infinite α] (x : ℕ), Infinite.natEmbeddingAux✝ α x = Classical.choose ⋯
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.whiskeringRight_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] (F : D ⥤ₗ E) {X Y : C ⥤ₗ D} (f : X ⟶ Y),
  ((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).map f =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_subset_support_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (hadj : G.Adj v w), p.support ⊆ (p.concat hadj).support
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.subset : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s t : Set ι}, s ⊆ t → AntivaryOn f g t → AntivaryOn f g s
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.one_anti : ∀ {α : Type u_5} {β : Type u_6} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : One β], Antitone 1
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instReflectsColimitsOfShapeForgetOrderEmbeddingCarrier : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.ReflectsColimitsOfShape J (CategoryTheory.forget PartOrdEmb)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_zsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (z : ℤ) (f : C(α, β)), ⇑(z • f) = z • ⇑f
-- Mathlib.Analysis.Convex.Between
not_sbtw_self_left : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), ¬Sbtw R x x y
-- Mathlib.Data.Vector3
/-- Alternate definition of `Vector` based on `Fin2`.  -/
Vector3 : Type u → ℕ → Type u
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x`, it maps its domain chart's target to its codomain chart's target:
`(h.domChart.extend I).target` to `(h.domChart.extend J).target`.

Roig and Domingues' [roigdomingues1992] definition of immersions only asks for this inclusion
between the targets of the local charts: using mathlib's formalisation conventions, that condition
is *slightly* weaker than `source_subset_preimage_source`: the latter implies that
`h.codChart.extend J ∘ f` maps `h.domChart.source` to
`(h.codChart.extend J).target = (h.codChart.extend I) '' h.codChart.source`,
but that does *not* imply `f` maps `h.domChart.source` to `h.codChart.source`;
a priori `f` could map some point `f ∘ h.domChart.extend I x ∉ h.codChart.source` into the target.
Note that this difference only occurs because of our design using junk values;
this is not a mathematically meaningful difference.

At the same time, this condition is fairly weak: it is implied, for instance, by `f` being
continuous at `x` (see `mk_of_continuousAt`), which is easy to ascertain in practice.

See `target_subset_preimage_target` for a version stated using preimages instead of images.
 -/
Manifold.IsImmersionAt.map_target_subset_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x),
  (⇑h.equiv ∘ fun x_1 => (x_1, 0)) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target
-- Init.Data.String.Basic
/-- Given a position in `s` that is between `p₀` and `p₁`, obtain the corresponding position in
`s.slice p₀ p₁ h`.  -/
String.Slice.Pos.slice : {s : String.Slice} → (pos p₀ p₁ : s.Pos) → (h₁ : p₀ ≤ pos) → (h₂ : pos ≤ p₁) → (s.slice p₀ p₁ ⋯).Pos
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.biUnion_lt_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) (r : ℝ),
  ⋃ r', ⋃ (_ : r' < r), Metric.closedBall x r' = Metric.ball x r
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Further truncation of truncated simplicial objects.  -/
CategoryTheory.SimplicialObject.Truncated.trunc : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n m : ℕ) →
      autoParam (m ≤ n) CategoryTheory.SimplicialObject.Truncated.trunc._auto_1 →
        CategoryTheory.Functor (CategoryTheory.SimplicialObject.Truncated C n)
          (CategoryTheory.SimplicialObject.Truncated C m)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedMVarErrorInfo : Inhabited Lean.Elab.Term.MVarErrorInfo
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.NatTrans.tensor_naturality : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map g))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app Y')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (F'.map f) (G'.map g))
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.nhdsNE_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] [NoncompactSpace X]
  (x : OnePoint X), (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.homInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (M : CategoryTheory.Comon C) → Inhabited (M.Hom M)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The inverse of the unit isomorphism of the equivalence
`widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J`  -/
CategoryTheory.Limits.widePullbackShapeOpUnop : (J : Type w) →
  (CategoryTheory.Limits.widePullbackShapeUnop J).comp (CategoryTheory.Limits.widePushoutShapeOp J) ≅
    CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ
-- Mathlib.Topology.MetricSpace.Closeds
/-- In emetric spaces, the Hausdorff edistance defines an emetric space structure
on the type of closed subsets  -/
TopologicalSpace.Closeds.instEMetricSpace : {α : Type u_1} → [inst : EMetricSpace α] → EMetricSpace (TopologicalSpace.Closeds α)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableEqOffset : DecidableEq Std.Time.Month.Offset
-- Mathlib.Control.Fold
Traversable.toList_map : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] (f : α → β) (xs : t α),
  Traversable.toList (f <$> xs) = f <$> Traversable.toList xs
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).getD k' fallback = cast ⋯ v
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
/-- Effective epi families in a precoherent category are transitive, in the sense that an
`EffectiveEpiFamily` and an `EffectiveEpiFamily` over each member, the composition is an
`EffectiveEpiFamily`.
Note: The finiteness condition is an artifact of the proof and is probably unnecessary.
 -/
CategoryTheory.EffectiveEpiFamily.transitive_of_finite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Precoherent C] {X : C} {α : Type}
  [Finite α] {Y : α → C} (π : (a : α) → Y a ⟶ X),
  CategoryTheory.EffectiveEpiFamily Y π →
    ∀ {β : α → Type} [∀ (a : α), Finite (β a)] {Y_n : (a : α) → β a → C} (π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a),
      (∀ (a : α), CategoryTheory.EffectiveEpiFamily (Y_n a) (π_n a)) →
        CategoryTheory.EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c =>
          CategoryTheory.CategoryStruct.comp (π_n c.fst c.snd) (π c.fst)
-- Std.Internal.Do.WP.Basic
/-- `Option`'s `WP` interpretation: `Prop` assertions and a single `Prop` exception postcondition.  -/
Std.Internal.Do.Option.wpInst : {α : Type u} → Std.Internal.Do.WP (Option α) α Prop Prop
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_dite_pos_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} (p : β → Prop)
  [inst_2 : DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β},
  b ∈ s → ∀ (h₁ : p b), (s.inf fun i => if h : p i then f i h else g i h) ≤ f b h₁
-- Init.Data.String.Basic
String.Slice.Pos.byte_eq_byte_copy : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos}, pos.byte h = pos.copy.byte ⋯