mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Basic
Std.Iterators.Productive.mk : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β],
  WellFounded Std.IterM.IsPlausibleSkipSuccessorOf → Std.Iterators.Productive α m
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- **Alias** of `Fintype.sum_bijective`.

---

`Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.sum_comp` for a version without `h`.  -/
Function.Bijective.finsetSum : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  (e : ι → κ), Function.Bijective e → ∀ (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∑ x, f x = ∑ x, g x
-- Mathlib.Dynamics.Newton
/-- Given a single-variable polynomial `P` with derivative `P'`, this is the map:
`x ↦ x - P(x) / P'(x)`. When `P'(x)` is not a unit we use a junk-value pattern and send `x ↦ x`.  -/
Polynomial.newtonMap : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Polynomial R → S → S
-- Mathlib.CategoryTheory.Quotient
/-- Composition in the quotient category.  -/
CategoryTheory.Quotient.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) →
      ⦃a b c : CategoryTheory.Quotient r⦄ →
        CategoryTheory.Quotient.Hom r a b → CategoryTheory.Quotient.Hom r b c → CategoryTheory.Quotient.Hom r a c
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.find?_eq_findSome? : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Finite α m] {it : Std.IterM m β} {f : β → Bool},
  it.find? f = it.findSome? fun x => if f x = true then some x else none
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.mul : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s t : Set E},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.pi_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] {γ : Type w} [Nonempty I] [inst_2 : MulOneClass γ]
  (g : (i : I) → γ →* f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(MonoidHom.pi g)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_sup_iff : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α} {a : α}, a ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `F` and `H` are finite such that `ker(G →* H) = im(F →* G)`, then `G` is finite.  -/
Group.fintypeOfKerEqRange : {F : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Group F] →
        [inst_1 : Group G] →
          [inst_2 : Group H] → [Fintype F] → [Fintype H] → (f : F →* G) → (g : G →* H) → g.ker = f.range → Fintype G
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts_of_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  {J : Type w'},
  W.colimitsOfShape (CategoryTheory.Discrete J) f →
    ∀ [Small.{w, w'} J], CategoryTheory.MorphismProperty.coproducts.{w, v, u} W f
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.appAt.inj : ∀ {arr arr_1 : Array Mathlib.Tactic.ClickSuggestions.ApplyAtLemma},
  Mathlib.Tactic.ClickSuggestions.Candidates.appAt✝ arr = Mathlib.Tactic.ClickSuggestions.Candidates.appAt✝ arr_1 →
    arr = arr_1
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.symmetry₂_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier R),
  (CategoryTheory.ConcreteCategory.hom p₂) ((CategoryTheory.ConcreteCategory.hom self.s) x) =
    (CategoryTheory.ConcreteCategory.hom p₁) x
-- Init.System.IO
/-- Write contents of a string to a file at the specified path using UTF-8 encoding.
 -/
IO.FS.writeFile : System.FilePath → String → IO Unit
-- Mathlib.MeasureTheory.Group.Defs
/-- A measure `μ` on a measurable additive group is right invariant
if the measure of right translations of a set are equal to the measure of the set itself.  -/
MeasureTheory.Measure.IsAddRightInvariant : {G : Type u_1} → [inst : MeasurableSpace G] → [Add G] → MeasureTheory.Measure G → Prop
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.add_right_inj : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a b c : M), a + b = a + c ↔ b = c
-- Mathlib.RingTheory.PicardGroup
/-- The relative Picard group of an `R`-algebra `A`, denoted `Pic(A/R)`,
defined to be the kernel of `Pic.mapAlgebra R A`.  -/
CommRing.relPic : (R : Type u) →
  [inst : CommSemiring R] → (A : Type u_5) → [inst_1 : CommSemiring A] → [Algebra R A] → Subgroup (CommRing.Pic R)
-- Init.Data.Array.Erase
Array.eraseP_comm : ∀ {α : Type u_1} {p q : α → Bool} {xs : Array α},
  (∀ a ∈ xs, ¬p a = true ∨ ¬q a = true) → (xs.eraseP p).eraseP q = (xs.eraseP q).eraseP p
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The object `succ W Z` is the multicoequalizer of all pairs of morphisms
`g₁ g₂ : Y ⟶ step W Z` with a `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.  -/
CategoryTheory.OrthogonalReflection.succ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [inst_3 : CategoryTheory.Limits.HasPushouts C] →
              [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                C
-- Init.MetaTypes
Lean.Meta.Simp.NormCastConfig.mk.injEq : ∀ (toConfig toConfig_1 : Lean.Meta.Simp.Config),
  ({ toConfig := toConfig } = { toConfig := toConfig_1 }) = (toConfig = toConfig_1)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) {X_2 Y : C₂}
  (f : X_2 ⟶ Y) (X_3 : C₃),
  ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X_1).map f).app X_3 =
    ((X.obj (F₁.obj X_1)).map (F₂.map f)).app (F₃.obj X_3)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFreeOn_singleton : ∀ {α : Type u_1} (G : SimpleGraph α) {a : α} {n : ℕ}, G.CliqueFreeOn {a} n ↔ 1 < n
-- Mathlib.Topology.Algebra.UniformConvergence
instNSMulUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [inst : SMul M β],
  instNSMulUniformOnFun = { smul := fun a a_1 => instNSMulUniformOnFun._aux_1 a_1 a }
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- The homeomorphism between `AddCircle` and `Circle`.  -/
AddCircle.homeomorphCircle : {T : ℝ} → T ≠ 0 → AddCircle T ≃ₜ Circle
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_sup : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G) (f : G →+ N),
  AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K
-- Mathlib.Data.Int.Init
Int.leInduction_add_one : ∀ {m : ℤ} {motive : (n : ℤ) → m ≤ n → Sort u_1} (base : motive m ⋯)
  (succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯) (n : ℤ) (hmn : m ≤ n),
  Int.leInduction base succ (n + 1) ⋯ = succ n hmn (Int.leInduction base succ n hmn)
-- Lean.Level
Lean.mkLevelMax : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_J : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).J = ι
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Table : Type → Type
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- If a `G`-representation on `A` is trivial, this is the natural map `H₁(G, A) → Gᵃᵇ ⊗[ℤ] A`
sending `⟦single g a⟧` to `⟦g⟧ ⊗ₜ a`.  -/
groupHomology.H1ToTensorOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        [A.IsTrivial] → ↑(groupHomology.H1 A) →ₗ[ℤ] TensorProduct ℤ (Additive (Abelianization G)) ↑A
-- Mathlib.RingTheory.Invariant.Basic
/-- This theorem will be made redundant by `IsFractionRing.stabilizerHom_surjective`.  -/
_private.Mathlib.RingTheory.Invariant.Basic.0.fixed_of_fixed2 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : SMulCommClass G A B] (P : Ideal A)
  (Q : Ideal B) [Q.IsPrime] [inst_8 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_9 : Field K] [inst_10 : Field L]
  [inst_11 : Algebra (A ⧸ P) K] [inst_12 : Algebra (B ⧸ Q) L] [inst_13 : Algebra (A ⧸ P) L]
  [inst_14 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_15 : Algebra K L] [inst_16 : IsScalarTower (A ⧸ P) K L]
  [Algebra.IsInvariant A B G] [inst_18 : IsFractionRing (A ⧸ P) K] [inst_19 : IsFractionRing (B ⧸ Q) L] (f : Gal(L/K))
  (x : L), (∀ (g : ↥(MulAction.stabilizer G Q)), ((IsFractionRing.stabilizerHom G P Q K L) g) x = x) → f x = x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).isEmpty = false
-- Mathlib.Data.Finset.Sum
/-- Given a finset of elements `α ⊕ β`, extract all the elements of the form `α`. This
forms a quasi-inverse to `disjSum`, in that it recovers its left input.

See also `List.partitionMap`.
 -/
Finset.toLeft : {α : Type u_1} → {β : Type u_2} → Finset (α ⊕ β) → Finset α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α},
  (Std.ExtTreeMap.filter f t)[k]! = (t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Data.Set.Lattice
Set.sUnion_subset_iff : ∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, ⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Inherit `R`-module structure from `C(X, R) →L[R] E`.  -/
AbstractMeasure.instModule : {X : Type u_1} →
  {R : Type u_3} →
    {E : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : TopologicalSpace E] →
            [inst_3 : IsTopologicalAddGroup E] →
              [inst_4 : CommRing R] →
                [inst_5 : TopologicalSpace R] →
                  [inst_6 : IsTopologicalRing R] →
                    [inst_7 : Module R E] → [ContinuousSMul R E] → Module R (AbstractMeasure X R E)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.coe_iInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
  (p : ι → Submodule R M), ↑(⨅ i, p i) = ⋂ i, ↑(p i)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.eq_normS_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr), Lean.Grind.CommRing.eq_normS_cert lhs rhs = (lhs.toPolyS == rhs.toPolyS)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.ins.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Lean.Language.Lean.Types
/-- State after all elaborator tasks are finished. In particular, contains the complete info tree.
 -/
Lean.Language.Lean.CommandElaboratingSnapshot.infoTreeSnap : Lean.Language.Lean.CommandElaboratingSnapshot → Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.map.congr_simp : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] {n : ℕ} (s s_1 : Affine.Simplex k P n),
  s = s_1 → ∀ (f f_1 : P →ᵃ[k] P₂) (e_f : f = f_1) (hf : Function.Injective ⇑f), s.map f hf = s_1.map f_1 ⋯
-- Mathlib.Data.Real.Basic
Real.instRing : Ring ℝ
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.

WARNING: This has the potential to send `ext` into a loop if someone locally adds the inverse ext
lemma proving equality in `α →+ Additive β` from equality in `Multiplicative α →* β`.  -/
Multiplicative.monoidHom_ext : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (f g : Multiplicative α →* β),
  MonoidHom.toAdditiveRight f = MonoidHom.toAdditiveRight g → f = g
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.buildAdditionalGlobalRules : Option Lean.Name →
  Aesop.Frontend.RuleExpr → Lean.Elab.TermElabM (Array (Aesop.GlobalRuleSetMember × Array Aesop.RuleSetName))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} {fallback : β a}, m.getD a fallback = (m.get? a).getD fallback
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.toRingHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), f.toRingHom = ↑f
-- Std.Do.WP.SimpLemmas
Std.Do.WP.liftWith_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps] [inst_1 : MonadControl n o] [inst_2 : MonadControlT m n]
  (f : ({β : Type u} → o β → m (stM m o β)) → m α),
  (Std.Do.wp (liftWith f)).apply Q =
    (Std.Do.wp (MonadControl.liftWith fun x₂ => liftWith fun x₁ => f fun {β} => x₁ ∘ x₂)).apply Q
-- Mathlib.RingTheory.Ideal.Quotient.Operations
AlgEquiv.quotientBot_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : S),
  (AlgEquiv.quotientBot R S) ((Ideal.Quotient.mk ⊥) s) = s
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E), (M.map f hf).eRank = M.eRank
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousLinearMap.toContinuousAffineMap_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] [inst_6 : TopologicalSpace W]
  [inst_7 : IsTopologicalAddGroup V] [inst_8 : IsTopologicalAddGroup W] (f : V →L[R] W),
  f.toContinuousAffineMap.contLinear = f
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.cell_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.CWComplex C] (n : ℕ),
  Topology.RelCWComplex.cell C n = Topology.CWComplex.cell C n
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X_1 : Cᵒᵖ),
  (hF.homNatIso X).hom.app X_1 = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom
-- Mathlib.Analysis.Asymptotics.TVS
ContinuousLinearMap.isBigOTVS_comp : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} (g : E →L[𝕜] F), (⇑g ∘ f) =O[𝕜; l] f
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The pullback of an equalizer is an equalizer.  -/
CategoryTheory.Limits.isLimitPrecompFork : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {Z : C} →
          (h : Z ⟶ X) →
            {s : CategoryTheory.Limits.Fork f g} →
              CategoryTheory.Limits.IsLimit s →
                {c : CategoryTheory.Limits.PullbackCone s.ι h} →
                  CategoryTheory.Limits.IsLimit c →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.precompFork h s c)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instSubsingleton : ∀ {M : Type u_1} [Subsingleton M], Subsingleton (MulArchimedeanOrder M)
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedHost : Inhabited Std.Http.URI.Host
-- Mathlib.Topology.Closure
compl_frontier_eq_union_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, (frontier s)ᶜ = interior s ∪ interior sᶜ
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instHasQuotientAddSubgroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α],
  QuotientAddGroup.instHasQuotientAddSubgroup = { Quotient := fun s => Quotient (QuotientAddGroup.leftRel s) }
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.restrictScalars_toSubmodule : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  {U : Subalgebra S A},
  Subalgebra.toSubmodule (Subalgebra.restrictScalars R U) = Submodule.restrictScalars R (Subalgebra.toSubmodule U)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.inst : ∀ {R : Type u} [inst : CommSemiring R], Module.Invertible R R
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
isPrimitiveRoot_of_mem_rootsOfUnity : ∀ {M : Type u_1} [inst : CommMonoid M] {u : Mˣ} {n : ℕ} [NeZero n],
  u ∈ rootsOfUnity n M → ∃ d, d ≠ 0 ∧ d ∣ n ∧ IsPrimitiveRoot u d
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).ι =
    CategoryTheory.Limits.kernel.ι
      (CategoryTheory.Limits.cokernel.π
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g)
          (CategoryTheory.Limits.cokernel.π S.f)))
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isSemisimpleRing_of_isReduced : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] [IsReduced R], IsSemisimpleRing R
-- Init.Data.UInt.Bitwise
UInt8.toUSize_not : ∀ (a : UInt8), (~~~a).toUSize = ~~~a.toUSize % 256
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.mk.injEq : ∀ {ι : Type u_1} (faces : Set (Finset ι)) (isRelLowerSet_faces : IsRelLowerSet faces Finset.Nonempty)
  (faces_1 : Set (Finset ι)) (isRelLowerSet_faces_1 : IsRelLowerSet faces_1 Finset.Nonempty),
  ({ faces := faces, isRelLowerSet_faces := isRelLowerSet_faces } =
      { faces := faces_1, isRelLowerSet_faces := isRelLowerSet_faces_1 }) =
    (faces = faces_1)
-- Mathlib.Data.Finset.NAry
Finset.sup'_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeSup δ] (g : γ → δ) (h : (Finset.image₂ f s t).Nonempty),
  (Finset.image₂ f s t).sup' h g = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.natDegree = 1 ↔ ∃ a, a ≠ 0 ∧ ∃ b, Polynomial.C a * Polynomial.X + Polynomial.C b = p
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.proof? : Lean.Meta.Grind.ENode → Option Lean.Expr
-- Std.Data.DHashMap.Basic
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.DHashMap.Equiv : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → Std.DHashMap α β → Prop
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.Ioo a b)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGT?ₘ k t =
    Std.DTreeMap.Internal.Impl.applyPartition (fun k' => (compare k k').then Ordering.gt) t fun x x_1 x_2 r => r.head?
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅} {hc : t.maxKey he ∈ t}, t.getKey (t.maxKey he) hc = t.maxKey he
-- Mathlib.RingTheory.Unramified.LocalStructure
Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
  [inst_3 : Q.IsPrime] [Module.Finite R S] [Algebra.IsUnramifiedAt R Q]
  [inst_6 : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q],
  ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk_of_isEmpty : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [IsEmpty 𝓧], ProbabilityTheory.avgRisk ℓ P κ π = 0
-- Mathlib.Computability.Primrec.Basic
Primrec₂.of_eq : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f g : α → β → σ}, Primrec₂ f → (∀ (a : α) (b : β), f a b = g a b) → Primrec₂ g
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.monadToFunctor_mapIso_monad_iso_mk : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Monad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X)
  (f_μ :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X)),
  (CategoryTheory.monadToFunctor C).mapIso (CategoryTheory.MonadIso.mk f f_η f_μ) = f