mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Lattice
InfHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] {g : InfHom β γ}
  {f₁ f₂ : InfHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_v_fst_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m)
  (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃) {Z : C} (h_1 : F.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p₂ p₃ h₂₃) h_1) =
    CategoryTheory.CategoryStruct.comp (α.v p₁ p₃ ⋯) h_1
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_sup : ∀ {G : Type u_2} [inst : Group G] (S₁ S₂ : Subgroup G), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.List.mapIdx.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → Array β → Sort u_3) →
      (x : List α) →
        (x_1 : Array β) →
          ((acc : Array β) → motive [] acc) →
            ((a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc) → motive x x_1
-- Mathlib.Algebra.Group.Defs
natCast_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G) (n : ℕ), ↑n • a = n • a
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.instMonoidalSkeletonFunctorSkeletonEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.skeletonEquivalence C).functor.Monoidal
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Limits.Multifork.ι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (a : J.L),
  K.ι a = K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.empty_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C),
  (CategoryTheory.PreZeroHypercover.empty S).I₀ = PEmpty.{w + 1}
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  (X : CategoryTheory.MonoOver (⊤_ C)),
  ((CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.obj X).obj = X.obj.left
-- Mathlib.Topology.Algebra.InfiniteSum.Real
Set.sigmaEquiv.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (s : α → Set β) (hs : ∀ (b : β), ∃! i, b ∈ s i),
  Set.sigmaEquiv s hs = Set.sigmaEquiv s hs
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value is multiplicative  -/
IsAbsoluteValue.abv_mul' : ∀ {S : Type u_5} {inst : Semiring S} {inst_1 : PartialOrder S} {R : Type u_6} {inst_2 : Semiring R} {f : R → S}
  [self : IsAbsoluteValue f] (x y : R), f (x * y) = f x * f y
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint64 : Lean.IR.IRType
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_smul : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] [inst_8 : LieAlgebra R L] [inst_9 : LieModule R L N] (t : R)
  (f : M →ₗ⁅R,L⁆ N), ⇑(t • f) = t • ⇑f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (↑(t.insertMany! l)).getKey? k = t.getKey? k
-- Mathlib.RingTheory.Algebraic.Integral
instIsAlgebraicMvPolynomialOfNoZeroDivisors : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] {σ : Type u_4} [NoZeroDivisors R],
  Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
-- Mathlib.Geometry.Manifold.Notation
/-- Try a strategy `x : TermElabM` which either successfully finds a `ModelWithCorners` or fails.
On failure in `x`, exceptions are caught, traced (`trace.Elab.DiffGeo.MDiff`), and `none` is
successfully returned.

We run `x` with `errToSorry == false` to convert elaboration errors into
exceptions, and under `withSynthesize` in order to force typeclass synthesis errors to appear and
be caught.

Trace messages produced during the execution of `x` are wrapped in a collapsible trace node titled
with `strategyDescr` and an indicator of success.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.tryStrategy : Lean.MessageData →
  Lean.Elab.TermElabM Manifold.Elab.FindModelResult → Lean.Elab.TermElabM (Option Manifold.Elab.FindModelResult)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_pos`.  -/
add_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  0 < a → 0 < b → 0 < a + b
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.mk.inj : ∀ {R : Type u_1} {M : Type u_2} {inst : Semiring R} {inst_1 : TopologicalSpace R} {inst_2 : AddCommGroup M}
  {inst_3 : Module R M} {toAddGroupFilterBasis : AddGroupFilterBasis M}
  {smul' : ∀ {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis.sets, V • W ⊆ U}
  {smul_left' :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U}
  {smul_right' : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U}
  {toAddGroupFilterBasis_1 : AddGroupFilterBasis M}
  {smul'_1 :
    ∀ {U : Set M}, U ∈ toAddGroupFilterBasis_1.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis_1.sets, V • W ⊆ U}
  {smul_left'_1 :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis_1.sets → ∃ V ∈ toAddGroupFilterBasis_1.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U}
  {smul_right'_1 : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis_1.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U},
  { toAddGroupFilterBasis := toAddGroupFilterBasis, smul' := smul', smul_left' := smul_left',
        smul_right' := smul_right' } =
      { toAddGroupFilterBasis := toAddGroupFilterBasis_1, smul' := smul'_1, smul_left' := smul_left'_1,
        smul_right' := smul_right'_1 } →
    toAddGroupFilterBasis = toAddGroupFilterBasis_1
-- Mathlib.Order.CompleteLattice.Basic
iInf_pos : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α} (hp : p), ⨅ (h : p), f h = f hp
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindExceptT : ∀ {m : Type u_1 → Type u_2} {ε : Type u_1} [inst : Monad m] [inst_1 : (α : Type u_1) → Lean.Order.PartialOrder (m α)]
  [Lean.Order.MonoBind m], Lean.Order.MonoBind (ExceptT ε m)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_eq_sInf : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CompleteLattice ι] {u : ι → Ω → β} {s : Set β} (ω : Ω),
  MeasureTheory.hittingBtwn u s ⊥ ⊤ ω = sInf {i | u i ω ∈ s}
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isExplicit : Lean.Syntax → Bool
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a negative constant, `fun x ↦ r * f x` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`.  -/
Filter.tendsto_const_mul_atBot_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop)
-- Mathlib.Order.Concept
Order.isIntent_upperPolar : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α}, Order.IsIntent r (upperPolar r s)
-- Init.Omega.Int
Lean.Omega.Fin.ofNat_val_add : ∀ {n : ℕ} {x y : Fin n}, ↑↑(x + y) = (↑↑x + ↑↑y) % ↑n
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.inrX_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder] (i : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K i) ((HomologicalComplex.cylinder.π K).f i) =
    (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id K)).f i
-- Init.Data.List.Find
List.findSome?_cons_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} {l : List α},
  (f a).isNone = true → List.findSome? f (a :: l) = List.findSome? f l
-- Init.Data.List.Perm
List.Perm.eqv : ∀ (α : Type u_1), Equivalence List.Perm
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.mono : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCancelCommMonoid α] [inst_1 : AddCancelCommMonoid β] {A : Set α} {B : Set β}
  {f : α → β} {m n : ℕ} {hmn : m ≤ n}, IsAddFreimanIso n A B f → IsAddFreimanIso m A B f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.memP_iff_lowerBound? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    (RBTree.RBNode.MemP cut t ↔ ∃ x, RBTree.RBNode.lowerBound? cut t = some x ∧ cut x = Ordering.eq)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instSMulNatHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → SMul ℕ (M ⟶ N)
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- The identity map is a bialgebra equivalence.  -/
BialgEquiv.refl : (R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : CoalgebraStruct R A] → A ≃ₐc[R] A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.filterMap_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ},
  Std.ExtDTreeMap.filterMap f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.ExtDTreeMap.Const.get t k h) = none
-- Mathlib.Data.Finset.Preimage
Equiv.restrictPreimageFinset_symm_apply_coe : ∀ {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) (b : ↥s), ↑((e.restrictPreimageFinset s).symm b) = e.symm ↑b
-- Init.Data.SInt.Bitwise
Int16.toInt8_not : ∀ (a : Int16), (~~~a).toInt8 = ~~~a.toInt8
-- Mathlib.RingTheory.Etale.QuasiFinite
PrimeSpectrum.primesOverOrderIsoFiber.eq_1 : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime],
  PrimeSpectrum.primesOverOrderIsoFiber R S p =
    OrderIso.trans
      { toFun := fun q => ⟨{ asIdeal := ↑q, isPrime := ⋯ }, ⋯⟩, invFun := fun q => ⟨(↑q).asIdeal, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯, map_rel_iff' := ⋯ }
      (PrimeSpectrum.preimageOrderIsoFiber R S { asIdeal := p, isPrime := inst_3 })
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(∀ ..., ...)⌝` syntax from applications of `SPred.forall`, lifting
nested applications of `spred(...)` from the body.
 -/
Std.Do.SPred.Notation.unexpandForall : Lean.PrettyPrinter.Unexpander
-- Batteries.CodeAction.Basic
/-- A code action which calls `@[tactic_code_action]` code actions.  -/
Batteries.CodeAction.tacticCodeActionProvider : Lean.Server.CodeActionProvider
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.neg_eq_of_add_eq_zero_left : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, a + ↑u = 0 → ↑(-u) = a
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo.mk : String → Option String → Lean.Lsp.ClientInfo
-- Lean.MetavarContext
Lean.MetavarContext.findDecl? : Lean.MetavarContext → Lean.MVarId → Option Lean.MetavarDecl
-- Mathlib.RingTheory.LocalProperties.Basic
Algebra.idealMap_eq_ofEq_comp_toLocalized₀ : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [inst_3 : IsLocalization p S] (I : Ideal R),
  Algebra.idealMap S I =
    ↑(LinearEquiv.ofEq (Submodule.localized₀ p (Algebra.linearMap R S) I)
          (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯) ∘ₗ
      Submodule.toLocalized₀ p (Algebra.linearMap R S) I
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingHom_apply : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α →+* β) (hf : Continuous ⇑f) {x : UniformSpace.Completion α},
  (UniformSpace.Completion.mapRingHom f hf) x = UniformSpace.Completion.map (⇑f) x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.vadd_def : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → VAdd R (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] (i : ι)
  (x : G i) (r : R), r +ᵥ ⟦⟨i, x⟩⟧ = ⟦⟨i, r +ᵥ x⟩⟧
-- Mathlib.Order.SetDissipate
Set.biInter_dissipate : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {s : α → Set β} {x : α},
  ⋂ y, ⋂ (_ : y ≤ x), Set.dissipate s y = Set.dissipate s x
-- Mathlib.Analysis.Calculus.LogDeriv
/-- If two functions agree in a punctured neighborhood of `x`, then so do their logarithmic derivatives.
 -/
logDeriv_congr_nhdsNE : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {x : 𝕜},
  f =ᶠ[nhdsWithin x {x}ᶜ] g → logDeriv f =ᶠ[nhdsWithin x {x}ᶜ] logDeriv g
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a monoid is isomorphic to the center of its opposite.  -/
Submonoid.centerToMulOpposite : {M : Type u_2} → [inst : MulOneClass M] → ↥(Submonoid.center M) ≃* ↥(Submonoid.center Mᵐᵒᵖ)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq_equiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  {i j : E.I₀} (k : E.I₁ i j),
  (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k =
    s₁.symm ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (s₁ k))
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.map_mono : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S T : CategoryTheory.Subgroupoid C),
  S ≤ T → CategoryTheory.Subgroupoid.map φ hφ S ≤ CategoryTheory.Subgroupoid.map φ hφ T
-- Mathlib.Algebra.Lie.Weights.Linear
/-- A type synonym for the `χ`-weight space but with the action of `x : L`
on `m : genWeightSpace M χ`, shifted to act as `⁅x, m⁆ - χ x • m`.  -/
LieModule.shiftedGenWeightSpace : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [LieModule R L M] → [LieRing.IsNilpotent L] → (L → R) → LieSubmodule R L M
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), Std.Internal.List.getKey a l h = a
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddCommGrpCat fun x1 x2 => ↑x1 →+ ↑x2
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumElim_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L')
  (_n : ℕ) (a : L.Relations _n ⊕ L''.Relations _n),
  (ϕ.sumElim ψ).onRelation a = Sum.elim (fun f => ϕ.onRelation f) (fun f => ψ.onRelation f) a
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.Ref.cast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (ref : aig1.Ref)
  (h : aig1.decls.size ≤ aig2.decls.size), ref.cast h = { gate := ref.gate, invert := ref.invert, hgate := ⋯ }
-- Mathlib.Algebra.Lie.OfAssociative
LieSubalgebra.toEnd_mk : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (K : LieSubalgebra R L) {x : L} (hx : x ∈ K), (LieModule.toEnd R (↥K) M) ⟨x, hx⟩ = (LieModule.toEnd R L M) x
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.algebraMap_apply : ∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R (LaurentPolynomial A)) r = LaurentPolynomial.C ((algebraMap R A) r)
-- Init.Data.Fin.Lemmas
Fin.one_lt_succ_succ : ∀ {n : ℕ} (a : Fin n), 1 < a.succ.succ
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `InvImage.isTrans`. -/
InvImage.trans : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsTrans β r], IsTrans α (InvImage r f)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.inf : ∀ {α : Type u_1} {l l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → l'.HasBasis p' s' → (l ⊓ l').HasBasis (fun i => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_comp : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f g : Module.End R₁' M₁'),
  e.conj (g ∘ₗ f) = e.conj g ∘ₗ e.conj f
-- Mathlib.Logic.Function.Conjugate
Function.Commute.refl : ∀ {α : Type u_1} (f : α → α), Function.Commute f f
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {m n : WithTop ℕ∞} [CompleteSpace E]
  [inst_7 : IsManifold I 1 M] {V : (x : M) → TangentSpace I x},
  ContMDiffWithinAt I I.tangent m (fun x => ⟨x, V x⟩) s x →
    UniqueMDiff[s] →
      x ∈ s →
        m + 1 ≤ n →
          m ≠ ↑⊤ →
            ∀ᶠ (y : M) in nhdsWithin x s,
              ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent m
                (fun x_1 =>
                  ⟨x_1,
                    VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I)
                      x_1⟩)
                ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.singleAlgHom_apply : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] [inst_3 : DecidableEq ι] (i : ι) (a : A i),
  (PiTensorProduct.singleAlgHom i) a = (PiTensorProduct.tprod R) ((MonoidHom.mulSingle A i) a)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.instInhabitedEmbedFmt : Inhabited Lean.Widget.EmbedFmt✝
-- Init.Data.List.Lex
List.lex_eq_true_iff_lt : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : LT α] [inst_3 : DecidableLT α] {l₁ l₂ : List α},
  (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔ l₁ < l₂
-- Std.Http.Server.Connection
/-- Waits for the next I/O event across all active sources described by `sources`.
Computes the socket recv size from `config`, then races all active selectables.
Calls `Handler.onFailure` and returns `.close` on transport errors.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.pollNextEvent : {α σ β : Type} →
  [Std.Http.Transport α] →
    [Std.Http.Server.Handler σ] →
      [Std.Http.Body β] →
        Std.Http.Config →
          σ → Std.Http.Server.Connection.PollSources✝ α β → Std.Async.Async (Std.Http.Server.Connection.Recv✝ β)
-- Mathlib.Topology.Order.ScottTopology
Topology.instIsScottHausdorff : ∀ (α : Type u_3) (D : Set (Set α)) [inst : Preorder α], Topology.IsScottHausdorff α D
-- Mathlib.Algebra.Star.Unitary
Unitary.mapEquiv_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R ≃⋆* S) (a : ↥(unitary R)), (Unitary.mapEquiv f) a = (Unitary.map f.toStarMonoidHom) a
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.computeDistance_eq_prefixFunctionRecurrence : ∀ {s : String.Slice} (i : ℕ) (hi : i < s.copy.toByteArray.size) {patByte : UInt8},
  patByte = s.copy.toByteArray[i] →
    ∀ (table : Array ℕ) {ht : table.size ≤ s.utf8ByteSize},
      String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ s.copy.toByteArray table →
        ∀ {h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i} {guess : ℕ} {hg : guess < i} {hg' : guess < table.size},
          ↑(String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ s patByte table ht h guess hg') =
            String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ s.copy.toByteArray i hi guess hg
-- Mathlib.NumberTheory.MulChar.Basic
/-- Extensionality. See `ext` below for the version that will actually be used.  -/
MulChar.ext' : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {χ χ' : MulChar R R'},
  (∀ (a : R), χ a = χ' a) → χ = χ'
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instSMul : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → SMul α (LowerSet α)
-- Std.Time.Format.Basic
Std.Time.FormatConfig.mk.injEq : ∀ (allowLeapSeconds : Bool) (dateformat : Std.Time.DateFormat) (allowLeapSeconds_1 : Bool)
  (dateformat_1 : Std.Time.DateFormat),
  ({ allowLeapSeconds := allowLeapSeconds, dateformat := dateformat } =
      { allowLeapSeconds := allowLeapSeconds_1, dateformat := dateformat_1 }) =
    (allowLeapSeconds = allowLeapSeconds_1 ∧ dateformat = dateformat_1)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
-- Mathlib.Combinatorics.Matroid.Basic
/-- A set `X` has the maximal subset property for a predicate `P` if every subset of `X` satisfying
`P` is contained in a maximal subset of `X` satisfying `P`.  -/
Matroid.ExistsMaximalSubsetProperty : {α : Type u_1} → (Set α → Prop) → Set α → Prop