mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_nil : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β}, List.minIdxOn? f [] = none
-- Init.Prelude
/-- The homogeneous version of `HPow`: `a ^ b : α` where `a : α`, `b : β`.
(The right argument is not the same as the left since we often want this even
in the homogeneous case.)

Types can choose to subscribe to particular defaulting behavior by providing
an instance to either `NatPow` or `HomogeneousPow`:
- `NatPow` is for types whose exponents is preferentially a `Nat`.
- `HomogeneousPow` is for types whose base and exponent are preferentially the same.
 -/
Pow : Type u → Type v → Type (max u v)
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forIn'.loop.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive __do_lift
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instIteratorLoop.loop : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [DecidableLT α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          {n : Type u → Type w} →
            [Monad n] →
              (γ : Type u) →
                (Pl : α → γ → ForInStep γ → Prop) →
                  (LargeEnough : α → Prop) →
                    (∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) →
                      (upperBound : α) →
                        γ →
                          (next : α) →
                            LargeEnough next →
                              ((out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))) → n γ
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.fst_integral_withLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [CompleteSpace F],
  MeasureTheory.Integrable f μ → (∫ (x : X), f x ∂μ).fst = ∫ (x : X), (f x).fst ∂μ
-- Mathlib.Order.Defs.LinearOrder
LinOrd.str : (self : LinOrd) → LinearOrder ↑self
-- Mathlib.Order.Hom.Lattice
SupHom.mk_le_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (toFun₁ toFun₂ : α → β)
  (map_sup₁ : ∀ (a b : α), toFun₁ (a ⊔ b) = toFun₁ a ⊔ toFun₁ b)
  (map_sup₂ : ∀ (a b : α), toFun₂ (a ⊔ b) = toFun₂ a ⊔ toFun₂ b),
  { toFun := toFun₁, map_sup' := map_sup₁ } ≤ { toFun := toFun₂, map_sup' := map_sup₂ } ↔ toFun₁ ≤ toFun₂
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- `autMap` is surjective, if the source is also Galois.  -/
CategoryTheory.PreGaloisCategory.autMap_surjective_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsGalois A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f : A ⟶ B), Function.Surjective (CategoryTheory.PreGaloisCategory.autMap f)
-- Lean.Meta.LazyDiscrTree
/-- Creates an entry for a subterm of an initial entry.

This is slightly more efficient than using `fromExpr` on subterms since it avoids a redundant call
to `whnf`.
 -/
Lean.Meta.LazyDiscrTree.InitEntry.mkSubEntry : {α : Type} → Lean.Meta.LazyDiscrTree.InitEntry α → ℕ → α → Lean.MetaM (Lean.Meta.LazyDiscrTree.InitEntry α)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.termT : Lean.ParserDescr
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.toFun_unique' : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g : L ≃+* L)
  (c : ZMod (Nat.card ↥(rootsOfUnity n L))),
  (∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val) → c = modularCyclotomicCharacter.toFun n g
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.ExtTreeMap.unitOfList l cmp).getKey! k' = k
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The essential image of a full and faithful functor between cartesian-monoidal categories is the
same on group objects as on objects.  -/
CategoryTheory.Functor.essImage_mapGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful] {G : CategoryTheory.Grp D},
  F.mapGrp.essImage G ↔ F.essImage G.X
-- Init.Grind.AC
Lean.Grind.AC.eq_orient : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs →
    Lean.Grind.AC.Seq.denote ctx rhs = Lean.Grind.AC.Seq.denote ctx lhs
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.S.eq_1 : ModularGroup.S = ⟨!![0, -1; 1, 0], ModularGroup.S._proof_1⟩
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀`, and
`g` is integrable and has a limit at `x₀`, then `φᵢ • g` is eventually integrable.  -/
integrableOn_peak_smul_of_integrableOn_of_tendsto : ∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E}
  {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → ℝ} {a : E},
  MeasurableSet s →
    t ∈ nhdsWithin x₀ s →
      (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)) →
        Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) →
          (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) →
            MeasureTheory.IntegrableOn g s μ →
              Filter.Tendsto g (nhdsWithin x₀ s) (nhds a) →
                ∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn (fun x => φ i x • g x) s μ
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.b : ℝ → ℕ → ℝ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → Inhabited (CategoryTheory.Grp C)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toList_flatMap : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] [inst_8 : Std.Iterator α m β] [inst_9 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β},
  (Std.IterM.flatMap f it₁).toList = List.flatten <$> (Std.IterM.mapM (fun b => (f b).toList) it₁).toList
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitCoconeOfComp_isColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.ColimitCocone (F.comp G)),
  (CategoryTheory.Functor.Final.colimitCoconeOfComp F t).isColimit =
    (CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv F t.cocone).symm t.isColimit
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.coeFn.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : MulOneClass α] [inst_1 : CommMonoid β],
  MonoidHom.coeFn α β = { toFun := fun g => ⇑g, map_one' := ⋯, map_mul' := ⋯ }
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.specParse : String → Except String Std.Time.FormatString
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList_C : ∀ {R : Type u_1} [inst : Semiring R] {x : R}, x ≠ 0 → (Polynomial.C x).coeffList = [x]
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
/-- Variant of `toList_filterMapWithPostcondition_filterMapWithPostcondition` that is intended to be
used with the `apply` tactic. Because neither the LHS nor the RHS determine all implicit parameters,
it cannot be used easily with `rw` or `simp`.
 -/
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition' : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : γ → Std.Iterators.PostconditionT o (Option δ)} {fg : β → Std.Iterators.PostconditionT o (Option δ)}
  {it : Std.IterM m β},
  (∀ (b : β),
      (fg b).run = do
        let __do_lift ← liftM (f b).run
        match __do_lift with
          | none => pure none
          | some fb => (g fb).run) →
    (Std.IterM.filterMapWithPostcondition g (Std.IterM.filterMapWithPostcondition f it)).toList =
      (Std.IterM.filterMapWithPostcondition fg it).toList
-- Mathlib.Data.Fin.Fin2
/-- Converts a `Fin` into a `Fin2`.  -/
Fin2.ofFin : {n : ℕ} → Fin n → Fin2 n
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.add_right : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {a b : FreeNonUnitalNonAssocAlgebra R X}
  (c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (a + c) (b + c)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context : Type
-- Mathlib.Data.Part
/-- Retrieves the value of `a : Part α` if it exists, and return the provided default value
otherwise.  -/
Part.getOrElse : {α : Type u_1} → (a : Part α) → [Decidable a.Dom] → α → α
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G G_1 : C} (e_G : G = G_1) [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} (A A_1 : CategoryTheory.Subobject X),
  A = A_1 →
    CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG A =
      CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject ⋯ A_1
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- Given monoid morphisms `φᵢ : Nᵢ → M` and `f : M → P`, if we have sufficient commutativity, then
`f ∘ (∐ᵢ φᵢ) = ∐ᵢ (f ∘ φᵢ)`  -/
MonoidHom.comp_noncommPiCoprod : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)} {P : Type u_4} [inst_3 : Monoid P]
  {f : M →* P}
  (hcomm' : optParam (Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y)) ⋯),
  f.comp (MonoidHom.noncommPiCoprod ϕ hcomm) = MonoidHom.noncommPiCoprod (fun i => f.comp (ϕ i)) hcomm'
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_equiv_eq_map_symm' : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : N ≃* G) (K : Subgroup G),
  Subgroup.comap f.toMonoidHom K = Subgroup.map f.symm.toMonoidHom K
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.e : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Weekday
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.comp_id : ∀ {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), f.comp (NonUnitalStarAlgHom.id R A) = f
-- Init.Omega.Coeffs
/-- Shim for `List.length`.  -/
Lean.Omega.Coeffs.length : Lean.Omega.Coeffs → ℕ
-- Mathlib.Data.Finsupp.Order
Finsupp.instSMulPosMono : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Zero β] [inst_2 : Preorder β]
  [inst_3 : SMulZeroClass α β] [SMulPosMono α β], SMulPosMono α (ι →₀ β)
-- Mathlib.MeasureTheory.Group.Arithmetic
List.measurable_sum : ∀ {M : Type u_2} {α : Type u_3} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} (l : List (α → M)), (∀ f ∈ l, Measurable f) → Measurable l.sum
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.smul : ∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E}
  [inst_2 : SMul 𝕝 E] [SMulCommClass 𝕜 𝕝 E] (a : 𝕝), Balanced 𝕜 s → Balanced 𝕜 (a • s)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_add_right : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Add β] [inst_1 : Add γ] (f : α → β → γ),
  (∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂) →
    ∀ (A : Matrix l m α) (B₁ B₂ : Matrix n p β),
      Matrix.kroneckerMap f A (B₁ + B₂) = Matrix.kroneckerMap f A B₁ + Matrix.kroneckerMap f A B₂
-- Mathlib.Order.Preorder.Chain
IsMaxChain.symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxChain r s → IsMaxChain (flip r) s
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Metric.isClosed_closedEBall : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {a : α} {r : ENNReal}, IsClosed (Metric.closedEBall a r)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.oneMul : FirstOrder.Field.FieldAxiom
-- Init.Data.Option.Lemmas
Option.eq_none_iff_forall_not_mem : ∀ {α : Type u_1} {o : Option α}, o = none ↔ ∀ (a : α), a ∉ o
-- Mathlib.Order.BooleanAlgebra.Basic
compl_sdiff_compl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ \ yᶜ = y \ x
-- Mathlib.Analysis.Complex.Basic
RCLike.toContinuousLinearMap_complexLinearIsometryEquiv : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (h : RCLike.im RCLike.I = 1),
  ↑↑(RCLike.complexLinearIsometryEquiv h) = RCLike.map 𝕜 ℂ
-- Init.Core
/-- A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quotient.mk`.
 -/
Quotient.ind : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop}, (∀ (a : α), motive ⟦a⟧) → ∀ (q : Quotient s), motive q
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.algebraMap_def : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : CommSemiring R] [inst_6 : (i : ι) → Semiring (G i)] [inst_7 : (i : ι) → Algebra R (G i)]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] (i : ι) (r : R),
  (algebraMap R (DirectLimit G f)) r = ⟦⟨i, (algebraMap R (G i)) r⟩⟧
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.target.injEq : ∀ (a a_1 : Lean.SubExpr.Pos), (Lean.SubExpr.GoalLocation.target a = Lean.SubExpr.GoalLocation.target a_1) = (a = a_1)
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.instToFormatRewriteLemma : Std.ToFormat Mathlib.Tactic.LibraryRewrite.RewriteLemma
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {f g : Y ⟶ h.pullback},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f h.p₁ = CategoryTheory.CategoryStruct.comp g h.p₁ ∧
      CategoryTheory.CategoryStruct.comp f h.p₂ = CategoryTheory.CategoryStruct.comp g h.p₂
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_π_two : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨2, SSet.horn₃₁.desc.multicofork_π_two._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 2).inv f₂
-- Mathlib.Algebra.Star.Subalgebra
/-- If some predicate holds for all `x ∈ (s : Set A)` and this predicate is closed under the
`algebraMap`, addition, multiplication and star operations, then it holds for `a ∈ adjoin R s`.  -/
StarAlgebra.adjoin_induction : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A}
  {p : (x : A) → x ∈ StarAlgebra.adjoin R s → Prop},
  (∀ (x : A) (h : x ∈ s), p x ⋯) →
    (∀ (r : R), p ((algebraMap R A) r) ⋯) →
      (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
            p x hx → p y hy → p (x * y) ⋯) →
          (∀ (x : A) (hx : x ∈ StarAlgebra.adjoin R s), p x hx → p (star x) ⋯) →
            ∀ {a : A} (ha : a ∈ StarAlgebra.adjoin R s), p a ha
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageActionItem.mk : String → Lean.Lsp.MessageActionItem
-- Lean.Meta.Tactic.Simp.Rewrite
/-- For `(← getConfig).index := false`, Lean 3 style `simp` theorem retrieval.
Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.
 -/
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.rewrite?.rewriteNoIndex? : Lean.Expr →
  Lean.Meta.SimpTheoremTree →
    Lean.PHashSet Lean.Meta.Origin → String → Bool → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Mathlib.Order.Filter.Basic
Filter.NeBot.ne : ∀ {α : Type u} {f : Filter α}, f.NeBot → f ≠ ⊥
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.left' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.MonoidalCoherence X Y] →
          CategoryTheory.MonoidalCoherence X
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_sub_nonneg : ∀ {α : Type u_1} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ),
  0 ≤ BoundedContinuousFunction.const α ‖f‖ - f
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {f : A → B} {h : ∀ (x y : A), f (x + y) = f x + f y}
  {h₀ :
    ∀ (m : R) (x : A),
      { toFun := f, map_add' := h }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h }.toFun x}
  {h₁ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = CoalgebraStruct.counit}
  {h₂ :
    TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ
        CoalgebraStruct.comul =
      CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ }}
  {h₃ : B → A}
  {h₄ :
    Function.LeftInverse h₃
      { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun}
  {h₅ :
    Function.RightInverse h₃
      { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun},
  ⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄,
        right_inv := h₅ } =
    f
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.cocone_naturality : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat) {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (MonCat.Colimits.coconeMorphism F j') =
    MonCat.Colimits.coconeMorphism F j
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path includes the data of `n + 1` 0-simplices in `X`.  -/
SSet.Path.vertex : {X : SSet} → {n : ℕ} → X.Path n → Fin (n + 1) → X.obj (Opposite.op { len := 0 })
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P P_1 : RootPairing ι R M N} (e_P : P = P_1) [inst_8 : P.IsCrystallographic] (i i_1 : ι),
  i = i_1 → ∀ (j j_1 : ι), j = j_1 → RootPairing.chainTopCoeff i j = RootPairing.chainTopCoeff i_1 j_1
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.ι_mapBifunctorMapMap : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  (g : Y₁ ⟶ Y₂) [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (i : I) (j : J) (k : K)
  (h : p (i, j) = k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h)
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) =
    CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j))
      (CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j))
        (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h))
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and
`g` tends to `Filter.atBot` then `f * g` tends to `Filter.atBot`.  -/
Filter.Tendsto.pos_mul_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  0 < C →
    Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_bijective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂],
  Function.Bijective ContinuousAffineEquiv.symm
-- Mathlib.Tactic.TermCongr
/-- Replace all `term` antiquotations in a term using the given `expand` function.  -/
Mathlib.Tactic.TermCongr.processAntiquot : Lean.Term → (Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term
-- Init.Data.List.Zip
List.zipWith_foldl_eq_zip_foldl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : δ}
  {g : δ → γ → δ}, List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun r p => g r (f p.1 p.2)) i (l₁.zip l₂)