mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.PersistentArray
Lean.PersistentArray.findSomeRev? : {α : Type u} → {β : Type u_1} → Lean.PersistentArray α → (α → Option β) → Option β
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.toCocycles_comp_isoCocycles₂_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 1 2) (groupCohomology.isoCocycles₂ A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).hom
      (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.f'
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.fg_adjoin_singleton : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R x → (Subalgebra.toSubmodule R[x]).FG
-- Lean.Data.FuzzyMatching
/-- Match the given pattern with the given word using a fuzzy matching
algorithm. Return `false` if no match was found or the found match received a
score below the given threshold.  -/
Lean.FuzzyMatching.fuzzyMatch : String → String → optParam Float 0.2 → Bool
-- Mathlib.RingTheory.Etale.Kaehler
KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  [inst_7 : Algebra.FormallyEtale S T] (s : S),
  (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R S T).symm
      ((KaehlerDifferential.D R T) ((algebraMap S T) s)) =
    1 ⊗ₜ[S] (KaehlerDifferential.D R S) s
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.map.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit t) (α : F ⟶ G),
  CategoryTheory.Limits.IsLimit.map s P α = P.lift ((CategoryTheory.Limits.Cone.postcompose α).obj s)
-- Plausible.Testable
/-- Try `n` times to find a counter-example for `p`.  -/
Plausible.Testable.runSuiteAux : (p : Prop) →
  [Plausible.Testable p] → Plausible.Configuration → Plausible.TestResult p → ℕ → Plausible.Gen (Plausible.TestResult p)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueData_V : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (ij : ↑X.affineOpens × ↑X.affineOpens),
  I.glueData.V ij = I.glueDataObjPullback ij.1 ij.2
-- Mathlib.RingTheory.PicardGroup
/-- An isomorphism between a flat `R`-module and its realization as a submodule in
a faithful `R`-algebra.  -/
Module.Flat.submoduleAlgebraEquiv : {R : Type u} →
  {M : Type v} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (e : TensorProduct R A M ≃ₗ[A] A) →
                  [Module.Flat R M] → [FaithfulSMul R A] → ↥(Module.Flat.submoduleAlgebra e) ≃ₗ[R] M
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.algebraMap_apply_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : R),
  ((algebraMap R (ArithmeticFunction S)) x) 1 = (algebraMap R S) x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.lift_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H₁ H₂ : CategoryTheory.Grp C} (f : G ⟶ H₁) (g : G ⟶ H₂),
  (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `neg_add_lt_iff_lt_add`. -/
neg_add_lt_of_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a < b + c → -b + a < c
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- A more general version of `Multipliable.congr`, allowing the functions to
disagree on a finite set.

Note that this requires the target to be a group, and hence fails for products valued
in a ring. See `Multipliable.congr_cofinite₀` for a version applying in this case,
with an additional non-vanishing hypothesis.
 -/
Multipliable.congr_cofinite : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α},
  Multipliable f → f =ᶠ[Filter.cofinite] g → Multipliable g
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk.sizeOf_spec : ∀ {M : Type u_3} [inst : Add M] [inst_1 : SizeOf M] (carrier : Set M)
  (add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier),
  sizeOf { carrier := carrier, add_mem' := add_mem' } = 1
-- Lean.Parser.Term
/-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
If present, the identifier `h` is bound to a proof of `x = e`.  -/
Lean.Parser.Term.namedPattern : Lean.Parser.TrailingParser
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_fill : ∀ {w i : ℕ} {v : Bool}, (BitVec.fill w v).getMsbD i = (v && decide (i < w))
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- The integral closure of `R` in an `R`-algebra `A`.  -/
integralClosure : (R : Type u_1) → (A : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → Subalgebra R A
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).minKey? = t.minKey?
-- Mathlib.Algebra.WithConv
/-- The linear equivalence between `WithConv A` and `A`.  -/
WithConv.linearEquiv : (R : Type u_1) →
  (A : Type u_2) → [inst : AddCommMonoid A] → [inst_1 : Semiring R] → [inst_2 : Module R A] → WithConv A ≃ₗ[R] A
-- Batteries.Data.Fin.Lemmas
Fin.countP_le : ∀ {n : ℕ} (p : Fin n → Bool), Fin.countP p ≤ n
-- Init.Data.SInt.Basic
instHashableInt32 : Hashable Int32
-- Lean.Util.Trace
Lean.setTraceState : {m : Type → Type} → [Lean.MonadTrace m] → Lean.TraceState → m Unit
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, (Std.ExtTreeMap.filter f t)[k]? = t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_add_one : ∀ (r : ENNReal), ⌈r + 1⌉ₑ = ⌈r⌉ₑ + 1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_skipPrefixWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String} {h : s.skipPrefixWhile p ≠ s.endPos}, p ((s.skipPrefixWhile p).get h) = false
-- Aesop.Stats.Extension
/-- The collected stats.
 -/
Aesop.StatsExtensionEntry.stats : Aesop.StatsExtensionEntry → Aesop.Stats
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.lift_symm_apply : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A]
  (F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A),
  (FreeNonUnitalNonAssocAlgebra.lift R).symm F = ⇑F ∘ FreeNonUnitalNonAssocAlgebra.of R
-- Lean.Meta.Transform
Lean.TransformStep.visit.inj : ∀ {e e_1 : Lean.Expr}, Lean.TransformStep.visit e = Lean.TransformStep.visit e_1 → e = e_1
-- Batteries.Tactic.OpenPrivate
/-- Collects the names of private declarations referenced in definition `n`.  -/
Lean.Meta.collectPrivateIn : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → optParam Lean.NameSet Lean.NameSet.empty → m Lean.NameSet
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
_private.Mathlib.Algebra.Homology.Embedding.ExtendHomotopy.0.Homotopy.extend.homAux.match_1.splitter : {ι : Type u_1} →
  (motive : Option ι → Option ι → Sort u_2) →
    (i' j' : Option ι) →
      ((x : Option ι) → motive none x) →
        ((x : Option ι) → (x = none → False) → motive x none) → ((i j : ι) → motive (some i) (some j)) → motive i' j'
-- Mathlib.Algebra.FreeMonoid.Basic
_private.Mathlib.Algebra.FreeMonoid.Basic.0.FreeMonoid.prodAux.match_1.splitter : {M : Type u_1} →
  (motive : List M → Sort u_2) →
    (x : List M) → (Unit → motive []) → ((x : M) → (xs : List M) → motive (x :: xs)) → motive x
-- Mathlib.Data.ENat.Basic
ENat.one_ne_top : 1 ≠ ⊤
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.orderedInsert.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((b : α) → (l : List α) → motive (b :: l)) → motive x
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a<...=b`
by varying the upper bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a`, the statement holds for the empty range `a<...=b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, if the
statement holds for `a<...=b`, it also holds for the larger range `a<...=(b + 1)`.

The following is an example reproving `length_toList_roc`.

```
example (a b : Nat) : (a<...=b).toList.length = b - a := by
  induction a, b using Nat.induct_roc_right
  case base =>
    simp only [Nat.toList_roc_eq_nil, List.length_nil, *]; omega
  case step a b hle ih =>
    rw [Nat.toList_roc_eq_append (by omega),
      List.length_append, List.length_singleton, Nat.add_sub_cancel, ih]
    omega
``` -/
Nat.induct_roc_right : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a → motive a b) → (∀ (a b : ℕ), a ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℕ), motive a b
-- Mathlib.Analysis.Calculus.FDeriv.Mul
differentiableAt_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R] {x : R}, IsUnit x → DifferentiableAt 𝕜 Ring.inverse x
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.exists_lt : ∀ {α : Type u} {s : Set α} [inst : LinearOrder α], s.Nontrivial → ∃ x ∈ s, ∃ y ∈ s, x < y
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instConcreteCategoryLinearMapIdCarrier : (R : Type u) → [inst : Semiring R] → CategoryTheory.ConcreteCategory (SemimoduleCat R) fun x1 x2 => ↑x1 →ₗ[R] ↑x2
-- Mathlib.Topology.Covering.Basic
/-- A covering map is a continuous function `f : E → X` with discrete fibers such that each point
of `X` has an evenly covered neighborhood.  -/
IsCoveringMap : {E : Type u_1} → {X : Type u_2} → [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → Prop
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftByMin : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A) [P.IsStableUnderShiftBy a]
  [Q.IsStableUnderShiftBy a], (P ⊓ Q).IsStableUnderShiftBy a
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
PrincipalSeg.cocone_pt : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β) {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_1, u_3} C] (F : CategoryTheory.Functor β C), (f.cocone F).pt = F.obj f.top
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableInf.mk : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Min M],
  autoParam (∀ (c : M), Measurable fun x => c ⊓ x) MeasurableInf.measurable_const_inf._autoParam →
    autoParam (∀ (c : M), Measurable fun x => x ⊓ c) MeasurableInf.measurable_inf_const._autoParam → MeasurableInf M
-- Init.Data.UInt.Log2
/-- Base-two logarithm of 8-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `UInt8.log2 0 = 0`
 * `UInt8.log2 1 = 0`
 * `UInt8.log2 2 = 1`
 * `UInt8.log2 4 = 2`
 * `UInt8.log2 7 = 2`
 * `UInt8.log2 8 = 3`
 -/
UInt8.log2 : UInt8 → UInt8
-- Mathlib.RingTheory.Flat.Basic
Submodule.quotEquivOfEq.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M)
  (h : p = p'), p.quotEquivOfEq p' h = p.quotEquivOfEq p' h
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.semilinearEquivOfRingEquiv_comp : ∀ {A : Type u_8} {B : Type u_9} (K : Type u_10) (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (f : A ≃+* B) {C : Type u_12} (M : Type u_13)
  [inst_8 : CommRing C] [inst_9 : CommRing M] [inst_10 : Algebra C M] [inst_11 : IsFractionRing C M] (g : B ≃+* C),
  have this := ⋯;
  have this_1 := ⋯;
  IsFractionRing.semilinearEquivOfRingEquiv K M (f.trans g) =
    (IsFractionRing.semilinearEquivOfRingEquiv K L f).trans (IsFractionRing.semilinearEquivOfRingEquiv L M g)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber_singleton : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (x : X), Metric.packingNumber ε {x} = 1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eVariationOn_Ioc_eq_Icc_of_continuousWithinAt' : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {a b : α} [h : (nhdsWithin a (Set.Ioi a)).NeBot],
  ContinuousWithinAt f (Set.Ici a) a → eVariationOn f (Set.Ioc a b) = eVariationOn f (Set.Icc a b)
-- Mathlib.Data.Rel
SetRel.irrefl : ∀ {α : Type u_1} (R : SetRel α α) (a : α) [R.IsIrrefl], (a, a) ∉ R
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.insideFor : Lean.Elab.Term.Do.ToCodeBlock.Context → Bool
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {ι : Type u_2} (f : ι → A) {m : ι → ℕ} (f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i))
  (hm : ∀ (i : ι), 0 < m i) (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)),
  AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan 𝒜 f f_deg hm hf =
    { I₀ := ι, X := fun i => CommRingCat.of (HomogeneousLocalization.Away 𝒜 (f i)),
      f := fun i => AlgebraicGeometry.Proj.awayι 𝒜 (f i) ⋯ ⋯, idx := fun x => ⋯.choose, covers := ⋯, map_prop := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_negAddY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).negAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_eq_mul_twoPow : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x <<< n = x * BitVec.twoPow w n
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel and collects results in the original order,
discarding state information.

Unlike `par`, this doesn't return state information from tasks.

The final TermElabM state is restored to the initial state (before tasks ran).
 -/
Lean.Elab.Term.TermElabM.par' : {α : Type} → List (Lean.Elab.TermElabM α) → Lean.Elab.TermElabM (List (Except Lean.Exception α))
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats.mk : Aesop.RuleName → Array Aesop.ForwardClusterStateStats → Aesop.ForwardRuleStateStats
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_le_max_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  a ≤ b → b ≤ c → ∀ (d : G), |b - d| ≤ max (c - d) (d - a)
-- Mathlib.Logic.Godel.GodelBetaFunction
Nat.unbeta.eq_1 : ∀ (l : List ℕ),
  Nat.unbeta l =
    Nat.pair (↑(Nat.chineseRemainderOfFinset (fun x => l[x]) (Nat.coprimes✝ fun x => l[x]) Finset.univ ⋯ ⋯))
      (Nat.supOfSeq✝ fun x => l[x]).factorial
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.PullbackCone.fst_limit_cone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)],
  CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) =
    CategoryTheory.Limits.pullback.fst f g
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The tensor product of two graded objects.  -/
CategoryTheory.GradedObject.Monoidal.tensorObj : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X₁ X₂ : CategoryTheory.GradedObject I C) → [X₁.HasTensor X₂] → CategoryTheory.GradedObject I C
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Product rule for Lie brackets: given two vector fields `V` and `W` on `M` and a function
`f : M → 𝕜`, we have `[f • V, W] = -(df W) • V + f • [V, W]`. Version within a set.
 -/
VectorField.mlieBracketWithin_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜},
  MDiffAt[s] f x →
    (MDiffAt[s] fun x => ⟨x, V x⟩) x →
      UniqueMDiffAt[s] x →
        VectorField.mlieBracketWithin I (f • V) W s x =
          -(d[s] f x) (W x) • V x + f x • VectorField.mlieBracketWithin I V W s x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.op_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g) (X_1 : CategoryTheory.Limits.WalkingSpan),
  c.op.ι.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (match X_1 with
        | none => CategoryTheory.Iso.refl (Opposite.op Z)
        | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op X)
        | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Y)).hom
      (c.π.app X_1).op
-- Mathlib.Topology.Separation.Regular
NormalSpace.mk : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t) → NormalSpace X
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.instReprComp.repr : Mathlib.Tactic.Linarith.Comp → ℕ → Std.Format
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instCoeSortType.eq_1 : CommMonCat.instCoeSortType = { coe := CommMonCat.carrier }
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_add : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : Norm α] [inst_1 : Norm β],
  0 < p.toReal → ∀ (f : WithLp p (α × β)), ‖f‖ = (‖f.fst‖ ^ p.toReal + ‖f.snd‖ ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_natCast : ∀ (x : ENNReal) (n : ℕ), x ^ ↑n = x ^ n
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.edgeSetSumEquiv.match_1.congr_eq_1 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (x x_1 : V ⊕ W) (x_2 : (G ⊕g H).Adj x x_1)
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h) (u v : V)
  (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)),
  x = Sum.inl u →
    x_1 = Sum.inl v →
      x_2 ≍ h →
        (match x, x_1, x_2 with
          | Sum.inl u, Sum.inl v, h => h_1 u v h
          | Sum.inr u, Sum.inr v, h => h_2 u v h
          | Sum.inl u, Sum.inr v, h => h_3 u v h
          | Sum.inr u, Sum.inl v, h => h_4 u v h) ≍
          h_1 u v h
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.sub : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α}, IsLocalMax f a → IsLocalMin g a → IsLocalMax (fun x => f x - g x) a
-- Mathlib.Combinatorics.Graph.Basic
Graph.instSymmAdj : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, Std.Symm G.Adj
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forwardRuleMatches? : Aesop.RuleTacDescr → Option (Array Aesop.ForwardRuleMatch)
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.lintegral_prod_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : α → γ} (hf : Measurable f) (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (a : α) {g : β × γ → ENNReal},
  Measurable g →
    ∫⁻ (p : β × γ), g p ∂(κ.prod (ProbabilityTheory.Kernel.deterministic f hf)) a = ∫⁻ (b : β), g (b, f a) ∂κ a
-- Mathlib.Geometry.Manifold.Sheaf.Basic
/-- Let `P` be a `LocalInvariantProp` for functions between spaces with the groupoids `G`, `G'`
and let `M`, `M'` be charted spaces modelled on the model spaces of those groupoids.  Then there is
an induced `LocalPredicate` on the functions from `M` to `M'`, given by `LiftProp P`.  -/
StructureGroupoid.LocalInvariantProp.localPredicate : {H : Type u_1} →
  [inst : TopologicalSpace H] →
    {H' : Type u_2} →
      [inst_1 : TopologicalSpace H'] →
        {G : StructureGroupoid H} →
          {G' : StructureGroupoid H'} →
            {P : (H → H') → Set H → H → Prop} →
              (M : Type u) →
                [inst_2 : TopologicalSpace M] →
                  [ChartedSpace H M] →
                    (M' : Type u) →
                      [inst_4 : TopologicalSpace M'] →
                        [ChartedSpace H' M'] → G.LocalInvariantProp G' P → TopCat.LocalPredicate fun x => M'
-- Mathlib.Order.RelIso.Basic
RelHomClass.isWellFounded : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) [IsWellFounded β s], IsWellFounded α r
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.normEq0.eq_2 : ∀ (c : ℕ) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p_2 : Lean.Grind.CommRing.Poly),
  (Lean.Grind.CommRing.Poly.add k m p_2).normEq0 c =
    bif k % ↑c == 0 then p_2.normEq0 c else Lean.Grind.CommRing.Poly.add k m (p_2.normEq0 c)
-- Mathlib.RepresentationTheory.Tannaka
/-- The `rightFDRep` component of `η : Aut (forget k G)` gives rise to
an algebra morphism `(G → k) →ₐ[k] (G → k)`.  -/
TannakaDuality.FiniteGroup.algHomOfRightFDRepComp : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → [Finite G] → CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G) → (G → k) →ₐ[k] G → k
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → {P : C} → Inhabited (CategoryTheory.Abelian.Pseudoelement P)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints_of_isGaloisGroup : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L)
  [hGKL : IsGaloisGroup G K L] [hHFL : IsGaloisGroup (↥H) (↥F) L], FixedPoints.intermediateField ↥H = F
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_nat : ∀ {x : ℝ}, Irrational x → ∀ (m : ℕ), x ≠ ↑m
-- Std.Http.Data.URI.Basic
/-- Returns a new URI with the authority replaced.
 -/
Std.Http.URI.withAuthority : Std.Http.URI → Option Std.Http.URI.Authority → Std.Http.URI