mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.single : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_3}
  [inst_2 : (i : ι) → PseudoEMetricSpace (E i)] [inst_3 : (i : ι) → Zero (E i)] (i : ι), Isometry (Pi.single i)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} {μ : MeasureTheory.Measure α} [ClosedIciTopology α], MeasureTheory.NullMeasurableSet (Set.Ico a b) μ
-- Lean.Meta.Closure
Lean.Meta.Closure.State.newLocalDeclsForMVars : Lean.Meta.Closure.State → Array Lean.LocalDecl
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log.eq_1 : ∀ {M : Type u_4} [inst : AddMonoid M] (x : WithZero (Multiplicative M)),
  x.log = WithZero.recZeroCoe 0 (⇑Multiplicative.toAdd) x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_addY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Affine R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (x₁ y₁ x₂ ℓ : A),
  (W'.baseChange B).addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((W'.baseChange A).addY x₁ x₂ y₁ ℓ)
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mk.inj : ∀ {Map Set : Type} {mkState : Unit → Map × Set} {mapFind? : Map → ShareCommon.Object → Option ShareCommon.Object}
  {mapInsert : Map → ShareCommon.Object → ShareCommon.Object → Map}
  {setFind? : Set → ShareCommon.Object → Option ShareCommon.Object} {setInsert : Set → ShareCommon.Object → Set}
  {Map_1 Set_1 : Type} {mkState_1 : Unit → Map_1 × Set_1}
  {mapFind?_1 : Map_1 → ShareCommon.Object → Option ShareCommon.Object}
  {mapInsert_1 : Map_1 → ShareCommon.Object → ShareCommon.Object → Map_1}
  {setFind?_1 : Set_1 → ShareCommon.Object → Option ShareCommon.Object}
  {setInsert_1 : Set_1 → ShareCommon.Object → Set_1},
  { Map := Map, Set := Set, mkState := mkState, mapFind? := mapFind?, mapInsert := mapInsert, setFind? := setFind?,
        setInsert := setInsert } =
      { Map := Map_1, Set := Set_1, mkState := mkState_1, mapFind? := mapFind?_1, mapInsert := mapInsert_1,
        setFind? := setFind?_1, setInsert := setInsert_1 } →
    Map = Map_1 ∧
      Set = Set_1 ∧
        mkState ≍ mkState_1 ∧
          mapFind? ≍ mapFind?_1 ∧ mapInsert ≍ mapInsert_1 ∧ setFind? ≍ setFind?_1 ∧ setInsert ≍ setInsert_1
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.instUniformSpace : {α : Type u} → [inst : UniformSpace α] → UniformSpace (SeparationQuotient α)
-- Mathlib.Order.Category.LinOrd
LinOrd.coe_comp : ∀ {X Y Z : LinOrd} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instZeroHom : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] → (M N : CategoryTheory.AddMon D) → Zero (M ⟶ N)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.σ.eq_1 : ∀ {n : ℕ} (i : Fin (n + 1)), SimplexCategory.σ i = SimplexCategory.mkHom i.predAboveOrderHom
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_comp_rev : ∀ {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α), Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.apply_union_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {s₁ s₂ : Set Ω},
  μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.instIsClosedUnderIsomorphismsHomologicalKernel : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A),
  F.homologicalKernel.IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Opposites
/-- The opposite category.  -/
CategoryTheory.Category.opposite : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Category.{v₁, u₁} Cᵒᵖ
-- Mathlib.Data.Int.Sqrt
Int.sqrt.eq_1 : ∀ (z : ℤ), Int.sqrt z = ↑z.toNat.sqrt
-- Init.Data.Rat.Lemmas
Rat.num_eq_zero : ∀ {q : ℚ}, q.num = 0 ↔ q = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : SizeOf C] (left : S.LeftHomologyData) (right : S.RightHomologyData)
  (iso : left.H ≅ right.H)
  (comm :
    autoParam
      (CategoryTheory.CategoryStruct.comp left.π (CategoryTheory.CategoryStruct.comp iso.hom right.ι) =
        CategoryTheory.CategoryStruct.comp left.i right.p)
      CategoryTheory.ShortComplex.HomologyData.comm._autoParam),
  sizeOf { left := left, right := right, iso := iso, comm := comm } =
    1 + sizeOf left + sizeOf right + sizeOf iso + sizeOf comm
-- Mathlib.Topology.NhdsWithin
nhdsWithin_eq_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t u : Set α},
  a ∈ s → IsOpen s → t ∩ s = u ∩ s → nhdsWithin a t = nhdsWithin a u
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.sub b →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_8 a b
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hom_ofHom : ∀ {R S : Type u} [inst : Group R] [inst_1 : Group S] (f : R →* S), GrpCat.Hom.hom (GrpCat.ofHom f) = f
-- Mathlib.Order.MinMax
min_eq_left_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, min a b = a ↔ a ≤ b
-- Mathlib.Data.Finset.Filter
Finset.filter_congr_decidable : ∀ {α : Type u_1} (s : Finset α) (p : α → Prop) (h : DecidablePred p) [inst : DecidablePred p],
  Finset.filter p s = Finset.filter p s
-- Mathlib.Topology.Algebra.Monoid.Defs
continuous_const_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] (m : M),
  Continuous fun x => m * x
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- `Matroid.IsRkFinite M X` means that every basis of `X` in `M` is finite.  -/
Matroid.IsRkFinite : {α : Type u_1} → Matroid α → Set α → Prop
-- Mathlib.Geometry.Manifold.ChartedSpace
mem_chart_target : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), ↑(chartAt H x) x ∈ (chartAt H x).target
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Two finite Borel measures are equal if the integrals of all non-negative bounded continuous
functions with respect to both agree.  -/
MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω]
  {μ ν : MeasureTheory.FiniteMeasure Ω},
  (∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν) → μ = ν
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.hinjSuffix : String
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin (n + 1 + 1) → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1 + 1)
  (h_1 : (isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩) (h_2 : (i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨i.succ, hi⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_2 i hi
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccLimit_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α), ¬Order.IsSuccLimit (Order.succ a)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapAddMon_functor : ∀ {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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapAddMon.functor = e.functor.mapAddMon
-- Mathlib.ModelTheory.Substructures
/-- A substructure `S` includes `closure L s` if and only if it includes `s`.  -/
FirstOrder.Language.Substructure.closure_le : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M},
  (FirstOrder.Language.Substructure.closure L).toFun s ≤ S ↔ s ⊆ ↑S
-- Init.Data.UInt.Lemmas
UInt8.zero_mul : ∀ {a : UInt8}, 0 * a = 0
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
      (AlgebraicGeometry.Scheme.Hom.fromNormalization f) =
    f
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangleMorphism₁.hom₃ = h.m₁
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Conversion of normal form does not affect orders.
 -/
meromorphicOrderAt_toMeromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U → x ∈ U → meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.point_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C))
      (CategoryTheory.SimplicialObject.const C)),
  CategoryTheory.SimplicialObject.Augmented.point.obj X = X.right
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.iterationObjSuccIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  (κ : Cardinal.{w}) [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [inst_7 : Fact κ.IsRegular] (j : κ.ord.ToType),
  CategoryTheory.OrthogonalReflection.iterationObjSuccIso W Z κ j =
    CategoryTheory.OrthogonalReflection.iterationObjSuccIso W Z κ j
-- Mathlib.Analysis.Convex.Function
convexOn_of_convex_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β}, Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2} → ConvexOn 𝕜 s f
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.GroupTheory.GroupAction.Basic
/-- If the stabilizer of `a` is `S`, then the stabilizer of `g +ᵥ a` is `g+S-g`.  -/
AddAction.stabilizer_vadd_eq_stabilizer_map_addConj : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
  AddAction.stabilizer G (g +ᵥ a) =
    AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.addConj g)) (AddAction.stabilizer G a)
-- Init.Data.SInt.Bitwise
Int8.and_not_self : ∀ {a : Int8}, a &&& ~~~a = 0
-- Init.Data.SInt.Lemmas
Int64.toBitVec_toUInt64 : ∀ (x : Int64), x.toUInt64.toBitVec = x.toBitVec
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (P.map f.op) (Φ.toPresheafFiber X x P) =
    Φ.toPresheafFiber Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x) P
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.leftOpWhiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor E C} (α : F ⟶ G),
  CategoryTheory.NatTrans.leftOp (H.whiskerLeft α) =
    CategoryTheory.CategoryStruct.comp (H.leftOpComp G).hom
      (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.leftOp α)) (H.leftOpComp F).inv)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.support_subset_vars_of_mem_support : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ ℕ},
  s ∈ p.support → s.support ⊆ p.vars
-- Init.Data.String.Subslice
String.Slice.Subslice.str_toSlice : ∀ {s : String.Slice} {sl : s.Subslice}, sl.toSlice.str = s.str
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The **correspondence theorem**, or lattice theorem,
or fourth isomorphism theorem for multiplicative groups  -/
QuotientGroup.comapMk'OrderIso : {G : Type u} → [inst : Group G] → (N : Subgroup G) → [hn : N.Normal] → Subgroup (G ⧸ N) ≃o { H // N ≤ H }
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_3 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.both with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_3 ()
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
LiouvilleNumber.partialSum_succ : ∀ (m : ℝ) (n : ℕ), LiouvilleNumber.partialSum m (n + 1) = LiouvilleNumber.partialSum m n + 1 / m ^ (n + 1).factorial
-- Init.Data.SInt.Basic
/-- Decides whether one 8-bit signed integer is strictly less than another. Usually accessed via the
`DecidableLT Int64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int64) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : Int64) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : Int64) < 7) by decide`
 -/
Int64.decLt : (a b : Int64) → Decidable (a < b)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpTriggerKind : Lean.ToJson Lean.Lsp.SignatureHelpTriggerKind
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s →
    ∀ {t : Set α}, MeasurableSet t → (μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addRight_toEquiv : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a : α),
  (OrderIso.addRight a).toEquiv = Equiv.addRight a
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_le_piecewise' : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g f' g' : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)],
  (∀ x ∈ s, f x ≤ f' x) → (∀ x ∉ s, g x ≤ g' x) → s.piecewise f g ≤ s.piecewise f' g'
-- Mathlib.NumberTheory.LucasLehmer
/-- `q` is defined as the minimum factor of `mersenne p`, bundled as an `ℕ+`.  -/
LucasLehmer.q : ℕ → ℕ+
-- Aesop.Forward.PremiseIndex
Aesop.instHashablePremiseIndex.hash : Aesop.PremiseIndex → UInt64
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[s] f x f' → MDiffAt[s] f x
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- `LinearMap.normDet` can be calculated with any pair of orthonormal basis if the domain and the
codomain have equal dimension.
 -/
LinearMap.normDet_eq_norm_det_toMatrix : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {ι : Type u_5} [inst_6 : Fintype ι] [inst_7 : DecidableEq ι] (f : U →ₗ[𝕜] V)
  (bu : OrthonormalBasis ι 𝕜 U) (bv : OrthonormalBasis ι 𝕜 V),
  f.normDet = ‖((LinearMap.toMatrix bu.toBasis bv.toBasis) f).det‖
-- Init.PropLemmas
forall₅_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5}
  {p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop},
  (∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e) →
    ((∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e) ↔
      ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), q a b c d e)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instFullFunctor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], (CategoryTheory.Preadditive.RightFreyd.functor V).Full
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.div_lt_div_iff_mul_lt_mul : ∀ {a b c d : ℤ}, 0 < b → 0 < d → (↑a / ↑b < ↑c / ↑d ↔ a * d < c * b)
-- Mathlib.Algebra.Module.Basic
Set.indicator_smul_const_apply : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (s : Set α)
  (r : α → R) (m : M) (a : α), s.indicator (fun x => r x • m) a = s.indicator r a • m
-- Init.Data.Array.Lemmas
Array.toList_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β},
  (Array.flatMap f xs).toList = List.flatMap (fun a => (f a).toList) xs.toList
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_biUnion_eq : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m : MeasureTheory.AddContent G C}
  {ι : Type u_3},
  MeasureTheory.IsSetRing C →
    ∀ {s : ι → Set α} {S : Finset ι}, (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.MIntl.mk : {F : PFunctor.{uA, uB}} → (approx : (n : ℕ) → PFunctor.Approx.CofixA F n) → PFunctor.Approx.AllAgree approx → F.MIntl
-- Mathlib.Order.Fin.Basic
Fin.castLE_lt_castLE_iff : ∀ {m n : ℕ} {i j : Fin n} (h : n ≤ m), Fin.castLE h i < Fin.castLE h j ↔ i < j
-- Mathlib.Topology.Algebra.MulAction
/-- The stabilizer of a continuous group action on a discrete space is an open subgroup.  -/
stabilizer_isOpen : ∀ (M : Type u_1) {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Group M]
  [inst_3 : MulAction M X] [ContinuousSMul M X] [DiscreteTopology X] (x : X), IsOpen ↑(MulAction.stabilizer M x)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {e' : OpenPartialHomeomorph M' H'} {f : M → M'} {s : Set M} {x : M} {n : WithTop ℕ∞},
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I' n M' →
      x ∈ e.source →
        f x ∈ e'.source →
          (ContMDiffWithinAt I I' n f s x ↔
            ContinuousWithinAt f s x ∧
              ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ Set.range ↑I)
                (↑(e.extend I) x))