mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant.eq_1 : ∀ {n : ℕ} (original_assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (original_assignments_size : original_assignments.size = n)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant original_assignments original_assignments_size
      units assignments assignments_size =
    ∀ (i : Fin n),
      have assignments_i := assignments[↑i];
      have original_assignments_i := original_assignments[↑i];
      (assignments_i = original_assignments_i ∧ ∀ (j : Fin units.size), ↑units[j].1 ≠ ↑i) ∨
        (∃ j b,
            ∃ (i_gt_zero : ↑i > 0),
              units[j] = (⟨↑i, ⋯⟩, b) ∧
                assignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b original_assignments_i ∧
                  ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b original_assignments_i = true ∧
                    ∀ (k : Fin units.size), k ≠ j → ↑units[k].1 ≠ ↑i) ∨
          ∃ j1 j2,
            ∃ (i_gt_zero : ↑i > 0),
              units[j1] = (⟨↑i, ⋯⟩, true) ∧
                units[j2] = (⟨↑i, ⋯⟩, false) ∧
                  assignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both ∧
                    original_assignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned ∧
                      ∀ (k : Fin units.size), k ≠ j1 → k ≠ j2 → ↑units[k].1 ≠ ↑i
-- Mathlib.Analysis.Complex.Isometry
rotation_apply : ∀ (a : Circle) (z : ℂ), (rotation a) z = ↑a * z
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.orderHom_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] (f : M →*o N) (a : M),
  (MulArchimedeanClass.orderHom f) (MulArchimedeanClass.mk a) = MulArchimedeanClass.mk (f a)
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The coefficient of `X ^ n` in `uniqueAlgEquiv R σ P` is the coefficient of the unique
monomial of degree `n` in `P`.  -/
MvPolynomial.coeff_uniqueAlgEquiv : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Unique σ] (P : MvPolynomial σ R) (n : ℕ),
  ((MvPolynomial.uniqueAlgEquiv R σ) P).coeff n = MvPolynomial.coeff (fun₀ | default => n) P
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.add` -/
MeromorphicAt.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (fun i => f i + g i) x
-- Init.Data.List.Nat.TakeDrop
List.drop_take_self : ∀ {i : ℕ} {α : Type u_1} {l : List α}, List.drop i (List.take i l) = []
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerRight_comp : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' X'' : C}
  (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C),
  CategoryTheory.eHomWhiskerRight V (CategoryTheory.CategoryStruct.comp f f') Y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f' Y) (CategoryTheory.eHomWhiskerRight V f Y)
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concat.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  (f : C(↑(Set.Icc a b), E)) (g : C(↑(Set.Icc b c), E)),
  f.concat g =
    if hb : f ⊤ = g ⊥ then
      let h := fun t => if t ≤ b then (ContinuousMap.IccExtendCM f) t else (ContinuousMap.IccExtendCM g) t;
      have this := ⋯;
      { toFun := fun t => h ↑t, continuous_toFun := ⋯ }
    else ContinuousMap.const (↑(Set.Icc a c)) (f ⊥)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Extension for the `positivity` tactic: distances are nonnegative.  -/
Mathlib.Meta.Positivity.evalDist : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.trans_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) {Z : C}
  (h' : CategoryTheory.Retract Y Z), (h.trans h').i = CategoryTheory.CategoryStruct.comp h.i h'.i
-- Mathlib.Data.Finset.Pairwise
List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint : ∀ {α : Type u_5} {ι : Type u_6} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
  {f : ι → α}, l.Nodup → ((↑l.toFinset).PairwiseDisjoint f ↔ List.Pairwise (Function.onFun Disjoint f) l)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_inj : ∀ {R : Type u_1} {A : Type u_2} [inst : Zero R] {x y : A}, ↑x = ↑y ↔ x = y
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_mul : ∀ {M : Type u_1} [inst : Monoid M] {a b : M} (ha : IsUnit a) (hb : IsUnit b), ⋯.unit = ha.unit * hb.unit
-- Mathlib.Data.List.Cycle
Cycle.coe_cons_eq_coe_append : ∀ {α : Type u_1} (l : List α) (a : α), ↑(a :: l) = ↑(l ++ [a])
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.ofPiNat_inj : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {x y : Metric.PiNatEmbed X Y f},
  x.ofPiNat = y.ofPiNat ↔ x = y
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- If `cond` is true, wraps the syntax produced by `d` in a type ascription.
 -/
Lean.PrettyPrinter.Delaborator.withTypeAscription : Lean.PrettyPrinter.Delaborator.Delab → optParam Bool true → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Hom.Basic
OrderIso.symm_trans_self : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.symm.trans e = OrderIso.refl β
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.reduce_flatten_replicate : ∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.IsReduced L →
    ∀ (n : ℕ),
      FreeGroup.reduce (List.replicate n L).flatten =
        if n = 0 then []
        else
          FreeGroup.reduceCyclically.conjugator L ++ (List.replicate n (FreeGroup.reduceCyclically L)).flatten ++
            FreeGroup.invRev (FreeGroup.reduceCyclically.conjugator L)
-- Mathlib.Data.NNReal.Defs
NNReal.mul_sup : ∀ (a b c : NNReal), a * max b c = max (a * b) (a * c)
-- Mathlib.Data.Finsupp.Defs
/-- `Finsupp α M`, denoted `α →₀ M`, is the type of functions `f : α → M` such that
`f x = 0` for all but finitely many `x`.  -/
Finsupp : Type u_9 → (M : Type u_10) → [Zero M] → Type (max u_10 u_9)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_triangle`.

---

The Hausdorff distance satisfies the triangle inequality.  -/
EMetric.hausdorffEdist_triangle : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t u : Set α},
  Metric.hausdorffEDist s u ≤ Metric.hausdorffEDist s t + Metric.hausdorffEDist t u
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Auxiliary definition for `final_functor`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄ : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] →
        (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) →
          {m₁ : J} →
            ((x : Subtype D.P) → ↑x ⟶ m₁) → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.brecOn.eq : ∀ {α : Type u} {β : α → Type v} {motive : Std.DTreeMap.Internal.Impl α β → Sort u_1}
  (t : Std.DTreeMap.Internal.Impl α β)
  (F_1 : (t : Std.DTreeMap.Internal.Impl α β) → Std.DTreeMap.Internal.Impl.below t → motive t),
  Std.DTreeMap.Internal.Impl.brecOn t F_1 = F_1 t (Std.DTreeMap.Internal.Impl.brecOn.go t F_1).2
-- Lean.Message
Lean.MessageData.brecOn_1.eq : ∀ {motive_1 : Lean.MessageData → Sort u} {motive_2 : Array Lean.MessageData → Sort u}
  {motive_3 : List Lean.MessageData → Sort u} (t : Array Lean.MessageData)
  (F_1 : (t : Lean.MessageData) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.MessageData) → Lean.MessageData.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.MessageData) → Lean.MessageData.below_2 t → motive_3 t),
  Lean.MessageData.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.MessageData.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Topology.Maps.Basic
IsOpenMap.preimage_frontier_subset_frontier_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {s : Set Y}, f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] [Inhabited α]
  {k : α} {f : Option (β k) → Option (β k)} {h : k ∈ m.alter k f}, (m.alter k f).getKey k h = k
-- Init.Data.Nat.Lemmas
Nat.mod_eq_sub : ∀ (x w : ℕ), x % w = x - w * (x / w)
-- Mathlib.Topology.PartitionOfUnity
/-- The collections of continuous functions underlying this bump covering  -/
BumpCovering.toFun : {ι : Type u_1} →
  {X : Type u_2} → [inst : TopologicalSpace X] → {s : optParam (Set X) Set.univ} → BumpCovering ι X s → ι → C(X, ℝ)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  ∅.size = 0
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The identity relating the isomorphisms between `X ⊗ (𝟙_ C ⊗ Y)`, `(X ⊗ 𝟙_ C) ⊗ Y` and `X ⊗ Y`
 -/
CategoryTheory.MonoidalCategory.triangle_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y) h
-- ProofWidgets.Cancellable
ProofWidgets.CheckRequestResponse.done.sizeOf_spec : ∀ (result : ProofWidgets.LazyEncodable Lean.Json), sizeOf (ProofWidgets.CheckRequestResponse.done result) = 1
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.linearEquivTuple_symm_apply : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] (x : Fin 2 → R),
  (QuadraticAlgebra.linearEquivTuple a b).symm x = { re := x 0, im := x 1 }
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Any morphism `k : S.X₂ ⟶ A` such that `S.f ≫ k = 0` descends
to a morphism `Q ⟶ A`  -/
CategoryTheory.ShortComplex.RightHomologyData.descQ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) → {A : C} → (k : S.X₂ ⟶ A) → CategoryTheory.CategoryStruct.comp S.f k = 0 → (h.Q ⟶ A)
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_one_iff : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : One F] [inst_2 : One β]
  [IsOneApply F α β] (f : F), ⇑f = 1 ↔ f = 1
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the monadic predicate `p` returns `ULift.up true` for
any element emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first match. The outputs of `it` are
examined in order of iteration.
 -/
Std.IterM.anyM : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → (β → m (ULift.{w, 0} Bool)) → Std.IterM m β → m (ULift.{w, 0} Bool)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_eq_one : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I : Ideal R}, ↑I = 1 ↔ I = 1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G]
  {ν : MeasureTheory.Measure α},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → (MeasureTheory.Measure.sum fun g => ν.restrict (g +ᵥ s)) = ν
-- Init.Data.Rat.Lemmas
Rat.num_mkRat : ∀ (n : ℤ) (d : ℕ), (mkRat n d).num = if d = 0 then 0 else n / ↑(d.gcd n.natAbs)
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_6 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (cf cg : Nat.Partrec.Code) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match cf.comp cg with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_6 cf cg
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_toAdditive_symm_apply : ∀ (R : Type u_3) (M : Type u_6) [inst : Semiring R] [inst_1 : Mul M] (x : AddMonoidAlgebra R (Additive M)),
  ((MonoidAlgebra.toAdditive R M).symm x).coeff = Finsupp.mapDomain (⇑Additive.toMul) x.coeff
-- Lean.Structure
/-- Conflicts that must come before `badParent`. The flag is whether it is a direct parent.  -/
Lean.StructureResolutionOrderConflict.conflicts : Lean.StructureResolutionOrderConflict → Array (Bool × Lean.Name)
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoalCore.mk.injEq : ∀ (hyps : Array Lean.Widget.InteractiveHypothesisBundle) (type : Lean.Widget.CodeWithInfos)
  (ctx : Lean.Server.WithRpcRef Lean.Elab.ContextInfo) (hyps_1 : Array Lean.Widget.InteractiveHypothesisBundle)
  (type_1 : Lean.Widget.CodeWithInfos) (ctx_1 : Lean.Server.WithRpcRef Lean.Elab.ContextInfo),
  ({ hyps := hyps, type := type, ctx := ctx } = { hyps := hyps_1, type := type_1, ctx := ctx_1 }) =
    (hyps = hyps_1 ∧ type = type_1 ∧ ctx = ctx_1)
-- Mathlib.Analysis.Distribution.Support
Filter.HasBasis.mem_dsupport : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} {ι : Sort u_11} {p : ι → Prop} {s : ι → Set α} {x : α},
  (nhds x).HasBasis p s → (x ∈ Distribution.dsupport f ↔ ∀ (i : ι), p i → ¬Distribution.IsVanishingOn f (s i))
-- Mathlib.Analysis.Normed.Operator.Basic
/-- Operator seminorm on the space of continuous (semi)linear maps, as `Seminorm`.

We use this seminorm to define a `SeminormedGroup` structure on `E →SL[σ] F`,
but we have to override the projection `UniformSpace`
so that it is definitionally equal to the one coming from the topologies on `E` and `F`.  -/
ContinuousLinearMap.seminorm : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      {F : Type u_5} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜₂ F] → {σ₁₂ : 𝕜 →+* 𝕜₂} → [RingHomIsometric σ₁₂] → Seminorm 𝕜₂ (E →SL[σ₁₂] F)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = true ↔ ∀ (a : α), m.contains a = false)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.isInvertible_zero_iff : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ContinuousLinearMap.IsInvertible 0 ↔ Subsingleton M ∧ Subsingleton M₂
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeriesEquivSubring_coe_apply : ∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
  ↑((LaurentSeries.powerSeriesEquivSubring K) f) = (HahnSeries.ofPowerSeries ℤ K) f
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfNat : ∀ (K : Type w) [inst : Field K], IsCyclotomicExtension {0} K (CyclotomicField 0 K)
-- Lean.Elab.PreDefinition.Main
/-- Letrec declarations produce terms of the form `(fun .. => ..) d` where `d` is a (partial) application of an auxiliary declaration for a letrec declaration.
This method beta-reduces them to make sure they can be eliminated by the well-founded recursion module.  -/
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.betaReduceLetRecApps : Array Lean.Elab.PreDefinition → Lean.MetaM (Array Lean.Elab.PreDefinition)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNNNorm_lsmul_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : NormSMulClass R E] [inst_7 : IsScalarTower 𝕜 R E] [Nontrivial E] {a : R},
  ‖(ContinuousLinearMap.lsmul 𝕜 R) a‖₊ = ‖a‖₊
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- The `CStarAlgebra.spectralOrder` on a C⋆-algebra is a `StarOrderedRing`.  -/
CStarAlgebra.spectralOrderedRing : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.noConfusionType : Sort v✝ → Std.Tactic.BVDecide.Gate → Std.Tactic.BVDecide.Gate → Sort v✝
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone containing a generating cone is also a generating cone.  -/
ConvexCone.IsGenerating.mono : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C₁ C₂ : ConvexCone R M}, C₁ ≤ C₂ → C₁.IsGenerating → C₂.IsGenerating
-- Init.Data.List.MinMax
List.min.eq_1 : ∀ {α : Type u} [inst : Min α] (a : α) (tail : List α) (x_2 : a :: tail ≠ []),
  (a :: tail).min x_2 = List.foldl min a tail
-- Init.WF
/-- A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a measure `h`, it expects
its higher order function argument `F` to invoke its argument only on values `y` that are smaller
than `x` with regard to `h`.

In contrast to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
when `h x` evaluates to a ground value)

 -/
WellFounded.Nat.fix : {α : Sort u} →
  {motive : α → Sort v} →
    (h : α → ℕ) →
      ((x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x) → (x : α) → motive x
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax right unity.  -/
CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) h =
    CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom h))
-- Aesop.Tree.Data
Aesop.RappUnsafe.mk : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Aesop.RappUnsafe
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β k}, (m.containsThenInsertIfNew k v).1 = m.contains k
-- Mathlib.Order.Monotone.Defs
antitone_iff_forall_lt : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f ↔ ∀ ⦃a b : α⦄, a < b → f b ≤ f a
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_coe_finset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s : Finset α),
  ∑ᶠ (i : α) (_ : i ∈ ↑s), f i = ∑ i ∈ s, f i
-- Mathlib.GroupTheory.FiniteAbelian.Basic
_private.Mathlib.GroupTheory.FiniteAbelian.Basic.0.directSumNeZeroMulHom.eq_1 : ∀ {ι : Type} [inst : DecidableEq ι] (p n : ι → ℕ),
  directSumNeZeroMulHom✝ p n = DirectSum.toAddMonoid fun i => DirectSum.of (fun i => ZMod (p i ^ n i)) ↑i
-- Init.Data.UInt.Lemmas
UInt16.toNat_lt : ∀ (n : UInt16), n.toNat < 2 ^ 16
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.mk : ∀ {K : Type u_1} [inst : Field K] [inst_1 : CharZero K] [to_isTotallyComplex : NumberField.IsTotallyComplex K]
  [is_quadratic : Algebra.IsQuadraticExtension (↥(NumberField.maximalRealSubfield K)) K], NumberField.IsCMField K
-- Mathlib.Order.Interval.Set.Image
_private.Mathlib.Order.Interval.Set.Image.0.Set.image_subtype_val_Ixx_Iix : ∀ {α : Type u_1} {p q r : α → α → Prop} {a b : α} (c : { x // p a x ∧ q x b }),
  (∀ {x : α}, r x ↑c → q x b) → Subtype.val '' {y | r ↑y ↑c} = {y | p a y ∧ r y ↑c}
-- Mathlib.Topology.Path
Path.reparam.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ γ_1 : Path x y),
  γ = γ_1 →
    ∀ (f f_1 : ↑unitInterval → ↑unitInterval) (e_f : f = f_1) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1),
      γ.reparam f hfcont hf₀ hf₁ = γ_1.reparam f_1 ⋯ ⋯ ⋯
-- Mathlib.Algebra.Divisibility.Basic
DecompositionMonoid.mk : ∀ {α : Type u_1} [inst : Semigroup α], (∀ (a : α), IsPrimal a) → DecompositionMonoid α
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- The identity pseudofunctor.  -/
CategoryTheory.Pseudofunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Pseudofunctor B B
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : 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} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₂'.RespectsIso] [L.IsLocalizedEquivalence] [R.IsLocalizedEquivalence]
  [R.functor.EssSurj] [T.IsLeftDerivabilityStructure] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
  [CategoryTheory.TwoSquare.GuitartExact iso.inv], B.IsLeftDerivabilityStructure
-- Mathlib.Data.Nat.Factorization.Basic
/-- A crude upper bound on `n.factorization p`  -/
Nat.factorization_lt : ∀ {n : ℕ} (p : ℕ), n ≠ 0 → n.factorization p < n