mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_mem_unit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashMap α Unit},
  (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁ = m₂
-- Init.Data.Array.Lemmas
Array.foldr_eq_foldl : ∀ {α : Type u_1} {init : α} {xs : Array α} {f : α → α → α} [Std.Associative f] [Std.LawfulIdentity f init],
  Array.foldr f init xs = Array.foldl f init xs
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The cocone over the proposed colimit additive commutative monoid.  -/
AddCommMonCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J AddCommMonCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coe_id : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P], ⇑AffineIsometry.id = id
-- Mathlib.Algebra.Group.Defs
add_right_cancel : ∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] {a b c : G}, a + b = c + b → a = c
-- Mathlib.Data.Num.Basic
/-- Converts a `Num` to a `ZNum`.  -/
Num.toZNum : Num → ZNum
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_one_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, orderOf x = 1 ↔ x = 1
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.monomial_eq_mk : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R),
  (PowerSeries.monomial n) a = PowerSeries.mk fun m => if m = n then a else 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateFun! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Lean.HeadIndex
Lean.HeadIndex.forallE.sizeOf_spec : sizeOf Lean.HeadIndex.forallE = 1
-- Mathlib.Algebra.Group.Prod
Prod.instIsLeftCancelMul : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H],
  IsLeftCancelMul (G × H)
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.toPartialEquiv = e.toPartialEquivOfImageEq Set.univ Set.univ ⋯
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_id_apply : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPowerSeries σ R), (MvPowerSeries.rename id) p = p
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.prod_mk : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_3} {A : Type u_4} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {S : Submonoid R} (t : Finset ι) (a : ι → A) (s : ι → ↥S),
  ∏ i ∈ t, LocalizedModule.mk (a i) (s i) = LocalizedModule.mk (∏ i ∈ t, a i) (∏ i ∈ t, s i)
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.algEquivEquivAlgHom_apply : ∀ (K : Type u_1) (L : Type u_2) [inst : CommRing K] [inst_1 : IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Module.IsTorsionFree K L] [inst_5 : Algebra.IsAlgebraic K L] (ϕ : L ≃ₐ[K] L),
  (Algebra.IsAlgebraic.algEquivEquivAlgHom K L) ϕ = ↑ϕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM (fun k v => f ⟨k, v⟩) t = forM t.toList f
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, the Localization of `M` at the Submonoid generated by `x`, as a quotient.  -/
Localization.Away : {M : Type u_1} → [CommMonoid M] → M → Type u_1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedExtensionState.default : Lean.Meta.Grind.ExtensionState
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.ofUpper_symm : ∀ {α : Type u_1}, Topology.WithUpper.ofUpper.symm = Topology.WithUpper.toUpper
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftRight_and_distrib : ∀ {i a b : ℕ}, (a &&& b) >>> i = a >>> i &&& b >>> i
-- Init.PropLemmas
Bool.dite_then_true : ∀ {p : Prop} [inst : Decidable p] {x : ¬p → Bool}, (if h : p then true else x h) = true ↔ ∀ (h : ¬p), x h = true
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given `J : CardinalDirectedPoset κ`, this is the predicate
on `Set J.obj` that is satisfied by subsets that are of
cardinality `< κ` and have a terminal object.  -/
CategoryTheory.CardinalDirectedPoset.PropSet : {κ : Cardinal.{u}} → [inst : Fact κ.IsRegular] → (J : CategoryTheory.CardinalDirectedPoset κ) → Set ↑J.obj → Prop
-- Mathlib.NumberTheory.Height.NumberField
NumberField.IsFinitePlace.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w w_1 : AbsoluteValue K ℝ),
  w = w_1 → NumberField.IsFinitePlace w = NumberField.IsFinitePlace w_1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The `Matrix` version of `inv_sub_inv'`  -/
Matrix.inv_sub_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  (IsUnit A ↔ IsUnit B) → A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_eq_self : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), MeasureTheory.OuterMeasure.boundedBy ⇑m = m
-- Init.Data.Int.Gcd
Int.gcd_eq_natAbs_gcd_natAbs : ∀ (m n : ℤ), m.gcd n = m.natAbs.gcd n.natAbs
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates limits of `K.op : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsColimitOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
                [CategoryTheory.CreatesLimit K.leftOp F.unop] → CategoryTheory.CreatesColimit K F
-- Mathlib.GroupTheory.Goursat
Subgroup.goursatSnd.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (I : Subgroup (G × H)),
  I.goursatSnd = Subgroup.map ((MonoidHom.snd G H).comp I.subtype) ((MonoidHom.fst G H).comp I.subtype).ker
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two real-valued functions on an arbitrary set.  -/
regionBetween : {α : Type u_1} → (α → ℝ) → (α → ℝ) → Set α → Set (α × ℝ)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1.eq_1 : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  groupHomology.mapShortComplexH1 f φ =
    { τ₁ := groupHomology.chainsMap₂ f φ, τ₂ := groupHomology.chainsMap₁ f φ, τ₃ := Rep.Hom.toModuleCatHom φ,
      comm₁₂ := ⋯, comm₂₃ := ⋯ }
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.diagramCompIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) (X : C), J.diagramCompIso F P X = J.diagramCompIso F P X
-- Mathlib.RingTheory.Localization.Module
LinearIndependent.localization_localization : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [inst_4 : CommSemiring A] [inst_5 : Algebra R A]
  (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ] [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ]
  [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5}
  {v : ι → A}, LinearIndependent R v → LinearIndependent Rₛ (⇑(algebraMap A Aₛ) ∘ v)
-- Init.Data.SInt.Lemmas
ISize.toBitVec_mod : ∀ {a b : ISize}, (a % b).toBitVec = a.toBitVec.srem b.toBitVec
-- Mathlib.Order.Nucleus
/-- See Note [custom simps projection]  -/
Nucleus.Simps.apply : {X : Type u_1} → [inst : SemilatticeInf X] → Nucleus X → X → X
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.asyncCtx? : Lean.Environment → Option Lean.AsyncContext✝
-- Mathlib.Analysis.Normed.Ring.Basic
List.norm_prod_le : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] (l : List α), ‖l.prod‖ ≤ (List.map norm l).prod
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α} [inst_1 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).get! k = m.get! k
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_natCast : ∀ {R : Type u} {M : Type v} [inst : AddMonoidWithOne R] [inst_1 : AddMonoid M] (n : ℕ), TrivSqZeroExt.inl ↑n = ↑n
-- Mathlib.Tactic.NoncommRing
Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (r : R) (n : ℕ) [inst_1 : n.AtLeastTwo],
  r * OfNat.ofNat n = OfNat.ofNat n • r
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Init.Data.BitVec.Lemmas
BitVec.toFin_extractLsb' : ∀ {n s m : ℕ} {x : BitVec n}, (BitVec.extractLsb' s m x).toFin = Fin.ofNat (2 ^ m) (x.toNat >>> s)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Construct an adjunction between functors `F` and `G` given a unit and counit for the adjunction
satisfying the triangle identities.  -/
CategoryTheory.Adjunction.mkOfUnitCounit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → CategoryTheory.Adjunction.CoreUnitCounit F G → (F ⊣ G)
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isStrongGenerator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular], P.IsCardinalFilteredGenerator κ → P.IsStrongGenerator
-- Mathlib.Topology.Order.OrderClosed
le_of_tendsto_of_tendsto_of_frequently : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {f g : β → α}
  {b : Filter β} {a₁ a₂ : α},
  Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → (∃ᶠ (x : β) in b, f x ≤ g x) → a₁ ≤ a₂
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dot : Lean.Elab.TermInfo → Option Lean.Expr → Lean.Elab.CompletionInfo
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_mul : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ R β), (s.mul t).hsum = s.hsum * t.hsum
-- Mathlib.Algebra.Group.Conj
IsConj.symm : ∀ {α : Type u} [inst : Monoid α] {a b : α}, IsConj a b → IsConj b a
-- Lean.Expr
/-- Return `true` if `e` is of the form `semiOutParam _`  -/
Lean.Expr.isSemiOutParam : Lean.Expr → Bool
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.mapExtendScalars_apply_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_4} {N' : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (Rₛ : Type u_6)
  [inst_11 : CommSemiring Rₛ] [inst_12 : Algebra R Rₛ] [inst_13 : Module Rₛ M'] [inst_14 : Module Rₛ N']
  [inst_15 : IsScalarTower R Rₛ M'] [inst_16 : IsScalarTower R Rₛ N'] [inst_17 : IsLocalization S Rₛ] (x : M →ₗ[R] N)
  (a : M'), ((IsLocalizedModule.mapExtendScalars S f g Rₛ) x) a = ((IsLocalizedModule.map S f g) x) a
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.brecOn.go : {motive : Lean.Expr.ProdTree → Sort u} →
  (t : Lean.Expr.ProdTree) →
    ((t : Lean.Expr.ProdTree) → Lean.Expr.ProdTree.below t → motive t) → motive t ×' Lean.Expr.ProdTree.below t
-- Aesop.Frontend.Extension.Init
Aesop.getDeclaredRuleSets : IO (Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name))
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_ofNat_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoMod hp a (OfNat.ofNat m * p + b) = toIcoMod hp a b
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Focus.this : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ⊣⊢ₛ ⌜True⌝ ∧ P
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.toSubmonoidClass : ∀ {S : Type u_1} {R : outParam (Type u)} {inst : NonAssocSemiring R} {inst_1 : SetLike S R}
  [self : SubsemiringClass S R], SubmonoidClass S R
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.IsAEKolmogorovProcess : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsKolmogorovProcess X P p q M → ProbabilityTheory.IsAEKolmogorovProcess X P p q M
-- Mathlib.Data.Seq.Computation
Computation.LiftRel.imp : ∀ {α : Type u} {β : Type v} {R S : α → β → Prop},
  (∀ {a : α} {b : β}, R a b → S a b) →
    ∀ (s : Computation α) (t : Computation β), Computation.LiftRel R s t → Computation.LiftRel S s t
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.whiskerEquiv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C}
  (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [inst_1 : CategoryTheory.Limits.HasCoproduct f]
  [inst_2 : CategoryTheory.Limits.HasCoproduct g],
  (CategoryTheory.Limits.Sigma.whiskerEquiv e w).inv =
    CategoryTheory.Limits.Sigma.map' ⇑e.symm fun k =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (w (e.symm k)).hom
-- Mathlib.Data.Multiset.Bind
Multiset.card_bind : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β),
  (s.bind f).card = (Multiset.map (Multiset.card ∘ f) s).sum
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_ne_top : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → ∀ (n : ℤ), a ^ n ≠ ⊤
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.etalePrecoverage.eq_1 : AlgebraicGeometry.Scheme.etalePrecoverage = AlgebraicGeometry.Scheme.precoverage @AlgebraicGeometry.Etale
-- Mathlib.Data.Set.Function
Set.BijOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ},
  Set.BijOn g t p → Set.BijOn f s t → Set.BijOn (g ∘ f) s p
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.X.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alterₘ.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst : ∀ {M : Type u_1} [inst : DivInvOneMonoid M] {l l_n n : M}, l = l_n / 1 → l_n = n → l = n
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_nsmul : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (n : ℕ) (x : L × M),
  (LieAlgebra.ofProd c) (n • x) = n • (LieAlgebra.ofProd c) x
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.exact_iff_degreewise_exact : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  S.Exact ↔ ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).Exact
-- Mathlib.Analysis.Calculus.MeanValue
/-- Let `s` be a convex set in a real normed vector space `E`, let `f : E → G` be a function
differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'` is
continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `‖f' x‖₊`, `f` is Lipschitz
on some neighborhood of `x` within `s`. See also
`Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt` for a version
with an explicit estimate on the Lipschitz constant.  -/
Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G},
  Convex ℝ s →
    ∀ {f : E → G},
      (∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) →
        ContinuousWithinAt f' s x → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_iInf : ∀ {ι : Sort u_1} {G : Type u_2} [inst : Group G] (S : ι → Subgroup G), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.Control.Fold
Monoid.foldlM.ofFreeMonoid_apply : ∀ {m : Type u → Type u} [inst : Monad m] {α β : Type u} [inst_1 : LawfulMonad m] (f : β → α → m β) (xs : FreeMonoid α),
  (Monoid.foldlM.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldlM f) (FreeMonoid.toList xs))
-- Lean.Parser.Basic
Lean.Parser.ParserContext.mkEmptySubstringAt : Lean.Parser.ParserContext → String.Pos.Raw → Substring.Raw
-- Init.Data.UInt.Bitwise
USize.toUInt32_xor : ∀ (a b : USize), (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
-- Mathlib.Order.Defs.Unbundled
/-- `IsPartialOrder X r` means that the binary relation `r` on `X` is a partial order, that is,
`IsPreorder X r` and `Std.Antisymm r`.  -/
IsPartialOrder : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_iInf : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) {x : M},
  x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The canonical isomorphism between `(Cofork.ofπ π w).unop` and `Fork.ofι π.unop w'`.  -/
CategoryTheory.Limits.Cofork.ofπUnopIsoOfι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : Cᵒᵖ} →
      {f g : X ⟶ Y} →
        (π π' : Y ⟶ P) →
          (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) →
            (w' :
                CategoryTheory.CategoryStruct.comp π'.unop f.unop = CategoryTheory.CategoryStruct.comp π'.unop g.unop) →
              π = π' → ((CategoryTheory.Limits.Cofork.ofπ π w).unop ≅ CategoryTheory.Limits.Fork.ofι π'.unop w')
-- Lean.Expr
Lean.MVarIdMap.insert : {α : Type} → Lean.MVarIdMap α → Lean.MVarId → α → Lean.MVarIdMap α
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxo.HasSize α] (r : Std.Rco α), r.size = Std.Rxo.HasSize.size r.lower r.upper
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Pull back a cover along a morphism.  -/
CategoryTheory.GrothendieckTopology.Cover.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {J : CategoryTheory.GrothendieckTopology C} → J.Cover X → (Y ⟶ X) → J.Cover Y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_eq_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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] [W.HasRightCalculusOfFractions] {X Y : C}
  (φ ψ : W.RightFraction X Y), φ.map L ⋯ = ψ.map L ⋯ ↔ CategoryTheory.MorphismProperty.RightFractionRel φ ψ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_addX : ∀ {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₁ x₂ ℓ : A), (W'.baseChange B).addX (f x₁) (f x₂) (f ℓ) = f ((W'.baseChange A).addX x₁ x₂ ℓ)
-- Mathlib.Data.Set.Restrict
Set.domRestrict_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), s.domRestrict f = f ∘ Subtype.val
-- Mathlib.RingTheory.Congruence.Hom
RingCon.liftₐEquiv_apply : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M) (f : { f // c ≤ RingCon.ker ↑f }),
  c.liftₐEquiv f = c.liftₐ ↑f ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Lean.Meta.Injective
Lean.Meta.mkHInjectiveTheoremNameFor : Lean.Name → Lean.Name
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.bijOn_coreflection_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  Set.BijOn (⇑(P.coreflection i)) (Set.range ⇑P.coroot) (Set.range ⇑P.coroot)
-- Batteries.Data.Fin.Coding
/-- Decode `{ i : Fin n // P i }` from `Fin (Fin.countP P)` where `P` is a decidable predicate.  -/
Fin.decodeSubtype : {n : ℕ} → (P : Fin n → Prop) → [inst : DecidablePred P] → Fin (Fin.countP fun x => decide (P x)) → { i // P i }
-- Mathlib.Algebra.Order.IsBotOne
ne_zero_of_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], a < b → b ≠ 0
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.bot_join : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.join Lean.Order.bot P = P