mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Tape
/-- The `BlankExtends` partial order holds of `l₁` and `l₂` if `l₂` is obtained by adding
blanks (`default : Γ`) to the end of `l₁`.  -/
Turing.BlankExtends : {Γ : Type u_1} → [Inhabited Γ] → List Γ → List Γ → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_div_base : ∀ {a b : ℝ}, a ≠ 0 → b ≠ 0 → ∀ (c : ℝ), Real.logb (a / b) c = ((Real.logb a c)⁻¹ - (Real.logb b c)⁻¹)⁻¹
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_eq_one_of_not_module_finite : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ¬Module.Finite R M → ∀ (f : M →ₗ[R] M), LinearMap.det f = 1
-- Mathlib.Order.CompactlyGenerated.Basic
sSup_compact_le_eq : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] (b : α), sSup {c | IsCompactElement c ∧ c ≤ b} = b
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Translate a finite pattern `p` so that it occurs at the translate `v`, before completing into
a configuration.

On input `h : G`, we proceed as follows:
* if `h` lies in the left-translate of the support, i.e. `h ∈ p.support.image (v + ·)`,
  choose (noncomputably) `w ∈ p.support` with `v + w = h` and return `p.config w`;
* otherwise return `default`.

This definition does not assume left-cancellation; it only *chooses* a preimage.
Uniqueness (and the usual equations such as `Pattern.shift p v (v + w) = p.config w`)
require a left-cancellation hypothesis and are proved in separate lemmas.
 -/
SymbolicDynamics.FullShift.Pattern.shift : {A : Type u_1} →
  [inst : Inhabited A] → {G : Type u_2} → [AddMonoid G] → SymbolicDynamics.FullShift.Pattern A G → G → G → A
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.mk_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (f : A →⋆ₙₐ[R] B)
  (h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x) (h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
        { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
          { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y)
  (h₅ :
    ∀ (a : A),
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) =
        star ({ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)),
  { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } = f
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) (μ : MeasureTheory.Measure α)
  [μ.OuterRegular], (MeasureTheory.Measure.map (⇑f) μ).OuterRegular
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- `cocone F` is a colimit cocone, i.e. `F` is pro-represented by `incl F`.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.isColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone F)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Given a predicate `P`, one may associate to a multilinear map `f` a multilinear map
from the elements satisfying `P` to the multilinear maps on elements not satisfying `P`.
In other words, splitting the variables into two subsets one gets a multilinear map into
multilinear maps.
This is a linear map version of the function `MultilinearMap.domDomRestrict`.  -/
MultilinearMap.domDomRestrictₗ : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  MultilinearMap R M₁ M₂ →
                    (P : ι → Prop) →
                      [DecidablePred P] → MultilinearMap R (fun i => M₁ ↑i) (MultilinearMap R (fun i => M₁ ↑i) M₂)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The associator isomorphism which associates a binary biproduct.  -/
CategoryTheory.Limits.biprod.associator : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] → (P Q R : C) → (P ⊞ Q) ⊞ R ≅ P ⊞ Q ⊞ R
-- Mathlib.Data.Sym.Sym2
Sym2.mem_iff_exists : ∀ {α : Type u_1} {x : α} {z : Sym2 α}, x ∈ z ↔ ∃ y, z = s(x, y)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.of_constant_on_preconnected_clopens : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y},
  (∀ (U : Set X), IsPreconnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x) → IsLocallyConstant f
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_updateBucket_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β},
      Std.DHashMap.Internal.Raw.WFImp
        (Std.DHashMap.Internal.withComputedSize
          (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a (Std.DHashMap.Internal.AssocList.Const.alter a f)))
-- Init.SizeOf
Lean.ParserDescr.sepBy1.sizeOf_spec : ∀ (p : Lean.ParserDescr) (sep : String) (psep : Lean.ParserDescr) (allowTrailingSep : optParam Bool false),
  sizeOf (p.sepBy1 sep psep allowTrailingSep) = 1 + sizeOf p + sizeOf sep + sizeOf psep + sizeOf allowTrailingSep
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_gcd_cert.eq_3 : ∀ (a b g g_1 k : ℤ) (v : Lean.Grind.CommRing.Mon) (p_4 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.num g) (Lean.Grind.CommRing.Poly.num g_1)
      (Lean.Grind.CommRing.Poly.add k v p_4) =
    false
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSet_map_const : ∀ (X : TopCat) {Y : TopCat} (y : ↑Y), TopCat.toSSet.map (TopCat.const y) = SSet.const (TopCat.toSSetObj₀Equiv.symm y)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- Turn a right exact functor into an additive functor.  -/
CategoryTheory.AdditiveFunctor.ofRightExact : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [CategoryTheory.Limits.HasZeroObject C] →
              [CategoryTheory.Limits.HasZeroObject D] →
                [CategoryTheory.Limits.HasBinaryBiproducts C] → CategoryTheory.Functor (C ⥤ᵣ D) (C ⥤+ D)
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_subset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ⊆ Set.Iic b ↔ a ≤ b
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonzero.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα? : Option Q(PartialOrder «$α»)}
  {pf pf_1 : Q(«$e» ≠ 0)},
  Mathlib.Meta.Positivity.Strictness.nonzero pf = Mathlib.Meta.Positivity.Strictness.nonzero pf_1 → pf = pf_1
-- Init.Data.Dyadic.Basic
Rat.toDyadic.eq_2 : ∀ (x : ℚ) (n : ℕ), x.toDyadic (Int.negSucc n) = Dyadic.ofIntWithPrec (x.num / ↑(x.den <<< (n + 1))) (Int.negSucc n)
-- Init.Data.Nat.Div.Lemmas
Nat.div_le_iff_le_mul : ∀ {k x y : ℕ}, 0 < k → (x / k ≤ y ↔ x ≤ y * k + k - 1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coe_toContinuousMap : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (f : A →ₜ* B), f.toContinuousMap = ↑f
-- Init.Data.String.Bootstrap
String.Internal.extract : String → String.Pos.Raw → String.Pos.Raw → String
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.map_w : ∀ {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}
  {c c' : CategoryTheory.Limits.Cocone F} (f : c' ⟶ c) (G : CategoryTheory.Functor C D) (j : J),
  CategoryTheory.CategoryStruct.comp (G.map (c'.ι.app j)) (G.map f.hom) = G.map (c.ι.app j)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.toFunctor : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} → CategoryTheory.BasedFunctor 𝒳 𝒴 → CategoryTheory.Functor 𝒳.obj 𝒴.obj
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instMonad : {ι : Type} → Monad (Std.Internal.Parsec ι)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {C : Type u_3} {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{v_1, u_3} C] [inst_2 : CategoryTheory.Category.{v_2, u_4} D]
  (F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) C) (G : CategoryTheory.Functor C D),
  CategoryTheory.ReflQuiv.adj.homEquiv (F.comp G) = CategoryTheory.ReflQuiv.adj.homEquiv F ⋙rq G.toReflPrefunctor
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_omega0_omega0_opow : ∀ {a b : Ordinal.{u_1}},
  b ≠ 0 → (a < Ordinal.omega0 ^ Ordinal.omega0 ^ b ↔ ∃ c < b, ∃ n, a < Ordinal.omega0 ^ (Ordinal.omega0 ^ c * ↑n))
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves finite colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F.unop],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.Order.SuccPred.Relation
/-- For `n ≠ m`,`(n, m)` is in the transitive closure of a relation `~` if `i ~ succ i` and
`succ i ~ i` for all `i` between `n` and `m`.  -/
transGen_of_succ_of_ne : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → n ≠ m → Relation.TransGen r n m
-- Mathlib.Algebra.Homology.Opposite
/-- Given a category of complexes with objects in `V`, there is a natural equivalence between its
opposite category and a category of complexes with objects in `Vᵒᵖ`.  -/
HomologicalComplex.opEquivalence : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → (HomologicalComplex V c)ᵒᵖ ≌ HomologicalComplex Vᵒᵖ c.symm
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to
`N` using `Finsupp.sum`. This is an upgraded version of `Finsupp.liftAddHom`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
 -/
Finsupp.lsum : {α : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {R : Type u_5} →
        {R₂ : Type u_6} →
          (S : Type u_8) →
            [inst : Semiring R] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : AddCommMonoid N] →
                        [inst_6 : Module R₂ N] →
                          {σ : R →+* R₂} →
                            [inst_7 : Module S N] →
                              [inst_8 : SMulCommClass R₂ S N] → (α → M →ₛₗ[σ] N) ≃ₗ[S] (α →₀ M) →ₛₗ[σ] N
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerived_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  [inst_7 : H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ),
  CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n)
      (CategoryTheory.NatTrans.leftDerived β n)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α)
  (h_1 : (bs : List β) → motive [] bs) (h_2 : (a : α) → (as : List α) → motive (a :: as) [])
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)),
  (match a :: as, [] with
    | [], bs => h_1 bs
    | a :: as, [] => h_2 a as
    | a :: as, b :: bs => h_3 a as b bs) =
    h_2 a as
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe.eq_1 : ∀ (r : ℝ), ↑r = ↑r
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- **Alias** of `CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap`.

---

If `f` and `g` are simplicially homotopic maps of simplicial sets,
then they induce chain-homotopic maps on the singular chain complexes
with coefficients in `R`. The assumption is in `SimplicialObject.Homotopy`,
see also `SSet.Homotopy.chainComplexMap` for the
variant using `SSet.Homotopy` as an assumption.
 -/
singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasCoproducts C] →
        {X Y : SSet} →
          {f g : X ⟶ Y} →
            CategoryTheory.SimplicialObject.Homotopy f g →
              (R : C) → Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).getKey? k = (t₂.getKey? k).or (t₁.getKey? k)
-- Mathlib.Data.Opposite
/-- Make sure that `Opposite.op a` is pretty-printed as `op a` instead of `{ unop := a }` or
`⟨a⟩`.  -/
Opposite.unexpander_op : Lean.PrettyPrinter.Unexpander
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_iff_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, a ∈ m ↔ (m.get? a).isSome = true
-- Mathlib.Data.ZMod.Basic
ZMod.val_pow : ∀ {m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)], a.val ^ m < n → (a ^ m).val = a.val ^ m
-- Lean.DocString.Syntax
/-- Named argument  -/
Lean.Doc.Syntax.named_no_paren : Lean.ParserDescr
-- Mathlib.Topology.Compactness.Compact
prod_nhds_le_of_disjoint_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : Filter X} (y : Y),
  Disjoint f (Filter.cocompact X) → f ×ˢ nhds y ≤ nhdsSet (Set.univ ×ˢ {y})
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsFundamentalGroup.non_trivial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] {G : Type u_1} [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [inst_4 : TopologicalSpace G] [inst_5 : IsTopologicalGroup G]
  [inst_6 : CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G),
  (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
-- Init.Data.String.Lemmas.Splits
/-- Given a position that splits `s` into `t₁` and `t₂ ++ t₃` with witness `h`, constructs a position
`h.rotateRight` that splits `s` into `t₁ ++ t₂` and `t₃`. Use `h.splits_rotateRight` for the witness
that `h.rotateRight` splits `s` as required.
 -/
String.Slice.Pos.Splits.rotateRight : {s : String.Slice} → {p : s.Pos} → {t₁ t₂ t₃ : String} → p.Splits t₁ (t₂ ++ t₃) → s.Pos
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' → (Std.ExtHashMap.filterMap f m).getD k fallback = (m[k]?.bind (f k')).getD fallback
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.instReprFixedParamPerms.repr : Lean.Elab.FixedParamPerms → ℕ → Std.Format
-- Mathlib.Analysis.Real.Sqrt
/-- Bernoulli's inequality for exponent `1 / 2`, stated using `sqrt`.  -/
Real.sqrt_one_add_le : ∀ {x : ℝ}, -1 ≤ x → √(1 + x) ≤ 1 + x / 2
-- Lean.Language.Lean.Types
/-- Resulting parser state.  -/
Lean.Language.Lean.HeaderParsedState.parserState : Lean.Language.Lean.HeaderParsedState → Lean.Parser.ModuleParserState
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldr_eq_foldr_toProd' : ∀ {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δ → α → β → δ} {init : δ},
  List.foldr (fun a b => f b a.fst a.snd) init l =
    List.foldr (fun a b => f b a.1 a.2) init (List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivWithinAt.sin : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') s x
-- Mathlib.Order.Filter.ENNReal
NNReal.liminf_of_not_isCoboundedUnder : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal},
  ¬Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u → Filter.liminf u f = 0
-- Mathlib.Topology.Baire.Lemmas
/-- A set is residual (comeagre) if and only if it includes a dense `Gδ` set.  -/
mem_residual : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s : Set X}, s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t
-- Mathlib.Algebra.Order.Ring.Basic
/-- **Alias** of the reverse direction of `sq_pos_iff`. -/
sq_pos_of_ne_zero : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {a : R},
  a ≠ 0 → 0 < a ^ 2
-- Mathlib.Data.Multiset.FinsetOps
/-- **Alias** of the reverse direction of `Multiset.ndinter_eq_zero_iff_disjoint`. -/
Multiset.Disjoint.ndinter_eq_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, Disjoint s t → s.ndinter t = 0
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Kind.noConfusionType : Sort v✝ → Mathlib.Tactic.LibraryRewrite.Kind → Mathlib.Tactic.LibraryRewrite.Kind → Sort v✝
-- Mathlib.Logic.Equiv.Set
Equiv.preimage_image : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α), ⇑e ⁻¹' ⇑e '' s = s
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_lt_top_of_subset : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, t ⊆ s → μ s ≠ ⊤ → μ t < ⊤
-- Mathlib.Order.GaloisConnection.Basic
sSup_image2_eq_sInf_sInf : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) →
    (∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) →
      sSup (Set.image2 l s t) = l (sInf s) (sInf t)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom.ext : ∀ {B : Type u_1} {C : Type u_2} {inst : CategoryTheory.Bicategory C} {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {x y : X.Hom Y}, x.hom = y.hom → x = y
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.functor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C),
  (CategoryTheory.ShrinkHoms.functor C).obj X = CategoryTheory.ShrinkHoms.toShrinkHoms X
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.instIsModuleConvexSpaceSubtypeMem : ∀ {F : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : SetLike F M]
  [inst_6 : AddSubmonoidClass F M] [inst_7 : SMulMemClass F R M] [inst_8 : Convexity.ConvexSpace R M]
  [inst_9 : Convexity.IsModuleConvexSpace R M] (S : F), Convexity.IsModuleConvexSpace R ↥S
-- Lean.Elab.PreDefinition.WF.Main
Lean.Elab.wfRecursion : Lean.LocalContext × Lean.LocalInstances →
  Array Lean.Elab.PreDefinition → Array (Option Lean.Elab.TerminationMeasure) → Lean.Elab.TermElabM Unit
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_congr_set : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s =ᵐ[μ] t → μ.restrict s = μ.restrict t
-- Init.Data.List.Basic
List.elem.eq_2 : ∀ {α : Type u} [inst : BEq α] (a a_1 : α) (as : List α),
  List.elem a (a_1 :: as) =
    match a == a_1 with
    | true => true
    | false => List.elem a as
-- Batteries.Data.List.Basic
List.sectionsTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (acc : Array (List α)),
  List.sectionsTR.go l acc = Array.foldl (fun acc' l' => List.foldl (fun acc' a => acc'.push (a :: l')) acc' l) #[] acc
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- An `R`-finite torsion-free module has positive `finrank` iff it is nontrivial.  -/
Module.finrank_pos_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M], 0 < Module.finrank R M ↔ Nontrivial M
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_compl_iff : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded sᶜ ↔ Bornology.IsCobounded s
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Class `ProperlyDiscontinuousSMul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
`γ : Γ` move `K` to have nontrivial intersection with `L`.
 -/
ProperlyDiscontinuousSMul : (Γ : Type u_4) → (T : Type u_5) → [TopologicalSpace T] → [SMul Γ T] → Prop
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If `f x - x` is an integer number `m` for some point `x`, then `τ f = m`.
On the circle this means that a map with a fixed point has rotation number zero.  -/
CircleDeg1Lift.translationNumber_of_eq_add_int : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, f x = x + ↑m → f.translationNumber = ↑m
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.mk.inj : ∀ {name : Lean.Name} {levelParams : List Lean.Name} {type : Lean.Expr} {name_1 : Lean.Name}
  {levelParams_1 : List Lean.Name} {type_1 : Lean.Expr},
  { name := name, levelParams := levelParams, type := type } =
      { name := name_1, levelParams := levelParams_1, type := type_1 } →
    name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      ((CochainComplex.mappingCone.snd φ).v p p ⋯) =
    CategoryTheory.CategoryStruct.id (G.X p)