mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.nsmul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → ∀ (n : ℕ), MonovaryOn (n • f) g s
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.elabPrecheckedQuot : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
one_lt_mul_iff : ∀ {α : Type u} [inst : CommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedMul α] {a b : α},
  1 < a * b ↔ 1 < a ∨ 1 < b
-- Mathlib.RingTheory.FiniteStability
Algebra.FiniteType.baseChange : ∀ {R : Type w₁} [inst : CommRing R] {A : Type w₂} [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type w₃)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [hfa : Algebra.FiniteType R A],
  Algebra.FiniteType B (TensorProduct R B A)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.faithful_ιOfLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P'),
  (CategoryTheory.ObjectProperty.ιOfLE h).Faithful
-- Mathlib.Geometry.Manifold.Immersion
/-- A choice of chart on the co-domain `N` of an immersion `f` at `x`:
w.r.t. this chart and the data `h.domChart` and `h.equiv`,
`f` will look like an inclusion `u ↦ (u, 0)` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.equiv` and `h.domChart`.  -/
Manifold.IsImmersionAtOfComplement.codChart : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsImmersionAtOfComplement F I J n f x →
                                                      OpenPartialHomeomorph N G
-- Mathlib.CategoryTheory.Sums.Basic
/-- `swap` gives an equivalence between `C ⊕ D` and `D ⊕ C`.  -/
CategoryTheory.Sum.Swap.equivalence : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → C ⊕ D ≌ D ⊕ C
-- Mathlib.Algebra.Ring.Units
/-- Each element of the group of units of a ring has an additive inverse.  -/
Units.instNeg : {α : Type u} → [inst : Monoid α] → [HasDistribNeg α] → Neg αˣ
-- Mathlib.Data.Sym.Sym2
Sym2.map_id : ∀ {α : Type u_1}, Sym2.map id = id
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.default : Bool → Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.exists_mem : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∃ x, x ∈ s
-- Mathlib.Order.Atoms
/-- **Alias** of the reverse direction of `isCoatom_dual_iff_isAtom`. -/
IsAtom.dual : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → IsCoatom (OrderDual.toDual a)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.set.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → α → Sort u_2) (head : α) (as : List α) (b : α)
  (h_1 : (head : α) → (as : List α) → (b : α) → motive (head :: as) 0 b)
  (h_2 : (a : α) → (as : List α) → (n : ℕ) → (b : α) → motive (a :: as) n.succ b)
  (h_3 : (x : ℕ) → (x_1 : α) → motive [] x x_1),
  (match head :: as, 0, b with
    | head :: as, 0, b => h_1 head as b
    | a :: as, n.succ, b => h_2 a as n b
    | [], x, x_1 => h_3 x x_1) =
    h_1 head as b
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_iff_eqLocus_coFG : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {u v : V →ₗ[K] V₂}, u ≈ v ↔ (u.eqLocus v).CoFG
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0),
  CochainComplex.HomComplex.Cocycle.fromSingleMk (-f) h q' hq' ⋯ =
    -CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instCategoryComonad : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Category.{max u₁ v₁, max u₁ v₁} (CategoryTheory.Comonad C)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.exfalso : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊢ₛ ⌜False⌝) → P ⊢ₛ Q
-- Init.Tactics
/-- `+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
 -/
Lean.Parser.Tactic.posConfigItem : Lean.ParserDescr
-- Mathlib.Algebra.RingQuot
RingQuot.mkAlgHom_surjective : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] (s : A → A → Prop),
  Function.Surjective ⇑(RingQuot.mkAlgHom S s)
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_fun_eq_lift_mul : ∀ {R : Type u} {M : Type v} {η : Type u₁'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [StrongRankCondition R] [Module.Free R M] [inst_5 : Fintype η],
  Module.rank R (η → M) = ↑(Fintype.card η) * Cardinal.lift.{u₁', v} (Module.rank R M)
-- Init.Data.Array.MinMax
Array.min?_replicate : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {n : ℕ} {a : α},
  (Array.replicate n a).min? = if n = 0 then none else some a
-- Mathlib.RingTheory.PowerBasis
PowerBasis.exists_eq_aeval : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Nontrivial S]
  (pb : PowerBasis R S) (y : S), ∃ f, f.natDegree < pb.dim ∧ y = (Polynomial.aeval pb.gen) f
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.setOfPred_isOpen : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → {s | IsOpen s} = Set.preimage f '' {t | IsOpen t}
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMapM.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_center_dist : ∀ (z w : UpperHalfPlane), dist ↑z ↑(w.center (dist z w)) = w.im * Real.sinh (dist z w)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instInf : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] →
        [inst_2 : Lattice β] → [HasSolidNorm β] → [IsOrderedAddMonoid β] → Min (BoundedContinuousFunction α β)
-- Mathlib.Combinatorics.Colex
_private.Mathlib.Combinatorics.Colex.0.Finset.Colex.antisymm_aux : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α}, toColex s ≤ toColex t → toColex t ≤ toColex s → s ⊆ t
-- Mathlib.Order.Antichain
/-- **Alias** of `IsAntichain.eq_setOfPred_minimal`.

---

If `t` is an antichain shadowed by and including the set of minimal elements of `s`,
then `t` *is* the set of minimal elements of `s`.  -/
IsAntichain.eq_setOf_minimal : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) t →
    (∀ (x : α), Minimal (fun x => x ∈ s) x → x ∈ t) →
      (∀ a ∈ t, ∃ b, a ≤ b ∧ Minimal (fun x => x ∈ s) b) → {x | Minimal (fun x => x ∈ s) x} = t
-- Mathlib.Order.Cover
Set.Ioi_eq_singleton_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a = {b} ↔ IsTop b ∧ a ⋖ b
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Pi.instIsUniformAddGroup : ∀ {ι : Type u_4} {G : ι → Type u_5} [inst : (i : ι) → UniformSpace (G i)] [inst_1 : (i : ι) → AddGroup (G i)]
  [∀ (i : ι), IsUniformAddGroup (G i)], IsUniformAddGroup ((i : ι) → G i)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.ofList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  (Std.TreeSet.Raw.ofList l cmp).Equiv (List.foldl (fun acc a => acc.insert a) ∅ l)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassMod.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f f_1 : PowerSeries A),
  f = f_1 →
    ∀ (g g_1 : PowerSeries A), g = g_1 → ∀ [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A], f %ʷ g = f_1 %ʷ g_1
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.majFlt : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Topology.Homotopy.Path
ContinuousMap.Homotopy.pathExtend_evalAt : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g)
  (x : X), ⇑(H.evalAt x).extend = fun t => (H.extend t) x
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f h) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} {u : Set (E × F)}
  (h : IsBoundedBilinearMap 𝕜 b) (p : E × F), UniqueDiffWithinAt 𝕜 u p → fderivWithin 𝕜 b u p = h.deriv p
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableVAdd₂.mk : ∀ {M : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : MeasurableSpace M] [inst_2 : MeasurableSpace α],
  Measurable (Function.uncurry fun x1 x2 => x1 +ᵥ x2) → MeasurableVAdd₂ M α
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The type of TM2 statements used by this machine.  -/
Turing.PartrecToTM2.Stmt' : Type
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The Fourier transform on a real inner product space, as a continuous linear map on the
Schwartz space.

This definition is only to define the Fourier transform, use `FourierTransform.fourierCLM` instead.
 -/
SchwartzMap.fourierTransformCLM : (𝕜 : Type u_1) →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℂ E] →
          [inst_3 : NormedSpace 𝕜 E] →
            [inst_4 : SMulCommClass ℂ 𝕜 E] →
              {V : Type u_3} →
                [inst_5 : NormedAddCommGroup V] →
                  [inst_6 : InnerProductSpace ℝ V] →
                    [FiniteDimensional ℝ V] →
                      [inst_8 : MeasurableSpace V] → [BorelSpace V] → SchwartzMap V E →L[𝕜] SchwartzMap V E
-- Init.Data.Vector.Lemmas
Vector.getElem?_flatten : ∀ {β : Type u_1} {m n : ℕ} {xss : Vector (Vector β m) n} {i : ℕ},
  xss.flatten[i]? = if hi : i < n * m then some xss[i / m][i % m] else none
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.isFinite : ∀ (self : FiniteAddGrp.{u}), Finite ↑self.toAddGrp
-- Mathlib.Data.DFinsupp.Multiset
/-- A DFinsupp version of `Multiset.toFinsupp`.  -/
Multiset.toDFinsupp : {α : Type u_1} → [DecidableEq α] → Multiset α →+ Π₀ (x : α), ℕ
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_whiskerRight'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.inv f) Z)
        h) =
    h
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The prime ideals in the localization of a commutative ring at a prime ideal I are in
order-preserving bijection with the prime ideals contained in I.  -/
IsLocalization.AtPrime.orderIsoOfPrime : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (I : Ideal R) →
            [hI : I.IsPrime] → [IsLocalization.AtPrime S I] → { p // p.IsPrime } ≃o { p // p.IsPrime ∧ p ≤ I }
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_functor_obj_ι_app_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K} (Y : J),
  (CategoryTheory.WithInitial.coconeEquiv.functor.obj t).ι.app (CategoryTheory.WithInitial.of Y) =
    CategoryTheory.Under.Hom.right (t.ι.app Y)
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.chunkedBody.inj : ∀ {ext : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)} {remaining : ℕ}
  {ext_1 : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)} {remaining_1 : ℕ},
  Std.Http.Protocol.H1.Reader.BodyState.chunkedBody ext remaining =
      Std.Http.Protocol.H1.Reader.BodyState.chunkedBody ext_1 remaining_1 →
    ext = ext_1 ∧ remaining = remaining_1
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_mulVec : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n]
  [inst_2 : Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α), M.mulVec (N.mulVec v) = (M * N).mulVec v
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (x : L),
  Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly
-- Mathlib.Control.Monad.Cont
ReaderT.mkLabel : {m : Type u → Type v} →
  {α : Type u_1} → {β : Type u} → (ρ : Type u) → MonadCont.Label α m β → MonadCont.Label α (ReaderT ρ m) β
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- An operator `T` is a formal adjoint of `S` if for all `x` in the domain of `T` and `y` in the
domain of `S`, we have that `⟪T x, y⟫ = ⟪x, S y⟫`.  -/
LinearPMap.IsFormalAdjoint : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : InnerProductSpace 𝕜 F] → (E →ₗ.[𝕜] F) → (F →ₗ.[𝕜] E) → Prop
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.instLEDynkinSystem : {α : Type u_3} → LE (MeasurableSpace.DynkinSystem α)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.reduceLTLE : Lean.Name → ℕ → Bool → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Algebra.Group.Defs
/-- An additive monoid is torsion-free if scalar multiplication by every non-zero element `n : ℕ` is
injective.  -/
IsAddTorsionFree : (M : Type u_2) → [AddMonoid M] → Prop
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftHomotopy_zero : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E))
  (H_0 : ∀ (a : A), H (0, a) = p (f a)) (a : A), (cov.liftHomotopy H f H_0) (0, a) = f a
-- Lean.Meta.SynthInstance
/-- Return type for `preprocess`  -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult : Type
-- Mathlib.Algebra.Algebra.Equiv
ULift.down_algEquiv_symm_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  (ULift.algEquiv.{u_1, u_2, u_3}.symm a).down = a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.productTriangle.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T T_1 : J → CategoryTheory.Pretriangulated.Triangle C) (e_T : T = T_1)
  [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  CategoryTheory.Pretriangulated.productTriangle T = CategoryTheory.Pretriangulated.productTriangle T_1
-- Mathlib.Topology.Algebra.Affine
Filter.Tendsto.midpoint : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V] {α : Type u_6} {l : Filter α}
  [inst_9 : Invertible 2] {f₁ f₂ : α → P} {p₁ p₂ : P},
  Filter.Tendsto f₁ l (nhds p₁) →
    Filter.Tendsto f₂ l (nhds p₂) → Filter.Tendsto (fun x => midpoint R (f₁ x) (f₂ x)) l (nhds (midpoint R p₁ p₂))
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.mono_right : ∀ {α : Type u_1} [inst : Preorder α] {x y : α},
  x ≤ y → ∀ {t : Ordnode α} {o : WithBot α}, t.Bounded o ↑x → t.Bounded o ↑y
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiff_toFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (self : Diffeomorph I I' M M' n), ContMDiff I I' n ⇑self.toEquiv
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  (X₁ X₂ : C),
  ((CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X₁)
        ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G X₁ X₂)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
          (F.map (CategoryTheory.Functor.OplaxMonoidal.δ L X₁ X₂))))
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionSemiHomClass.toMulActionSemiHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {φ : outParam (M → N)}
  {A : outParam (Type u_13)} {B : outParam (Type u_14)} {inst : Monoid M} {inst_1 : Monoid N} {inst_2 : Monoid A}
  {inst_3 : Monoid B} {inst_4 : MulDistribMulAction M A} {inst_5 : MulDistribMulAction N B} {inst_6 : FunLike F A B}
  [self : MulDistribMulActionSemiHomClass F φ A B], MulActionSemiHomClass F φ A B
-- Init.Data.SInt.Lemmas
Int16.ofNat_toNatClampNeg : ∀ (x : Int16), 0 ≤ x → Int16.ofNat x.toNatClampNeg = x
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- The additive character from `ZMod N` to the unit circle in `ℂ`, sending `j mod N` to
`exp (2 * π * I * j / N)`.  -/
ZMod.toCircle : {N : ℕ} → [NeZero N] → AddChar (ZMod N) Circle
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.range_le : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  Set.range ⇑(algebraMap R A) ⊆ ↑S
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- A *pattern* is a finite configuration in the full shift `A^G`.

It consists of:
* a full configuration `config : G → A` in the full shift;
* a finite subset `support : Finset G` of coordinates, called the support of `p`;
* a proof `condition` that outside `support`, `config` takes the default value of `A`.

Intuitively, a pattern is a "partial configuration" specifying finitely many values of
a configuration in `G → A` (the rest being `default`).
Patterns are the basic building blocks used to define subshifts via forbidden configurations.
Note that each pattern corresponds to a cylinder, which is the set of configurations
which agree with this pattern on its support.  -/
SymbolicDynamics.FullShift.Pattern : (A : Type u_1) → Type u_2 → [Inhabited A] → Type (max u_1 u_2)
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.heq_imp_of_eq_imp : ∀ {α : Sort u_1} {x y : α} {p : x ≍ y → Prop}, (∀ (he : x = y), p ⋯) → ∀ (he : x ≍ y), p he