mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.PushoutCocone.isoMk t).hom.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
AEMeasurable.norm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable (fun a => ‖f a‖) μ
-- Mathlib.Data.Rat.Defs
Rat.addSemigroup : AddSemigroup ℚ
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_abs : ∀ (x : ℝ), Real.cos |x| = Real.cos x
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.ref : Lean.Elab.Term.LetRecToLift → Lean.Syntax
-- Mathlib.CategoryTheory.Sigma.Basic
/-- Given a collection of functors `F i : C i ⥤ D`, we can produce a functor `(Σ i, C i) ⥤ D`.

The produced functor `desc F` satisfies: `incl i ⋙ desc F ≅ F i`, i.e. restricted to just the
subcategory `C i`, `desc F` agrees with `F i`, and it is unique (up to natural isomorphism) with
this property.

This witnesses that the sigma-type is the coproduct in Cat.
 -/
CategoryTheory.Sigma.desc : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          ((i : I) → CategoryTheory.Functor (C i) D) → CategoryTheory.Functor ((i : I) × C i) D
-- Mathlib.Data.Nat.ModEq
Nat.mul_modulus_add_modEq_iff : ∀ {n a b c : ℕ}, b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- **Alias** of `Filter.map_atTop_finsetProd_le_of_prod_eq`.

---

Let `f` and `g` be two maps to the same commutative monoid. This lemma gives a sufficient
condition for comparison of the filter `atTop.map (fun s ↦ ∏ b ∈ s, f b)` with
`atTop.map (fun s ↦ ∏ b ∈ s, g b)`. This is useful to compare the set of limit points of
`Π b in s, f b` as `s → atTop` with the similar set for `g`.  -/
Filter.map_atTop_finset_prod_le_of_prod_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] {f : α → M} {g : β → M},
  (∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) →
    Filter.map (fun s => ∏ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∏ x ∈ s, g x) Filter.atTop
-- Init.Data.Cast
/-- The canonical homomorphism `Nat → R`. In most use cases, the target type will have a (semi)ring
structure, and this homomorphism should be a (semi)ring homomorphism.

`NatCast` and `IntCast` exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent `simp` normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
`NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a
`NatCast R` instance) whenever `R` is an additive monoid with a `1`.

The prototypical example is `Int.ofNat`.
 -/
Nat.cast : {R : Type u} → [NatCast R] → ℕ → R
-- Lean.Elab.Tactic.SolveByElim
/-- Elaborator for apply_rules.

See `Lean.MVarId.applyRules` for a `MetaM` level analogue of this tactic.
 -/
Lean.Elab.Tactic.SolveByElim.evalApplyRules : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Hom.Defs
/-- See note [hom simp lemma priority]  -/
map_mul : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] (f : F) (x y : M), f (x * y) = f x * f y
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
_private.Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence.0.Mathlib.Tactic.Monoidal.«term_▷_» : Lean.TrailingParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_filter_le_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool},
  (Std.TreeMap.filter f t).size ≤ t.size
-- Mathlib.GroupTheory.ResiduallyFinite
Group.residuallyFinite_iff_forall_finiteIndex : ∀ {G : Type u_1} [inst : Group G],
  Group.ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.isAdjMatrix_submatrix_iff : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} {A : Matrix V V α} [inst : Zero α] [inst_1 : One α] {f : W → V},
  Function.Surjective f → ((A.submatrix f f).IsAdjMatrix ↔ A.IsAdjMatrix)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.comp_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Functor SimplexCategory C}
  (α : CategoryTheory.NatTrans X Y) (β : CategoryTheory.NatTrans Y Z) (X_1 : SimplexCategory),
  (CategoryTheory.CategoryStruct.comp α β).app X_1 = CategoryTheory.CategoryStruct.comp (α.app X_1) (β.app X_1)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.apply_ofInjective_symm : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f)
  (x : ↥f.range), f ((AddMonoidHom.ofInjective hf).symm x) = ↑x
-- Mathlib.Data.Set.Card
Set.ncard_union_add_ncard_inter : ∀ {α : Type u_1} (s t : Set α),
  autoParam s.Finite Set.ncard_union_add_ncard_inter._auto_1 →
    autoParam t.Finite Set.ncard_union_add_ncard_inter._auto_3 → (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard
-- Mathlib.Algebra.Ring.BooleanRing
/-- The meet operation in a Boolean ring is `x * y`.  -/
BooleanRing.inf : {α : Type u_1} → [BooleanRing α] → Min α
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.instCompleteSpace : ∀ {α : Type u_1} [inst : UniformSpace α] [CompleteSpace α], CompleteSpace (TopologicalSpace.NonemptyCompacts α)
-- Init.Data.Order.MinMaxOn
apply_maxOn : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : Max β]
  [Std.LawfulOrderLeftLeaningMax β] {f : α → β} {x y : α}, f (maxOn f x y) = f x ⊔ f y
-- Lean.Environment
/-- Starts an asynchronous modification of the kernel environment. The environment is split into a
"main" branch that will block on access to the kernel environment until
`PromiseCheckedResult.commitChecked` has been called on the "async" environment branch.
 -/
Lean.Environment.promiseChecked : Lean.Environment → BaseIO Lean.Environment.PromiseCheckedResult
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.get_eq_get_ofSlice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} {h' : pos ≠ (s.slice p₀ p₁ h).endPos},
  pos.get h' = (String.Slice.Pos.ofSlice pos).get ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.isSome = true ↔ t.isEmpty = false
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.truncateToReal_le : ∀ {t : ENNReal}, t ≠ ⊤ → ∀ {x : ENNReal}, t.truncateToReal x ≤ t.toReal
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivWithinAt.congr_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' g' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → f' = g' → HasFDerivWithinAt f g' s x
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- the map which sends an arrow to its reverse  -/
Quiver.HasReverse.reverse' : {V : Type u_2} → {inst : Quiver V} → [self : Quiver.HasReverse V] → {a b : V} → (a ⟶ b) → (b ⟶ a)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpMeasSubgroupToLpTrim` preserves the norm.  -/
MeasureTheory.lpMeasSubgroupToLpTrim_norm_map : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hp : Fact (1 ≤ p)] (hm : m ≤ m0) (f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)),
  ‖MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.Constraint.isImpossible.match_1.splitter : (motive : Lean.Omega.Constraint → Sort u_1) →
  (x : Lean.Omega.Constraint) →
    ((x y : ℤ) → motive { lowerBound := some x, upperBound := some y }) →
      ((x : Lean.Omega.Constraint) →
          (∀ (x_1 y : ℤ), x = { lowerBound := some x_1, upperBound := some y } → False) → motive x) →
        motive x
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The radical of an ideal sheaf.  -/
AlgebraicGeometry.Scheme.IdealSheafData.radical : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → X.IdealSheafData
-- Init.Data.Vector.Lemmas
Vector.toArray_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, (xs.push x).toArray = xs.toArray.push x
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `lift_rank_le_of_injective_injective`.  -/
rank_le_of_injective_injectiveₛ : ∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R' M₁] (i : R' → R) (j : M →+ M₁),
  Function.Injective i →
    Function.Injective ⇑j → (∀ (r : R') (m : M), j (i r • m) = r • j m) → Module.rank R M ≤ Module.rank R' M₁
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.div_two_lt_floor : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a : K},
  1 ≤ a → a / 2 < ↑⌊a⌋₊
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_add_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α}, μ ≤ ν → μ ≤ ν + ν'
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.instPresheafIsFiniteObjFunctorOppositeTypeYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.PresheafIsFinite (CategoryTheory.yoneda.obj X)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- If two morphisms are exact on pseudoelements, they are exact.  -/
CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (∀ (b : CategoryTheory.Abelian.Pseudoelement S.X₂),
      CategoryTheory.Abelian.Pseudoelement.pseudoApply S.g b = 0 →
        ∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply S.f a = b) →
    S.Exact
-- Mathlib.SetTheory.Cardinal.UnivLE
univLE_iff_cardinal_le : UnivLE.{u, v} ↔ Cardinal.univ.{u, v + 1} ≤ Cardinal.univ.{v, u + 1}
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_ofArray : ∀ {n : ℕ} (arr : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray arr).ReadyForRatAdd
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforward_comp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R),
  SheafOfModules.pushforwardComp (CategoryTheory.CategoryStruct.id S) φ =
    (SheafOfModules.pushforward φ).isoWhiskerLeft (SheafOfModules.pushforwardId S) ≪≫
      (SheafOfModules.pushforward φ).rightUnitor
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofNatIsoRight.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : H ⊣ F) (iso : F ≅ G),
  adj.ofNatIsoRight iso =
    { unit := CategoryTheory.CategoryStruct.comp adj.unit (H.whiskerLeft iso.hom),
      counit := CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight iso.inv H) adj.counit,
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Algebra.Group.Basic
zsmul_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α) (n : ℤ), n • (a - b) = n • a - n • b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_mem_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, a ∈ m.insert k → (k == a) = false → a ∈ m
-- Init.Control.Lawful.Basic
Function.const.eq_1 : ∀ {α : Sort u} (β : Sort v) (a : α) (x : β), Function.const β a x = a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂_inv_comp_iCycles_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A 2))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i
          (groupHomology.chainsIso₂ A).inv))
      x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.coequifibered_op_iff : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered (CategoryTheory.NatTrans.op α) ↔ CategoryTheory.NatTrans.Equifibered α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_push : ∀ {m n : ℕ}, m < n → (m...n).toArray = (m...n - 1).toArray.push (n - 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_minKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).minKey?.isSome = !t.isEmpty
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyFaithful.of_jointly_reflects_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)}
  [CategoryTheory.Limits.HasEqualizers C]
  [∀ (i : I), CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (F i)],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) [CategoryTheory.Mono f],
      (∀ (i : I), CategoryTheory.IsIso ((F i).map f)) → CategoryTheory.IsIso f) →
    CategoryTheory.JointlyFaithful F
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instIsFiniteMeasureProdVolume : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasureTheory.MeasureSpace α] [inst_1 : MeasureTheory.MeasureSpace β]
  [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume],
  MeasureTheory.IsFiniteMeasure MeasureTheory.volume
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instToStringOffset : ToString Std.Time.Hour.Offset
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S] [inst_10 : NonUnitalRing A]
  [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A] [inst_14 : SMulCommClass S A A]
  [inst_15 : Algebra R S] [inst_16 : Module R A] [inst_17 : IsScalarTower R S A] [inst_18 : StarModule R S]
  [inst_19 : ContinuousSMul R S] [inst_20 : TopologicalSpace A] [CompleteSpace R] {a : A}
  {φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A},
  Topology.IsClosedEmbedding ⇑φ →
    ∀ {f : C(S, R)} (h : QuasispectrumRestricts a ⇑f),
      IsUniformEmbedding ⇑(algebraMap R S) →
        Topology.IsClosedEmbedding ⇑(QuasispectrumRestricts.nonUnitalStarAlgHom φ h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α},
      compare k k' = Ordering.eq → Std.DTreeMap.Internal.Impl.contains k t = Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_id : ∀ {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₂] [inst_1 : Semiring R₃]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃), f ∘ₛₗ LinearMap.id = f
-- Mathlib.Order.Sublocale
Sublocale.mem_carrier : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} {a : X}, a ∈ S.carrier ↔ a ∈ S
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed form of the inverse conjugation definition.  -/
CategoryTheory.conjugateEquiv_counit_symm : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : R₁ ⟶ R₂) (d : D),
  CategoryTheory.CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app d) =
    CategoryTheory.CategoryStruct.comp (((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d))
      (adj₁.counit.app d)
-- Mathlib.Order.Defs.LinearOrder
/-- In a linearly ordered type, we assume the order relations are all decidable.  -/
LinearOrder.toDecidableLT : {α : Type u_2} → [self : LinearOrder α] → DecidableLT α
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.mk_nnqsmul : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (q : ℚ≥0) (a : α)
  (ha : 0 ≤ a), ↑⟨q • a, ⋯⟩ = q • a
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddRightCancelSemigroup : {α : Type u_1} → [AddLeftCancelSemigroup α] → AddRightCancelSemigroup αᵃᵒᵖ
-- Lean.Meta.HaveTelescope
/-- Previous `have`s that the type of this `have` depends on, as indices into `HaveTelescopeInfo.haveInfo`.
Used in `computeFixedUsed` to compute used `have`s.  -/
Lean.Meta.HaveInfo.typeBackDeps : Lean.Meta.HaveInfo → Std.HashSet ℕ
-- Init.Control.Option
/-- Succeeds with the provided value.
 -/
OptionT.pure : {m : Type u → Type v} → [Monad m] → {α : Type u} → α → OptionT m α
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.exists_T_pow : ∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R),
  ∃ n f', Polynomial.toLaurent f' = f * LaurentPolynomial.T ↑n
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The natural semigroup hom from an `AddSubsemigroup` of
`AddSubsemigroup` `M` to `M`.  -/
AddMemClass.subtype : {M : Type u_1} →
  {A : Type u_3} → [inst : Add M] → [inst_1 : SetLike A M] → [hA : AddMemClass A M] → (S' : A) → ↥S' →ₙ+ M
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (F.map f)
-- Mathlib.RingTheory.Polynomial.Basic
/-- The span of every finite set of polynomials is contained in a `degreeLE n` for some `n`.  -/
Polynomial.span_le_degreeLE_of_finite : ∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)},
  s.Finite → ∃ n, Submodule.span R s ≤ Polynomial.degreeLE R ↑n
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.isCoinductive : Lean.Elab.Command.InductiveView → Bool
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_comapDomain_le_of_canonicallyOrderedAdd : ∀ {σ : Type u_1} {M : Type u_2} {τ : Type u_5} {f : σ → τ} [inst : AddCommMonoid M] [inst_1 : PartialOrder M]
  [CanonicallyOrderedAdd M] {x : τ →₀ M} (hf : Set.InjOn f (f ⁻¹' ↑x.support)),
  Finsupp.degree (Finsupp.comapDomain f x hf) ≤ Finsupp.degree x
-- Lean.Parser.Types
Lean.Parser.Error.instToString : ToString Lean.Parser.Error
-- Mathlib.Tactic.Ring.Common
/-- Raise a coefficient to some natural power.

The exponent is not necessarily a natural literal. If the tactic can only raise coefficients to
the power of a literal (e.g. `ring`), it should check for this and return `none` otherwise.  -/
Mathlib.Tactic.Ring.Common.RingCompute.pow : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          {x : Q(«$α»)} →
            {b : Q(ℕ)} →
              BaseType x →
                Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
                  OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» ^ «$b»))
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongr_apply_apply : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a))
  (f : (a : α) → W a) (a : α), (h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)
-- Lean.Meta.Basic
Lean.Meta.processPostponed : optParam Bool true → optParam Bool false → Lean.MetaM Bool
-- Mathlib.Data.Prod.Basic
Prod.fst_injective : ∀ {α : Type u_1} {β : Type u_2} [Subsingleton β], Function.Injective Prod.fst
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_fun : ∀ {α : Type u_3} {β : Type u_4}, ENat.card (α → β) = ENat.card β ^ ENat.card α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonCompIso_hom_app_hom : ∀ {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] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.AddMon C),
  (CategoryTheory.Functor.mapAddMonCompIso.hom.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.CategoryTheory.Limits.Sifted
/-- A category with binary coproducts is sifted or empty.  -/
CategoryTheory.IsSifted.instIsSiftedOrEmptyOfHasBinaryCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C],
  CategoryTheory.IsSiftedOrEmpty C
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.continuous_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace Y]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Z],
  Topology.IsInducing g → (Continuous f ↔ Continuous (g ∘ f))
-- Init.Data.Array.MapIdx
Array.mapIdx_set : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α} {i : ℕ} {h : i < xs.size} {a : α},
  Array.mapIdx f (xs.set i a h) = (Array.mapIdx f xs).set i (f i a) ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- An affine subspace constructed from a point and a direction contains that point.  -/
AffineSubspace.self_mem_mk' : ∀ {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) (direction : Submodule k V), p ∈ AffineSubspace.mk' p direction
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivFunOnFintype_single : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι)
  (m : β i), (DFinsupp.equivFunOnFintype fun₀ | i => m) = Pi.single i m
-- Mathlib.Order.BooleanAlgebra.Basic
compl_le_iff_compl_le : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ ≤ y ↔ yᶜ ≤ x
-- Init.Omega.Int
Lean.Omega.Int.ofNat_congr : ∀ {a b : ℕ}, a = b → ↑a = ↑b