mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
Units.val_mk : ∀ {α : Type u} [inst : Monoid α] (a b : α) (h₁ : a * b = 1) (h₂ : b * a = 1),
  ↑{ val := a, inv := b, val_inv := h₁, inv_val := h₂ } = a
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (a a_1 : K₁ ⟶ K₂) (e_a : a = a_1) (b b_1 : L₁ ⟶ L₂) (e_b : b = b_1)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂),
  CochainComplex.mappingCone.map φ₁ φ₂ a b comm = CochainComplex.mappingCone.map φ₁ φ₂ a_1 b_1 ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Defs
iteratedFDerivWithin_eq_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ},
  UniqueDiffOn 𝕜 s → ContDiffAt 𝕜 (↑n) f x → x ∈ s → iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.mk.sizeOf_spec : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : SizeOf X]
  [inst_3 : SizeOf Y] (toFun : C(X, Y)) (invFun : C(Y, X))
  (left_inv : (invFun.comp toFun).Homotopic (ContinuousMap.id X))
  (right_inv : (toFun.comp invFun).Homotopic (ContinuousMap.id Y)),
  sizeOf { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    1 + sizeOf toFun + sizeOf invFun + sizeOf left_inv + sizeOf right_inv
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∃ ι σ, ∃ (x : Finite σ), Finite ι ∧ Nonempty (Algebra.SubmersivePresentation R S ι σ)) → Algebra.IsStandardSmooth R S
-- Std.Http.Protocol.H1.Message
/-- Inverts the message direction.
 -/
Std.Http.Protocol.H1.Direction.swap : Std.Http.Protocol.H1.Direction → Std.Http.Protocol.H1.Direction
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.shrinkYonedaEquiv (CategoryTheory.shrinkYoneda.{w, v, u}.map f) =
    CategoryTheory.shrinkYonedaObjObjEquiv.symm f
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The cocone at `A` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∈ closure {p₀}`
 -/
skyscraperPresheafCoconeOfSpecializes : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              {y : ↑X} →
                p₀ ⤳ y →
                  CategoryTheory.Limits.Cocone
                    ((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A))
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_eq : ∀ {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} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} {χ : E →ₗ[R] F}, (∀ (u : ↥p), φ u = χ ↑u) → (∀ (u : ↥q), ψ u = χ ↑u) → LinearMap.ofIsCompl h φ ψ = χ
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.instInhabitedFreeMonoidalCategory.default : {C : Type u} → CategoryTheory.FreeMonoidalCategory C
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toReal_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) (x : α), f.toReal x = ↑(f x)
-- Aesop.RuleTac.Basic
Aesop.mvarIdToSubgoal : Lean.MVarId → Lean.MVarId → Aesop.BaseM Aesop.Subgoal
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instSetLike : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → SetLike (OpenNormalAddSubgroup G) G
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.HashMap.Raw α Unit},
  m₁.WF → m₂.WF → (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → m₁.Equiv m₂
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instMul : Mul Cardinal.{u}
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMap_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], ContinuousAlternatingMap.toContinuousMultilinearMap 0 = 0
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.instArchimedean : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  Archimedean (ArchimedeanClass.FiniteResidueField K)
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative_smul : ∀ (k c : ℂ) (F : UpperHalfPlane → ℂ),
  MDiff F → Derivative.serreDerivative k (c • F) = c • Derivative.serreDerivative k F
-- Mathlib.Order.Hom.Basic
/-- A bundled expression of the fact that a map between partial orders that is strictly monotone
is weakly monotone.  -/
RelHom.toOrderHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → ((fun x1 x2 => x1 < x2) →r fun x1 x2 => x1 < x2) → α →o β
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_apply : ∀ (i : ℕ) {n m : ℕ} (j : Fin (n + 1)) (hi : autoParam (n + i = m) SimplexCategory.δ₀Iter_apply._auto_1),
  (CategoryTheory.ConcreteCategory.hom (SimplexCategory.δ₀Iter i hi)) j = ⟨↑j + i, ⋯⟩
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₂)) (F.map f₂₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) h) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv h))
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.lctx : Lean.Elab.Command.FinalizeContext✝ → Lean.LocalContext
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.Model.realize_of_mem : ∀ {L : FirstOrder.Language} {M : Type w} {inst : L.Structure M} {T : L.Theory} [self : M ⊨ T], ∀ φ ∈ T, M ⊨ φ
-- Mathlib.RingTheory.Valuation.LocalSubring
Ideal.image_subset_nonunits_valuationSubring : ∀ {K : Type u_3} [inst : Field K] {A : Subring K} (I : Ideal ↥A),
  I ≠ ⊤ → ∃ B, A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictPeriods_le_periods : ∀ {R : Type u_1} [inst : Ring R] (𝒢 : Subgroup (GL (Fin 2) R)), 𝒢.strictPeriods ≤ 𝒢.periods
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.mk.sizeOf_spec : ∀ (content : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (priorParts : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)) (titleString : String)
  (title : Array (Lean.Doc.Inline Lean.ElabInline)),
  sizeOf { content := content, priorParts := priorParts, titleString := titleString, title := title } =
    1 + sizeOf content + sizeOf priorParts + sizeOf titleString + sizeOf title
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_lt_wf : ∀ {R : Type u} [inst : Semiring R], WellFounded fun p q => p.trailingDegree < q.trailingDegree
-- Std.Data.TreeMap.Raw.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.TreeMap.Raw.modify : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → (β → β) → Std.TreeMap.Raw α β cmp
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
/-- Use `isCaratheodory_iUnion` instead, which does not require the disjoint assumption.  -/
MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
  (∀ (i : ℕ), m.IsCaratheodory (s i)) → Pairwise (Function.onFun Disjoint s) → m.IsCaratheodory (⋃ i, s i)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology : ∀ {X : AlgebraicGeometry.Scheme} {U : X.AffineZariskiSite} {S : CategoryTheory.Sieve U},
  S ∈ (AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X) U ↔
    ∀ x ∈ U.toOpens, ∃ V f, S.arrows f ∧ x ∈ V.toOpens
-- Init.Data.List.ToArray
List.isPrefixOfAux_toArray_succ' : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : ℕ),
  l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) =
    (List.drop (i + 1) l₁).toArray.isPrefixOfAux (List.drop (i + 1) l₂).toArray ⋯ 0
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotIdx.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] (i j : ι),
  RootPairing.chainBotIdx i j = if h : LinearIndependent R ![P.root i, P.root j] then Exists.choose ⋯ else j
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_ofAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommSemiring S] [inst_2 : Algebra S R] (p : Polynomial R),
  ⇑(AdjoinRoot.ofAlgHom S p) = ⇑(AdjoinRoot.of p)
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.EStateM.instWP.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_1 a s'
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayProps.mk.sizeOf_spec : ∀ (html : ProofWidgets.Html), sizeOf { html := html } = 1 + sizeOf html
-- Mathlib.Probability.Process.Filtration
/-- The right continuity property.  -/
MeasureTheory.Filtration.IsRightContinuous.RC : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {inst : PartialOrder ι} {𝓕 : MeasureTheory.Filtration ι m}
  [self : 𝓕.IsRightContinuous], 𝓕.rightCont ≤ 𝓕
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_inv_comp_descOpcycles_assoc : ∀ {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)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_2 : S.HasRightHomology] {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv (CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) h_1) =
    CategoryTheory.CategoryStruct.comp (h.descQ k hk) h_1
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.map.eq_1 : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : Add β] (f : α →ₙ+ β),
  AddMagma.FreeAddSemigroup.map f = AddMagma.FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of.comp f)
-- Mathlib.Order.Bounds.Image
/-- The image under an antitone function of a set which is bounded below is bounded
above.  -/
AntitoneOn.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  AntitoneOn f t → s ⊆ t → (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.num_le_denom_iff : ∀ {q : ℚ}, q.num ≤ ↑q.den ↔ q ≤ 1
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs.add : ∀ (a : ℤ) (x : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
  a ≥ 0 → p.NonnegCoeffs → (Lean.Grind.Linarith.Poly.add a x p).NonnegCoeffs
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.contDiff_qParam : ∀ {h : ℝ} (m : WithTop ℕ∞), ContDiff ℂ m (Function.Periodic.qParam h)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.domCongrBialgEquiv.eq_1 : ∀ (R : Type u_1) (A : Type u_3) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N),
  AddMonoidAlgebra.domCongrBialgEquiv R A e = BialgEquiv.ofAlgEquiv (AddMonoidAlgebra.domCongr R A e) ⋯ ⋯
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pushforward a `MulActionWithZero` structure along a surjective zero-preserving homomorphism.  -/
Function.Surjective.mulActionWithZero : {M₀ : Type u_2} →
  {A : Type u_7} →
    {A' : Type u_8} →
      [inst : MonoidWithZero M₀] →
        [inst_1 : Zero A] →
          [inst_2 : MulActionWithZero M₀ A] →
            [inst_3 : Zero A'] →
              [inst_4 : SMul M₀ A'] →
                (f : ZeroHom A A') →
                  Function.Surjective ⇑f → (∀ (a : M₀) (b : A), f (a • b) = a • f b) → MulActionWithZero M₀ A'
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.coe_unop : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R Aᵐᵒᵖ), ↑S.unop = MulOpposite.op ⁻¹' ↑S
-- Mathlib.Data.Finsupp.Basic
Finsupp.split_apply : ∀ {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [inst : Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) (x : αs i),
  (l.split i) x = l ⟨i, x⟩
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_div_right_comm : ∀ {a b c : ENNReal}, a * b / c = a / c * b
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.mapsTo_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x : α) (r : ℝ), Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (↑K * r))
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
Nat.Coprime.sum_divisors_mul : ∀ {m n : ℕ}, m.Coprime n → ∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isTheta_exp_comp_exp_comp : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ},
  ((fun x => Real.exp (f x)) =Θ[l] fun x => Real.exp (g x)) ↔
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |f x - g x|
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instOrdOffset : Ord Std.Time.Minute.Offset
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.union_insert_right_eq_insert_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {p : (a : α) × β a}, t₁ ∪ t₂.insert p.fst p.snd = (t₁ ∪ t₂).insert p.fst p.snd
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_some_memP : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} {t : RBTree.RBSet α cmp},
  t.findP? cut = some y → RBTree.RBSet.MemP cut t
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match none with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_1 ()
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_neg_left`. -/
MonovaryOn.of_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn (-f) g s → AntivaryOn f g s
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
/-- Given a functor `F : C ⥤ D`, this is the property of objects of `C`
satisfied by those `X : C` such that `IsZero (F.obj X)`.  -/
CategoryTheory.Functor.kernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty C
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.get : Substring.Raw → String.Pos.Raw → Char
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_insertIfNew!_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).keysArray.Perm
        (if Std.DTreeMap.Internal.Impl.contains k t = true then t.keysArray else t.keysArray.push k)
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toStalkₗ'.eq_1 : ∀ (R M : Type u) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  AlgebraicGeometry.StructureSheaf.toStalkₗ'✝ R M x =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (AlgebraicGeometry.StructureSheaf.toOpenₗ R M ⊤))
      ((AlgebraicGeometry.structurePresheafInModuleCat R M).germ ⊤ x trivial)
-- Init.Data.List.Erase
List.length_erase : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α},
  (l.erase a).length = if a ∈ l then l.length - 1 else l.length
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.instInhabitedFunPropDecl : Inhabited Mathlib.Meta.FunProp.FunPropDecl
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
/-- The entropy of `φ '' F` equals the entropy of `F` if `X` is endowed with the pullback by `φ`
of the uniform structure of `Y`. This version uses a `liminf`.  -/
Dynamics.coverEntropyInf_image_of_comap : ∀ {X : Type u_1} {Y : Type u_2} (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T → ∀ (F : Set X), Dynamics.coverEntropyInf T (φ '' F) = Dynamics.coverEntropyInf S F
-- Init.Data.SInt.Basic
instOrOpInt8 : OrOp Int8
-- Lean.Level
Lean.Level.mvar.inj : ∀ {a a_1 : Lean.LMVarId}, Lean.Level.mvar a = Lean.Level.mvar a_1 → a = a_1
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.subtype_injective : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), Function.Injective ⇑I.subtype
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The relation 'in the same orbit'.  -/
AddAction.orbitRel : (G : Type u_1) → (α : Type u_2) → [inst : AddGroup G] → [AddAction G α] → Setoid α
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderBraiding.braiding_hom_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderBraiding]
  (c c' : C), P (β_ c c').hom
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- `a ^ (n + 1) = a ^ n * a`  -/
LinearOrderedCommGroupWithZero.zpow_succ' : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α] (n : ℕ) (a : α), a ^ ↑n.succ = a ^ ↑n * a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_union_of_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.instSMulSpecialLinearGroupFixedDetMatrix : (n : Type u_1) →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      (R : Type u_2) → [inst_2 : CommRing R] → (m : R) → SMul (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo : Type
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
instRankConditionMulOpposite : ∀ {R : Type u_1} [inst : Semiring R] [RankCondition R], RankCondition Rᵐᵒᵖ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.f = 0 → S.g = 0 → CategoryTheory.Limits.IsZero S.X₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxi.HasSize α] [inst_1 : Std.PRange.UpwardEnumerable α] (r : Std.Roi α),
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some lower => Std.Rxi.HasSize.size lower
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.eq_4 : ∀ {α : Type u_1} (motive : RegularExpression α → Sort u_2) (P Q : RegularExpression α)
  (h_1 : Unit → motive RegularExpression.zero) (h_2 : Unit → motive RegularExpression.epsilon)
  (h_3 : (a : α) → motive (RegularExpression.char a)) (h_4 : (P Q : RegularExpression α) → motive (P.plus Q))
  (h_5 : (P Q : RegularExpression α) → motive (P.comp Q)) (h_6 : (P : RegularExpression α) → motive P.star),
  (match P.plus Q with
    | RegularExpression.zero => h_1 ()
    | RegularExpression.epsilon => h_2 ()
    | RegularExpression.char a => h_3 a
    | P.plus Q => h_4 P Q
    | P.comp Q => h_5 P Q
    | P.star => h_6 P) =
    h_4 P Q
-- Mathlib.Algebra.Group.Units.Basic
AddRightCancelMonoid.add_eq_zero : ∀ {α : Type u} [inst : AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.hom_ext_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} {f g : F ⟶ G},
  f = g ↔ f.hom = g.hom
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Transport an adjunction along a natural isomorphism on the left.  -/
CategoryTheory.Adjunction.ofNatIsoLeft : {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} → {H : CategoryTheory.Functor D C} → (F ⊣ H) → (F ≅ G) → (G ⊣ H)