mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.add b →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_3 a b
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.mem_finsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) {i : ι},
  i ∈ ρ.finsupport x₀ ↔ i ∈ Function.support fun i => (ρ i) x₀
-- Init.Sym.Lemmas
Lean.Sym.decide_isFalse_congr : ∀ (p p' : Prop), p = p' → ∀ {inst : Decidable p} {hnp : ¬p'}, decide p = false
-- Init.Data.UInt.Lemmas
UInt64.ofFin_bitVecToFin : ∀ (n : BitVec 64), UInt64.ofFin n.toFin = { toBitVec := n }
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ext : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f g : NormedAddGroupHom V₁ V₂}, (∀ (x : V₁), f x = g x) → f = g
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Icc_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isLocalization_stalk : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U),
  IsLocalization.AtPrime (↑(X.presheaf.stalk ↑x)) (hU.primeIdealOf x).asIdeal
-- Lean.Expr
Lean.Literal.natVal.sizeOf_spec : ∀ (val : ℕ), sizeOf (Lean.Literal.natVal val) = 1 + sizeOf val
-- Mathlib.GroupTheory.Index
AddSubgroup.fintypeOfIndexNeZero.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (hH : H.index ≠ 0),
  AddSubgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)
-- Mathlib.Data.List.Lookmap
List.lookmap_congr : ∀ {α : Type u_1} {f g : α → Option α} {l : List α}, (∀ a ∈ l, f a = g a) → List.lookmap f l = List.lookmap g l
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalReduce : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.Int.Init
Int.inductionOn'.pos.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n : ℕ),
  x = n.succ →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withExistingLocalDeclsImp : {α : Type} → List Lean.LocalDecl → Lean.MetaM α → Lean.MetaM α
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.mk : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            (c : CategoryTheory.Limits.Cone D) →
              CategoryTheory.Limits.IsLimit c →
                (i : I) →
                  (a : D.obj i ⟶ X) →
                    t.app i = CategoryTheory.CategoryStruct.comp a f →
                      (b : D.obj i ⟶ X) →
                        t.app i = CategoryTheory.CategoryStruct.comp b f →
                          CategoryTheory.CategoryStruct.comp (c.π.app i) a =
                              CategoryTheory.CategoryStruct.comp (c.π.app i) b →
                            (𝒰S : S.OpenCover) →
                              [h𝒰S : ∀ (i : 𝒰S.I₀), AlgebraicGeometry.IsAffine (𝒰S.X i)] →
                                (𝒰X :
                                    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) →
                                      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).X i).OpenCover) →
                                  [h𝒰X :
                                      ∀ (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀)
                                        (j : (𝒰X i).I₀), AlgebraicGeometry.IsAffine ((𝒰X i).X j)] →
                                    AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f
-- Init.Data.Array.Lemmas
Array.ne_of_not_mem_push : ∀ {α : Type u_1} {a b : α} {xs : Array α}, a ∉ xs.push b → a ≠ b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ γ_1 : CochainComplex.HomComplex.Cochain K L n),
  γ = γ_1 →
    ∀ (a n' : ℤ) (hn' : n' + a = n) (T : CochainComplex.HomComplex.Triplet n'),
      γ.rightShift a n' hn' T = γ_1.rightShift a n' hn' T
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).p =
    CategoryTheory.CategoryStruct.comp φ.τ₂ h.p
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.splitMonoBiprodComparison'_retraction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [inst_6 : F.PreservesZeroMorphisms],
  (F.splitMonoBiprodComparison' X Y).retraction = F.biprodComparison X Y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldr_eq_foldr_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {f : α → β → δ → δ} {init : δ},
  Std.DTreeMap.foldr f init t = Array.foldr (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Const.toArray t)
-- Mathlib.GroupTheory.CoprodI
/-- Construct a new `Word` without any reduction. The underlying list of
`cons m w _ _` is `⟨_, m⟩::w`  -/
Monoid.CoprodI.Word.cons : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {i : ι} → (m : M i) → (w : Monoid.CoprodI.Word M) → w.fstIdx ≠ some i → m ≠ 1 → Monoid.CoprodI.Word M
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftPath_const : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {e : E} {x : X} (hpe : x = p e),
  cov.liftPath (ContinuousMap.const (↑unitInterval) x) e hpe = ContinuousMap.const (↑unitInterval) e
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [inst : Add α] [inst_1 : Sub β],
  Function.Periodic f c → Function.Periodic g c → Function.Periodic (f - g) c
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
/-- The norm of the restricted sum is less than the full sum of the norms.  -/
EisensteinSeries.norm_le_tsum_norm : ∀ (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ),
  3 ≤ k → ∀ (z : UpperHalfPlane), ‖eisensteinSeries a k z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖EisensteinSeries.eisSummand k x z‖
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- The ring homomorphism from `A` to `𝒜 0` sending every `a : A` to `a₀`.  -/
GradedRing.projZeroRingHom' : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddCommMonoid ι] →
            [inst_3 : PartialOrder ι] →
              [CanonicallyOrderedAdd ι] →
                [inst_5 : SetLike σ A] →
                  [inst_6 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [inst_7 : GradedRing 𝒜] → A →+* ↥(𝒜 0)
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeftLI_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F), ContinuousAlternatingMap.curryLeftLI f = f.curryLeft
-- Mathlib.Util.Superscript
/-- The core function for super/subscript parsing. It consists of three stages:

1. Parse a run of superscripted characters, skipping whitespace and stopping when we hit a
   non-superscript character.
2. Un-superscript the text and pass the body to the inner parser (usually `term`).
3. Take the resulting `Syntax` object and align all the positions to fit back into the original
   text (which as a side effect also rewrites all the substrings to be in subscript text).

If `many` is false, then whitespace (and comments) are not allowed inside the superscript.
 -/
Mathlib.Tactic.Superscript.scriptFnNoAntiquot : Mathlib.Tactic.Superscript.Mapping → String → Lean.Parser.ParserFn → optParam Bool true → Lean.Parser.ParserFn
-- Batteries.Data.Vector.Lemmas
Vector.tail_eq_of_zero : ∀ {α : Type u_1} {v : Vector α 0}, v.tail = #v[]
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  Measurable f →
    (∀ᵐ (x : α) ∂μ, f x < ⊤) → ∀ (g : α → ENNReal), ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {h : k ∈ Std.ExtHashMap.filterMap f m},
  (Std.ExtHashMap.filterMap f m)[k] = (f (m.getKey k ⋯) m[k]).get ⋯
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- A non-unital subring is a non-unital `ℤ`-subalgebra.  -/
nonUnitalSubalgebraOfNonUnitalSubring : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → NonUnitalSubring R → NonUnitalSubalgebra ℤ R
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux.match_1.splitter : (motive : Option Char → Sort u_1) →
  (x : Option Char) → (Unit → motive none) → ((cₙ : Char) → motive (some cₙ)) → motive x
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_eq_div : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (r : R) (s : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk r s = (ValuativeRel.valuation R) r / (ValuativeRel.valuation R) ↑s
-- Mathlib.RingTheory.Perfection
PreTilt.valAux_one : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O → ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p], PreTilt.valAux K v O p 1 = 1
-- Mathlib.Order.Sublattice
Sublattice.isSublattice : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), IsSublattice ↑L
-- Mathlib.Algebra.Group.Action.Defs
SemigroupAction.mk : {α : Type u_9} →
  {β : Type u_10} →
    [inst : Semigroup α] → [toSMul : SMul α β] → (∀ (x y : α) (b : β), (x * y) • b = x • y • b) → SemigroupAction α β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).isEmpty = t.isEmpty
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.coe_singletonAddMonoidHom : ∀ {α : Type u_2} [inst : AddZeroClass α], ⇑Set.singletonAddMonoidHom = singleton
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_9 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.shiftRight rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_9 w n lhs rhs
-- Mathlib.Data.Set.Lattice
Set.biUnion_singleton : ∀ {α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β), ⋃ x ∈ {a}, s x = s a
-- Mathlib.Control.ULiftable
ULiftable.refl : (f : Type u₀ → Type u₁) → [inst : Functor f] → [LawfulFunctor f] → ULiftable f f
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMono.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularMono f] (k : W ⟶ Y)
  (h :
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.left f) =
      CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.right f))
  {Z : C} (h_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularMono.lift f k h)
      (CategoryTheory.CategoryStruct.comp f h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Order.Basic
GT.gt.lt : ∀ {α : Type u_2} [inst : LT α] {a b : α}, a > b → b < a
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgEquiv.lift_trdeg_eq : ∀ {R : Type u_2} {A : Type v} {A' : Type v'} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing A']
  [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (e : A ≃ₐ[R] A'),
  Cardinal.lift.{v', v} (Algebra.trdeg R A) = Cardinal.lift.{v, v'} (Algebra.trdeg R A')
-- Init.Core
instDecidableEqSum.decEq : {α : Type u_1} → {β : Type u_2} → [DecidableEq α] → [DecidableEq β] → (x x_1 : α ⊕ β) → Decidable (x = x_1)
-- Init.Data.Vector.Lemmas
Vector.map_inj_left : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector α n} {f g : α → β},
  Vector.map f xs = Vector.map g xs ↔ ∀ a ∈ xs, f a = g a
-- Mathlib.Topology.UniformSpace.Equicontinuity
EquicontinuousWithinAt.eq_1 : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α)
  (S : Set X) (x₀ : X),
  EquicontinuousWithinAt F S x₀ = ∀ U ∈ uniformity α, ∀ᶠ (x : X) in nhdsWithin x₀ S, ∀ (i : ι), (F i x₀, F i x) ∈ U
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k}, (compare (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey! t.minKey!).isLE = true
-- Mathlib.Order.LiminfLimsup
/-- In a complete lattice, the liminf of a function is the infimum over sets `s` in the filter
of the supremum of the function over `s`  -/
Filter.liminf_eq_iSup_iInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
  Filter.liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_seq : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {n : ℕ} {r : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow (basis_hd :: basis_tl) n r).seq =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl n r
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` moves `(j • h) +ᵥ x` iff `g` moves `x`.  -/
AddAction.vadd_zsmul_movedBy_eq_of_addCommute : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g h : G},
  AddCommute g h → ∀ (j : ℤ), j • h +ᵥ (AddAction.fixedBy α g)ᶜ = (AddAction.fixedBy α g)ᶜ
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.add : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α}, IsLocalMax f a → IsLocalMax g a → IsLocalMax (fun x => f x + g x) a
-- Init.Data.List.Lemmas
List.filterMap_append : ∀ {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → Option β},
  List.filterMap f (l ++ l') = List.filterMap f l ++ List.filterMap f l'
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k fallback : α} {v : β}, (m.insert k v).getKeyD k fallback = k
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- In a vector space `ι → K`, a linear independent family indexed by `ι` is a basis.  -/
basisOfPiSpaceOfLinearIndependent : {K : Type u} →
  [inst : DivisionRing K] →
    {ι : Type u_1} →
      [Fintype ι] → [Decidable (Nonempty ι)] → {b : ι → ι → K} → LinearIndependent K b → Module.Basis ι K (ι → K)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A)),
  (HomotopicalAlgebra.Cylinder.ofFactorizationData h).i₀ =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h.i
-- Mathlib.Data.PNat.Prime
Nat.Primes.coe_pnat_inj : ∀ (p q : Nat.Primes), ↑p = ↑q ↔ p = q
-- Init.Data.BitVec.Lemmas
BitVec.sdivOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w),
  x.sdivOverflow y = (decide (2 ^ (w - 1) ≤ x.toInt / y.toInt) || decide (x.toInt / y.toInt < -2 ^ (w - 1)))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Non commutative semirings.
 -/
Lean.Meta.Grind.Arith.CommRing.State.ncSemirings : Lean.Meta.Grind.Arith.CommRing.State → Array Lean.Meta.Grind.Arith.CommRing.Semiring
-- Mathlib.SetTheory.Lists
Lists.Equiv.symm : ∀ {α : Type u_1} {l₁ l₂ : Lists α}, l₁.Equiv l₂ → l₂.Equiv l₁
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E} {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f s x →
      DifferentiableWithinAt 𝕜 g s x →
        fderivWithin 𝕜 (fun y => f y - g y) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.coe_trans : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {L : Type u_3} [inst_4 : Mul L] [inst_5 : TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L),
  ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_reindex : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E]
  [inst_4 : Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i => s (e.symm i)) E)
  (x : PiTensorProduct R fun i => s i),
  (PiTensorProduct.lift φ) ((PiTensorProduct.reindex R s e) x) =
    (PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e).symm φ)) x
-- Aesop.Forward.State
/-- Add a hypothesis or pattern substitution to the rule state. The
hypothesis's type does not necessarily need to match the given premise. If it
does not, this is detected by `update` and the hyp is not added.  -/
Aesop.RuleState.enqueueRawHyp : Aesop.RawHyp → Aesop.PremiseIndex → Aesop.RuleState → Aesop.RuleState
-- Lean.Parser.Basic
Lean.Parser.ParserState.keepNewError : Lean.Parser.ParserState → ℕ → Lean.Parser.ParserState
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- All functions from a well-formed basis tend to `atTop`.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.tendsto_atTop : ∀ {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    ∀ {f : ℝ → ℝ}, f ∈ basis → Filter.Tendsto f Filter.atTop Filter.atTop
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
SSet.Subcomplex.Pairing.instIsRegularOp : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], P.op.IsRegular
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.pow_add_congr : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a r : α) (k k₁ k₂ : ℕ), k = k₁ + k₂ → a ^ k₁ * a ^ k₂ = r → a ^ k = r
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_add_self : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E},
  Bornology.IsVonNBounded 𝕜 (s + s) ↔ Bornology.IsVonNBounded 𝕜 s
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} [inst_1 : SizeOf C]
  [inst_2 : ⦃Y : C⦄ → (a : Y ⟶ X) → SizeOf (S a)]
  [inst_3 : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (a : S f) → ⦃Y_1 : C⦄ → (a_1 : Y_1 ⟶ Y) → SizeOf (R a a_1)] (Y : C) (g : Z ⟶ Y)
  (f : Y ⟶ X) (hf : S f) (hg : R hf g) (fac : CategoryTheory.CategoryStruct.comp g f = h),
  sizeOf { Y := Y, g := g, f := f, hf := hf, hg := hg, fac := fac } =
    1 + sizeOf Y + sizeOf g + sizeOf f + sizeOf hf + sizeOf hg + sizeOf fac