mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subring.Units
RingHom.instIsLocalHomSubtypeMemSubringEqLocusSubtype : ∀ {R : Type u_1} {T : Type u_2} [inst : Semiring T] [inst_1 : Ring R] (f g : R →+* T), IsLocalHom (f.eqLocus g).subtype
-- Mathlib.RingTheory.Etale.Finite
/-- Construct an isomorphism in `FiniteEtale R` from an algebra equivalence.  -/
CommAlgCat.FiniteEtale.isoMk : {R : Type u} → [inst : CommRing R] → {S T : CommAlgCat.FiniteEtale R} → (↑S.obj ≃ₐ[R] ↑T.obj) → (S ≅ T)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.toAddEquiv_toIntLinearEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {modM : Module ℤ M}
  {modM₂ : Module ℤ M₂} (e : M ≃ₗ[ℤ] M₂), (↑e).toIntLinearEquiv = e
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeM?.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (a : α) (as : List α),
  List.findSomeM? f (a :: as) = do
    let __do_lift ← f a
    match __do_lift with
      | some b => pure (some b)
      | none => List.findSomeM? f as
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.not_lt_of_not_le : ∀ {α : Type u} [inst : Preorder α] {x y : α}, ¬x ≤ y → ¬x < y
-- Mathlib.Data.List.Chain
List.IsChain.right_of_append : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α}, List.IsChain R (l₁ ++ l₂) → List.IsChain R l₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp},
  List.map Sigma.fst t.toList = t.keys
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Local equivalence between subsets `source` and `target` of `α` and `β` respectively. The
(global) maps `toFun : α → β` and `invFun : β → α` map `source` to `target` and conversely, and are
inverse to each other there. The values of `toFun` outside of `source` and of `invFun` outside of
`target` are irrelevant.  -/
PartialEquiv : Type u_5 → Type u_6 → Type (max u_5 u_6)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.mk : {A : Type u} →
  [inst : AddGroup A] →
    (toFilterBasis : FilterBasis A) →
      (∀ {U : Set A}, U ∈ toFilterBasis.sets → 0 ∈ U) →
        (∀ {U : Set A}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V + V ⊆ U) →
          (∀ {U : Set A}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V ⊆ (fun x => -x) ⁻¹' U) →
            (∀ (x₀ : A) {U : Set A},
                U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U) →
              AddGroupFilterBasis A
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  (x : CategoryTheory.SmallObject.FunctorObjIndex f πX),
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).π x = x.i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.contains (t.maxKeyD fallback) = true
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_one : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G],
  ContinuousLinearMap.lTensor G 1 = 1
-- Mathlib.Topology.Category.TopPair
TopPair.inclAdjProj₁_counit_app : ∀ (X : TopPair),
  TopPair.inclAdjProj₁.counit.app X =
    TopPair.ofHom (CategoryTheory.CategoryStruct.id TopPair.fst) (TopCat.isInitialPEmpty.to TopPair.snd) ⋯
-- Mathlib.FieldTheory.Finite.Basic
ZMod.castHom.congr_simp : ∀ {n m m_1 : ℕ} (e_m : m = m_1) (h : m ∣ n) (R : Type u_2) [inst : Ring R] [inst_1 : CharP R m],
  ZMod.castHom h R = ZMod.castHom ⋯ R
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.le_iff_exists_eq_append : ∀ {s : String} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String},
  p₁.Splits t₁ t₂ → p₂.Splits t₃ t₄ → (p₁ ≤ p₂ ↔ ∃ t₅, t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄)
-- Mathlib.Logic.Relation
Relation.EqvGen.instIsEquiv : ∀ {α : Type u_1} (r : α → α → Prop), IsEquiv α (Relation.EqvGen r)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lid_tmul : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (a : A),
  (Algebra.TensorProduct.lid R A) (r ⊗ₜ[R] a) = r • a
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.foldlM.loop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match 0 with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_1 ()
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.toIsValuativeTopology : ∀ {K : Type u_1} {inst : Field K} {inst_1 : ValuativeRel K} {inst_2 : TopologicalSpace K}
  [self : IsNonarchimedeanLocalField K], IsValuativeTopology K
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_inv_snd_assoc : ∀ (X Y : TopCat) {Z : TopCat} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp TopCat.prodSnd h
-- Mathlib.Algebra.Ring.Action.Pointwise.Finset
Finset.zero_mem_smul_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommMonoid M] [inst_3 : DecidableEq M]
  [inst_4 : Module R M] [Module.IsTorsionFree R M] {s : Finset R} {t : Finset M},
  0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
-- Mathlib.Algebra.IsPrimePow
isPrimePow_nat_iff_bounded : ∀ (n : ℕ), IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation from a metric space is an embedding  -/
Dilation.isEmbedding : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : EMetricSpace α] [inst_1 : FunLike F α β]
  [inst_2 : PseudoEMetricSpace β] [DilationClass F α β] (f : F), Topology.IsEmbedding ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.nodup_dropLast_support : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.support.dropLast.Nodup
-- Mathlib.Order.Filter.Map
Filter.mem_map_seq_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {m : α → β → γ} {s : Set γ},
  s ∈ (Filter.map m f).seq g ↔ ∃ t u, t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- An alternate formulation of `hasDerivAt_ofReal_cpow_const'`.  -/
hasDerivAt_ofReal_cpow_const : ∀ {x : ℝ}, x ≠ 0 → ∀ {r : ℂ}, r ≠ 0 → HasDerivAt (fun y => ↑y ^ r) (r * ↑x ^ (r - 1)) x
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context.mk.inj : ∀ {maxDepth? : Option ℕ} {forwardHypData : Aesop.ForwardHypData} {maxDepth?_1 : Option ℕ}
  {forwardHypData_1 : Aesop.ForwardHypData},
  { maxDepth? := maxDepth?, forwardHypData := forwardHypData } =
      { maxDepth? := maxDepth?_1, forwardHypData := forwardHypData_1 } →
    maxDepth? = maxDepth?_1 ∧ forwardHypData = forwardHypData_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- The pointwise subtraction of two finsets `s` and `t`: `s -ᵥ t = {x -ᵥ y | x ∈ s, y ∈ t}`.  -/
Finset.vsub : {α : Type u_2} → {β : Type u_3} → [VSub α β] → [DecidableEq α] → VSub (Finset α) (Finset β)
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.snd_prodOfFinsuppNat : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (f : P × M →ₗ[R] M) (x : ℕ →₀ P),
  (f.prodOfFinsuppNat x).2 = f (f.prodOfFinsuppNat ((Finsupp.comapDomain.addMonoidHom ⋯) x))
-- Mathlib.Analysis.Convex.StdSimplex
/-- The edges are contained in the simplex.  -/
segment_single_subset_stdSimplex : ∀ (𝕜 : Type u_2) {ι : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] [ZeroLEOneClass 𝕜] [IsOrderedRing 𝕜] (i j : ι),
  segment 𝕜 (Pi.single i 1) (Pi.single j 1) ⊆ stdSimplex 𝕜 ι
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], Topology.IsLocallyConstructible Set.univ
-- Init.Data.Bool
Bool.lt_of_le_of_ne : ∀ {x y : Bool}, x ≤ y → x ≠ y → x < y
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_lintegral_enorm_tendsto' : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : NNReal),
      MeasureTheory.AEStronglyMeasurable f μ →
        Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (nhds ↑I) → MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitor_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.f =
    CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X.src) (CategoryTheory.Limits.terminal.from X.src)
-- Mathlib.GroupTheory.QuotientGroup.ModEq
AddCommGroup.not_modEq_iff_ne_mod_zmultiples : ∀ {G : Type u_1} [inst : AddCommGroup G] {a b p : G}, ¬a ≡ b [PMOD p] ↔ ↑a ≠ ↑b
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.mul.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} [inst_1 : SizeOf J]
  (a a_1 : RingCat.Colimits.Prequotient F), sizeOf (a.mul a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable sections of a vector bundle at a point within a set
in terms of the preferred trivialization at that point.  -/
mdifferentiableWithinAt_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] (s : (b : B) → E b) {u : Set B}
  {b₀ : B}, MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun b => (↑(trivializationAt F E b₀) ⟨b, s b⟩).2) b₀
-- Mathlib.Topology.Algebra.MulAction
Specializes.smul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] {a b : M} {x y : X}, a ⤳ b → x ⤳ y → (a • x) ⤳ (b • y)
-- Mathlib.RingTheory.Etale.Kaehler
/-- let `p` be a submonoid of an `R`-algebra `S`. Then `Sₚ ⊗ H¹(L_{S/R}) ≃ H¹(L_{Sₚ/R})`.  -/
Algebra.tensorH1CotangentOfIsLocalization : (R : Type u_1) →
  {S : Type u_2} →
    (T : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [IsScalarTower R S T] →
                    (M : Submonoid S) →
                      [IsLocalization M T] → TensorProduct S T (Algebra.H1Cotangent R S) ≃ₗ[T] Algebra.H1Cotangent R T
-- Std.Http.Data.Headers
/-- Retrieves the last header value for the given key.
Returns `none` if the header is absent.
 -/
Std.Http.Headers.getLast? : Std.Http.Headers → Std.Http.Header.Name → Option Std.Http.Header.Value
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_1.splitter : (motive : Lean.Meta.Grind.SolverTerms × Lean.Meta.Grind.PendingSolverPropagationsData✝ → Sort u_1) →
  (x : Lean.Meta.Grind.SolverTerms × Lean.Meta.Grind.PendingSolverPropagationsData✝) →
    ((s : Lean.Meta.Grind.SolverTerms) → (p : Lean.Meta.Grind.PendingSolverPropagationsData✝) → motive (s, p)) →
      motive x
-- Mathlib.MeasureTheory.OuterMeasure.AE
Set.EqOn.aeEq : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {s : Set α} {f g : α → β},
  Set.EqOn f g s → μ sᶜ = 0 → f =ᵐ[μ] g
-- Batteries.Lean.Meta.InstantiateMVars
/-- Instantiate metavariables in the type of the given metavariable, update the
metavariable's declaration and return the new type.
 -/
Lean.MVarId.instantiateMVarsInType : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → [Lean.MonadError m] → Lean.MVarId → m Lean.Expr
-- Mathlib.Data.NNReal.Basic
NNReal.coe_sum : ∀ {ι : Type u_2} (s : Finset ι) (f : ι → NNReal), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.IsoLift.mk.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂Iso) (eq : Lean.Expr) (e_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (eq_1 : Lean.Expr), ({ e := e, eq := eq } = { e := e_1, eq := eq_1 }) = (e = e_1 ∧ eq = eq_1)
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.insert_empty : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s → TopologicalSpace.IsTopologicalBasis (insert ∅ s)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The (exact) sequence `H^n(f₁) ⊞ H^{n-1}(f₃) ⟶ H^n(f₁ ≫ f₂) ⟶ E^n(f₁, f₂, f₃) ⟶ 0`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (k ⟶ l) →
                    (f₁₂ : i ⟶ k) →
                      CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂ →
                        (n₀ n₁ n₂ : ℤ) →
                          autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_1 →
                            autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_3 →
                              CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).A = c.pt
-- Lean.Meta.Tactic.Repeat
/-- Implementation of `repeat'` and `repeat1'`.

`repeat'Core f` runs `f` on all of the goals to produce a new list of goals,
then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
or until `maxIters` total calls to `f` have occurred.

Returns a boolean indicating whether `f` succeeded at least once, and
all the remaining goals (i.e. those on which `f` failed).
 -/
Lean.Meta.repeat'Core : {m : Type → Type} →
  {ε : Type u_1} →
    {s : Type} →
      [Monad m] →
        [MonadExcept ε m] →
          [Lean.MonadBacktrack s m] →
            [Lean.MonadMCtx m] →
              (Lean.MVarId → m (List Lean.MVarId)) → List Lean.MVarId → optParam ℕ 100000 → m (Bool × List Lean.MVarId)
-- Mathlib.NumberTheory.Divisors
/-- `properDivisors n` is the `Finset` of divisors of `n`, other than `n`.
By convention, we set `properDivisors 0 = ∅`.  -/
Nat.properDivisors : ℕ → Finset ℕ
-- Mathlib.Topology.Algebra.Group.Pointwise
IsTopologicalAddGroup.t2Space_of_zero_sep : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G],
  (∀ (x : G), x ≠ 0 → ∃ U ∈ nhds 0, x ∉ U) → T2Space G
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- If `g` generates the group `G` and `g'` is an element of another group `G'` whose order
divides that of `g`, then there is a homomorphism `G →* G'` mapping `g` to `g'`.  -/
monoidHomOfForallMemZpowers : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : Group G] →
      [inst_1 : Group G'] → {g : G} → (∀ (x : G), x ∈ Subgroup.zpowers g) → {g' : G'} → orderOf g' ∣ orderOf g → G →* G'
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- The monoidal category structure on the category of `R`-coalgebras induced by the
equivalence with `Comon(R-Mod)`. This is just an auxiliary definition; the `MonoidalCategory`
instance we make in `Mathlib/Algebra/Category/CoalgCat/Monoidal.lean` has better
definitional equalities.  -/
CoalgCat.instMonoidalCategoryAux : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalCategory (CoalgCat R)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.one_add_tan_sq_mul_cos_sq_eq_one : ∀ {x : ℂ}, Complex.cos x ≠ 0 → (1 + Complex.tan x ^ 2) * Complex.cos x ^ 2 = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The essential image of a fully faithful functor between cartesian-monoidal categories is the
same on additive monoid objects as on objects.  -/
CategoryTheory.Functor.essImage_mapAddMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful] {M : CategoryTheory.AddMon D},
  F.mapAddMon.essImage M ↔ F.essImage M.X
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (toPartialEquiv : PartialEquiv H E) →
                toPartialEquiv.source = Set.univ →
                  (if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv)
                    else Set.range ↑toPartialEquiv = Set.univ) →
                    (interior (Set.range ↑toPartialEquiv)).Nonempty →
                      autoParam (Continuous ↑toPartialEquiv) ModelWithCorners.continuous_toFun._autoParam →
                        autoParam (Continuous toPartialEquiv.invFun) ModelWithCorners.continuous_invFun._autoParam →
                          ModelWithCorners 𝕜 E H
-- Mathlib.Data.FinEnum
List.Pi.enum.eq_1 : ∀ {α : Type u_1} [inst : FinEnum α] (β : α → Type u_3) [inst_1 : (a : α) → FinEnum (β a)],
  List.Pi.enum β = List.map (fun f x => f x ⋯) ((FinEnum.toList α).pi fun x => FinEnum.toList (β x))
-- Lean.DocString.Types
/-- Textual content.
 -/
Lean.Doc.Inline.text : {i : Type u} → String → Lean.Doc.Inline i
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The canonical limit presentation of any object over a point.  -/
CategoryTheory.Limits.LimitPresentation.self : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (X : C) → CategoryTheory.Limits.LimitPresentation PUnit.{s + 1} X
-- Aesop.Rule
Aesop.SafeRuleInfo.penalty : Aesop.SafeRuleInfo → ℤ
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.trans.eq_1 : ∀ {ι : Type u_1} (c₁ c₂ : ComplexShape ι),
  c₁.trans c₂ = { Rel := Relation.Comp c₁.Rel c₂.Rel, next_eq := ⋯, prev_eq := ⋯ }
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRco.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Rco α) → Decidable (x = x_1)
-- Init.Data.Array.Count
Array.count_eq_zero : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, Array.count a xs = 0 ↔ a ∉ xs
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_inf_eq_iInf : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [WellFoundedLT β] (f : α → β), ∃ t, t.inf f = ⨅ a, f a
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.replaceRecApps.processApp : (recFnName : Lean.Name) → ℕ → Lean.Expr → Lean.Expr → Lean.Elab.WF.RecM✝ recFnName Lean.Expr
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- See `IsLocalSite.faithful_constantSheaf` for a version for `w`-locally small sites.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafConstantSheafOfHasColimitsOfSizeOfHasProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.IsLocalSite]
  (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{v, v, v', u'} A]
  [CategoryTheory.Limits.HasProducts A] [inst_5 : CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.constantSheaf J A).Faithful
-- Mathlib.Algebra.Exact.Basic
AddMonoidHom.exact_of_comp_eq_zero_of_ker_le_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, g.comp f = 0 → g.ker ≤ f.range → Function.Exact ⇑f ⇑g
-- Mathlib.Logic.Equiv.Defs
/-- Restatement of `Equiv.left_inv` in terms of `Function.LeftInverse`.  -/
Equiv.left_inv' : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.LeftInverse ⇑e.symm ⇑e
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLT.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithTop α → WithTop α → Sort u_2) (x : WithTop α) (h_1 : (x : WithTop α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match x, none with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_1 x
-- Mathlib.Algebra.Notation.Prod
Prod.swap_mul : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).swap = p.swap * q.swap
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.eq_1 : ∀ (M : Type u_1), MulArchimedeanOrder M = M
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' : C} (f' : Y' ⟶ X') (g' : Z' ⟶ X')
  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] (γ₁ : Y' ⟶ Y) (γ₂ : Z' ⟶ Z) (γ₃ : X' ⟶ X)
  (comm₁ : CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
  (comm₂ : CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g),
  CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂ =
    CategoryTheory.ChosenPullbacksAlong.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f' g') γ₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f' g') γ₂) ⋯
-- Mathlib.GroupTheory.QuotientGroup.Defs
Subgroup.orderIsoCon.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.orderIsoCon =
    { toFun := fun N => QuotientGroup.con ↑N, invFun := fun c => ⟨c.subgroup, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.minkowskiBound_lt_top : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  NumberField.mixedEmbedding.minkowskiBound K I < ⊤
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallySeparated_empty : ∀ {α : Type u} [inst : TopologicalSpace α], IsTotallySeparated ∅
-- Mathlib.AlgebraicTopology.SingularSet
/-- The singular simplicial set of a totally disconnected space is the constant simplicial set.  -/
TopCat.toSSetIsoConst : (X : TopCat) →
  [TotallyDisconnectedSpace ↑X] → TopCat.toSSet.obj X ≅ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ↑X