mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.instMonoICycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], CategoryTheory.Mono S.iCycles
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is both purely inseparable and separable, then `algebraMap F E` is surjective.  -/
IsPurelyInseparable.surjective_algebraMap_of_isSeparable : ∀ (F : Type u_1) (E : Type u_2) [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  [Algebra.IsSeparable F E], Function.Surjective ⇑(algebraMap F E)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A row partitioned matrix when transposed gives a column partitioned matrix with rows of the
initial matrix transposed to become columns.  -/
Matrix.transpose_fromRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R),
  (A₁.fromRows A₂).transpose = A₁.transpose.fromCols A₂.transpose
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.ιFunctorObj_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y) (j : κ.ord.ToType),
  CategoryTheory.SmallObject.ιFunctorObj I.homFamily
      (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).F.map (CategoryTheory.homOfLE ⋯))
      (CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso I κ f j).hom
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_eq_add : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F}, LinearMap.ofIsCompl hpq φ ψ = φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯
-- Init.Data.Vector.Lemmas
Vector.flatMap_push : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {x : α} {f : α → Vector β m},
  (xs.push x).flatMap f = Vector.cast ⋯ (xs.flatMap f ++ f x)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.Internal.foldRev.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → (a : α) → β a → δ) (init : δ) (b : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.Internal.foldRev f init b =
    (Std.DHashMap.Raw.Internal.foldRevM (fun x1 x2 x3 => pure (f x1 x2 x3)) init b).run
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.LocallyConstant.Basic
/-- If a locally constant function factors through an injection, then it factors through a locally
constant function.  -/
LocallyConstant.desc : {X : Type u_5} →
  {α : Type u_6} →
    {β : Type u_7} →
      [inst : TopologicalSpace X] →
        {g : α → β} → (f : X → α) → (h : LocallyConstant X β) → g ∘ f = ⇑h → Function.Injective g → LocallyConstant X α
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_subtype_le_map_subtype : ∀ {G : Type u_1} [inst : Group G] {G' : Subgroup G} {H K : Subgroup ↥G'},
  Subgroup.map G'.subtype H ≤ Subgroup.map G'.subtype K ↔ H ≤ K
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter.congr_simp : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (p p_1 : ι → Prop),
  p = p_1 →
    ∀ {inst_1 : DecidablePred p} [inst_2 : DecidablePred p_1] (x x_1 : Π₀ (i : ι), β i),
      x = x_1 → DFinsupp.filter p x = DFinsupp.filter p_1 x_1
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.add_snd : ∀ {q : ℕ} (x y : LucasLehmer.X q), (x + y).2 = x.2 + y.2
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.SetTheory.Ordinal.Veblen
_private.Mathlib.SetTheory.Ordinal.Veblen.0.Ordinal.cmp_veblenWith.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.lt)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.eq => h_1 ()
    | Ordering.lt => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Lean.Expr
Lean.Expr.updateForall! : Lean.Expr → Lean.BinderInfo → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} {f : A ⟶ B}
  [inst_1 : CategoryTheory.Mono f] (h : X ≤ CategoryTheory.Subobject.mk f),
  CategoryTheory.CategoryStruct.comp (X.ofLEMk f h) f = X.arrow
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A summable family can be reindexed by an embedding without changing its sum.  -/
HahnSeries.SummableFamily.embDomain : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      {β : Type u_6} →
        [inst : PartialOrder Γ] →
          [inst_1 : AddCommMonoid R] → HahnSeries.SummableFamily Γ R α → (α ↪ β) → HahnSeries.SummableFamily Γ R β
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_strictMono : StrictMono ENat.toENNReal
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Category.{v, max u v} (CategoryTheory.CommRingObjCat C)
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.tendstoInDistribution_of_isEmpty : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [inst : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} [inst_1 : MeasureTheory.IsProbabilityMeasure μ']
  {mE : MeasurableSpace E} {X : (i : ι) → Ω i → E} {Z : Ω' → E} {l : Filter ι} [inst_2 : TopologicalSpace E]
  [inst_3 : IsEmpty E], MeasureTheory.TendstoInDistribution X l Z μ μ'
-- Lean.Elab.Tactic.Basic
/-- Like `throwError`, but, if recovery is enabled, logs the error instead.
 -/
Lean.Elab.Tactic.throwOrLogError : Lean.MessageData → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_one : ∀ (R : Type u) [inst : Ring R], descPochhammer R 1 = Polynomial.X
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State.mk.inj : ∀ {varMap : Lean.Meta.KExprMap ℕ} {vars : Array Lean.Expr} {varMap_1 : Lean.Meta.KExprMap ℕ} {vars_1 : Array Lean.Expr},
  { varMap := varMap, vars := vars } = { varMap := varMap_1, vars := vars_1 } → varMap = varMap_1 ∧ vars = vars_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape : ∀ {C : Type u} {D : Type u'} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Category.{v', u'} D}
  {J : Type w} {inst_2 : LinearOrder J} {G : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G] (j : J),
  Order.IsSuccLimit j → CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
_private.Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite.0.SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding.match_1.splitter : (motive : Fin 3 → Sort u_1) → (x : Fin 3) → (Unit → motive 0) → (Unit → motive 1) → (Unit → motive 2) → motive x
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatCtorInfo : Std.ToFormat Lean.IR.CtorInfo
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.mem.decidable : {α : Type u_1} → [inst : LE α] → [inst_1 : DecidableLE α] → (x : α) → (t : Ordnode α) → Decidable (x ∈ t)
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_add_cpow_hasFPowerSeriesAt_zero : ∀ {a : ℂ}, HasFPowerSeriesAt (fun x => (1 + x) ^ a) (binomialSeries ℂ a) 0
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_1.eq_1 : ∀ (motive : Lean.Meta.Grind.SolverTerms × Lean.Meta.Grind.PendingSolverPropagationsData✝ → Sort u_1)
  (s : Lean.Meta.Grind.SolverTerms) (p : Lean.Meta.Grind.PendingSolverPropagationsData✝)
  (h_1 : (s : Lean.Meta.Grind.SolverTerms) → (p : Lean.Meta.Grind.PendingSolverPropagationsData✝) → motive (s, p)),
  (match (s, p) with
    | (s, p) => h_1 s p) =
    h_1 s p
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.closure_pi : ∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [Finite η] {s : (i : η) → Set (f i)},
  (∀ (i : η), 1 ∈ s i) →
    Subgroup.closure (Set.univ.pi fun i => s i) = Subgroup.pi Set.univ fun i => Subgroup.closure (s i)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.instNormedSpace : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] →
                  [inst_5 : Fintype ι] →
                    {𝕜' : Type u_1} →
                      [inst_6 : NormedField 𝕜'] →
                        [inst_7 : NormedSpace 𝕜' F] → [SMulCommClass 𝕜 𝕜' F] → NormedSpace 𝕜' (E [⋀^ι]→L[𝕜] F)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_impl_11 : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → NonScalar → Lean.PHashMap α (Task Dynamic)
-- Mathlib.Order.WithBot
WithBot.bot_lt_coe : ∀ {α : Type u_1} [inst : LT α] (a : α), ⊥ < ↑a
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- make an element of Lp from a function verifying `MemLp`  -/
MeasureTheory.MemLp.toLp : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] → (f : α → E) → MeasureTheory.MemLp f p μ → ↥(MeasureTheory.Lp E p μ)
-- Init.Prelude
instInhabitedBool.default : Bool
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filter_eq_self_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, Std.ExtDHashMap.filter f m = m ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = true
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the composition of the two given morphisms is zero  -/
CategoryTheory.ShortComplex.zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (self : CategoryTheory.ShortComplex C) {Z : C} (h : self.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp self.g h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.Set.Restrict
/-- If `f` and `g` are injective, then `extend f g j` is injective on the range of `f`.  -/
Function.Injective.extend_injOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {j : β → γ},
  Function.Injective f → Function.Injective g → Set.InjOn (Function.extend f g j) (Set.range f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- An integral model of an integral Weierstrass curve.  -/
WeierstrassCurve.integralModel : (R : Type u_1) →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] → (W : WeierstrassCurve K) → [hW : WeierstrassCurve.IsIntegral R W] → WeierstrassCurve R
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_5 : Std.Time.Weekday.friday.toOrdinal = 5
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.IsCut.mk : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering},
  (∀ {x y : α} [Std.TransCmp cmp], cmp x y ≠ Ordering.gt → cut x = Ordering.lt → cut y = Ordering.lt) →
    (∀ {x y : α} [Std.TransCmp cmp], cmp x y ≠ Ordering.gt → cut y = Ordering.gt → cut x = Ordering.gt) →
      RBTree.RBNode.IsCut cmp cut
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.ppow_one : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R}, f.ppow 1 = f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → Std.DHashMap.Const.get? (m₁.inter m₂) k = none
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffWithinAt_pi_space : ∀ {𝕜 : 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] {s : Set M} {x : M} {n : WithTop ℕ∞} {ι : Type u_16}
  [inst_6 : Fintype ι] {Fi : ι → Type u_17} [inst_7 : (i : ι) → NormedAddCommGroup (Fi i)]
  [inst_8 : (i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M → (i : ι) → Fi i},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ s x ↔
    ∀ (i : ι), ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (Fi i)) n (fun x => φ x i) s x
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Semigroup` across an `Equiv`  -/
Equiv.semigroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Semigroup β] → Semigroup α
-- Mathlib.Algebra.Quaternion
Quaternion.mul_coe_eq_smul : ∀ {R : Type u_3} [inst : CommRing R] (r : R) (a : Quaternion R), a * ↑r = r • a
-- Mathlib.Data.Int.Fib.Basic
Int.fib_dvd : ∀ (m n : ℤ), m ∣ n → Int.fib m ∣ Int.fib n
-- Init.Data.List.Monadic
List.mapM'.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β) (x : List α),
  List.mapM' f x =
    match x with
    | [] => pure []
    | a :: l => do
      let __do_lift ← f a
      let __do_lift_1 ← List.mapM' f l
      pure (__do_lift :: __do_lift_1)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (Opposite.unop x)).symm.op
-- Mathlib.Data.ZMod.Basic
/-- The inversion on `ZMod n`.
It is setup in such a way that `a * a⁻¹` is equal to `gcd a.val n`.
In particular, if `a` is coprime to `n`, and hence a unit, `a * a⁻¹ = 1`.  -/
ZMod.inv : (n : ℕ) → ZMod n → ZMod n
-- Aesop.Rule.Name
Aesop.instBEqPhaseName.beq : Aesop.PhaseName → Aesop.PhaseName → Bool
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.coe_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [inst_4 : PartialOrder 𝕜] (s : AbsConvexOpenSets 𝕜 E), IsOpen ↑s
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.instSplitEpiCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  CategoryTheory.SplitEpiCategory C
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.leftModule : {R : Type u_1} →
  {R'' : Type u_5} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring R''] →
        {M : Type u_7} →
          {N : Type u_8} →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R'' M] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → [SMulCommClass R R'' M] → Module R'' (TensorProduct R M N)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isNone_max?_eq_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.max?.isNone = t.isEmpty
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).size = if t.contains k = true then t.size else t.size + 1
-- Init.Prelude
/-- Macro scope used internally. It is not available for our frontend.  -/
Lean.reservedMacroScope : ℕ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t₁ ∪ t₂).getKey! k = t₂.getKeyD k (t₁.getKey! k)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] {k : α},
  m.contains k = true → m.get? k = some k
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instZeroQuotient : {R : Type u_1} → [inst : AddZeroClass R] → [inst_1 : Mul R] → (c : RingCon R) → Zero c.Quotient
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mk.injEq : ∀ {D : Type u_1} {Q : Type u_2} (left : Q → D) (right : Q) (left_1 : Q → D) (right_1 : Q),
  ({ left := left, right := right } = { left := left_1, right := right_1 }) = (left = left_1 ∧ right = right_1)
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.leastExt.eq_1 : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E],
  Field.Emb.Cardinal.leastExt F E =
    ⋯.fix fun i ih =>
      let s := Set.range fun j => (Field.Emb.Cardinal.wellOrderedBasis F E) (ih ↑j ⋯);
      ⋯.min {k | (Field.Emb.Cardinal.wellOrderedBasis F E) k ∉ IntermediateField.adjoin F s} ⋯
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →ₐ[R] B) (h : Continuous (↑↑f.toRingHom).toFun), ⇑{ toAlgHom := f, cont := h } = ⇑f
-- Mathlib.Order.OrderDual
OrderDual.ofDual_inj : ∀ {α : Type u_1} {a b : αᵒᵈ}, OrderDual.ofDual a = OrderDual.ofDual b ↔ a = b
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The variance of a real Gaussian distribution `gaussianReal μ v` is
its variance parameter `v`.  -/
ProbabilityTheory.variance_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, ProbabilityTheory.variance id (ProbabilityTheory.gaussianReal μ v) = ↑v
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁_supports' : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'} {K : Finset Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.Supports S q →
    Turing.PartrecToTM2.trStmts₁ q ∪ K ⊆ S →
      (K ⊆ S → Turing.PartrecToTM2.Supports K S) → Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.trStmts₁ q ∪ K) S
-- Std.Time.Date.Unit.Year
Std.Time.Year.instSubOffset : Sub Std.Time.Year.Offset
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof
-- Mathlib.Algebra.Category.Ring.Under.Property
/-- If `Q` is stable under equalizers, the inclusion from the subcategory of `Under R` defined
by `Q` creates equalizers.  -/
RingHom.HasEqualizers.createsLimitsWalkingParallelPair : {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} →
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) →
      (R : CommRingCat) →
        CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair
          (CategoryTheory.MorphismProperty.Under.forget
            (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ R)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.mul_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {a₁ a₂ b₁ b₂ : M},
  Associated a₁ b₁ → Associated a₂ b₂ → Associated (a₁ * a₂) (b₁ * b₂)
-- Mathlib.Algebra.CharP.Lemmas
add_pow_eq_mul_pow_add_pow_div_char : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
-- Mathlib.Algebra.Module.SpanRank
Submodule.generators_card : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  Cardinal.mk ↑p.generators = p.spanRank
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_inj : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] {p q : ℚ≥0}, ↑p = ↑q ↔ p = q
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH2_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.shortComplexH2 A).g = groupHomology.d₂₁ A
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_degree_eq_two : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R} {x : R}, f.degree = 2 → Polynomial.eval x f = 0 → f.Splits
-- Mathlib.Algebra.GroupWithZero.Defs
CancelCommMonoidWithZero.toIsLeftCancelMulZero : ∀ {M₀ : Type u_2} (self : CancelCommMonoidWithZero M₀), IsLeftCancelMulZero M₀
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.insertManyIfNewUnit : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.TreeMap.Raw α Unit cmp}, t.WF → (t.insertManyIfNewUnit l).WF
-- Mathlib.Analysis.Normed.Group.Uniform
antilipschitzWith_inv_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E},
  AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.single_mul_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MulZeroClass (α i)] [inst_1 : DecidableEq ι] {i : ι}
  {f : (i : ι) → α i} (a : α i), Pi.single i (f i * a) = f * Pi.single i a
-- Mathlib.Logic.Basic
Fact.mk : ∀ {p : Prop}, p → Fact p
-- Mathlib.Order.Height
Set.chainHeight_coe_univ : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), (Set.univ.chainHeight fun x1 x2 => r ↑x1 ↑x2) = s.chainHeight r
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_le_iff_le_embedding : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R} {g : (MonoidWithZeroHom.ofClass v).ValueGroup₀},
  v.restrict x ≤ g ↔ v x ≤ MonoidWithZeroHom.ValueGroup₀.embedding g
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_succ_last : ∀ {w : ℕ} (x : BitVec (w + 1)), x.getLsbD w = decide (2 ^ w ≤ x.toNat)