mathlib-initiative/mathlib-types huggingface dataset:
-- Init.MetaTypes
/-- When `true` (default : `true`), then `simp` will attempt to transform `let`s into `have`s
if they are non-dependent. This only applies when `zeta := false`.
 -/
Lean.Meta.Simp.Config.letToHave : Lean.Meta.Simp.Config → Bool
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coeFn_coe : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (f : Derivation R A M),
  ⇑↑f = ⇑f
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForILeans : Lean.FromJson Lean.Lsp.WaitForILeans
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- A Lie-Rinehart subalgebra forms a new Lie-Rinehart algebra.  -/
LieRinehartSubalgebra.instLieRinehartAlgebraSubtypeMem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] (R : Type u_3)
  [inst_5 : CommRing R] [inst_6 : Algebra R A] [inst_7 : LieAlgebra R L] [inst_8 : LieRinehartAlgebra R A L],
  LieRinehartAlgebra R A ↥L'
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.ascii_turnstile.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.botEquivPUnit_symm_apply : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : PUnit.{v + 1}), Submodule.botEquivPUnit.symm x = 0
-- Mathlib.Analysis.ODE.Transform
isIntegralCurveAt_comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ dt : ℝ},
  IsIntegralCurveAt (γ ∘ fun x => x - dt) (v ∘ fun x => x - dt) (t₀ + dt) ↔ IsIntegralCurveAt γ v t₀
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_C_mul_T_le : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ) (a : R), (LaurentPolynomial.C a * LaurentPolynomial.T n).degree ≤ ↑n
-- Mathlib.Data.Finset.NatAntidiagonal
/-- The antidiagonal of a natural number `n` is
the finset of pairs `(i, j)` such that `i + j = n`.  -/
Finset.Nat.instHasAntidiagonal : Finset.HasAntidiagonal ℕ
-- Mathlib.LinearAlgebra.DFinsupp
/-- A characterisation of the span of a family of submodules.

See also `Submodule.mem_iSup_iff_exists_finsupp`.  -/
Submodule.mem_iSup_iff_exists_dfinsupp : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Submodule R N) (x : N),
  x ∈ iSup p ↔ ∃ f, ((DFinsupp.lsum ℕ) fun i => (p i).subtype) f = x
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A variant of `NormedAddCommGroup.tendsto_atTop` that
uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`
 -/
NormedAddCommGroup.tendsto_atTop' : ∀ {α : Type u_2} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] [NoMaxOrder α] {β : Type u_5}
  [inst_3 : SeminormedAddCommGroup β] {f : α → β} {b : β},
  Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε
-- Mathlib.Combinatorics.Matroid.Closure
/-- An alternative version of `Matroid.indep_iff_forall_notMem_closure_sdiff` where the
hypothesis that `I ⊆ M.E` is contained in the RHS rather than the hypothesis.  -/
Matroid.indep_iff_forall_notMem_closure_sdiff' : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkInstanceCmds : Lean.Elab.Deriving.Context → Lean.Name → Array Lean.Name → optParam Bool true → Lean.Elab.TermElabM (Array Lean.Command)
-- Mathlib.Order.Cover
Set.Ioo_eq_singleton_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioo a b = {c} ↔ a ⋖ c ∧ c ⋖ b
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_eq : ∀ (n : ℕ), (n * n).sqrt = n
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.isAlgebraic_field : ∀ {ι : Type u} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsTranscendenceBasis F x → Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (Set.range x))) E
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_false`. -/
Set.setOf_false : ∀ {α : Type u}, {_a | False} = ∅
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_reverse : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.le_def : ∀ {α : Type u_7} {a b : MeasurableSpace α}, a ≤ b ↔ MeasurableSpace.MeasurableSet' a ≤ MeasurableSpace.MeasurableSet' b
-- Mathlib.Order.Hom.BoundedLattice
/-- Special case of `map_sdiff` for Boolean algebras.  -/
map_sdiff' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  [inst_2 : FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a b : α), f (a \ b) = f a \ f b
-- Mathlib.Logic.Relation
Relation.map_onFun_le : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (f : α → β), Relation.Map (Function.onFun r f) f f ≤ r
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- **Alias** of `norm_add_sq`.

---

Expand the square  -/
norm_add_pow_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re (inner 𝕜 x y) + ‖y‖ ^ 2
-- Mathlib.MeasureTheory.Constructions.SimpleGraph
/-- A simple graph-valued map is measurable iff all induced adjacency maps are measurable.  -/
SimpleGraph.measurable_iff_adj : ∀ {V : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} {G : Ω → SimpleGraph V},
  Measurable G ↔ ∀ (u v : V), Measurable fun ω => (G ω).Adj u v
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.sub_snd : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β]
  (x y : WithLp p (α × β)), (x - y).snd = x.snd - y.snd
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `erase` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.eraseₘ : {α : Type u} →
  {β : α → Type v} → [Ord α] → α → (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Std.DTreeMap.Internal.Impl α β
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P →ₗ[R] Q)
  (f : N →ₗ[R] P), LinearMap.lTensor M (g ∘ₗ f) = LinearMap.lTensor M g ∘ₗ LinearMap.lTensor M f
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveMessageProps.mk.sizeOf_spec : ∀ (msg : Lean.Server.WithRpcRef Lean.MessageData), sizeOf { msg := msg } = 1 + sizeOf msg
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrRight_apply : ∀ {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [inst : (i : ι) → UniformSpace (β₁ i)]
  [inst_1 : (i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) (a : (i : ι) → β₁ i) (i : ι),
  (UniformEquiv.piCongrRight F) a i = (F i) (a i)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.Monadic.isPlausibleStep_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.IterM Id α}
  {step : Std.IterStep (Std.IterM Id α) α}, it.IsPlausibleStep step ↔ step = Std.Rxo.Iterator.Monadic.step it
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductColimit_desc : ∀ (X Y : Type u) (s : CategoryTheory.Limits.BinaryCofan X Y),
  (CategoryTheory.Limits.Types.binaryCoproductColimit X Y).desc s =
    TypeCat.ofHom (Sum.elim ⇑(CategoryTheory.ConcreteCategory.hom s.inl) ⇑(CategoryTheory.ConcreteCategory.hom s.inr))
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- If an initial object `0` exists in a CCC then every morphism from it is monic.  -/
CategoryTheory.initial_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {I : C}
  (B : C) (t : CategoryTheory.Limits.IsInitial I) [CategoryTheory.MonoidalClosed C], CategoryTheory.Mono (t.to B)
-- Mathlib.RingTheory.Ideal.Operations
/-- `Ideal.radical` as an `InfTopHom`, bundling in that it distributes over `inf`.  -/
Ideal.radicalInfTopHom : {R : Type u} → [inst : CommSemiring R] → InfTopHom (Ideal R) (Ideal R)
-- Mathlib.Data.ENat.Defs
/-- Extended natural numbers `ℕ∞ = WithTop ℕ`.  -/
«termℕ∞» : Lean.ParserDescr
-- Mathlib.GroupTheory.Congruence.Defs
/-- The smallest congruence relation containing a binary relation `r` is contained in any
congruence relation containing `r`.  -/
Con.conGen_le : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {c : Con M}, conGen r ≤ c ↔ r ≤ ⇑c
-- Lean.Util.MonadBacktrack
Lean.commitWhen : {m : Type → Type} →
  {s : Type} → {ε : Type u_1} → [Monad m] → [Lean.MonadBacktrack s m] → [MonadExcept ε m] → m Bool → m Bool
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  Function.Surjective HomotopicalAlgebra.BifibrantObject.toHoCat.obj
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.Context.mk.inj : ∀ {userName : Lean.Name} {explicitPatternVars : Array Lean.FVarId} {userName_1 : Lean.Name}
  {explicitPatternVars_1 : Array Lean.FVarId},
  { userName := userName, explicitPatternVars := explicitPatternVars } =
      { userName := userName_1, explicitPatternVars := explicitPatternVars_1 } →
    userName = userName_1 ∧ explicitPatternVars = explicitPatternVars_1
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.gc : ∀ {R : Type u_1} [inst : Ring R], GaloisConnection ⇑TwoSidedIdeal.fromIdeal ⇑TwoSidedIdeal.asIdeal
-- Mathlib.Algebra.Lie.Basic
LieEquiv.eq_symm_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) {x : L₂} {y : L₁}, y = e.symm x ↔ e y = x
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.mono_iff_ker_eq_bot : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y), CategoryTheory.Mono f ↔ (ModuleCat.Hom.hom f).ker = ⊥
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_of_subsingleton' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [Subsingleton 𝓧] [Nonempty 𝓨] [MeasureTheory.SFinite π],
  Measurable (Function.uncurry ℓ) → ProbabilityTheory.bayesRisk ℓ P π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given any `Finset` of objects `{X, ...}` and
indexed collection of `Finset`s of morphisms `{f, ...}` in `C`,
there exists an object `S`, with a morphism `T X : S ⟶ X` from each `X`,
such that the triangles commute: `T X ≫ f = T Y`, for `f : X ⟶ Y` in the `Finset`.
 -/
CategoryTheory.IsCofiltered.inf_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))),
  ∃ S T,
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp (T mX) f = T mY
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.getSimprocDeclKeys? : Lean.Name → Lean.CoreM (Option (Array Lean.Meta.SimpTheoremKey))
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.map_loops : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α → β} {hf : Set.InjOn f M.E}, (M.map f hf).loops = f '' M.loops
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getKey! a l = (Std.Internal.List.getKey? a l).get!
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.exists_isBasis_inter_ground_isBasis_closure : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_const_right' : ∀ {w b c : ℕ} {a : BitVec w}, a + BitVec.ofNat w b + BitVec.ofNat w c = BitVec.ofNat w b + BitVec.ofNat w c + a
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ioc_intCast : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α],
  ⋃ n, Set.Ioc (↑n) (↑n + 1) = Set.univ
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_cont_eq_h_one : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.conts 0 = { a := g.h, b := 1 }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
differentiableOn_iteratedDerivWithin_cotTerm : ∀ (n l : ℕ),
  DifferentiableOn ℂ (iteratedDerivWithin l (fun z => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet)
    UpperHalfPlane.upperHalfPlaneSet
-- Init.Data.Order.ClassesExtra
Std.LawfulOrderOrd.isGE_compare_eq_false : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] {a b : α}, (compare a b).isGE = false ↔ ¬b ≤ a
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex_isPrenex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n), φ.toPrenex.IsPrenex
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.add_add_add_comm : ∀ {S : Type u_3} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a d : S), a + b + (c + d) = a + c + (b + d)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_toArray_roc : ∀ {m n : ℤ}, (m<...=n).toArray.toList = (m<...=n).toList
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.helper : ∀ {w' : ℕ} (w : ℕ) (b : BitVec (w' + w)) (v : BitVec w'),
  b &&& BitVec.allOnes w' ++ 0#w = v ++ 0#w ↔ BitVec.extractLsb' w w' b = v
-- Mathlib.Algebra.Group.WithOne.Basic
AddEquiv.withZeroCongr_apply : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β) (a : WithZero α),
  e.withZeroCongr a = (WithZero.mapAddHom e.toAddHom) a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.right_nonuniformWitnesses_subset : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t → (G.nonuniformWitnesses ε s t).2 ⊆ t
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- The Hausdorff dimension of a nonempty convex set equals the dimension of its affine span.  -/
Real.Convex.dimH_eq_finrank_vectorSpan : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E},
  Convex ℝ s → s.Nonempty → dimH s = ↑(Module.finrank ℝ ↥(vectorSpan ℝ s))
-- Lean.Meta.Tactic.Grind.Cases
/-- A collection of `CasesTypes`.  -/
Lean.Meta.Grind.CasesTypesArray : Type
-- Mathlib.Tactic.CategoryTheory.Slice
/-- `slice_lhs a b => tac` zooms to the left-hand side, uses associativity for categorical
composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
 -/
Mathlib.Tactic.Slice.sliceLHS : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.CodescendsAlong.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C},
  (∀ {Z X Y A : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A},
      CategoryTheory.IsPushout f g inl inr → Q f → P inl → P g) →
    P.CodescendsAlong Q
-- Mathlib.Topology.Category.Compactum
/-- The monadic join.  -/
Compactum.join : (X : Compactum) → Ultrafilter (Ultrafilter X.A) → Ultrafilter X.A
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.instHasBinaryBiproductsOpposite : ∀ (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasBinaryBiproducts C], CategoryTheory.Limits.HasBinaryBiproducts Cᵒᵖ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`.  -/
VectorField.leibniz_identity_lieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E],
  minSmoothness 𝕜 2 ≤ n →
    ∀ {U V W : E → E} {x : E},
      ContDiffAt 𝕜 n U x →
        ContDiffAt 𝕜 n V x →
          ContDiffAt 𝕜 n W x →
            VectorField.lieBracket 𝕜 U (VectorField.lieBracket 𝕜 V W) x =
              VectorField.lieBracket 𝕜 (VectorField.lieBracket 𝕜 U V) W x +
                VectorField.lieBracket 𝕜 V (VectorField.lieBracket 𝕜 U W) x
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_self : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι), b.repr (b i) = fun₀ | i => 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The group homology of a `k`-linear `G`-representation `A`, as the homology of its complex
of inhomogeneous chains.  -/
groupHomology : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ℕ → ModuleCat k
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The type of cusp orbits of `𝒢`, i.e. orbits for the action of `𝒢` on its own cusps.  -/
CuspOrbits : Subgroup (GL (Fin 2) ℝ) → Type
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_map : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (n : ℕ) (s : Finset α),
  Finset.powersetCard n (Finset.map f s) = Finset.map (Finset.mapEmbedding f).toEmbedding (Finset.powersetCard n s)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_smul : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (r : R) (a : A), D (r • a) = r • D a
-- Init.Data.BitVec.Lemmas
BitVec.not_sshiftRight_not : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, ~~~(~~~x).sshiftRight n = x.sshiftRight n
-- Mathlib.Combinatorics.Quiver.Path
Quiver.instIsPreorderReachable : ∀ {V : Type u} [inst : Quiver V], IsPreorder V Quiver.Reachable
-- Init.Internal.Order.Lemmas
Array.foldlM.loop.induct : ∀ {α : Type u} {β : Type v} (as : Array α),
  ∀ stop ≤ as.size,
    ∀ (motive : ℕ → ℕ → β → Prop),
      (∀ (j : ℕ) (b : β), j < stop → motive 0 j b) →
        (∀ (j : ℕ) (b : β),
            j < stop →
              ∀ (i' : ℕ), j < as.size → (∀ (__do_lift : β), motive i' (j + 1) __do_lift) → motive i'.succ j b) →
          (∀ (t j : ℕ) (b : β), ¬j < stop → motive t j b) → ∀ (i j : ℕ) (b : β), motive i j b
-- Mathlib.Tactic.DuplicateDecls
/-- Search for duplicate theorems.  -/
Mathlib.Tactic.DuplicateDecls.Target.theorems : Mathlib.Tactic.DuplicateDecls.Target
-- Lean.Environment
Lean.EffectiveImport.mk.sizeOf_spec : ∀ (toImport : Lean.Import) (irPhases : Lean.IRPhases) (hasData : Bool),
  sizeOf { toImport := toImport, irPhases := irPhases, hasData := hasData } =
    1 + sizeOf toImport + sizeOf irPhases + sizeOf hasData
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Return the immediate prefix of `n` (if any).  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Lean.Name.prefix? : Lean.Name → Option Lean.Name
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_pos_iff_one_lt : ∀ {n : ℕ}, 0 < ArithmeticFunction.cardFactors n ↔ 1 < n
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), (s.restrict S hS).exradius = s.exradius
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.quasicoherentData_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat}
  [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_4 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation),
  P.quasicoherentData.I = C
-- Lean.Expr
/-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`.  -/
Lean.Expr.isAppOf : Lean.Expr → Lean.Name → Bool
-- Batteries.Data.Vector.Lemmas
Vector.finIdxOf?_eq_some_iff : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {v : Vector α n} {a : α} {i : Fin n},
  v.finIdxOf? a = some i ↔ v.get i = a ∧ ∀ j < i, ¬v.get j = a
-- Mathlib.Data.NNRat.Defs
NNRat.instOrderBot : OrderBot ℚ≥0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.commute_of_mem_adjoin_of_forall_mem_commute : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {a b : A} {s : Set A},
  b ∈ NonUnitalAlgebra.adjoin R s → (∀ b ∈ s, Commute a b) → Commute a b
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.SMulMemClass.subtype_apply : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] {S' : A} (x : ↥S'), (SubMulAction.SMulMemClass.subtype S') x = ↑x
-- Init.Data.SInt.Basic
instMulISize : Mul ISize
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_lt_iff_lt_of_lt_aleph0 : ∀ {c d : Cardinal.{u}}, c < Cardinal.aleph0 → d < Cardinal.aleph0 → (Cardinal.toNat c < Cardinal.toNat d ↔ c < d)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inclusion map is injective.  -/
AddGroupExtension.inl_injective : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (self : AddGroupExtension N E G), Function.Injective ⇑self.inl
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_sliceTo_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p < p₀.sliceTo q h ↔ String.Slice.Pos.ofSliceTo p < q
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.elab : Lean.TSyntax `Aesop.builder_option → Aesop.ElabM Aesop.Frontend.BuilderOption
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasse_preconnected_of_pred : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α], (SimpleGraph.hasse α).Preconnected
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryBiproductData_bicone_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂)
  (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃)
  (fst : T.obj₂ ⟶ T.obj₁)
  (total :
    CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr =
      CategoryTheory.CategoryStruct.id T.obj₂),
  (CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inr = inr