mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
/-- The identity map from a type with zero to itself.  -/
ZeroHom.id : (M : Type u_10) → [inst : Zero M] → ZeroHom M M
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- Every local site has a canonical point, given as a fibre functor by the coyoneda embedding of
the terminal object `⊤_ C`.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.point : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) → [CategoryTheory.LocallySmall.{w, v, u} C] → [J.IsLocalSite] → J.Point
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See also `pow_right_strictMono'`.  -/
pow_right_strictMono₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀], 1 < a → StrictMono fun x => a ^ x
-- Mathlib.Data.Multiset.Defs
/-- `Multiset α` is the quotient of `List α` by list permutation. The result
is a type of finite sets with duplicates allowed.  -/
Multiset : Type u → Type u
-- Mathlib.RingTheory.IntegralDomain
/-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.
 -/
sum_hom_units_eq_zero : ∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Group G] [inst_3 : Fintype G] (f : G →* R),
  f ≠ 1 → ∑ g, f g = 0
-- Mathlib.RingTheory.Nakayama
Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  {N : Submodule R M}, N.FG → N = r • N → r ∈ N.annihilator.jacobson → N = ⊥
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Bool}, (↑m).WF → (↑(Std.DHashMap.Internal.Raw₀.filter f m)).size ≤ (↑m).size
-- Mathlib.Data.Set.Function
/-- If `f` maps `s` to `t` and `s` is non-empty, `t` is non-empty.  -/
Set.MapsTo.nonempty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t → s.Nonempty → t.Nonempty
-- Mathlib.Order.Concept
Order.IsExtent.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α), Order.IsExtent r s = (s ∈ Set.range (lowerPolar r))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Y W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g h)) h_1
-- Mathlib.Topology.Hom.Open
/-- `simp`-normal form of `toFun_eq_coe`.  -/
ContinuousOpenMap.coe_toContinuousMap : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α →CO β),
  ⇑f.toContinuousMap = ⇑f
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsMaximal.mem_iff_models : ∀ {L : FirstOrder.Language} {T : L.Theory}, T.IsMaximal → ∀ (φ : L.Sentence), φ ∈ T ↔ T ⊨ᵇ φ
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_of_lt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a b → Std.PRange.UpwardEnumerable.LE a b
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- One direction of `CliffordAlgebra.evenEquivEvenNeg`  -/
CliffordAlgebra.evenToNeg : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q Q' : QuadraticForm R M) → Q' = -Q → ↥(CliffordAlgebra.even Q) →ₐ[R] ↥(CliffordAlgebra.even Q')
-- Mathlib.Order.RelClasses
LE.total' : ∀ {α : Type u} [inst : LinearOrder α], Std.Total fun x1 x2 => x2 ≤ x1
-- Mathlib.Order.PropInstances
Pi.instSymmTopForallForallProp : ∀ (α : Type u_4), Std.Symm ⊤
-- Mathlib.CategoryTheory.Shift.CommShift
/-- If `F : C ⥤ D` is a fully faithful functor which is used
to construct a shift by `A` on `C` from a shift on `D`,
then the functor `F` itself commutes with the shift by `A`.  -/
CategoryTheory.Functor.CommShift.ofHasShiftOfFullyFaithful : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_4} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F : CategoryTheory.Functor C D} →
                (hF : F.FullyFaithful) →
                  (s : A → CategoryTheory.Functor C C) →
                    (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) → F.CommShift A
-- Init.Data.RArray
/-- A `RArray` can model `Fin n → α` or `Array α`, but is optimized for a fast kernel-reducible `get`
operation.

The primary intended use case is the “denote” function of a typical proof by reflection proof, where
only the `get` operation is necessary. It is not suitable as a general-purpose data structure.

There is no well-formedness invariant attached to this data structure, to keep it concise; it's
semantics is given through `RArray.get`. In that way one can also view an `RArray` as a decision
tree implementing `Nat → α`.

See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for functions that construct an
`RArray`.
 -/
Lean.RArray : Type u → Type u
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.StdSimplex.map_join : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {N : Type u_10}
  [inst_2 : IsStrictOrderedRing R] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) (g : M → N),
  Convexity.StdSimplex.map g f.join = (Convexity.StdSimplex.map (fun x => Convexity.StdSimplex.map g x) f).join
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_simple_comm : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E),
  IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯ = IntermediateField.restrictScalars F (↥F⟮β⟯)⟮α⟯
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.skipPrefixWhile_char_eq_skipPrefixWhile_beq : ∀ {c : Char} {s : String.Slice}, s.skipPrefixWhile c = s.skipPrefixWhile fun x => x == c
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Iic_add_zero_comm : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∑ i ≤ a + 1, f i = f (a + 1) + ∑ i ≤ a, f i
-- Mathlib.NumberTheory.ModularForms.Petersson
SlashInvariantFormClass.petersson_smul : ∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] {k : ℤ}
  {g : GL (Fin 2) ℝ} {τ : UpperHalfPlane} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [SlashInvariantFormClass F Γ k]
  {f : F} [SlashInvariantFormClass F' Γ k] {f' : F'},
  g ∈ Γ → UpperHalfPlane.petersson k (⇑f) (⇑f') (g • τ) = UpperHalfPlane.petersson k (⇑f) (⇑f') τ
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1 : ∀ {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] {P : Ideal R} [inst_4 : P.IsPrime] [inst_5 : Algebra S T] [inst_6 : Algebra R T]
  [inst_7 : IsScalarTower R S T],
  IsScalarTower R (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
    (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.default.sizeOf_spec : sizeOf Aesop.Frontend.DBuilderName.default = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_pi_single : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : (a : ι) → AddCommMonoid (M a)] (a : ι)
  (f : (a : ι) → M a) (s : Finset ι), ∑ a' ∈ s, Pi.single a' (f a') a = if a ∈ s then f a else 0
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_apply : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A]
  [inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)] (r r' : DirectSum ι fun i => ↥(A i)) (n : ι),
  ↑((r * r') n) = ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)
-- Init.Data.List.Impl
List.eraseP.eq_def : ∀ {α : Type u} (p : α → Bool) (x : List α),
  List.eraseP p x =
    match x with
    | [] => []
    | a :: l => bif p a then l else a :: List.eraseP p l
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The homology in degree `i` of a homological complex.  -/
HomologicalComplex.homology : {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 : ι) → [K.HasHomology i] → C
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
CategoryTheory.bijection.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory D] [inst_6 : CategoryTheory.ExponentialIdeal i]
  [inst_7 : CategoryTheory.BraidedCategory C] (A B : C) (X : D),
  CategoryTheory.bijection i A B X =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans
                        ((CategoryTheory.reflectorAdjunction i).homEquiv
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj A B) X)
                        ((β_ A B).homCongr (CategoryTheory.Iso.refl (i.obj X))))
                      ((CategoryTheory.ihom.adjunction B).homEquiv A (i.obj X)))
                    (CategoryTheory.unitCompPartialBijective A ⋯))
                  ((CategoryTheory.ihom.adjunction B).homEquiv (i.obj ((CategoryTheory.reflector i).obj A))
                      (i.obj X)).symm)
                ((β_ B (i.obj ((CategoryTheory.reflector i).obj A))).homCongr (CategoryTheory.Iso.refl (i.obj X))))
              ((CategoryTheory.ihom.adjunction (i.obj ((CategoryTheory.reflector i).obj A))).homEquiv B (i.obj X)))
            (CategoryTheory.unitCompPartialBijective B ⋯))
          ((CategoryTheory.ihom.adjunction (i.obj ((CategoryTheory.reflector i).obj A))).homEquiv
              (i.obj ((CategoryTheory.reflector i).obj B)) (i.obj X)).symm)
        ((CategoryTheory.CartesianMonoidalCategory.prodComparisonIso i ((CategoryTheory.reflector i).obj A)
                ((CategoryTheory.reflector i).obj B)).symm.homCongr
          (CategoryTheory.Iso.refl (i.obj X))))
      i.fullyFaithfulOfReflective.homEquiv.symm
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.continuous_extension : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀],
  Continuous Valued.extension
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [inst_4 : Std.PRange.InfinitelyUpwardEnumerable α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] [inst_6 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {lo : α},
  (Std.PRange.succ lo)<...*.toList = List.map Std.PRange.succ lo<...*.toList
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instContinuousAddOfLocallyCompactSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [LocallyCompactSpace α]
  [inst_3 : Add β] [inst_4 : ContinuousAdd β], ContinuousAdd C(α, β)
-- Mathlib.Control.Fold
/-- Conceptually, `toList` collects all the elements of a collection
in a list. This idea is formalized by

  `lemma toList_spec (x : t α) : toList x = foldMap FreeMonoid.mk x`.

The definition of `toList` is based on `foldl` and `List.cons` for
speed. It is faster than using `foldMap FreeMonoid.mk` because, by
using `foldl` and `List.cons`, each insertion is done in constant
time. As a consequence, `toList` performs in linear.

On the other hand, `foldMap FreeMonoid.mk` creates a singleton list
around each element and concatenates all the resulting lists. In
`xs ++ ys`, concatenation takes a time proportional to `length xs`. Since
the order in which concatenation is evaluated is unspecified, nothing
prevents each element of the traversable to be appended at the end
`xs ++ [x]` which would yield a `O(n²)` run time.  -/
Traversable.toList : {α : Type u} → {t : Type u → Type u} → [Traversable t] → t α → List α
-- Mathlib.Topology.UniformSpace.Basic
AddOpposite.uniformContinuous_unop : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous AddOpposite.unop
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- `padicNorm p q` takes discrete values `p ^ -z` for `z : ℤ`.  -/
padicNorm.values_discrete : ∀ {p : ℕ} {q : ℚ}, q ≠ 0 → ∃ z, padicNorm p q = ↑p ^ (-z)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.hom_ext : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {M : Type u_3} [inst_1 : Monoid M]
  {f g : HNNExtension G A B φ →* M},
  f.comp HNNExtension.of = g.comp HNNExtension.of → f HNNExtension.t = g HNNExtension.t → f = g
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_iSup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Type u_5} {f : M →ₙ+ N},
  Function.Surjective ⇑f →
    ∀ (S : ι → AddSubsemigroup N), AddSubsemigroup.map f (⨆ i, AddSubsemigroup.comap f (S i)) = iSup S
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instPartialOrderAddUnits.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : PartialOrder α],
  AddUnits.instPartialOrderAddUnits = PartialOrder.lift AddUnits.val ⋯
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.id.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.id X) = 1 + sizeOf X
-- Mathlib.AlgebraicGeometry.Properties
/-- A scheme `X` is integral if its is nonempty,
and `𝒪ₓ(U)` is an integral domain for each `U ≠ ∅`.  -/
AlgebraicGeometry.IsIntegral : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Data.List.Basic
List.getLast_singleton' : ∀ {α : Type u} (a : α), [a].getLast ⋯ = a
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.nonDegenerateEquiv_apply_apply : ∀ {n d : ℕ} (s : ↑((SSet.stdSimplex.obj { len := n }).nonDegenerate d)) (a : Fin (d + 1)),
  (SSet.stdSimplex.nonDegenerateEquiv s) a = ↑s a
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- If `H` is a characteristic subgroup of `G` and `K` is a characteristic subgroup of `H`, then
`K` is a characteristic subgroup of `G`.  -/
Subgroup.characteristic_of_characteristic_of_characteristic : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [H.Characteristic] {K : Subgroup ↥H} [hK : K.Characteristic],
  (Subgroup.map H.subtype K).Characteristic
-- Mathlib.Algebra.Quaternion
Cardinal.mk_quaternion_of_infinite : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] [Infinite R],
  Cardinal.mk (Quaternion R) = Cardinal.mk R
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_baseChange : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (A : Type u_8) [inst_9 : CommRing A]
  [inst_10 : Algebra R A],
  (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpolyAux (Algebra.TensorProduct.basis A b)
      (Algebra.TensorProduct.basis A bₘ) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b bₘ)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.instMonadTraverserFormatterM : Lean.Syntax.MonadTraverser Lean.PrettyPrinter.FormatterM
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.posLT.eq_1 : ∀ (s : String) (offset : String.Pos.Raw) (h : 0 < offset),
  s.posLT offset h = String.Pos.ofToSlice (s.toSlice.posLT offset h)
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instIteratorLoop : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {n : Type u_3 → Type u_4} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Std.IteratorAccess α m] →
          [inst_2 : Monad m] → [Monad n] → Std.IteratorLoop (Std.Iterators.Types.StepSizeIterator α m β) m n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅.getKey? a = none
-- Mathlib.Algebra.Group.ULift
ULift.addMonoid : {α : Type u} → [AddMonoid α] → AddMonoid (ULift.{u_1, u} α)
-- Init.Data.Array.Attach
Array.mem_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} {H : ∀ a ∈ xs, p a} {b : β},
  b ∈ Array.pmap f xs H ↔ ∃ a, ∃ (h : a ∈ xs), f a ⋯ = b
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_fun_inv'' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → c x ≠ 0 → deriv (fun x => (c x)⁻¹) x = -deriv c x / c x ^ 2
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.toModuleCat_map : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  {X Y : ModuleCat (Matrix ι ι R)} (f : X ⟶ Y),
  (MatrixModCat.toModuleCat R i).map f = ModuleCat.ofHom (MatrixModCat.fromMatrixLinear i (ModuleCat.Hom.hom f))
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwInfo.mk : Lean.Expr →
  Lean.Expr →
    Option Lean.Expr →
      Array Mathlib.Tactic.ClickSuggestions.GrwPos →
        Mathlib.Tactic.ClickSuggestions.RwKind → Mathlib.Tactic.ClickSuggestions.GrwInfo
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.mk : Array Lean.Meta.Grind.TParam → Array Lean.Meta.Grind.TAnchor✝ → Bool → Lean.Meta.Grind.Collector.State✝
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.pos_of_floor_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 < ⌊a⌋₊ → 0 < a
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsMulTorsionFree.pow_right_inj₀ : ∀ {M : Type u_2} [inst : MonoidWithZero M] [IsLeftCancelMulZero M] [IsMulTorsionFree M] {x : M},
  x ≠ 1 → x ≠ 0 → ∀ {n m : ℕ}, x ^ n = x ^ m ↔ n = m
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Roi.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Roi.HasRcoIntersection α}
  [self : Std.Roi.LawfulRcoIntersection α] {a : α} {r : Std.Roi α} {s : Std.Rco α},
  a ∈ Std.Roi.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectEpimorphisms.epi_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectEpimorphisms F →
    ∀ [∀ (i : I), (F i).PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Epi f ↔ ∀ (i : I), CategoryTheory.Epi ((F i).map f)
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_6.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : Array (IO.Ref Aesop.GoalUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_6 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_9 t (Aesop.GoalUnsafe.brecOn_6.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Std.Time.Date.Unit.Weekday
Std.Time.instDecidableEqWeekday : DecidableEq Std.Time.Weekday
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.isoSourceOfSelf_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  (CategoryTheory.Limits.equalizer.isoSourceOfSelf f).hom = CategoryTheory.Limits.equalizer.ι f f
-- Mathlib.Data.Set.Lattice
Set.union_eq_iUnion : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ∪ s₂ = ⋃ b, bif b then s₁ else s₂
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.addSubgroupOf_normalizer_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H N : AddSubgroup G},
  H ≤ N → (AddSubgroup.normalizer ↑H).addSubgroupOf N = AddSubgroup.normalizer ↑(H.addSubgroupOf N)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.comp_aeval_relation_inl : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T] (r : σ'),
  (MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val))) ((Q.comp P).relation (Sum.inl r)) =
    Q.relation r