mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Log
/-- Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)
 -/
Lean.getRefPosition : {m : Type → Type} → [Monad m] → [Lean.MonadLog m] → m Lean.Position
-- Init.Prelude
/-- `-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator). -/
Neg.neg : {α : Type u} → [self : Neg α] → α → α
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImpRight.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (_n : ℕ) (φ ψ : L.BoundedFormula α _n)
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α n) →
        (ψ : L.BoundedFormula α (n + 1)) →
          motive n φ
            ((ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum))
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α n) → (ψ : L.BoundedFormula α (n + 1)) → motive n φ ψ.all)
  (h_3 : (_n : ℕ) → (φ ψ : L.BoundedFormula α _n) → motive _n φ ψ),
  (∀ (ψ_1 : L.BoundedFormula α (_n + 1)),
      ψ = (ψ_1.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum →
        False) →
    (∀ (ψ_1 : L.BoundedFormula α (_n + 1)), ψ = ψ_1.all → False) →
      (match _n, φ, ψ with
        | n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum =>
          h_1 n φ ψ
        | n, φ, ψ.all => h_2 n φ ψ
        | _n, φ, ψ => h_3 _n φ ψ) =
        h_3 _n φ ψ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on `s` and `f 0 = 0` and `a : X → A` is continuous and `a x` is
nonnegative for all `x` and `s` is a common neighborhood of the quasispectra of `a x` for all `x`,
then `fun x ↦ cfcₙ f (a x)` is continuous.

This is weaker than `Continuous.cfcₙ_nnreal` since it requires `f` to be continuous on a
*neighborhood* of the quasispectra, but in practice it is often easier to apply because `s` is not
required to be compact, nor does it require an indexed family of compact sets. This is proven using
`Continuous.cfcₙ_nnreal` and `upperHemicontinuous_quasispectrum_nnreal` to produce the necessary
family of compact sets.  -/
Continuous.cfcₙ_nnreal_of_mem_nhdsSet : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [CompleteSpace A] [inst_13 : TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A},
  s ∈ nhdsSet (⋃ x, quasispectrum NNReal (a x)) →
    Continuous a →
      autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfcₙ_nnreal_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) Continuous.cfcₙ_nnreal_of_mem_nhdsSet._auto_3 →
          autoParam (f 0 = 0) Continuous.cfcₙ_nnreal_of_mem_nhdsSet._auto_5 → Continuous fun x => cfcₙ f (a x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKey! k = default
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- A real embedding as a ring homomorphism from `K` to `ℝ` .  -/
NumberField.ComplexEmbedding.IsReal.embedding : {K : Type u_1} → [inst : Field K] → {φ : K →+* ℂ} → NumberField.ComplexEmbedding.IsReal φ → K →+* ℝ
-- Mathlib.Data.Sym.Basic
Sym.mk.congr_simp : ∀ {α : Type u_1} {n : ℕ} (m m_1 : Multiset α) (e_m : m = m_1) (h : m.card = n), Sym.mk m h = Sym.mk m_1 ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.sub_emod_emod : ∀ (m n k : ℤ), (m - n % k) % k = (m - n) % k
-- Mathlib.Data.Matrix.DMatrix
DMatrix.map_add : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → AddMonoid (α i j)] {β : m → n → Type w}
  [inst_1 : (i : m) → (j : n) → AddMonoid (β i j)] (f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) (M N : DMatrix m n α),
  ((M + N).map fun i j => ⇑f) = (M.map fun i j => ⇑f) + N.map fun i j => ⇑f
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_comp_apply_of_eq : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {g : M' → M''} {y : M'},
  MDiffAt g y →
    MDiffAt f x → f x = y → ∀ (v : TangentSpace I x), (mfderiv% (g ∘ f) x) v = (mfderiv% g y) ((mfderiv% f x) v)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_getElem_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support[0] = u
-- Mathlib.Order.Category.Semilat
SemilatSupCat.Iso.mk_hom_toFun : ∀ {α β : SemilatSupCat} (e : α.X ≃o β.X) (a : α.X), (SemilatSupCat.Iso.mk e).hom a = e a
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] {K L : HomologicalComplex C c} (f : K ⟶ L),
  CategoryTheory.IsIso (HomologicalComplexUpToQuasiIso.Q.map f) ↔ HomologicalComplex.quasiIso C c f
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₁ : ∀ (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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X_1 : J),
  (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X).app X_1).τ₁ =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X₁
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.card_empty : FirstOrder.Language.empty.card = 0
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toSeminormedCommGroup : {E : Type u_5} → [NormedCommGroup E] → SeminormedCommGroup E
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instAdd : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → Add (ContDiffMapSupportedIn E F n K)
-- Mathlib.Data.Set.Countable
Set.Countable.image : ∀ {α : Type u} {β : Type v} {s : Set α}, s.Countable → ∀ (f : α → β), (f '' s).Countable
-- Mathlib.SetTheory.Ordinal.Exponential
_private.Mathlib.SetTheory.Ordinal.Exponential.0.Ordinal.log.eq_1 : ∀ (b x : Ordinal.{u_1}), Ordinal.log b x = sSup ((fun x => b ^ x) ⁻¹' Set.Iic x)
-- Mathlib.Data.List.TFAE
/-- **Alias** of the reverse direction of `List.tfae_not_iff`. -/
List.TFAE.not : ∀ {l : List Prop}, l.TFAE → (List.map Not l).TFAE
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- `SpecialLinearGroup n R` is the group of `n` by `n` `R`-matrices with determinant equal to 1.
 -/
Matrix.SpecialLinearGroup : (n : Type u) → [DecidableEq n] → [Fintype n] → (R : Type v) → [CommRing R] → Type (max 0 u v)
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- This lemma follows from the finite correctness proof, the determinant equality, and
by simplifying the difference.  -/
GenContFract.sub_convs_eq : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp →
    have g := GenContFract.of v;
    have B := (g.contsAux (n + 1)).b;
    have pB := (g.contsAux n).b;
    v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Typeclass expressing that for all `G`-split pairs `f,g`, `G` reflects colimits for
`parallelPair f g`.  -/
CategoryTheory.Monad.ReflectsColimitOfIsSplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor D C → Prop
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (G : C)
  (f : G ⟶ G), (CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite G) f = { unop' := f }
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- A reformulation of the isomorphism `toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁`  -/
CategoryTheory.Idempotents.DoldKan.isoN₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.IsIdempotentComplete C] →
        [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C] →
          (CategoryTheory.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor.comp
              CategoryTheory.Preadditive.DoldKan.equivalence.functor ≅
            AlgebraicTopology.DoldKan.N₁
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- Cast a valuation subring to a local subring.  -/
ValuationSubring.toLocalSubring : {K : Type u_3} → [inst : Field K] → ValuationSubring K → LocalSubring K
-- Mathlib.Order.Filter.Partial
/-- The forward map of a filter under a relation. Generalization of `Filter.map` to relations. Note
that `Rel.core` generalizes `Set.preimage`.  -/
Filter.rmap : {α : Type u} → {β : Type v} → SetRel α β → Filter α → Filter β
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.bijOn_periodicPts : ∀ {α : Type u_1} (f : α → α), Set.BijOn f (Function.periodicPts f) (Function.periodicPts f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Extract an isomorphism between right components from an isomorphism in
`CatCospanTransform F G F' G'`.  -/
CategoryTheory.Limits.CatCospanTransform.rightIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  (ψ ≅ ψ') → (ψ.right ≅ ψ'.right)
-- Mathlib.Order.Hom.Order
OrderHom.instTopOrderHom : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → [OrderTop β] → Top (α →o β)
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Finds theorems whose bodies were elaborated in the current infotrees and whose (full)
declaration names satisfy `nameFilter`. Checks their type to see if it contains instance hypotheses
that (1) are unused in the remainder of the type (2) have types which satisfy `instanceTypeFilter`.
(Note: `instanceTypeFilter` is non-monadic, and may encounter bound variables in its argument. This
is a performance optimization. `isAppOrForallOfConstP` may be useful in detecting constant
applications and types of the form `∀ (...), bar ..` here.)

If any such parameters are found in the type of a theorem `foo`, we create a telescope in which the
types and free variables of the unused parameters are available as
`unusedParams : Array Parameter := #[p₁, p₂, ..., pₙ]`, as well as the theorem `thm : ConstantVal`
and current infotree `t`, and run `log t thm unusedParams`.

A simple pattern is therefore
```
fun _ thm unusedParams => do
  logLint linter.fooLinter (← getRef) m!"\
    {thm.name.unusedInstancesMsg unusedParams}\n\n\
    <extra caption>"
```
which logs
```null
`{foo}` has the hypothes(is/es):
  • {p₁}
  • {p₂}
  ⋮
  • {pₙ}
which (is/are) not used in the remainder of the type.

<extra caption>

Note: This linter can be disabled with `set_option {linter.fooLinter.name} false`
```
pluralizing as appropriate.
 -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Lean.Syntax.logUnusedInstancesInTheoremsWhere : Lean.Syntax →
  (Lean.Expr → Bool) →
    (Lean.Elab.InfoTree →
        Lean.ConstantVal → Array Mathlib.Linter.UnusedInstancesInType.Parameter✝ → Lean.Elab.TermElabM Unit) →
      (optParam (Lean.ConstantVal → Bool) fun x => true) → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.LinearAlgebra.TensorProduct.Free
/-- The `A`-algebra isomorphism `A ⊗[R] V ≃ₗ[A] (ι → A)` coming from an
`ι`-indexed basis of a finite free `R`-module `V`.
 -/
Algebra.TensorProduct.equivPiOfFiniteBasis : {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring R] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → {ι : Type u_4} → Module.Basis ι R V → [Finite ι] → TensorProduct R A V ≃ₗ[A] ι → A
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.instInhabited : (V : Type u_3) → Inhabited (Digraph V)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformly.add` -/
TendstoLocallyUniformly.fun_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l → TendstoLocallyUniformly (fun i i_1 => F i i_1 + G i i_1) (fun i => f i + g i) l
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_comp : ∀ (R : Type u_1) [inst : Semiring R] (p q : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S],
  (p.comp q).smeval x = p.smeval (q.smeval x)
-- Mathlib.Data.Finset.Sum
Finset.disjSum_empty : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α), s.disjSum ∅ = Finset.map Function.Embedding.inl s
-- Mathlib.Data.Set.Function
Set.mapsTo_of_subsingleton' : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton β] (f : α → β),
  (s.Nonempty → t.Nonempty) → Set.MapsTo f s t
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_lt_sqrtTwoAddSeries : ∀ (n : ℕ), Real.pi < 2 ^ (n + 1) * √(2 - Real.sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
-- Mathlib.Data.Sym.Sym2
/-- The symmetric square is equivalent to multisets of cardinality
two. (This is currently a synonym for `equivSym`, but it's provided
in case the definition for `Sym` changes.)  -/
Sym2.equivMultiset : (α : Type u_4) → Sym2 α ≃ { s // s.card = 2 }
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.visitFn : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Util.Superscript
/-- The parser `superscript(term)` parses a superscript. Basic usage is:
```
local syntax:arg term:max superscript(term) : term
local macro_rules | `($a:term $b:superscript) => `($a ^ $b)
```
Given a notation like this, the expression `2⁶⁴` parses and expands to `2 ^ 64`.

Note that because of Unicode limitations, not many characters can actually be typed inside the
superscript, so this should not be used for complex expressions. Legal superscript characters:
```
⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ𐞥ʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾꟴᴿᵀᵁⱽᵂᵝᵞᵟᵋᶿᶥᶹᵠᵡ⁺⁻⁼⁽⁾
```
 -/
Mathlib.Tactic.superscript : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.ACounit_X : ∀ (A : Type u_1) {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (b : B),
  (MvPolynomial.ACounit A B) (MvPolynomial.X b) = b
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
mapping). It is a linear equivalence.  -/
toWeakSpace : (𝕜 : Type u_2) →
  (E : Type u_4) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] → [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → E ≃ₗ[𝕜] WeakSpace 𝕜 E
-- Mathlib.Algebra.CharP.Invertible
/-- A natural number `t` is invertible in a semifield `K` if the characteristic of `K` does not
divide `t`.  -/
invertibleOfRingCharNotDvd : {K : Type u_2} → [inst : Semifield K] → {t : ℕ} → ¬ringChar K ∣ t → Invertible ↑t
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
/-- A 2-square stays Guitart exact if we replace the top and bottom functors
by isomorphic functors. See also `whiskerHorizontal_iff`.  -/
CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {T' : CategoryTheory.Functor C₁ D₁} {B' : CategoryTheory.Functor C₂ D₂} [w.GuitartExact] (α : T ≅ T') (β : B ≅ B'),
  (w.whiskerHorizontal α.inv β.hom).GuitartExact
-- Mathlib.Order.UpperLower.Closure
UpperSet.erase_idem : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (a : α), (s.erase a).erase a = s.erase a
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- If a continuous linear map is a topology embedding, then it is expands the distances
by a positive factor.  -/
ContinuousLinearMap.antilipschitz_of_isEmbedding : ∀ {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (f : E →L[𝕜] Fₗ),
  Topology.IsEmbedding ⇑f → ∃ K, AntilipschitzWith K ⇑f
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.TimeZone.Offset
-- Lean.Meta.TryThis
/-- Style the same way as a hypothesis appearing in the infoview.  -/
Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis : Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instZero.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] [inst_3 : Zero X], AddOreLocalization.instZero = { zero := AddOreLocalization.zero }
-- Mathlib.LinearAlgebra.TensorAlgebra.Grading
TensorAlgebra.GradedAlgebra.ι_apply : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (TensorAlgebra.GradedAlgebra.ι R M) m =
    (DirectSum.of (fun i => ↥((TensorAlgebra.ι R).range ^ i)) 1) ⟨(TensorAlgebra.ι R) m, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.FullyFaithful.preservesZeroMorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (hF : F.FullyFaithful),
  F.PreservesZeroMorphisms
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.preserves_map : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α β : Type u} (x : α → β) (y : F α),
  (fun {α} => η.app α) (x <$> y) = x <$> (fun {α} => η.app α) y
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.opEquivOpOver_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T),
  (CategoryTheory.Under.opEquivOpOver X).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Under (Opposite.op X)))
-- Mathlib.Analysis.Asymptotics.Lemmas
Filter.Tendsto.isBigO_one : ∀ {α : Type u_1} (F : Type u_4) {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {f' : α → E'}
  {l : Filter α} [inst_2 : One F] [NormOneClass F] {c : E'}, Filter.Tendsto f' l (nhds c) → f' =O[l] fun _x => 1
-- Mathlib.Data.PNat.Basic
PNat.lt_add_one_iff : ∀ {a b : ℕ+}, a < b + 1 ↔ a ≤ b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView_tree_impl_eq_maxView! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  (Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).tree.impl = (Std.DTreeMap.Internal.Impl.maxView! k v l r).tree
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_comp_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
      h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h).hom h_1))
-- Init.Data.String.Lemmas.Intercalate
String.join_eq_foldl : ∀ {l : List String}, String.join l = List.foldl (fun r s => r ++ s) "" l
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `IsCyclotomicExtension {1} A B`, then the image of `A` in `B` equals `B`.  -/
IsCyclotomicExtension.singleton_one : ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [h : IsCyclotomicExtension {1} A B], ⊥ = ⊤
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.natCast_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (n : ℕ), ↑n = MonoidAlgebra.single 1 ↑n
-- Mathlib.Algebra.DirectSum.Module
/-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
components of the direct sum, the disjoint union of these bases is a basis for `M`.  -/
DirectSum.IsInternal.collectedBasis : {R : Type u} →
  [inst : Semiring R] →
    {ι : Type v} →
      [dec_ι : DecidableEq ι] →
        {M : Type u_1} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              {A : ι → Submodule R M} →
                DirectSum.IsInternal A →
                  {α : ι → Type u_2} → ((i : ι) → Module.Basis (α i) R ↥(A i)) → Module.Basis ((i : ι) × α i) R M
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulZeroClass : {M₀ : Type u_1} →
  [inst : TopologicalSpace M₀] → [inst_1 : MulZeroClass M₀] → [ContinuousMul M₀] → MulZeroClass (SeparationQuotient M₀)