mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ⟶ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
        CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.inv_mem_valueGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B) {b : Bˣ},
  ↑b ∈ Set.range ⇑f → b⁻¹ ∈ f.valueGroup
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAtFun_inj : ∀ {N : ℕ}, Function.Injective (Polynomial.revAtFun N)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The **Hellinger--Toeplitz theorem**: Construct a self-adjoint operator from an everywhere
defined symmetric operator.  -/
LinearMap.IsSymmetric.toSelfAdjoint : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] → {T : E →ₗ[𝕜] E} → T.IsSymmetric → ↥(selfAdjoint (E →L[𝕜] E))
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- A subgroup is either the trivial subgroup or nontrivial.  -/
Subgroup.bot_or_nontrivial : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ∨ Nontrivial ↥H
-- Mathlib.Algebra.Group.Semiconj.Basic
SemiconjBy.inv_inv_symm_iff : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.idealOfLE_self : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.idealOfLE A ⋯ = IsLocalRing.maximalIdeal ↥A
-- Mathlib.Algebra.Group.Units.Defs
Subsingleton.units_of_isUnit : ∀ {M : Type u_1} [inst : Monoid M], (∀ (a : M), IsUnit a → a = 1) → Subsingleton Mˣ
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWithTR.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Array γ) (a_1 : α) (as : List α) (b : β)
  (bs : List β), List.zipWithTR.go✝ f (a_1 :: as) (b :: bs) a = List.zipWithTR.go✝ f as bs (a.push (f a_1 b))
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_coe : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (l : List α), Multiset.filterMap f ↑l = ↑(List.filterMap f l)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_biUnion_partition : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  (∀ J ∈ π, (πi J).IsPartition) →
    BoxIntegral.integralSum f vol (π.biUnionPrepartition πi) = BoxIntegral.integralSum f vol π
-- Mathlib.Algebra.Module.Torsion.Free
smul_eq_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r • m = 0 ↔ r = 0 ∨ m = 0
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0),
  R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CochainComplex.HomComplex.CohomologyClass.mk
      (CochainComplex.HomComplex.Cocycle.toSingleMk
        (CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso (-↑n) n ⋯).hom f) ⋯ (-↑m) ⋯ ⋯)
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_nsmul : ∀ {M : Type u_10} {F : Type u_11} [inst : AddMonoid M] [inst_1 : FunLike F M M] [AddMonoidHomClass F M M] (f : F)
  (n : ℕ) (x : M) (k : ℕ), (⇑f)^[n] (k • x) = k • (⇑f)^[n] x
-- Lean.Data.Lsp.Basic
Lean.Lsp.ProgressParams.mk.inj : ∀ {α : Type} {token : Lean.Lsp.ProgressToken} {value : α} {token_1 : Lean.Lsp.ProgressToken} {value_1 : α},
  { token := token, value := value } = { token := token_1, value := value_1 } → token = token_1 ∧ value = value_1
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Cont.eval.match_1.splitter : (motive : Turing.ToPartrec.Cont → Sort u_1) →
  (x : Turing.ToPartrec.Cont) →
    (Unit → motive Turing.ToPartrec.Cont.halt) →
      ((fs : Turing.ToPartrec.Code) →
          (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k)) →
        ((ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k)) →
          ((f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k)) →
            ((f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)) →
              motive x
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  CategoryTheory.NatIso.op F.rightUnitor =
    F.op.rightUnitor.symm ≪≫
      F.op.isoWhiskerLeft (CategoryTheory.Functor.opId D).symm ≪≫ (F.opComp (CategoryTheory.Functor.id D)).symm
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.isEquivalent_nat_floor : ∀ {R : Type u_1} [inst : NormedField R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R]
  [inst_4 : FloorRing R], Asymptotics.IsEquivalent Filter.atTop (fun x => ↑⌊x⌋₊) fun x => x
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.replaceFTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (acc : Array α) (h_1 : (acc : Array α) → motive [] acc)
  (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | x :: xs, acc => h_2 x xs acc) =
    h_1 acc
-- Init.Data.String.Lemmas.FindPos
String.posLT_lt_iff : ∀ {s : String} {p : String.Pos.Raw} {h : 0 < p} {q : s.Pos}, s.posLT p h < q ↔ p ≤ q.offset
-- Init.Data.Range.Polymorphic.Iterators
Std.Rio.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LT α] →
        [inst_2 : DecidableLT α] →
          [inst_3 : Std.PRange.Least? α] →
            [Std.PRange.LawfulUpwardEnumerable α] →
              [Std.PRange.LawfulUpwardEnumerableLT α] →
                [Std.PRange.LawfulUpwardEnumerableLeast? α] →
                  [Monad m] → [Std.Iterators.Finite (Std.Rxo.Iterator α) Id] → ForIn' m (Std.Rio α) α inferInstance
-- Std.Sat.AIG.Basic
Std.Sat.AIG.BinaryInput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (lhs rhs lhs_1 rhs_1 : aig.Ref),
  ({ lhs := lhs, rhs := rhs } = { lhs := lhs_1, rhs := rhs_1 }) = (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Algebra.Regular.SMul
/-- The element `0` is `M`-regular if and only if `M` is trivial.  -/
IsSMulRegular.zero_iff_subsingleton : ∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M],
  IsSMulRegular M 0 ↔ Subsingleton M
-- Init.Data.List.Nat.Basic
List.append_eq_append_iff_of_size_eq_left : ∀ {α : Type u_1} {ws xs ys zs : List α}, ws.length = xs.length → (ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs)
-- Mathlib.Order.BoundedOrder.Basic
top_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [Nontrivial α], ⊤ ≠ ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] [T0Space α] {γ : β → Type u_4} {f : (b : β) × γ b → α},
  Summable f → ∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCohomologyRelation.refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (γ : CategoryTheory.PresheafOfGroups.OneCochain G U),
  CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ γ 1
-- Init.Data.Order.Ord
Std.OrientedCmp.not_gt_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.gt → cmp b a ≠ Ordering.gt
-- Lean.Meta.Sym.Pattern
/-- Creates a `Pattern` from a theorem, using the supplied selection function to extract the key from
the theorem's result type.

This function is used to implement `mkEqPatternFromDecl`.
Like `mkPatternFromDecl`, this strips all leading universal quantifiers, recording variable
types and instance status. However, instead of using the entire resulting type as the pattern,
it uses the selection function to extract the key.

For a theorem `∀ x₁ ... xₙ, type`, returns a pattern matching the first component of `selectKey type`
with `n` pattern variables.
 -/
Lean.Meta.Sym.mkPatternFromDeclWithKey : {α : Type} →
  Lean.Name → (Lean.Expr → Lean.MetaM (Lean.Expr × α)) → optParam Bool false → Lean.MetaM (Lean.Meta.Sym.Pattern × α)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The induced functor `FibrantObject.HoCat C ⥤ D`, when `D` is a localization
of `C` with respect to weak equivalences.  -/
HomotopicalAlgebra.FibrantObject.HoCat.toLocalization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject.HoCat C) D
-- Lean.Parser.Command
Lean.Parser.Command.checkAssertions.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.clm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {n : WithTop ℕ∞} {f : E → F →L[𝕜] G}
  {g : E → F}, ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => (f x) (g x)) s
-- Lean.Attributes
Lean.TagAttribute.mk.inj : ∀ {attr : Lean.AttributeImpl} {ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet}
  {attr_1 : Lean.AttributeImpl} {ext_1 : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet},
  { attr := attr, ext := ext } = { attr := attr_1, ext := ext_1 } → attr = attr_1 ∧ ext = ext_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ordered_keys_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a.fst b.fst = Ordering.lt) t.toList
-- Mathlib.Algebra.Order.Field.GeomSum
geom_sum_Ico_le_of_lt_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {x : K} {m n : ℕ},
  0 ≤ x → x < 1 → ∑ i ∈ Finset.Ico m n, x ^ i ≤ x ^ m / (1 - x)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (a : ↑e.target), ↑(e.toHomeomorphSourceTarget.symm a) = ↑e.symm ↑a
-- Init.Data.List.Lemmas
List.foldl_eq_foldlM : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {l : List α},
  List.foldl f b l = (List.foldlM (fun x1 x2 => pure (f x1 x2)) b l).run
-- Mathlib.Topology.LocallyFinite
locallyFinite_of_finite : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] [Finite ι] (f : ι → Set X), LocallyFinite f
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- Gradient of `f` at the point `x`, if it exists.  Zero otherwise.
Denoted as `∇` within the Gradient namespace.

If the derivative exists (i.e., `∃ f', HasGradientAt f f' x`), then
`f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` where `x'` converges to `x`.  -/
gradient : {𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → F → F
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.atMostFn : ℕ → Lean.Parser.ParserFn → String → Lean.Parser.ParserFn
-- Init.PropLemmas
/-- As `simp` does not index foralls, this `@[simp]` lemma is tried on every `forall` expression.
This is not ideal, and likely a performance issue, but it is difficult to remove this attribute at this time.
 -/
forall_exists_index : ∀ {α : Sort u_1} {p : α → Prop} {q : (∃ x, p x) → Prop}, (∀ (h : ∃ x, p x), q h) ↔ ∀ (x : α) (h : p x), q ⋯
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricVAdd.isometry_vadd : ∀ {M : Type u} (X : Type w) {inst : PseudoEMetricSpace X} {inst_1 : VAdd M X} [self : IsIsometricVAdd M X] (c : M),
  Isometry fun x => c +ᵥ x
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Composition of partial equivs respects equivalence.  -/
PartialEquiv.EqOnSource.trans' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e e' : PartialEquiv α β} {f f' : PartialEquiv β γ},
  e ≈ e' → f ≈ f' → e.trans f ≈ e'.trans f'
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- If a real-valued function has bounded variation on a set, then it is a difference of monotone
functions there.  -/
LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s → ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.insertIdx_loop_toArray : ∀ {α : Type u_1} (i : ℕ) (l : List α) (j : ℕ) (hj : j < l.toArray.size),
  i ≤ j →
    Array.insertIdx.loop✝ i l.toArray ⟨j, hj⟩ =
      (List.take i l ++ l[j] :: List.drop i (List.take j l) ++ List.drop (j + 1) l).toArray
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_extension₂ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] (f : α → β → γ) [CompleteSpace γ], UniformContinuous₂ (UniformSpace.Completion.extension₂ f)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k a : α},
  (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
-- Mathlib.Data.Fin.Tuple.Basic
Fin.contractNth_apply_of_ne : ∀ {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
  ↑j ≠ ↑k → j.contractNth op g k = g (j.succAbove k)
-- Mathlib.Algebra.Module.NatInt
/-- Convert back any exotic `ℤ`-smul to the canonical instance. This should not be needed since in
mathlib all `AddCommGroup`s should normally have exactly one `ℤ`-module structure by design.  -/
int_smul_eq_zsmul : ∀ {M : Type u_3} [inst : AddCommGroup M] (h : Module ℤ M) (n : ℤ) (x : M), SMul.smul n x = n • x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → γ} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.map f m) k = Option.map (f k) (Std.ExtDHashMap.Const.get? m k)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α}, (a +ᵥ s).Nonempty ↔ s.Nonempty
-- Mathlib.Data.Nat.Factorial.Basic
Nat.pow_sub_le_descFactorial : ∀ (n k : ℕ), (n + 1 - k) ^ k ≤ n.descFactorial k
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- `K.cycles i` is the kernel of `K.d i j` when `c.next i = j`.  -/
HomologicalComplex.cyclesIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) →
              [inst_2 : K.HasHomology i] →
                c.next i = j → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (K.iCycles i) ⋯)
-- Init.Data.Range.Polymorphic.NatLemmas
Std.PRange.Nat.toList_rco_succ_succ : ∀ {m n : ℕ}, ((m + 1)...n + 1).toList = List.map (fun x => x + 1) (m...n).toList
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.subtypeₐᵢ_linearIsometry : ∀ {𝕜 : 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] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s], s.subtypeₐᵢ.linearIsometry = s.direction.subtypeₗᵢ
-- Aesop.Forward.State
Aesop.ClusterState.mk.sizeOf_spec : ∀ (slots : Array Aesop.Slot) (conclusionDeps : Array Aesop.PremiseIndex) (variableMap : Aesop.VariableMap)
  (completeMatches : Lean.PHashSet Aesop.Match) (haveHypForEachSlot : Bool) (slotQueues : Array (Array Aesop.RawHyp))
  (slotQueues_size : slotQueues.size = slots.size),
  sizeOf
      { slots := slots, conclusionDeps := conclusionDeps, variableMap := variableMap,
        completeMatches := completeMatches, haveHypForEachSlot := haveHypForEachSlot, slotQueues := slotQueues,
        slotQueues_size := slotQueues_size } =
    1 + sizeOf slots + sizeOf conclusionDeps + sizeOf variableMap + sizeOf completeMatches + sizeOf haveHypForEachSlot +
        sizeOf slotQueues +
      sizeOf slotQueues_size
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_unitClosedBall_eq_addHaar_unitBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  μ (Metric.closedBall 0 1) = μ (Metric.ball 0 1)
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwiseDisjoint_prod_left : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : Order.Frame α] {s : Set ι} {t : Set ι'} {f : ι × ι' → α},
  (s ×ˢ t).PairwiseDisjoint f ↔
    (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.smul_def' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Matrix ι ι R) (v : ι → M), N • v = ∑ j, fun i => N i j • v j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {km : α} {hc : Std.DTreeMap.Internal.Impl.contains km t = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.toSchauderBasis_basis : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (b : HilbertBasis ℕ 𝕜 E) (a : ℕ), ↑b.toSchauderBasis a = b a
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_bijective : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N], Function.Bijective AddEquiv.symm
-- Mathlib.Algebra.Lie.Weights.Linear
/-- See `LieModule.exists_nontrivial_weightSpace_of_isSolvable` for the variant that
only assumes that `L` is solvable but additionally requires `k` to be of characteristic zero.  -/
LieModule.exists_nontrivial_weightSpace_of_isNilpotent : ∀ (k : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : LieRing.IsNilpotent L] [inst_4 : Field k] [inst_5 : LieAlgebra k L] [inst_6 : Module k M]
  [Module.Finite k M] [inst_8 : LieModule k L M] [LieModule.LinearWeights k L M] [LieModule.IsTriangularizable k L M]
  [Nontrivial M], ∃ χ, Nontrivial ↥(LieModule.weightSpace M ⇑χ)
-- Mathlib.Topology.MetricSpace.Holder
holderWith_id : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X], HolderWith 1 1 id
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instConcreteCategoryAddHomCarrier.eq_1 : AddSemigrp.instConcreteCategoryAddHomCarrier =
  { hom := fun {X Y} => AddSemigrp.Hom.hom', ofHom := fun {X Y} => AddSemigrp.Hom.mk✝,
    hom_ofHom := @AddSemigrp.instConcreteCategoryAddHomCarrier._proof_1,
    ofHom_hom := @AddSemigrp.instConcreteCategoryAddHomCarrier._proof_2,
    id_apply := @AddSemigrp.instConcreteCategoryAddHomCarrier._proof_3,
    comp_apply := @AddSemigrp.instConcreteCategoryAddHomCarrier._proof_4 }
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X`
will be a limit cone.  -/
CategoryTheory.Limits.IsLimit.OfNatIso.limitCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → {X : C} → F.cones.RepresentableBy X → CategoryTheory.Limits.Cone F
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_four : ∀ {c : Char} (h : c.utf8Size = 4),
  (String.utf8EncodeChar c)[0].toBitVec = 30#5 ++ BitVec.extractLsb' 18 3 c.val.toBitVec
-- Init.Data.String.PosRaw
String.Pos.Raw.le_dec : ∀ {p q : String.Pos.Raw}, q ≠ 0 → (p ≤ q.dec ↔ p < q)
-- Mathlib.Data.Set.Lattice
Set.disjoint_sUnion_left : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The isomorphism `K.opcycles i ≅ L.opcycles i` induced by an isomorphism
in `HomologicalComplex`.  -/
HomologicalComplex.opcyclesMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            (K ≅ L) → (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.opcycles i ≅ L.opcycles i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a t = true → (List.map Sigma.fst l).contains a = false) →
      (↑(t.insertMany l ⋯)).size = t.size + l.length
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_nsmul_assoc : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → ℕ) (a : M),
  ∑ i ∈ s, f i • a = (∑ i ∈ s, f i) • a
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_to_continuousMap : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q), ⇑↑f = ⇑f
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_zero_iff_zero : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) (x : ↥L'), ↑x = 0 ↔ x = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ofList_cons : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} {v : β} {tl : List (α × β)},
  Std.TreeMap.Raw.ofList ((k, v) :: tl) cmp = (∅.insert k v).insertMany tl