mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Concrete
/-- If `N` is a normal subgroup of `G`, then this is the group homomorphism
sending an element `g` of `G` to the `G`-endomorphism of `G ⧸ₐ N` given by
multiplication with `g⁻¹` on the right.  -/
Action.FintypeCat.toEndHom : {G : Type u_1} →
  [inst : Group G] →
    (N : Subgroup G) →
      [inst_1 : Fintype (G ⧸ N)] →
        [N.Normal] → G →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ == m₂) = true
-- Aesop.Search.Expansion.Norm
Aesop.NormM : Type → Type
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instFaithfulOverForget : ∀ (S : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.ProEt.forget S).Faithful
-- Mathlib.Algebra.Notation.Defs
instHSMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β], instHSMul = { hSMul := SMul.smul }
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.re_nnratCast : ∀ {K : Type u_1} [inst : Field K] {a b : K} (q : ℚ≥0), (NNRatCast.nnratCast q).re = ↑q
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instInv.eq_1 : ∀ {α : Type u_1} [inst : Inv α], OrderDual.instInv = inst
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_preOmega : ∀ {o : Ordinal.{u_1}}, Order.IsSuccPrelimit o → (Ordinal.preOmega o).cof = o.cof
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.instEffectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B X : C} (f : X ⟶ B) [CategoryTheory.EffectiveEpi f],
  CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => f
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.dep_of_insert : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e : α},
  M.IsBase B → e ∉ B → autoParam (e ∈ M.E) Matroid.IsBase.dep_of_insert._auto_1 → M.Dep (insert e B)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf_obj : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X : Cᵒᵖ),
  (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀).obj X =
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ (Opposite.unop X)
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- A point lying on angle bisectors from two vertices is an excenter.  -/
Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {p : P},
          2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p =
              2 • EuclideanGeometry.oangle p (t.points i₁) (t.points i₃) →
            2 • EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p =
                2 • EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) →
              ∃ signs, p = Affine.Simplex.excenter t signs
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_arrowCongr : ∀ {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  {V₄ : Type u_9} [inst : AddCommGroup V₁] [inst_1 : AddCommGroup V₂] [inst_2 : AddCommGroup V₃]
  [inst_3 : AddCommGroup V₄] [inst_4 : AddTorsor V₁ P₁] [inst_5 : AddTorsor V₂ P₂] [inst_6 : AddTorsor V₃ P₃]
  [inst_7 : AddTorsor V₄ P₄] {R : Type u_10} [inst_8 : CommRing R] [inst_9 : Module R V₁] [inst_10 : Module R V₂]
  [inst_11 : Module R V₃] [inst_12 : Module R V₄] (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : P₃ ≃ᵃ[R] P₄),
  (e₁.arrowCongr e₂).linear = e₁.arrowCongrₗ e₂.linear
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunLinear_tmul_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R), (PolyEquivTensor.toFunLinear R A) (a ⊗ₜ[R] p) = ((PolyEquivTensor.toFunBilinear R A) a) p
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mclosure_range : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), Submonoid.closure (Set.range ⇑f) = MonoidHom.mrange f
-- Init.Data.List.Monadic
List.forIn'_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {a : α} {as : List α}
  (f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)) (b : β),
  forIn' (a :: as) b f = do
    let x ← f a ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b
-- Mathlib.Topology.VectorBundle.Basic
/-- A fiberwise linear map equal to `e` on `e.baseSet`.  -/
Bundle.Pretrivialization.linearMapAt : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : AddCommMonoid F] →
                [inst_4 : Module R F] →
                  [inst_5 : (x : B) → AddCommMonoid (E x)] →
                    [inst_6 : (x : B) → Module R (E x)] →
                      (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) →
                        [Bundle.Pretrivialization.IsLinear R e] → (b : B) → E b →ₗ[R] F
-- Init.Data.List.Lemmas
List.replicate_eq_nil_iff : ∀ {α : Type u_1} {n : ℕ} (a : α), List.replicate n a = [] ↔ n = 0
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rco_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m...n).toArray[i]! = 0
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The boundary of any C¹ manifold is closed.

This is currently only proven for C¹ manifolds, but holds at least for finite-dimensional
topological manifolds too; see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`.  -/
ModelWithCorners.isClosed_boundary : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M],
  n ≠ 0 → IsClosed (ModelWithCorners.boundary M)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The function on the quotient by a congruence relation `c`
induced by a function that is constant on `c`'s equivalence classes.  -/
AddCon.liftOn : {M : Type u_1} →
  [inst : Add M] → {β : Sort u_4} → {c : AddCon M} → c.Quotient → (f : M → β) → (∀ (a b : M), c a b → f a = f b) → β
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] {α : Type}
  [inst_2 : Finite α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X)
  (hπ : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)),
  CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.Limits.pullback.fst f (π x))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_union!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.union! m₂) k fallback =
            Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.X_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.X.comp p = p
-- Std.Internal.Do.PredTrans
/-- `MonadExceptOf` instance lifted through an unrelated exception layer:
delegates to the inner instance, threading the extra exception postcondition.  -/
Std.Internal.Do.instMonadExceptOfPredTransConsForall_1 : {ε : Type u} →
  {Pred : Type v} →
    {EPred : Type w} →
      {ε' : Type u} →
        [MonadExceptOf ε (Std.Internal.Do.PredTrans Pred EPred)] →
          MonadExceptOf ε (Std.Internal.Do.PredTrans Pred (EPost.Cons✝ (ε' → Pred) EPred))
-- Lean.Language.Basic
/-- Constructs a reporting range by replacing a missing range with `inherit`, which is a reasonable
default to ensure that a range is shown in all cases.
 -/
Lean.Language.SnapshotTask.ReportingRange.ofOptionInheriting : Option Lean.Syntax.Range → Lean.Language.SnapshotTask.ReportingRange
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The first of two points lies in their affine span.  -/
left_mem_affineSpan_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), p₁ ∈ line[k, p₁, p₂]
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piUnique_apply : ∀ {ι : Type u_16} (M : ι → Type u_17) [inst : (j : ι) → Mul (M j)] [inst_1 : Unique ι] (f : (i : ι) → M i),
  (MulEquiv.piUnique M) f = f default
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_left`. -/
Set.union_diff_left : ∀ {α : Type u_1} {s t : Set α}, (s ∪ t) \ s = t \ s
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Agree.below : {F : PFunctor.{uA, uB}} →
  {motive :
      {n : ℕ} →
        (a : PFunctor.Approx.CofixA F n) →
          (a_1 : PFunctor.Approx.CofixA F (n + 1)) → PFunctor.Approx.Agree a a_1 → Prop} →
    {n : ℕ} →
      {a : PFunctor.Approx.CofixA F n} → {a_1 : PFunctor.Approx.CofixA F (n + 1)} → PFunctor.Approx.Agree a a_1 → Prop
-- Init.Data.Nat.Basic
Nat.zero_ne_add_one : ∀ (n : ℕ), 0 ≠ n + 1
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.symm_monoidHomCongrLeftEquiv : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂] [inst_2 : Monoid N]
  (e : M₁ ≃* M₂), e.monoidHomCongrLeftEquiv.symm = e.symm.monoidHomCongrLeftEquiv
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- `WeakDual.CharacterSpace.compContinuousMap` sends the identity to the identity.  -/
WeakDual.CharacterSpace.compContinuousMap_id : ∀ (A : Type u_1) {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [inst_3 : CompleteSpace A] [inst_4 : StarRing A],
  WeakDual.CharacterSpace.compContinuousMap (StarAlgHom.id 𝕜 A) = ContinuousMap.id ↑(WeakDual.characterSpace 𝕜 A)
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- The pullback of a cover of `S`-schemes with `Q` along a morphism of `S`-schemes. This is not
definitionally equal to `AlgebraicGeometry.Scheme.Cover.pullbackCover`, as here we take
the pullback in `Q.Over ⊤ S`, whose underlying scheme is only isomorphic but not equal to the
pullback in `Scheme`.  -/
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [Q.HasOfPostcompProperty Q] →
                          [Q.IsStableUnderBaseChange] →
                            [Q.IsStableUnderComposition] →
                              Q (X ↘ S) →
                                Q (W ↘ S) →
                                  (∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) W
-- Mathlib.Order.ScottContinuity.Complete
/-- **Alias** of the forward direction of `scottContinuous_iff_map_sSup`.

---

`f` is Scott continuous if and only if it commutes with `sSup` on directed sets  -/
ScottContinuous.map_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  ScottContinuous f → ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
-- Std.Do.PostCond
Std.Do.ExceptConds.false_and : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, (Std.Do.ExceptConds.false ∧ₑ x).entails Std.Do.ExceptConds.false
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst.eq_def : ∀ (x x_1 : ℕ),
  x.stirlingFirst x_1 =
    match x, x_1 with
    | 0, 0 => 1
    | 0, n.succ => 0
    | n.succ, 0 => 0
    | n.succ, k.succ => n * n.stirlingFirst (k + 1) + n.stirlingFirst k
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.foldlM_array : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  {xs : Array α} {init : β} {f : β → α → m β} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f b cur ⦃(fun b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      Array.foldlM f init xs ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, List.find? (fun x => x.1 == k) m.toList = none ↔ m.contains k = false
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opFunctorCompOpFunctorIso_inv_app_app_hom_apply : ∀ (X : SSet) (X_1 : SimplexCategoryᵒᵖ) (x : X.obj X_1),
  (CategoryTheory.ConcreteCategory.hom ((SSet.opFunctorCompOpFunctorIso.inv.app X).app X_1)) x =
    SSet.opObjEquiv.symm (SSet.opObjEquiv.symm x)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The sphere `s₁` is internally tangent to the sphere `s₂` at some point.  -/
EuclideanGeometry.Sphere.IsIntTangent : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [NormedAddTorsor V P] → EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → Prop
-- Mathlib.Data.Erased
/-- Erase a value.  -/
Erased.mk : {α : Sort u_1} → α → Erased α
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- Multiplying with `swap R i j` on the left swaps the `i`-th row with the `j`-th row.  -/
Matrix.swap_mul_apply_left : ∀ {R : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (i j : n) (a : m) (g : Matrix n m R), (Matrix.swap R i j * g) i a = g j a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_filter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.ExtTreeSet.filter f t).size ≤ t.size
-- Mathlib.Analysis.Normed.Module.Bases
/-- Composition of projections: `proj A (proj B x) = proj (A ∩ B) x`.  -/
GeneralSchauderBasis.proj_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A B : Finset β)
  (x : X), (b.proj A) ((b.proj B) x) = (b.proj (A ∩ B)) x
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instModule : (p : ENNReal) →
  (K : Type u_1) →
    (V : Type u_4) → [inst : Semiring K] → [inst_1 : AddCommGroup V] → [Module K V] → Module K (WithLp p V)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.C_minpolyX : ∀ {K : Type u_1} [inst : Field K] (x : K), (RatFunc.C x).minpolyX ↥K⟮RatFunc.C x⟯ = 0
-- Mathlib.Data.Num.Lemmas
Num.of_natCast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : ℕ), ↑↑n = ↑n
-- Batteries.Tactic.Lint.Simp
/-- Is this hypothesis a condition that might turn into a `simp` side-goal?
i.e. is it a proposition that isn't marked as instance implicit?  -/
Batteries.Tactic.Lint.isCondition : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p]
  [ContinuousMap.UniqueHom R A] (g f : R → R) (a : A),
  autoParam (p a) cfc_comp._auto_1 →
    autoParam (ContinuousOn g (f '' spectrum R a)) cfc_comp._auto_3 →
      autoParam (ContinuousOn f (spectrum R a)) cfc_comp._auto_5 → cfc (g ∘ f) a = cfc g (cfc f a)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.compare_getKey?_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.get? k) = true
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousAt_toReal : ∀ {x : ENNReal}, x ≠ ⊤ → ContinuousAt ENNReal.toReal x
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.matched.sizeOf_spec : sizeOf Mathlib.Tactic.GRewrite.Progress.matched✝ = 1
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.instInhabitedEndMonoidal : {C : Type u} → [inst : CategoryTheory.Bicategory C] → (X : C) → Inhabited (CategoryTheory.EndMonoidal X)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.op.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β],
  MulEquiv.op =
    {
      toFun := fun f =>
        { toFun := MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop, invFun := MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop,
          left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ },
      invFun := fun f =>
        { toFun := MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op, invFun := MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op,
          left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under the modulo operation.  -/
Dioph.mod_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v % g v
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_mks : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra 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₄ : { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1)
  (h₅ :
    ∀ (x y : A),
      { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) =
        { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x *
          { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y),
  ⇑{ toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄,
        map_mul' := h₅ } =
    f
-- Mathlib.Analysis.Calculus.Deriv.Mul
Differentiable.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, Differentiable 𝕜 (f i)) → Differentiable 𝕜 fun x => ∏ i ∈ u, f i x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)],
  CategoryTheory.Limits.colimit.pre F E =
    CategoryTheory.Limits.colimit.desc (E.comp F)
      (CategoryTheory.Limits.Cocone.whisker E (CategoryTheory.Limits.colimit.cocone F))
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash : Mathlib.Meta.FunProp.LambdaTheoremType → UInt64
-- Mathlib.Topology.Algebra.Affine
AffineMap.homothety_isOpenMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Field R]
  [inst_6 : Module R V] [ContinuousConstSMul R V] (x : P) (t : R), t ≠ 0 → IsOpenMap ⇑(AffineMap.homothety x t)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.mk.sizeOf_spec : ∀ (declName : Lean.Name) (keys : Array Lean.Meta.SimpTheoremKey),
  sizeOf { declName := declName, keys := keys } = 1 + sizeOf declName + sizeOf keys
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.left_unitality_assoc : ∀ {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) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (F.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv h =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X)) h))
-- Mathlib.Algebra.Homology.Homotopy
dNext_comp_left : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (g : (i j : ι) → D.X i ⟶ E.X j) (i : ι),
  ((dNext i) fun i j => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) =
    CategoryTheory.CategoryStruct.comp (f.f i) ((dNext i) g)