mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Basic
String.Slice.mk.congr_simp : ∀ (str : String) (startInclusive startInclusive_1 : str.Pos) (e_startInclusive : startInclusive = startInclusive_1)
  (endExclusive endExclusive_1 : str.Pos) (e_endExclusive : endExclusive = endExclusive_1)
  (startInclusive_le_endExclusive : startInclusive ≤ endExclusive),
  { str := str, startInclusive := startInclusive, endExclusive := endExclusive,
      startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
    { str := str, startInclusive := startInclusive_1, endExclusive := endExclusive_1,
      startInclusive_le_endExclusive := ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- If `f : X ⟶ Y` is a morphism of schemes with quasi-compact source and affine target,
`f` induces an injection on global sections, then `f` is dominant.  -/
AlgebraicGeometry.isDominant_of_of_appTop_injective : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [CompactSpace ↥X],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) →
    AlgebraicGeometry.IsDominant f
-- Mathlib.Order.Comparable
instReflCompRel : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], Std.Refl (CompRel r)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.unitCompPartialBijective_natural : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (A : C) {B B' : C} (h : B ⟶ B')
  (hB : i.essImage B) (hB' : i.essImage B') (f : A ⟶ B),
  (CategoryTheory.unitCompPartialBijective A hB') (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB) f) h
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.mem_finPairsLT : ∀ {n : ℕ} {a : (_ : Fin n) × Fin n}, a ∈ Equiv.Perm.finPairsLT n ↔ a.snd < a.fst
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.union_left_iff : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasureTheory.AEDisjoint μ (s ∪ t) u ↔ MeasureTheory.AEDisjoint μ s u ∧ MeasureTheory.AEDisjoint μ t u
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.bind_assoc : ∀ {α : Type u} {β : Type v} {γ : Type w} (s : Stream'.WSeq α) (f : α → Stream'.WSeq β) (g : β → Stream'.WSeq γ),
  (s.bind f).bind g ~ʷ s.bind fun x => (f x).bind g
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraidedObj_snd_β : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (CategoryTheory.Center.ofBraidedObj X).snd.β Y = β_ X Y
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S}
  {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A)
  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c)
  {d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)} (g : F.Hom G)
  (t : CategoryTheory.Limits.Multifork (G.multicospanIndex P)) (hd : CategoryTheory.Limits.IsLimit d),
  (f.comp g).mapMultiforkOfIsLimit P hc t =
    CategoryTheory.CategoryStruct.comp (g.mapMultiforkOfIsLimit P hd t) (f.mapMultiforkOfIsLimit P hc d)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- An upper estimate on the remainder. This estimate works with `m ∈ ℝ` satisfying `1 < m` and is
stronger than the estimate `LiouvilleNumber.remainder_lt` below. However, the latter estimate is
more useful for the proof.  -/
LiouvilleNumber.remainder_lt' : ∀ (n : ℕ) {m : ℝ}, 1 < m → LiouvilleNumber.remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1).factorial)
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is convex on `S` and left-differentiable at `y ∈ S`, then the slope of any secant
line with right endpoint at `y` is bounded above by the left derivative of `f` at `y`.  -/
ConvexOn.slope_le_of_hasDerivWithinAt_Iio : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Iio y) y → slope f x y ≤ f'
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteOfIsImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsImmersion f], AlgebraicGeometry.LocallyQuasiFinite f
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqLhs.inj : ∀ {gen gen_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen = Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen_1 → gen = gen_1
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instMin.eq_1 : ∀ {E : Type u_3} [inst : AddCommGroup E],
  AddGroupSeminorm.instMin =
    { min := fun p q => { toFun := fun x => ⨅ y, p y + q (x - y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.contDiffWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → x ∈ s → ContDiffWithinAt 𝕜 n f s x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_toSubtype : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
      (CategoryTheory.Limits.biproduct.toSubtype f p) =
    CategoryTheory.CategoryStruct.id (⨁ Subtype.restrict p f)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.ofEq_apply : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X), (AddActionHom.ofEq h f) a = f a
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The group isomorphism between group homs `G → H` and bialgebra homs `R[G] → R[H]` of group
algebras over a domain.  -/
AddMonoidAlgebra.mapDomainBialgHomAddEquiv : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] →
          [inst_2 : AddCommGroup G] →
            [inst_3 : AddCommGroup H] →
              (G →+ H) ≃+ Additive (WithConv (AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- Half of **Jordan's inequality** for `cos`.  -/
Real.one_sub_mul_le_cos : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 1 - 2 / Real.pi * x ≤ Real.cos x
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.toComplementedLattice : ∀ {R : Type u_2} {inst : Ring R} {M : Type u_4} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : IsSemisimpleModule R M], ComplementedLattice (Submodule R M)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_zero : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], NonemptyInterval.pure 0 = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {h' : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.DistinctKeys l →
    ∀ (h : l.Perm l'), Std.Internal.List.getEntry a l h' = Std.Internal.List.getEntry a l' ⋯
-- Mathlib.Logic.Small.Basic
small_quot : ∀ {α : Type u} [Small.{v, u} α] (r : α → α → Prop), Small.{v, u} (Quot r)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfcₙ_le_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : ℝ),
  autoParam (ContinuousOn f (quasispectrum 𝕜 a)) norm_cfcₙ_le_iff._auto_1 →
    autoParam (f 0 = 0) norm_cfcₙ_le_iff._auto_3 →
      autoParam (p a) norm_cfcₙ_le_iff._auto_5 → (‖cfcₙ f a‖ ≤ c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ ≤ c)
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_mul_of_summable_norm : ∀ {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : NormedRing R] [CompleteSpace R] {f : ι → R} {g : ι' → R},
  (Summable fun x => ‖f x‖) → (Summable fun x => ‖g x‖) → Summable fun x => f x.1 * g x.2
-- Mathlib.Data.List.MinMax
List.mem_argmin_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {m : α} [inst_1 : DecidableEq α],
  m ∈ List.argmin f l ↔ m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → List.idxOf m l ≤ List.idxOf a l
-- Lean.Parser.Basic
Lean.Parser.charLitFn : Lean.Parser.ParserFn
-- Mathlib.Topology.Compactness.Compact
IsClosed.exists_minimal_nonempty_closed_subset : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {S : Set X},
  IsClosed S → S.Nonempty → ∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V
-- Std.Async.Signal
/-- If:
- `s` is not yet running start listening and return an `AsyncTask` that will resolve once the
   previously configured signal is received.
- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`.

The resolved `AsyncTask` contains the signal number that was received.
 -/
Std.Async.Signal.Waiter.wait : Std.Async.Signal.Waiter → IO (Std.Async.AsyncTask ℤ)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_mono : ∀ {α : Type u_1} {s t : Set (Set α)}, s ⊆ t → MeasurableSpace.generateFrom s ≤ MeasurableSpace.generateFrom t
-- Mathlib.Order.Interval.Multiset
Multiset.Ioo_cons_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  a < b → a ::ₘ Multiset.Ioo a b = Multiset.Ico a b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.any_keys : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulHashable α] [EquivBEq α] {p : α → Bool}, (↑m).keys.any p = (↑m).any fun a x => p a
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.mul_left : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ᵣ b → ∀ (c : α), a ∣ᵣ c * b
-- Mathlib.Algebra.Lie.Abelian
/-- A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action
on it is trivial.  -/
LieModule.maxTrivLinearMapEquivLieModuleHom : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [inst_6 : LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] →
                            [inst_10 : LieModule R L N] →
                              ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N)) ≃ₗ[R] M →ₗ⁅R,L⁆ N
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Ric α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_induction : ∀ {M : Type u_3} [inst : AddCommMonoid M] (p : M → Prop) (s : Multiset M),
  (∀ (a b : M), p a → p b → p (a + b)) → p 0 → (∀ a ∈ s, p a) → p s.sum
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.comp₀.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
  (z₃ : W.LeftFraction z₁.Y' z₂.Y'),
  z₁.comp₀ z₂ z₃ =
    { Y' := z₃.Y', f := CategoryTheory.CategoryStruct.comp z₁.f z₃.f, s := CategoryTheory.CategoryStruct.comp z₂.s z₃.s,
      hs := ⋯ }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertManyIfNewUnit_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp],
  t.insertManyIfNewUnit [] = t
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.mono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X)
  [CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f)], CategoryTheory.Mono g
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (H : CategoryTheory.Functor C V)
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)],
  (CategoryTheory.MonoidalCategory.externalProduct (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
        H).IsLeftKanExtension
    (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
      (CategoryTheory.MonoidalCategory.DayConvolution.unit F G) H)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval_comp : ∀ {S : Type u} [inst : Semiring S] {R : Type u_1} [inst_1 : CommSemiring R] (n : ℕ) (p : Polynomial R)
  [inst_2 : Algebra R S] (x : S),
  Polynomial.eval x ((ascPochhammer S n).comp (Polynomial.map (algebraMap R S) p)) =
    Polynomial.eval (Polynomial.eval₂ (algebraMap R S) x p) (ascPochhammer S n)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {i : ℕ}
  {f : E → F}, iteratedFDeriv 𝕜 i (-f) = -iteratedFDeriv 𝕜 i f
-- Mathlib.Order.Category.PartOrd
/-- The underlying partially ordered type.  -/
PartOrd.carrier : PartOrd → Type u_1
-- Mathlib.Algebra.FiveLemma
/-- The five lemma in terms of modules. For a diagram explaining the variables,
see the module docstring.  -/
LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} {M₅ : Type u_6}
  {N₁ : Type u_7} {N₂ : Type u_8} {N₃ : Type u_9} {N₄ : Type u_10} {N₅ : Type u_11} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄] [inst_5 : AddCommGroup M₅]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R M₃] [inst_9 : Module R M₄] [inst_10 : Module R M₅]
  [inst_11 : AddCommGroup N₁] [inst_12 : AddCommGroup N₂] [inst_13 : AddCommGroup N₃] [inst_14 : AddCommGroup N₄]
  [inst_15 : AddCommGroup N₅] [inst_16 : Module R N₁] [inst_17 : Module R N₂] [inst_18 : Module R N₃]
  [inst_19 : Module R N₄] [inst_20 : Module R N₅] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (f₃ : M₃ →ₗ[R] M₄)
  (f₄ : M₄ →ₗ[R] M₅) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (g₃ : N₃ →ₗ[R] N₄) (g₄ : N₄ →ₗ[R] N₅) (i₁ : M₁ →ₗ[R] N₁)
  (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (i₄ : M₄ →ₗ[R] N₄) (i₅ : M₅ →ₗ[R] N₅),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ → g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ → g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃ → g₄ ∘ₗ i₄ = i₅ ∘ₗ f₄ → Function.Exact ⋯ ⋯ → ⋯ → ⋯
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mem_nonzeroDivisors_of_coeff_mem : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R} (n : ℕ),
  p.coeff n ∈ nonZeroDivisors R → p ∈ nonZeroDivisors (Polynomial R)
-- Std.Http.Data.Body.Basic
/-- Attempts to decode a `ByteArray` into the target type, returning an error message on failure.
 -/
Std.Http.Body.FromByteArray.fromByteArray : {α : Type} → [self : Std.Http.Body.FromByteArray α] → ByteArray → Except String α
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.mk.injEq : ∀ {M : Type u_10} {N : Type u_11} [inst : One M] [inst_1 : One N] (toFun : M → N) (map_one' : toFun 1 = 1)
  (toFun_1 : M → N) (map_one'_1 : toFun_1 1 = 1),
  ({ toFun := toFun, map_one' := map_one' } = { toFun := toFun_1, map_one' := map_one'_1 }) = (toFun = toFun_1)
-- Lean.DocString.Types
Lean.Doc.Inline.brecOn_1.eq : ∀ {i : Type u} {motive_1 : Lean.Doc.Inline i → Sort u_1} {motive_2 : Array (Lean.Doc.Inline i) → Sort u_1}
  {motive_3 : List (Lean.Doc.Inline i) → Sort u_1} (t : Array (Lean.Doc.Inline i))
  (F_1 : (t : Lean.Doc.Inline i) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_2 t → motive_3 t),
  Lean.Doc.Inline.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Doc.Inline.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality : ∀ {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) [self : F.OplaxMonoidal] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X)))
-- Init.Data.List.Find
List.IsSuffix.find?_eq_none : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <:+ l₂ → List.find? p l₂ = none → List.find? p l₁ = none
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- There exist two lists of `TransvectionStruct` such that multiplying by them on the left and
on the right makes a matrix block-diagonal.  -/
Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  ∃ L L',
    ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
        (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
-- Mathlib.Order.SuccPred.Basic
Order.Ico_succ_right_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  ¬IsMax b → Set.Ico a (Order.succ b) = Set.Icc a b
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.ofIso_compatibility : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (A : Type u_4)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F.CommShift A], CategoryTheory.NatTrans.CommShift e.hom A
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The discriminant of the power basis given by `ζ - 1`.  -/
IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  p ^ (k + 1) ≠ 2 →
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
      (-1) ^ ((p ^ (k + 1)).totient / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
-- Init.Data.Rat.Basic
/-- Auxiliary definition for `Rat.normalize`. Constructs `num / den` as a rational number,
dividing both `num` and `den` by `g` (which is the gcd of the two) if it is not 1.
 -/
Rat.maybeNormalize : (num : ℤ) → (den g : ℕ) → ↑g ∣ num → g ∣ den → den / g ≠ 0 → (num / ↑g).natAbs.Coprime (den / g) → ℚ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → (m.alter k f).contains k = (f (m.get? k)).isSome
-- Mathlib.Data.Tree.Basic
BinaryTree.traverse_pure : ∀ {α : Type u} (t : BinaryTree α) {m : Type u → Type u_1} [inst : Applicative m] [LawfulApplicative m],
  BinaryTree.traverse pure t = pure t
-- Init.Data.BitVec.Basic
/-- Fills a bitvector with `w` copies of the bit `b`.  -/
BitVec.fill : (w : ℕ) → Bool → BitVec w
-- Batteries.Data.Fin.Lemmas
Fin.isSome_findSome?_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSome? f).isSome = true ↔ ∃ i, (f i).isSome = true
-- Init.Data.Random
StdGen.mk : ℕ → ℕ → StdGen
-- Init.Data.SInt.Lemmas
instLawfulIdentityInt64HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearEquiv.congrRight₂_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N₁ : Type u_9}
  {N₂ : Type u_10} [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂] [inst_5 : Module R N₁] [inst_6 : Module R N₂]
  (e : N₁ ≃ₗ[R] N₂) (B : LinearMap.BilinMap R M N₁), e.congrRight₂ B = LinearMap.compr₂ B ↑e
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_lt_ofSubmodule : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {S T : Submodule R E}, ↑S < ↑T ↔ S < T
-- Std.Data.HashSet.RawLemmas
/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
in the statement of `get_insert`.  -/
Std.HashSet.Raw.mem_of_mem_insert' : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, a ∈ m.insert k → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_one_toType : ∀ (x : Ordinal.ToType 1), (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding x = 0
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instAlgebra : {α : Type u} →
  {γ : Type w} →
    {𝕜 : Type u_1} →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : NormedRing γ] → [NormedAlgebra 𝕜 γ] → Algebra 𝕜 (BoundedContinuousFunction α γ)
-- Mathlib.Topology.Piecewise
IsOpen.ite : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s s' t : Set α},
  IsOpen s → IsOpen s' → s ∩ frontier t = s' ∩ frontier t → IsOpen (t.ite s s')