mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeft_trans : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddZeroClass M₃] [inst_3 : AddCommMonoid N] (e₁₂ : M₁ ≃+ M₂) (e₂₃ : M₂ ≃+ M₃),
  (e₁₂.trans e₂₃).addMonoidHomCongrLeft = e₁₂.addMonoidHomCongrLeft.trans e₂₃.addMonoidHomCongrLeft
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.LeftAdjoint.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {right : b ⟶ a} {left : a ⟶ b}
  {adj : CategoryTheory.Bicategory.Adjunction left right} {left_1 : a ⟶ b}
  {adj_1 : CategoryTheory.Bicategory.Adjunction left_1 right},
  { left := left, adj := adj } = { left := left_1, adj := adj_1 } → left = left_1 ∧ adj ≍ adj_1
-- Init.ShareCommon
MonadShareCommon.mk : {m : Type u → Type v} → ({α : Type u} → α → m α) → MonadShareCommon m
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Given `Subsemigroup`s `s`, `t` of semigroups `M`, `N` respectively, `s × t` as a subsemigroup
of `M × N`.  -/
Subsemigroup.prod : {M : Type u_1} →
  {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → Subsemigroup M → Subsemigroup N → Subsemigroup (M × N)
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_const : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι},
  s.Nonempty → ∀ (a : M), (s.expect fun _i => a) = a
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.Functor.leftOp_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [F.Additive], F.leftOp.Additive
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind : Type
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_symm : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] {σ₂₁ : R₂ →+* R} [inst_10 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_11 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂),
  (TensorProduct.congr f g).symm = TensorProduct.congr f.symm g.symm
-- Lean.Elab.DocString
/-- A number  -/
Lean.Doc.DocArg.num : Lean.NumLit → Lean.Doc.DocArg
-- Lean.Meta.Tactic.Grind.Core
/-- Closes the goal when `True` and `False` are in the same equivalence class.  -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.closeGoalWithTrueEqFalse : Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f.range.subtype.dualMap → f.dualMap.range = f.ker.dualAnnihilator
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.mk.inj : ∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}}
  {toDiagram : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {top : J}
  {isTerminal : toDiagram.IsTerminal top} {uniq_terminal : ∀ (j : J) (hj : toDiagram.IsTerminal j), j = top}
  {toDiagram_1 : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {top_1 : J}
  {isTerminal_1 : toDiagram_1.IsTerminal top_1}
  {uniq_terminal_1 : ∀ (j : J) (hj : toDiagram_1.IsTerminal j), j = top_1},
  { toDiagram := toDiagram, top := top, isTerminal := isTerminal, uniq_terminal := uniq_terminal } =
      { toDiagram := toDiagram_1, top := top_1, isTerminal := isTerminal_1, uniq_terminal := uniq_terminal_1 } →
    toDiagram = toDiagram_1 ∧ top = top_1 ∧ isTerminal ≍ isTerminal_1
-- Std.Data.HashMap.Basic
Std.HashMap.instGetElem?Mem : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → GetElem? (Std.HashMap α β) α β fun m a => a ∈ m
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply : ∀ (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] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) [inst_8 : LieModule.LinearWeights R L M] (x : L)
  (m : ↥(LieModule.shiftedGenWeightSpace R L M χ)), ↑⁅x, m⁆ = ⁅x, ↑m⁆ - χ x • ↑m
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {b : α}, b ≠ ⊤ → StrictMono fun x => x - b
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.self_comp_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β), ⇑e ∘ ⇑e.symm = id
-- Init.Data.Iterators.Basic
Std.IterStep.yield.injEq : ∀ {α : Sort u_1} {β : Sort u_2} (it : α) (out : β) (it_1 : α) (out_1 : β),
  (Std.IterStep.yield it out = Std.IterStep.yield it_1 out_1) = (it = it_1 ∧ out = out_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- `simplicialEvalσ` is a lift to ℕ of `(toSimplexCategory.map (standardσ m L _ _)).toOrderHom`.
Rather than defining it as such, we define it inductively for less painful inductive reasoning,
(see `simplicialEvalσ_of_isAdmissible`).
It is expected to produce the correct result only if `L` is admissible, and values for
non-admissible lists should be considered junk values. Similarly, values for out-of-bounds inputs
are junk values.  -/
SimplexCategoryGenRel.simplicialEvalσ : List ℕ → ℕ → ℕ
-- Mathlib.Order.Category.BoolAlg
/-- The underlying `BoundedLatticeHom`.  -/
BoolAlg.Hom.hom' : {X Y : BoolAlg} → X.Hom Y → BoundedLatticeHom ↑X ↑Y
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- The morphism from a seminormed group to the quotient by the inseparable setoid.  -/
SeparationQuotient.normedMk : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → NormedAddGroupHom M (SeparationQuotient M)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.lift_add : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (x y : QuaternionAlgebra R c₁ c₂ c₃), q.lift (x + y) = q.lift x + q.lift y
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, Option.all (fun x_2 => x_2 == k) (m.get? k) = true
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_one : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : One α], Measurable 1
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.tuple.inj : ∀ {args args_1 : List Lean.Parser.Tactic.MRefinePat},
  Lean.Parser.Tactic.MRefinePat.tuple args = Lean.Parser.Tactic.MRefinePat.tuple args_1 → args = args_1
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.arrayElem.sizeOf_spec : sizeOf Lean.Json.CompressWorkItemKind.arrayElem✝ = 1
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instMax.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instMax = { max := fun s t => { carrier := ↑s ∩ ↑t, upper' := ⋯ } }
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.sum_hadamard_eq : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalSemiring α], ∑ i, ∑ j, A.hadamard B i j = (A * B.transpose).trace
-- Batteries.Data.String.Lemmas
String.utf8Len.eq_1 : String.utf8Len [] = 0
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
lowerHemicontinuousWithinAt_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, LowerHemicontinuousWithinAt (fun x => {f x}) s x ↔ ContinuousWithinAt f s x
-- Mathlib.NumberTheory.KummerDedekind
KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥)
  (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x),
  KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' =
    (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (KummerDedekind.quotMapEquivQuotQuotMap hx hx') ⋯ ⋯).trans
      (Ideal.normalizedFactorsEquivSpanNormalizedFactors ⋯).symm
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.comap_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₂₁ : R₂ →+* R}
  (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p) (p' : Submodule R ↥p),
  Submodule.comap (LinearMap.codRestrict p f hf) p' = Submodule.comap f (Submodule.map p.subtype p')
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.inf_apply : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R], ⌈0⌉ = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, a ∈ m.insert k v → (k == a) = false → a ∈ m
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckBinop : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffOn_zeroSection : ∀ {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B},
  ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.zeroSection F E) t
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.julian0.sizeOf_spec : ∀ (day : Std.Time.Internal.Bounded.LE 0 365), sizeOf (Std.Time.TimeZone.TransitionSpec.julian0 day) = 1 + sizeOf day
-- Lean.Parser.Basic
/-- `withoutForbidden(p)` runs `p` disabling the "forbidden token" (see `withForbidden`), if any.
This is usually used by bracketing constructs like `(...)` because there is no parsing ambiguity
inside these nested constructs.

This parser has the same arity as `p` - it just forwards the results of `p`.  -/
Lean.Parser.withoutForbidden : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_zero : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α), Matrix.vecCons x u 0 = x
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.instUnramified : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Algebra.Etale R A],
  Algebra.Unramified R A
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_iff_source_of_mem_maximalAtlas : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {f : M → M'} {s : Set M} {n : WithTop ℕ∞},
  e ∈ IsManifold.maximalAtlas I n M →
    s ⊆ e.source →
      (ContMDiffOn I I' n f s ↔
        ContMDiffOn (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s))
-- Std.Data.HashMap.Raw
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.HashMap.Raw.ofList : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → List (α × β) → Std.HashMap.Raw α β
-- Mathlib.Data.ENat.Pow
ENat.top_epow_top : ⊤ ^ ⊤ = ⊤
-- Mathlib.Order.SuccPred.Limit
WithTop.isSuccPrelimit_top : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α], Order.IsSuccPrelimit ⊤
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_one_iff_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a < 1 → (a ^ n ≤ 1 ↔ 0 ≤ n)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  Std.DHashMap.Raw.foldM f init ↑m = List.foldlM (fun a b => f a b.fst b.snd) init (↑m).toList
-- Mathlib.Order.RelIso.Basic
RelIso.instRelHomClass : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, RelHomClass (r ≃r s) r s
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_equiv_eq_map_symm : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring 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₂)
  (K : Submodule R₂ M₂), Submodule.comap (↑e) K = Submodule.map (↑e.symm) K
-- Mathlib.Topology.Category.UniformSpace
/-- The functor turning uniform spaces into complete separated uniform spaces.  -/
UniformSpaceCat.completionFunctor : CategoryTheory.Functor UniformSpaceCat CpltSepUniformSpace
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.goal.inj : ∀ {a a_1 : Lean.Widget.InteractiveGoal}, Lean.Widget.MsgEmbed.goal a = Lean.Widget.MsgEmbed.goal a_1 → a = a_1
-- Mathlib.Topology.Order
induced_fun_id : ∀ {α : Type u_1} {t : TopologicalSpace α}, TopologicalSpace.induced (fun x => x) t = t
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The setoid given by non-adjacency  -/
SimpleGraph.IsCompleteMultipartite.setoid : {α : Type u} → {G : SimpleGraph α} → G.IsCompleteMultipartite → Setoid α
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkRight_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : α × γ) (s : Set β),
  ((ProbabilityTheory.Kernel.prodMkRight γ κ) ca) s = (κ ca.1) s
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Existence of a `GCDMonoid` structure on a `CommMonoidWithZero`.  -/
IsGCDMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Prop
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the second left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction₂.f' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₂ X Y) → X ⟶ self.Y'
-- Mathlib.Algebra.Module.Equiv.Defs
SemilinearEquivClass.semilinearEquiv_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ] {F : Type u_14}
  [inst_6 : EquivLike F M M₂] [inst_7 : SemilinearEquivClass F σ M M₂] (f : F) (x : M), ↑f x = f x
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.IsNormal.blsub_eq : ∀ {f : Ordinal.{u} → Ordinal.{max u v}},
  Order.IsNormal f → ∀ {o : Ordinal.{u}}, Order.IsSuccLimit o → (o.blsub fun x x_1 => f x) = f o
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofBitVec : ∀ (b : BitVec 64), { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.uniformContinuousOn : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s → UniformContinuousOn f s
-- Mathlib.Data.Seq.Basic
Stream'.Seq.ofList_append : ∀ {α : Type u} (l l' : List α), ↑(l ++ l') = (↑l).append ↑l'
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The cardinality of a block divides the cardinality of the ambient type  -/
AddAction.IsBlock.ncard_dvd_card : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  {B : Set X}, AddAction.IsBlock G B → B.Nonempty → B.ncard ∣ Nat.card X
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Estimate for `log⁺` of a sum. See `Real.posLog_sum` for a variant involving multiple summands.
 -/
Real.posLog_add : ∀ {x y : ℝ}, (x + y).posLog ≤ Real.log 2 + x.posLog + y.posLog
-- Mathlib.Algebra.Homology.HomologySequence
/-- The natural transformation `K.opcyclesToCycles i j : K.opcycles i ⟶ K.cycles j` for all
`K : HomologicalComplex C c`.  -/
HomologicalComplex.natTransOpCyclesToCycles : (C : Type u_1) →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (c : ComplexShape ι) →
          (i j : ι) →
            [inst_2 : CategoryTheory.CategoryWithHomology C] →
              HomologicalComplex.opcyclesFunctor C c i ⟶ HomologicalComplex.cyclesFunctor C c j
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (a : α) (n : ℕ), {a} ^ n = {a ^ n}
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is `p`-radical, then for any ring `M` of exponential characteristic `p` whose
`p`-nilradical is zero, the map `(L →+* M) → (K →+* M)` induced by `i` is injective.  -/
IsPRadical.injective_comp_of_pNilradical_eq_bot : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (p : ℕ) [ExpChar M p] [IsPRadical i p], pNilradical M p = ⊥ → Function.Injective fun f => f.comp i
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f -ᵥ g` is generated by `{s -ᵥ t | s ∈ f, t ∈ g}` in scope `Pointwise`.  -/
Filter.instVSub : {α : Type u_2} → {β : Type u_3} → [VSub α β] → VSub (Filter α) (Filter β)
-- Lean.Server.FileSource
Lean.Lsp.FileSource.mk : {α : Type} → (α → Lean.Lsp.DocumentUri) → Lean.Lsp.FileSource α
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Variant of `get!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Internal.Raw₀.Const.get!_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ]
  {f : α → β → γ} {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.map f m) k =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯).get!
-- Init.Data.Int.DivMod.Lemmas
Int.sub_bmod_right : ∀ (a : ℤ) (b : ℕ), (a - ↑b).bmod b = a.bmod b
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `elimVarM a` performs one round of Fourier-Motzkin elimination, eliminating the variable `a`
from the `linarith` state.
 -/
Mathlib.Tactic.Linarith.elimVarM : ℕ → Mathlib.Tactic.Linarith.LinarithM Unit
-- Mathlib.NumberTheory.Padics.PadicNumbers
instFieldPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Field ℚ_[p]
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpen_mul : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f g : A),
  AlgebraicGeometry.Proj.basicOpen 𝒜 (f * g) =
    AlgebraicGeometry.Proj.basicOpen 𝒜 f ⊓ AlgebraicGeometry.Proj.basicOpen 𝒜 g
-- Init.Prelude
/-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. -/
Membership.mem : {α : outParam (Type u)} → {γ : Type v} → [self : Membership α γ] → γ → α → Prop
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.toBitVec_maxValueSealed_eq_intMaxSealed : Int32.maxValueSealed✝.toBitVec = BitVec.Signed.intMaxSealed✝ 32
-- Init.Data.List.Lemmas
List.append_eq_nil_iff : ∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.eq_1 : ∀ {α : Type u_2} [inst : Monoid α] (s : Set α),
  ThreeGPFree s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_replicate : ∀ {i n w : ℕ} {x : BitVec w}, (BitVec.replicate n x).getMsbD i = (decide (i < w * n) && x.getMsbD (i % w))
-- Mathlib.Combinatorics.Additive.Energy
/-- The multiplicative energy `Eₘ[s, t]` of two finsets `s` and `t` in a group is the number of
quadruples `(a₁, a₂, b₁, b₂) ∈ s × s × t × t` such that `a₁ * b₁ = a₂ * b₂`.

The notation `Eₘ[s, t]` is available in scope `Combinatorics.Additive`.  -/
Finset.mulEnergy : {α : Type u_1} → [DecidableEq α] → [Mul α] → Finset α → Finset α → ℕ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.of_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (a : Multiplicative M),
  (AddMonoidAlgebra.of R M) a = AddMonoidAlgebra.single (Multiplicative.toAdd a) 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `Cocycle K L n ≃+ Cocycle K L⟦a⟧ n'` when `n' + a = n`.  -/
CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (n a n' : ℤ) →
          n' + a = n →
            CochainComplex.HomComplex.Cocycle K L n ≃+
              CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.mk.sizeOf_spec : ∀ {X : Type u_3} [inst : SizeOf X] (as : X), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.toUniformOnFun_toFun : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  (f : ContinuousMultilinearMap 𝕜 E F), (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f.toUniformOnFun = ⇑f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_diff_le_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.Shrink.equivalence.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Small.{w, u} C],
  CategoryTheory.Shrink.equivalence C = (CategoryTheory.Equivalence.induced (equivShrink C).symm).symm