mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.EGauge
egauge_ball_le_of_one_lt_norm : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜} {x : E} {r : NNReal}, 1 < ‖c‖ → r ≠ 0 ∨ ‖x‖ ≠ 0 → egauge 𝕜 (Metric.ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r
-- Init.Meta.Defs
/-- Finds the first `SourceInfo` from the back of `stx` or `SourceInfo.none`
if no `SourceInfo` can be found.
 -/
Lean.Syntax.getTailInfo : Lean.Syntax → Lean.SourceInfo
-- Std.Http.Data.Chunk
/-- Converts the trailer headers to a list of key-value pairs.
 -/
Std.Http.Trailer.toList : Std.Http.Trailer → List (Std.Http.Header.Name × Std.Http.Header.Value)
-- Mathlib.GroupTheory.OrderOfElement
exists_nsmul_eq_self_of_coprime : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, n.Coprime (addOrderOf x) → ∃ m, m • n • x = x
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationLeftAdjoint.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c c_1 : C),
  c = c_1 → CategoryTheory.evaluationLeftAdjoint D c = CategoryTheory.evaluationLeftAdjoint D c_1
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_one : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Nontrivial A],
  spectralRadius 𝕜 1 = 1
-- Lean.Declaration
Lean.QuotKind.ctor.sizeOf_spec : sizeOf Lean.QuotKind.ctor = 1
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra : {α : Type u} → [self : CompleteAtomicBooleanAlgebra α] → CompleteBooleanAlgebra α
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.mk : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} → (T.comp R ≅ L.comp B) → CategoryTheory.CatCommSq T L R B
-- Mathlib.Util.AliasIn
/-- Adds an alias of this declaration in a different namespace.
Example:
```
@[alias_in Foo.Bar] def A.B.C.d := ...
```
behaves like
```
alias A.Foo.Bar.d := A.B.C.d
```
You can see the name of the alias by mousing over the name argument of `alias_in`.

We replace the rightmost/innermost namespaces, but always leave the final part of the name intact.
By default, `alias_in` assumes that we want to replace the same number of namespaces from the
original name as given in the new namespace. You can override this by adding a number at the end
```
@[alias_in Foo.Bar 3] def A.B.C.d := ...
```
behaves like
```
alias Foo.Bar.d := A.B.C.d
```
 -/
aliasIn : Lean.ParserDescr
-- Lean.Server.Requests
Lean.Server.RequestHandlerCompleteness.partial.sizeOf_spec : ∀ (refreshMethod : String) (refreshIntervalMs : ℕ),
  sizeOf (Lean.Server.RequestHandlerCompleteness.partial refreshMethod refreshIntervalMs) =
    1 + sizeOf refreshMethod + sizeOf refreshIntervalMs
-- Mathlib.GroupTheory.GroupAction.Hom
instFunLikeAddActionHom : {M : Type u_2} →
  {N : Type u_3} →
    (φ : M → N) → (X : Type u_5) → [inst : VAdd M X] → (Y : Type u_6) → [inst_1 : VAdd N Y] → FunLike (X →ₑ[φ] Y) X Y
-- Mathlib.Data.Set.Pairwise.Chain
IsChain.pairwiseDisjoint_sUnion : ∀ {α : Type u_1} {β : Type u_2} {c : Set (Set α)},
  IsChain (fun x1 x2 => x1 ⊆ x2) c →
    ∀ [inst : PartialOrder β] [inst_1 : OrderBot β] (f : α → β),
      (⋃₀ c).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.norm_deriv_mulExpNegMulSq_le_one : ∀ {ε : ℝ}, 0 < ε → ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖ ≤ 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.empty_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C) (a : PEmpty.{w + 1}),
  (CategoryTheory.PreZeroHypercover.empty S).X a = a.elim
-- Mathlib.Topology.Bornology.BoundedOperation
instBoundedMulOfLipschitzMul : ∀ {R : Type u_1} [inst : PseudoMetricSpace R] [inst_1 : Monoid R] [LipschitzMul R], BoundedMul R
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.injectiveSeminorm_def : ∀ {ι : Type u_2} [inst : Fintype ι] {𝕜 : Type u_3} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type u_4}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)],
  PiTensorProduct.injectiveSeminorm =
    sSup
      {p |
        ∃ G x x_1,
          p =
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp
              (PiTensorProduct.toDualContinuousMultilinearMap G)}
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If a group acts properly then in particular it acts continuously.  -/
ProperVAdd.toContinuousVAdd : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperVAdd G X], ContinuousVAdd G X
-- Init.Data.SInt.Lemmas
Int8.ofNat_le_iff_le : ∀ {a b : ℕ}, a < 2 ^ 7 → b < 2 ^ 7 → (Int8.ofNat a ≤ Int8.ofNat b ↔ a ≤ b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- When 2 is a unit, `Y² = X³ + X` is an elliptic curve.
It is of j-invariant 1728 (see `WeierstrassCurve.ofJ1728_j`).  -/
WeierstrassCurve.instIsEllipticOfJ1728OfFactIsUnitOfNat : ∀ (R : Type u_1) [inst : CommRing R] [hu : Fact (IsUnit 2)], (WeierstrassCurve.ofJ1728 R).IsElliptic
-- Mathlib.Algebra.Group.Ext
AddRightCancelMonoid.toAddMonoid_injective : ∀ {M : Type u}, Function.Injective (@AddRightCancelMonoid.toAddMonoid M)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.canonical_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.RightHomologyData.canonical S).p = S.pOpcycles
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.derivWithin_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R),
  UniqueDiffWithinAt 𝕜 s x →
    derivWithin (fun x => (Polynomial.aeval x) q) s x = (Polynomial.aeval x) (Polynomial.derivative q)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.mem_sInf : ∀ {M : Type u_1} [inst : Mul M] {S : Set (Subsemigroup M)} {x : M}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Init.Data.SInt.Basic
/-- Non-strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `≤` operator.
 -/
Int8.le : Int8 → Int8 → Prop
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (x : ℝ),
  MeasureTheory.StronglyMeasurable fun a => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x
-- Init.Data.Char.Ordinal
/-- Unpacks `Fin Char.numCodePoints` bijectively to `Char` by shifting code points which are
greater than the surrogate code points by the number of surrogate code points.

The inverse of this function is called `Char.ordinal`.
 -/
Char.ofOrdinal : Fin Char.numCodePoints → Char
-- Mathlib.Algebra.Ring.Units
Units.coe_neg_one : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α], ↑(-1) = -1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.ite : ∀ {α : Type u_1} {op₁ op₂ : Stream'.Seq α → Stream'.Seq α},
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op₁ →
    Tactic.ComputeAsymptotics.Seq.FriendlyOperation op₂ →
      ∀ {P : Option α → Prop} [inst : DecidablePred P],
        Tactic.ComputeAsymptotics.Seq.FriendlyOperation fun s => if P s.head then op₁ s else op₂ s
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S)
  (A : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) (x : ι),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).inverse.obj A).obj x = A.A
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toContinuousMapLinearMap_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (R : Type u_3)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Y] [inst_4 : Module R Y] [inst_5 : ContinuousAdd Y]
  [inst_6 : ContinuousConstSMul R Y] (f : LocallyConstant X Y), (LocallyConstant.toContinuousMapLinearMap R) f = ↑f
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.epi_homologyMap_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n q : ℤ),
  q < n →
    CategoryTheory.Epi
      (HomologicalComplex.homologyMap (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n) q)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.mk.inj : ∀ {env : Lean.Environment} {cmdEnv? : Option Lean.Environment} {fileMap : Lean.FileMap} {mctx : Lean.MetavarContext}
  {options : Lean.Options} {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl} {ngen : Lean.NameGenerator}
  {env_1 : Lean.Environment} {cmdEnv?_1 : Option Lean.Environment} {fileMap_1 : Lean.FileMap}
  {mctx_1 : Lean.MetavarContext} {options_1 : Lean.Options} {currNamespace_1 : Lean.Name}
  {openDecls_1 : List Lean.OpenDecl} {ngen_1 : Lean.NameGenerator},
  { env := env, cmdEnv? := cmdEnv?, fileMap := fileMap, mctx := mctx, options := options,
        currNamespace := currNamespace, openDecls := openDecls, ngen := ngen } =
      { env := env_1, cmdEnv? := cmdEnv?_1, fileMap := fileMap_1, mctx := mctx_1, options := options_1,
        currNamespace := currNamespace_1, openDecls := openDecls_1, ngen := ngen_1 } →
    env = env_1 ∧
      cmdEnv? = cmdEnv?_1 ∧
        fileMap = fileMap_1 ∧
          mctx = mctx_1 ∧
            options = options_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ ngen = ngen_1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_exact._auto_3),
  (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Exact
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.integralBasis_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  (NumberField.integralBasis K) i =
    (algebraMap (NumberField.RingOfIntegers K) K) ((NumberField.RingOfIntegers.basis K) i)
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Formula.sat_iff_forall : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (p : α → Bool) (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f ↔
    ∀ c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f, Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c
-- Mathlib.Computability.TuringMachine.Config
/-- `prec f g` implements the `prec` (primitive recursion) operation of partial recursive
functions. `prec f g` evaluates as:

* `prec f g [] = [f []]`
* `prec f g (0 :: v) = [f v]`
* `prec f g (n+1 :: v) = [g (n :: prec f g (n :: v) :: v)]`

It is implemented as:

    G (a :: b :: IH :: v) = (b :: a+1 :: b-1 :: g (a :: IH :: v) :: v)
    F (0 :: f_v :: v) = (f_v :: v)
    F (n+1 :: f_v :: v) = (fix G (0 :: n :: f_v :: v)).tail.tail
    prec f g (a :: v) = [(F (a :: f v :: v)).head]

Because `fix` always evaluates its body at least once, we must special case the `0` case to avoid
calling `g` more times than necessary (which could be bad if `g` diverges). If the input is
`0 :: v`, then `F (0 :: f v :: v) = (f v :: v)` so we return `[f v]`. If the input is `n+1 :: v`,
we evaluate the function from the bottom up, with initial state `0 :: n :: f v :: v`. The first
number counts up, providing arguments for the applications to `g`, while the second number counts
down, providing the exit condition (this is the initial `b` in the return value of `G`, which is
stripped by `fix`). After the `fix` is complete, the final state is `n :: 0 :: res :: v` where
`res` is the desired result, and the rest reduces this to `[res]`.  -/
Turing.ToPartrec.Code.prec : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_pos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K), 0 < Height.mulHeight₁ x
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.continuous_arsinh : Continuous Real.arsinh
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabSimpTheorems : Lean.Syntax →
  Lean.Meta.Simp.Context →
    Lean.Meta.Simp.SimprocsArray →
      Bool → Lean.Elab.Tactic.TacticM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.differentiableAt_completedCosZeta : ∀ (a : UnitAddCircle) {s : ℂ}, s ≠ 0 → s ≠ 1 ∨ a ≠ 0 → DifferentiableAt ℂ (HurwitzZeta.completedCosZeta a) s
-- Std.Data.ExtDHashMap.Basic
/-- Computes the union of the given hash maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtDHashMap.union : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → Std.ExtDHashMap α β → Std.ExtDHashMap α β
-- Mathlib.Tactic.Widget.Calc
/-- indentation level of the calc block.  -/
CalcParams.indent : CalcParams → ℕ
-- Mathlib.Tactic.CongrExclamation
/-- If `closePost := true`, then try to close goals that remain after no more congruence
lemmas can be applied, using the same tactics as `closePre`. These tactics are applied
with the transparency level specified by `postTransparency`, which is currently default
transparency but in the future will become `.reducible` by default.  -/
Congr!.Config.closePost : Congr!.Config → Bool
-- Mathlib.Data.TypeVec
/-- Support for extending a `TypeVec` by one element.  -/
TypeVec.«term_:::_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- In a flatten, taking the first elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the flatten of the first `i` sublists.  -/
List.take_sum_flatten : ∀ {α : Type u_2} (L : List (List α)) (i : ℕ),
  List.take (List.take i (List.map List.length L)).sum L.flatten = (List.take i L).flatten
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Similar to `proveEq?`, but for heterogeneous equality.  -/
Lean.Meta.Grind.proveHEq? : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
/-- If `f` is monotone on `a..(b + c)` where `a ≤ b` and `0 ≤ c`, then
`fun x ↦ slope f x (x + c)` is interval integrable on `a..b`.  -/
MonotoneOn.intervalIntegrable_slope : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  MonotoneOn f (Set.Icc a (b + c)) →
    a ≤ b → 0 ≤ c → IntervalIntegrable (fun x => slope f x (x + c)) MeasureTheory.volume a b
-- Init.Data.Nat.Div.Basic
Nat.div.go.congr_simp : ∀ (y y_1 : ℕ) (e_y : y = y_1) (hy : 0 < y) (fuel fuel_1 : ℕ) (e_fuel : fuel = fuel_1) (x x_1 : ℕ) (e_x : x = x_1)
  (hfuel : x < fuel), Nat.div.go y hy fuel x hfuel = Nat.div.go y_1 ⋯ fuel_1 x_1 ⋯
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If `f` and `g` are equivariant maps, then so is `x ↦ (f x, g x)`.  -/
AddActionHom.prod : {M : Type u_1} →
  {N : Type u_2} →
    {α : Type u_3} →
      {γ : Type u_5} →
        {δ : Type u_6} →
          [inst : VAdd M α] →
            [inst_1 : VAdd N γ] → [inst_2 : VAdd N δ] → {σ : M → N} → (α →ₑ[σ] γ) → (α →ₑ[σ] δ) → α →ₑ[σ] γ × δ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.mk.inj : ∀ {view : Lean.Elab.Tactic.ElimTargetView} {expr : Lean.Expr} {arg? : Option Lean.Meta.GeneralizeArg}
  {view_1 : Lean.Elab.Tactic.ElimTargetView} {expr_1 : Lean.Expr} {arg?_1 : Option Lean.Meta.GeneralizeArg},
  { view := view, expr := expr, arg? := arg? } = { view := view_1, expr := expr_1, arg? := arg?_1 } →
    view = view_1 ∧ expr = expr_1 ∧ arg? = arg?_1
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_const : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [h : NeZero μ]
  (c : ENNReal), ⨍⁻ (_x : α), c ∂μ = c
-- Mathlib.Topology.UniformSpace.Separation
eq_of_forall_symmetric : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α] {x y : α},
  (∀ {V : Set (α × α)}, V ∈ uniformity α → SetRel.IsSymm V → (x, y) ∈ V) → x = y
-- Init.Data.Vector.Find
Vector.isSome_find? : ∀ {α : Type} {n : ℕ} {xs : Vector α n} {f : α → Bool}, (Vector.find? f xs).isSome = xs.any fun x => f x
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.exists_disjoint_powers_of_span_eq_top : ∀ {α : Type u} [inst : CommSemiring α] (s : Set α),
  Ideal.span s = ⊤ → ∀ (I : Ideal α), I ≠ ⊤ → ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ico_add_Icc_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α),
  Set.Ico a b + Set.Icc c d ⊆ Set.Ico (a + c) (b + d)
-- Mathlib.Data.Set.Countable
/-- **Alias** of `Set.countable_ofPred_nonempty_of_disjoint`.

---

If a family of disjoint sets is included in a countable set, then only countably many of
them are nonempty.  -/
Set.countable_setOf_nonempty_of_disjoint : ∀ {α : Type u} {β : Type v} {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) →
    ∀ {s : Set α}, (∀ (t : β), f t ⊆ s) → s.Countable → {t | (f t).Nonempty}.Countable
-- Mathlib.Order.Basic
eq_of_forall_lt_iff : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), c < a ↔ c < b) → a = b
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C}
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  [inst_6 : F.PreservesLeftHomologyOf S] [inst_7 : G.PreservesLeftHomologyOf S] [inst_8 : F.PreservesRightHomologyOf S]
  [inst_9 : G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F ⟶ G),
  (CategoryTheory.ShortComplex.HomologyMapData.natTransApp h τ).left =
    CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h.left τ
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D`
preserves limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesLimit_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.leftOp F],
  CategoryTheory.Limits.PreservesLimit K F.leftOp
-- Init.System.IOError
IO.Error.unsatisfiedConstraints.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.unsatisfiedConstraints osCode details = IO.Error.unsatisfiedConstraints osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.coe_punitProd : ∀ (α : Type u) [inst : UniformSpace α], ⇑(UniformEquiv.punitProd α) = Prod.snd
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.toSeminormedAddGroup : {E : Type u_5} → [SeminormedAddCommGroup E] → SeminormedAddGroup E
-- Lean.Elab.Arg
Lean.Elab.Term.instInhabitedArg : Inhabited Lean.Elab.Term.Arg
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2Computable.mk.sizeOf_spec : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : SizeOf αΓ] [inst_3 : SizeOf βΓ] (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ)
  (outputsFun :
    (a : α) →
      Turing.TM2Outputs toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a))))),
  sizeOf { toTM2ComputableAux := toTM2ComputableAux, outputsFun := outputsFun } = 1 + sizeOf toTM2ComputableAux
-- Init.Data.UInt.Lemmas
UInt16.one_mul : ∀ (a : UInt16), 1 * a = a
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.finMulAntidiag_one : ∀ {d : ℕ}, d.finMulAntidiag 1 = {fun x => 1}
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMon_obj_mon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (A : CategoryTheory.Mon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X)
      (F.map CategoryTheory.MonObj.mul)
-- Mathlib.Order.Minimal
maximal_le_iff : ∀ {α : Type u_2} {x y : α} [inst : PartialOrder α], Maximal (fun x => x ≤ y) x ↔ x = y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFractionRel.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ : W.LeftFraction X Y},
  CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂ → CategoryTheory.MorphismProperty.RightFractionRel z₁.op z₂.op
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
differentiableAt_iteratedDerivWithin_cexp : ∀ (n a : ℕ) {s : Set ℂ},
  IsOpen s →
    ∀ {r : ℂ},
      r ∈ s → DifferentiableAt ℂ (iteratedDerivWithin a (fun z => Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) s) r
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationProps.mk.inj : ∀ {expr expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx}, { expr := expr } = { expr := expr_1 } → expr = expr_1