mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Monotone.MonovaryOrder
monovaryOn_iff_exists_monotoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ MonotoneOn g s
-- Mathlib.LinearAlgebra.Span.Basic
/-- **Alias** of `Submodule.mapsTo_span`. -/
Set.MapsTo.submoduleSpan : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {f : M →ₛₗ[σ₁₂] M₂} {s : Set M} {t : Set M₂},
  Set.MapsTo (⇑f) s t → Set.MapsTo ⇑f ↑(Submodule.span R s) ↑(Submodule.span R₂ t)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_iter_const_smul : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {R : Type u_3}
  [inst_2 : Monoid R] [inst_3 : DistribMulAction R G] (r : R) (f : M → G) (n : ℕ),
  (fwdDiff h)^[n] (r • f) = r • (fwdDiff h)^[n] f
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x : E},
  HasLineDerivAt 𝕜 f 0 x 0
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.isClosedMap_isStableUnderComposition : (AlgebraicGeometry.topologically @IsClosedMap).IsStableUnderComposition
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.ballSubgroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (c : FiniteMulArchimedeanClass M), c.ballSubgroup = FiniteMulArchimedeanClass.subgroup (UpperSet.Ioi c)
-- Mathlib.RingTheory.Perfection
PerfectionMap.mk : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₂}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R},
  (∀ ⦃x y : P⦄, (∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = π ((⇑(frobeniusEquiv P p).symm)^[n] y)) → x = y) →
    (∀ (f : ℕ → R), (∀ (n : ℕ), f (n + 1) ^ p = f n) → ∃ x, ∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = f n) →
      PerfectionMap p π
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.HasAnchor.mk : {α : Type u} → (α → UInt64) → Lean.Meta.Grind.HasAnchor α
-- Std.Data.HashMap.AdditionalOperations
/-- Updates the values of the hash map by applying the given function to all mappings.  -/
Std.HashMap.map : {α : Type u} →
  {β : Type v} → {γ : Type w} → [inst : BEq α] → [inst_1 : Hashable α] → (α → β → γ) → Std.HashMap α β → Std.HashMap α γ
-- Lean.Elab.Tactic.Omega.Core
/-- Our internal representation of an argument "justifying" that a constraint holds on some coefficients.
We'll use this to construct the proof term once a contradiction is found.
 -/
Lean.Elab.Tactic.Omega.Justification : Lean.Omega.Constraint → Lean.Omega.Coeffs → Type
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.propQCPrecoverage_le_precoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.Scheme.propQCPrecoverage P ≤ AlgebraicGeometry.Scheme.precoverage P
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
/-- If a ball in a proper space includes a closed set `s`, then there exists a ball with the same
center and a strictly smaller radius that includes `s`.  -/
exists_lt_subset_ball : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] {x : α} {r : ℝ} {s : Set α},
  IsClosed s → s ⊆ Metric.ball x r → ∃ r' < r, s ⊆ Metric.ball x r'
-- Aesop.Rule
Aesop.RegularRule.tac : Aesop.RegularRule → Aesop.RuleTacDescr
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.mk.inj : ∀ {footnotes : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline))}
  {urls : Std.HashMap String (Lean.Doc.Ref✝ String)} {deferred : Array Lean.Doc.DeferredCheck}
  {footnotes_1 : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline))}
  {urls_1 : Std.HashMap String (Lean.Doc.Ref✝ String)} {deferred_1 : Array Lean.Doc.DeferredCheck},
  { footnotes := footnotes, urls := urls, deferred := deferred } =
      { footnotes := footnotes_1, urls := urls_1, deferred := deferred_1 } →
    footnotes = footnotes_1 ∧ urls = urls_1 ∧ deferred = deferred_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X')
  {n : ℕ} (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (X.δ i) (f.app { len := n + 1 }) =
    CategoryTheory.CategoryStruct.comp (f.app { len := n }) (X'.δ i)
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurrySum_smul : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] (r : R)
  (g : MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)),
  (r • g).uncurrySum = r • g.uncurrySum
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `modify` which can be used in the absence of balance
information but still assumes the preconditions of `modify`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.Const.alter! : {α : Type u} →
  {β : Type v} →
    [Ord α] →
      α → (Option β → Option β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.subset_right : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {K : ℝ} {A B₁ B₂ : Set X},
  B₁ ⊆ B₂ → CovBySMul M K A B₁ → CovBySMul M K A B₂
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  (x : ExceptT ε m α) (h : ε → ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp x post (EPost.Cons.mk✝ (fun e => Std.Internal.Do.wp (h e) post epost) epost.tail) ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Mathlib.Order.Hom.WithTopBot
WithBot.toDualTopEquiv_symm_coe : ∀ {α : Type u_1} [inst : LE α] (a : α), WithBot.toDualTopEquiv.symm (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)
-- Std.Http.Data.Status
Std.Http.instReprStatus.repr : Std.Http.Status → ℕ → Std.Format
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁'_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.X₃ = S.L₃.X₁
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.comp_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G)
  (i : E.I₀), (f.comp g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link2.eq_1 : ∀ {α : Type u} {β : α → Type v} (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced)
  (hr_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.leaf.link2 r hr_2 hr = { impl := r, balanced_impl := ⋯, size_impl := ⋯ }
-- Init.Data.SInt.Bitwise
Int64.and_not_self : ∀ {a : Int64}, a &&& ~~~a = 0
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {F₁ F₂ : W.FunctorsInverting D} {α β : F₁ ⟶ F₂}, α = β ↔ α.hom.app = β.hom.app
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instForInKeysOfMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (RBTree.RBMap.Keys α β cmp) α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l → k ∈ List.map Prod.fst l → (m.insertMany l).getKey? k' = some k
-- Mathlib.Order.SupClosed
infClosure_min : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s t : Set α}, s ⊆ t → InfClosed t → infClosure s ⊆ t
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)`  -/
MulMemClass : (S : Type u_3) → (M : outParam (Type u_4)) → [Mul M] → [SetLike S M] → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Tactic.ComputeAsymptotics.Majorized.eq_1 : ∀ (f b : ℝ → ℝ) (exp : ℝ), Tactic.ComputeAsymptotics.Majorized f b exp = ∀ exp' > exp, f =o[Filter.atTop] (b ^ exp')
-- Mathlib.Topology.Covering.Quotient
/-- The group action on the domain of a quotient covering map is free.  -/
IsQuotientCoveringMap.isCancelSMul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → IsCancelSMul G E
-- Mathlib.Order.Bounds.Image
mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → a ∈ upperBounds s → b ∈ lowerBounds t → f a b ∈ lowerBounds (Set.image2 f s t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_alter_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k : α} {f : Option (β k) → Option (β k)} {hc : (m.alter k f).contains k = true},
  (m.alter k f).get k hc = (f (m.get? k)).get ⋯
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H))
  (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i))
  {α : ↥LieSubalgebra.root},
  α ∈ (LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q hq).rootSet ↔ (LieAlgebra.IsKilling.rootSystem H).root α ∈ q
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F}, iteratedDerivWithin n f Set.univ = iteratedDeriv n f
-- Mathlib.Tactic.Linter.TextBased
/-- Enables the old Python-based style linters.  -/
Mathlib.Linter.TextBased.linter.pythonStyle : Lean.Option Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β} {h₁ : a ∈ t.insert k v},
  Std.ExtDTreeMap.Const.get (t.insert k v) a h₁ =
    if h₂ : cmp k a = Ordering.eq then v else Std.ExtDTreeMap.Const.get t a ⋯
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equivFunctor_map : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (D : Type u'')
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D]
  {X Y : CategoryTheory.ForgetEnrichment V D} (f : X ⟶ Y),
  (CategoryTheory.ForgetEnrichment.equivFunctor V D).map f =
    (CategoryTheory.eHomEquiv V).symm (CategoryTheory.ForgetEnrichment.homTo V f)
-- Init.Data.Fin.Lemmas
Fin.coe_castLE : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), ↑(Fin.castLE h i) = ↑i
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- A wrapper for promoting any type to a category,
with a unique morphism between any two objects of the category.
 -/
CategoryTheory.Codiscrete : Type u → Type u
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
/-- Given two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` in the category
of cochain complexes, this is the canonical triangle
`mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧`.  -/
CochainComplex.mappingConeCompTriangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ X₃ : CochainComplex C ℤ} →
          (X₁ ⟶ X₂) → (X₂ ⟶ X₃) → CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)
-- Mathlib.Order.Hom.Basic
OrderHom.prodₘ_coe_coe_coe : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (x : α →o β) (a : α →o γ) (x_1 : α), ((OrderHom.prodₘ x) a) x_1 = (x x_1, a x_1)
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms.  -/
monoidHomOfTendsto : {α : Type u_2} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      [inst : TopologicalSpace M₂] →
        [T2Space M₂] →
          [inst_2 : MulOneClass M₁] →
            [inst_3 : MulOneClass M₂] →
              [ContinuousMul M₂] →
                {F : Type u_8} →
                  [inst_5 : FunLike F M₁ M₂] →
                    [MonoidHomClass F M₁ M₂] →
                      {l : Filter α} →
                        (f : M₁ → M₂) →
                          (g : α → F) → [l.NeBot] → Filter.Tendsto (fun a x => (g a) x) l (nhds f) → M₁ →* M₂
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.toFreeAddMonoid_ne_zero : ∀ {α : Type u_1} (x : FreeAddSemigroup α), FreeAddSemigroup.toFreeAddMonoid x ≠ 0
-- Mathlib.Data.NNRat.Defs
NNRat.den_mul_eq_num : ∀ (q : ℚ≥0), ↑q.den * q = ↑q.num
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.op : Lean.Meta.Grind.AC.Struct → Lean.Expr
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R},
  ∑ j, w₁ j = 1 →
    ∑ j, w₂ j = 1 →
      ∀ {i : Fin (n + 1)},
        (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide
            ((Finset.affineCombination R Finset.univ s.points) w₁)
            ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
          SignType.sign (w₁ i) = SignType.sign (w₂ i) ∧ w₁ i ≠ 0
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.match_1.splitter : {n : ℕ} →
  (motive : List (BitVec n) → Sort u_1) →
    (x : List (BitVec n)) →
      (Unit → motive []) →
        ((x : BitVec n) → motive [x]) →
          ((x y : BitVec n) → (rest : List (BitVec n)) → motive (x :: y :: rest)) → motive x
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.mulComm.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.mulComm = 1
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- Auxiliary definition for `totalShift₂Iso`.  -/
HomologicalComplex₂.totalShift₂XIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) →
        (y : ℤ) →
          [inst_2 : K.HasTotal (ComplexShape.up ℤ)] →
            (n n' : ℤ) →
              n + y = n' →
                ((((HomologicalComplex₂.shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ)).X n ≅
                  (K.total (ComplexShape.up ℤ)).X n')
-- Mathlib.Data.List.NodupEquivFin
/-- If there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`,
then `Sublist l l'`.
 -/
List.sublist_of_orderEmbedding_getElem?_eq : ∀ {α : Type u_1} {l l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), l[ix]? = l'[f ix]?) → l.Sublist l'
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.StrictPseudofunctor.mapAdjunction_unit' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.StrictPseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  (F.mapAdjunction adj).unit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (F.map₂ adj.unit) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.precompUniformConvergenceCLM_apply`. -/
ContinuousLinearMap.precomp_uniformConvergenceCLM_apply : ∀ {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_9} {F : Type u_10} (G : Type u_11) [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G] (𝔖 : Set (Set E))
  (𝔗 : Set (Set F)) [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F)
  (hL : Set.MapsTo (fun x => ⇑L '' x) 𝔖 𝔗) (f : UniformConvergenceCLM τ G 𝔗),
  (ContinuousLinearMap.precompUniformConvergenceCLM G 𝔖 𝔗 L hL) f = f ∘SL L
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.map_ne : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x y : P}, x ≠ y → e x ≠ e y
-- Mathlib.RingTheory.LinearDisjoint
/-- In a commutative ring, if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module,
then for any family of `R`-linearly independent elements of `A`,
they are also `B`-linearly independent.  -/
Subalgebra.LinearDisjoint.linearIndependent_left_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥B] {ι : Type u_1} {a : ι → ↥A}, LinearIndependent R a → LinearIndependent (↥B) (⇑A.val ∘ a)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso adj).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.heq_eqToHom_comp_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y),
  g ≍ CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f ↔ g ≍ f
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Etale) →
    AlgebraicGeometry.Etale f
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_indicator_const : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {s : Set α},
  MeasurableSet s → μ s ≠ ⊤ → ∀ (x : E), MeasureTheory.setToFun μ T hT (s.indicator fun x_1 => x) = (T s) x
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_succAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), i.cycleRange (i.succAbove j) = j.succ
-- Mathlib.Data.Set.Function
Set.BijOn.inter_mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.BijOn f s₁ t₁ → Set.MapsTo f s₂ t₂ → s₁ ∩ f ⁻¹' t₂ ⊆ s₂ → Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instIsSiftedOppositeElementsFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point),
  CategoryTheory.IsSifted Φ.fiber.Elementsᵒᵖ
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.IsContPerfPair.ext_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst : CommRing R} {inst_1 : TopologicalSpace R}
  {inst_2 : AddCommGroup M} {inst_3 : Module R M} {inst_4 : TopologicalSpace M} {inst_5 : AddCommGroup N}
  {inst_6 : Module R N} {inst_7 : TopologicalSpace N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsContPerfPair}, x = y ↔ True
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonIdIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  (CategoryTheory.Functor.mapAddMonIdIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Init.Core
Std.Refl.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), r a a) → Std.Refl r
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.unit.sizeOf_spec : sizeOf Lean.Grind.CommRing.Mon.unit = 1
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.isComplex₂_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 2),
  CategoryTheory.CategoryStruct.comp
        (S.map' 0 1 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_2
          CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4)
        (S.map' 1 2 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4
          CategoryTheory.ComposableArrows.isComplex₂_iff._proof_5) =
      0 →
    S.IsComplex
-- Lean.Data.KVMap
Lean.DataValue.ofSyntax.inj : ∀ {v v_1 : Lean.Syntax}, Lean.DataValue.ofSyntax v = Lean.DataValue.ofSyntax v_1 → v = v_1
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instSemigroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semigroup Y],
  LocallyConstant.instSemigroup = Function.Injective.semigroup DFunLike.coe ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.HasOrthogonalProjection.map_linearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {E' : Type u_4} [inst_4 : NormedAddCommGroup E']
  [inst_5 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E'), (Submodule.map (↑f.toLinearEquiv) K).HasOrthogonalProjection
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.aux.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (k n : ℕ) (x : R),
  Pentagonal.aux✝ k n x = x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))