mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.precoverage_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C},
  P ≤ Q → P.precoverage ≤ Q.precoverage
-- Mathlib.Topology.Separation.Basic
ContinuousWithinAt.eq_const_of_mem_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {f : X → Y}
  {s : Set X} {x : X} {c : Y}, ContinuousWithinAt f s x → x ∈ closure s → (∀ y ∈ s, f y = c) → f x = c
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.OuterMeasure.trim 0 = 0
-- Mathlib.RingTheory.Etale.Basic
RingHom.formallyEtale_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).FormallyEtale ↔ Algebra.FormallyEtale R S
-- Mathlib.Order.Ideal
Order.Ideal.coe_sup_eq : ∀ {P : Type u_1} [inst : DistribLattice P] {I J : Order.Ideal P}, ↑(I ⊔ J) = {x | ∃ i ∈ I, ∃ j ∈ J, x = i ⊔ j}
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) (a : B),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.mk' S).obj a = S.obj a
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.smulRight_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [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₂] [inst_5 : TopologicalSpace R] [inst_6 : (i : ι) → TopologicalSpace (M₁ i)]
  [inst_7 : TopologicalSpace M₂] [inst_8 : ContinuousSMul R M₂] (f : ContinuousMultilinearMap R M₁ R) (z : M₂)
  (a : (i : ι) → M₁ i), (f.smulRight z) a = f a • z
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_two_mul_add_one : ∀ (n : ℤ), (2 * n + 1).negOnePow = -1
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- An embedding of `X` into `Y`, with `X` nonempty, defines a partial homeomorphism
whose source is all of `X`. The converse is also true; see `PartialHomeomorph.isEmbedding`.  -/
Topology.IsEmbedding.toPartialHomeomorph : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (f : X → Y) → Topology.IsEmbedding f → [Nonempty X] → PartialHomeomorph X Y
-- Batteries.Data.Nat.Lemmas
Nat.testBit_ofBits_lt : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ) (h : i < n), (Nat.ofBits f).testBit i = f ⟨i, h⟩
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.leadingCoeff_abs : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)), (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|
-- Lean.Parser.Do
Lean.Parser.Term.doLetRec : Lean.Parser.Parser
-- Mathlib.Topology.Constructions
isOpenMap_sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, IsOpenMap (Sigma.mk i)
-- Init.Data.SInt.Lemmas
Int64.right_eq_add : ∀ {a b : Int64}, b = a + b ↔ a = 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.toInteger_coe : ∀ {K : Type u} [inst : Field K] {k : ℕ} [inst_1 : NeZero k] {x : NumberField.RingOfIntegers K}
  (hx : IsPrimitiveRoot (↑x) k), hx.toInteger = x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_union_of_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.of_finiteType : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [IsNoetherianRing A] {f : A →+* B},
  f.FiniteType ↔ f.FinitePresentation
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- The generators of a presented monoid generate the presented monoid. That is, the submonoid
closure of the set of generators equals `⊤`.  -/
PresentedMonoid.closure_range_of : ∀ {α : Type u_2} (rels : FreeMonoid α → FreeMonoid α → Prop),
  Submonoid.closure (Set.range (PresentedMonoid.of rels)) = ⊤
-- Mathlib.GroupTheory.IsSubnormal
AddSubgroup.IsSubnormal.below.step : ∀ {G : Type u_2} [inst : AddGroup G] {motive : (a : AddSubgroup G) → a.IsSubnormal → Prop} (H K : AddSubgroup G)
  (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.addSubgroupOf K).Normal),
  AddSubgroup.IsSubnormal.below hSubn → motive K hSubn → AddSubgroup.IsSubnormal.below ⋯
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.one_le_order_iff_constCoeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R},
  1 ≤ f.order ↔ MvPowerSeries.constantCoeff f = 0
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `⊤ \ a` is `￢a`  -/
CompletelyDistribLattice.top_sdiff : ∀ {α : Type u} [self : CompletelyDistribLattice α] (a : α), ⊤ \ a = ￢a
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε], q ≠ 0 → μ ≠ 0 → MeasureTheory.eLpNorm' 0 q μ = 0
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.add.inj : ∀ {a : Lean.Name} {a_1 : Lean.Syntax} {a_2 : Lean.Name} {a_3 : Lean.Syntax},
  Simps.ProjectionRule.add a a_1 = Simps.ProjectionRule.add a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Std.Net.Addr
/-- Either a `SocketAddressV4` or `SocketAddressV6`.
 -/
Std.Net.SocketAddress : Type
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.instHasLimitsOfShapeOverOfWithTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (X : C) [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.WithTerminal J) C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Over X)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.lift_comp_zero_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddMonObj.zero))
      CategoryTheory.AddMonObj.add =
    f
-- Mathlib.Topology.Inseparable
IsClosedMap.specializingMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → SpecializingMap f
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioc_disjoint_Ioi : ∀ {α : Type v} [inst : Preorder α] {a b c : α}, b ≤ c → Disjoint (Set.Ioc a b) (Set.Ioi c)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex)
  (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2))
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g +
        CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1)))
  {Z_1 : C} (h : Q.complex.X (n + 2) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w)
      (CategoryTheory.CategoryStruct.comp (Q.complex.d (n + 3) (n + 2)) h) =
    CategoryTheory.CategoryStruct.comp
      (f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g') h
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- More general version of `isIso_ι_of_isColimit`.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit' : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantFrom i₀ →
    ∀ [CategoryTheory.IsFiltered J] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
      (j : J) (ι : i₀ ⟶ j), CategoryTheory.IsIso (c.ι.app j)
-- Mathlib.Algebra.Group.PUnit
PUnit.inv_eq : ∀ (x : PUnit.{u_1 + 1}), x⁻¹ = PUnit.unit
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Functor.mapCocone₂_pt : ∀ {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] (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  {K₁ : CategoryTheory.Functor J₁ C₁} {K₂ : CategoryTheory.Functor J₂ C₂} (c₁ : CategoryTheory.Limits.Cocone K₁)
  (c₂ : CategoryTheory.Limits.Cocone K₂), (G.mapCocone₂ c₁ c₂).pt = (G.obj c₁.pt).obj c₂.pt
-- Mathlib.Tactic.Polynomial.Basic
Mathlib.Tactic.Polynomial.map_algebraMap : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (r : R),
  Polynomial.map (algebraMap R A) ((algebraMap R (Polynomial R)) r) = (algebraMap A (Polynomial A)) ((algebraMap R A) r)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.equiv_lim : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] (s : CauSeq β abv),
  s ≈ CauSeq.const abv s.lim
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- A version of `Set.pi` for subgroups. Given an index set `I` and a family of submodules
`s : Π i, Subgroup f i`, `pi I s` is the subgroup of dependent functions `f : Π i, f i` such that
`f i` belongs to `pi I s` whenever `i ∈ I`.  -/
Subgroup.pi : {η : Type u_7} →
  {f : η → Type u_8} → [inst : (i : η) → Group (f i)] → Set η → ((i : η) → Subgroup (f i)) → Subgroup ((i : η) → f i)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.hasSameRoot : Lean.Meta.Grind.Goal → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Analysis.Convex.EGauge
/-- The extended gauge of a point `x` in an indexed product
with respect to a product of finitely many balanced sets `U i`, `i ∈ I`,
(and the whole spaces for the other indices)
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.

This version assumes the following technical condition:
- either `I` is the universal set;
- or one of `x i`, `i ∈ I`, is nonzero;
- or `𝕜` is nontrivially normed.
 -/
egauge_pi' : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] {I : Set ι},
  I.Finite →
    ∀ {U : (i : ι) → Set (E i)},
      (∀ i ∈ I, Balanced 𝕜 (U i)) →
        ∀ (x : (i : ι) → E i),
          I = Set.univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (nhdsWithin 0 {0}ᶜ).NeBot →
            egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.eq_adjoin_primitive_root : ∀ (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  {μ : CyclotomicField n K}, IsPrimitiveRoot μ n → CyclotomicRing n A K = ↥A[μ]
-- Mathlib.Data.Finsupp.MonomialOrder
/-- `syn` is an additive commutative monoid  -/
MonomialOrder.addCommMonoidSyn : {σ : Type u_1} → (self : MonomialOrder σ) → AddCommMonoid self.syn
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_notMem_sub_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, 0 ∉ s - t ↔ Disjoint s t
-- Lean.Elab.App
/-- Process a `fType` of the form `{x : A} → B x`.
This method assume `fType` is a function type  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.processImplicitArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_apply_hom_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (X_1 : CategoryTheory.Sheaf J (Type (max v' v)))
  (a :
    (((CategoryTheory.evaluation Cᵒᵖ (Type (max v v'))).comp
              (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max v v'))
                        (Type (max (max v v') u))).obj
                    CategoryTheory.uliftFunctor.{u, max v v'}).comp
                ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type (max v v')))
                      (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj
                  (CategoryTheory.sheafToPresheaf J (Type (max v v')))))).obj
          X).obj
      X_1)
  (X_2 : Cᵒᵖ)
  (a_1 :
    (Opposite.unop
          (((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).comp
                  (CategoryTheory.sheafToPresheaf J (Type (max v v')))).op.obj
            X)).obj
      X_2),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app X_1)) a).hom.app X_2))
      a_1 =
    ((((CategoryTheory.uliftYonedaOpCompCoyoneda.inv.app X).app X_1.obj).hom' a).app X_2).hom'
      (((J.uliftYonedaCompSheafToPresheaf.hom.app (Opposite.unop X)).app X_2).hom' a_1)
-- Mathlib.Data.List.Sort
List.Subset.antisymm_of_sortedLT : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁ ⊆ l₂ → l₂ ⊆ l₁ → l₁.SortedLT → l₂.SortedLT → l₁ = l₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.getKey? (t.maxKey he) = some (t.maxKey he)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filterMap_eq_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a},
  Std.ExtDHashMap.filterMap (fun k v => some (f k v)) m = Std.ExtDHashMap.map f m
-- Mathlib.Order.Concept
/-- **Alias** of `Concept.extent_max`. -/
Concept.extent_sup : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r),
  (c ⊔ d).extent = lowerPolar r (c.intent ∩ d.intent)
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_eq_ofIntTruncate : ∀ {x : ℤ} {h₁ : ISize.minValue.toInt ≤ x} {h₂ : x ≤ ISize.maxValue.toInt}, ISize.ofIntLE x h₁ h₂ = ISize.ofIntClamp x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A category `HasWidePushouts` if it has all colimits of shape `WidePushoutShape J`, i.e. if it
has a wide pushout for every collection of morphisms with the same domain.  -/
CategoryTheory.Limits.HasWidePushouts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.ncoeff_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : VertexOperator R V) (n : ℤ), VertexOperator.ncoeff A n = HVertexOperator.coeff A (-n - 1)
-- Init.Prelude
/-- Although `TrailingParserDescr` is an abbreviation for `ParserDescr`, Lean will
look at the declared type in order to determine whether to add the parser to
the leading or trailing parser table. The determination is done automatically
by the `syntax` command.
 -/
Lean.TrailingParserDescr : Type
-- Mathlib.Data.Matrix.Basis
/-- For a commutative semiring `R`, the center of `Matrix n n R` is the range of `scalar n`
(i.e., the span of `{1}`).  -/
Matrix.center_eq_range : ∀ {n : Type u_3} (R : Type u_5) [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommSemiring R],
  Set.center (Matrix n n R) = Set.range ⇑(Matrix.scalar n)
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The range of a surjective `AddMonoid` homomorphism is the whole of the codomain.  -/
AddMonoidHom.range_eq_top_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_7} [inst_1 : AddGroup N] (f : G →+ N),
  Function.Surjective ⇑f → f.range = ⊤
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallIsBigOIsTheta : {α : Type u_1} →
  {E : Type u_3} →
    {G : Type u_5} →
      {F' : Type u_7} →
        [inst : Norm E] →
          [inst_1 : Norm G] →
            [inst_2 : SeminormedAddCommGroup F'] →
              {l : Filter α} → Trans (Asymptotics.IsBigO l) (Asymptotics.IsTheta l) (Asymptotics.IsBigO l)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.eq_1 : ∀ {α : Type u}, FreeGroup.Red = Relation.ReflTransGen FreeGroup.Red.Step
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- The zeroth convergent of `ξ` is `⌊ξ⌋`.  -/
Real.convergent_zero : ∀ (ξ : ℝ), ξ.convergent 0 = ↑⌊ξ⌋
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateIsoEquiv_apply_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : l₂ ≅ l₁),
  ((CategoryTheory.Bicategory.conjugateIsoEquiv adj₁ adj₂) α).inv =
    (CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₁) α.inv
-- Batteries.Data.String.Lemmas
String.utf8Len.eq_def : ∀ (x : List Char),
  String.utf8Len x =
    match x with
    | [] => 0
    | c :: cs => String.utf8Len cs + c.utf8Size
-- Mathlib.Analysis.Convex.GaugeRescale
mapsTo_gaugeRescale_closure : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {s t : Set E},
  Convex ℝ s → s ∈ nhds 0 → Convex ℝ t → 0 ∈ t → Absorbent ℝ t → Set.MapsTo (gaugeRescale s t) (closure s) (closure t)
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_alter_of_beq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β}, (k == k') = true → (k' ∈ m.alter k f ↔ (f m[k]?).isSome = true)
-- Mathlib.Order.BoundedOrder.Monotone
Monotone.forall : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop},
  (∀ (x : β), Monotone (P x)) → Monotone fun y => ∀ (x : β), P x y
-- Mathlib.Tactic.FBinop
FBinopElab.instInhabitedSRec : Inhabited FBinopElab.SRec
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.congr_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) {Y : C} {f g : Y ⟶ X} (h : f = g)
  (hf : (↑S).arrows f), ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instIsEquivalenceOppositeSymmOpFunctor : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V], (HomologicalComplex.opFunctor V c).IsEquivalence
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- The functor `FormalCoproduct C ⥤ SimplicialObject (FormalCoproduct C)`
which sends a formal coproduct to its Cech object.  -/
CategoryTheory.Limits.FormalCoproduct.cechFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasFiniteProducts C] →
      CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C)
        (CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C))
-- Mathlib.Order.InitialSeg
PrincipalSeg.ofElement_toFun : ∀ {α : Type u_4} (r : α → α → Prop) (a : α) (self : { x // r x a }), (PrincipalSeg.ofElement r a).toFun self = ↑self
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Arith.Linear.LinExpr →
      Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
  (left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam)
  (right_triangle :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam)
  (unit_1 : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (counit_1 : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
  (left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit_1 counit_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam)
  (right_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit_1 counit_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam),
  ({ unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
      { unit := unit_1, counit := counit_1, left_triangle := left_triangle_1, right_triangle := right_triangle_1 }) =
    (unit = unit_1 ∧ counit = counit_1)
-- Mathlib.Tactic.ITauto
/-- * `classical = false`: `(p: Decidable A) ⊢ A ∨ ¬A`
* `classical = true`: `(p: Prop) ⊢ p ∨ ¬p`
 -/
Mathlib.Tactic.ITauto.Proof.em : Bool → Lean.Name → Mathlib.Tactic.ITauto.Proof