mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Diagonal
/-- `diagonal d` is the square matrix such that `(diagonal d) i i = d i` and `(diagonal d) i j = 0`
if `i ≠ j`.

Note that bundled versions exist as:
* `Matrix.diagonalAddMonoidHom`
* `Matrix.diagonalLinearMap`
* `Matrix.diagonalRingHom`
* `Matrix.diagonalAlgHom`
 -/
Matrix.diagonal : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [Zero α] → (n → α) → Matrix n n α
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.vsub_apply : ∀ {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] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] (f g : P →ᴬ[R] Q) (p : P),
  (f -ᵥ g) p = f p -ᵥ g p
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of an integrable function is smaller than its integral,
while avoiding a null set.  -/
MeasureTheory.exists_notMem_null_le_integral : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → μ N = 0 → ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ
-- Std.Data.String.ToNat
String.Slice.isNat_congr : ∀ {s t : String.Slice}, s.copy = t.copy → s.isNat = t.isNat
-- Mathlib.Topology.VectorBundle.Riemannian
/-- In a continuous Riemannian bundle, the inverse of the trivialization at a point is locally
bounded in norm.  -/
eventually_norm_symmL_trivializationAt_lt : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F : Type u_2) [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  (E : B → Type u_3) [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E]
  [h : IsContinuousRiemannianBundle F E] (x : B),
  ∃ C > 0, ∀ᶠ (y : B) in nhds x, ‖Bundle.Trivialization.symmL ℝ (trivializationAt F E x) y‖ < C
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.horn.IsCompatible.exists_lift : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)},
  SSet.horn.IsCompatible f →
    ∀ {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y),
      (∀ (j : Fin (n + 2)) (hj : j ≠ i),
          CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b) →
        ∃ φ,
          (∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) φ = f j hj) ∧
            CategoryTheory.CategoryStruct.comp φ p = b
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α}, BddBelow s.measureOfNegatives
-- Mathlib.LinearAlgebra.Prod
LinearMap.comp_coprod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M₃ →ₗ[R] M₄) (g₁ : M →ₗ[R] M₃)
  (g₂ : M₂ →ₗ[R] M₃), f ∘ₗ g₁.coprod g₂ = (f ∘ₗ g₁).coprod (f ∘ₗ g₂)
-- Mathlib.NumberTheory.Divisors
Nat.nonempty_divisors : ∀ {n : ℕ}, n.divisors.Nonempty ↔ n ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
AddMonoidAlgebra.instVAddForallOfIsLeftCancelVAddOfVAddWithZero.eq_1 : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : VAdd G P] [inst_1 : IsLeftCancelVAdd G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V],
  AddMonoidAlgebra.instVAddForallOfIsLeftCancelVAddOfVAddWithZero =
    { smul := fun f x p => ∑ gh ∈ Finset.VAddAntidiagonal p ⋯, f.coeff gh.1 • x gh.2 }
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- In a vector space, given a nonzero linear form `f`,
a nonzero vector `v` such that `f v = 0`,
there exists a basis `b` with two distinct indices `i`, `j`
such that `v = b i` and `f = b.coord j`.  -/
exists_basis_of_pairing_eq_zero : ∀ {K : Type u_6} {V : Type u_7} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : V →ₗ[K] K}
  {v : V}, f v = 0 → f ≠ 0 → v ≠ 0 → ∃ n b i j, i ≠ j ∧ v = b i ∧ f = b.coord j
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_sub_sphere_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), {x} - Metric.sphere 0 δ = Metric.sphere x δ
-- Std.Time.Format
/-- Parses a date string in the American format (`MM-dd-uuuu`) and returns a `PlainDate`.
 -/
Std.Time.PlainDate.fromAmericanDateString : String → Except String Std.Time.PlainDate
-- Init.Data.UInt.Bitwise
UInt64.neg_one_xor : ∀ {a : UInt64}, -1 ^^^ a = ~~~a
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_iInf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {ι : Sort u_5} {S : ι → StarSubalgebra R A},
  ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Std.Http.Data.URI.Config
/-- Per-component size limits for the URI parser.
 -/
Std.Http.URI.Config : Type
-- Mathlib.Order.Cover
WCovBy.stdRefl' : ∀ {α : Type u_1} [inst : Preorder α], Std.Refl fun x1 x2 => x2 ⩿ x1
-- Mathlib.Analysis.RCLike.Basic
/-- The `ℝ → K` coercion, as a ⋆-algebra map.  -/
RCLike.ofRealStarAlgHom : (K : Type u_1) → [inst : RCLike K] → ℝ →⋆ₐ[ℝ] K
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getD.eq_1 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (k : α) (fallback : δ),
  Std.DTreeMap.Internal.Impl.Const.getD Std.DTreeMap.Internal.Impl.leaf k fallback = fallback
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonUnitalNonAssocSemiring : {R : Type u_1} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring Rᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.one_actLeft_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one self.X)
      (CategoryTheory.CategoryStruct.comp self.actLeft h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom h
-- Mathlib.LinearAlgebra.Pi
/-- If `I` and `J` are disjoint index sets, the product of the kernels of the `J`th projections of
`φ` is linearly equivalent to the product over `I`.  -/
LinearMap.iInfKerProjEquiv : (R : Type u) →
  {ι : Type x} →
    [inst : Semiring R] →
      (φ : ι → Type i) →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] →
            {I J : Set ι} →
              [DecidablePred fun i => i ∈ I] →
                Disjoint I J → Set.univ ⊆ I ∪ J → ↥(⨅ i ∈ J, (LinearMap.proj i).ker) ≃ₗ[R] (i : ↑I) → φ ↑i
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The formal inverse in `SmallShiftedHom.{w} W Y X m₀` of a morphism `f : Y ⟶ X`
such that `W f`.  -/
CategoryTheory.Localization.SmallShiftedHom.mk₀Inv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            {X Y : C} →
              [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X] →
                [W.RespectsIso] →
                  (m₀ : M) → m₀ = 0 → (f : X ⟶ Y) → W f → CategoryTheory.Localization.SmallShiftedHom W Y X m₀
-- Mathlib.Algebra.Lie.Engel
LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop : ∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {I : LieIdeal R L} {x : L},
  R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤ →
    IsNilpotent ((LieModule.toEnd R L M) x) → LieModule.IsNilpotent (↥I) M → LieModule.IsNilpotent L M
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- If `f` is closable, then the closure is closable.  -/
LinearPMap.IsClosable.closureIsClosable : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, f.IsClosable → f.closure.IsClosable
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Destructor for `Fix F`  -/
MvQPF.Fix.dest : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → MvQPF.Fix F α → F (α ::: MvQPF.Fix F α)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.toSubsemiring_inj : ∀ {R : Type u_1} [inst : CommRing R] {P₁ P₂ : RingPreordering R}, ↑P₁ = ↑P₂ ↔ P₁ = P₂
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finprod_eq_finsetProd_of_mulSupport_subset`. -/
finprod_eq_finset_prod_of_mulSupport_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Finset α},
  Function.mulSupport f ⊆ ↑s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.mk : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (toEmbedding : M ↪ N) →
            autoParam
                (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
                  toEmbedding.toFun (FirstOrder.Language.Structure.funMap f x) =
                    FirstOrder.Language.Structure.funMap f (toEmbedding.toFun ∘ x))
                FirstOrder.Language.Embedding.map_fun'._autoParam →
              autoParam
                  (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
                    FirstOrder.Language.Structure.RelMap r (toEmbedding.toFun ∘ x) ↔
                      FirstOrder.Language.Structure.RelMap r x)
                  FirstOrder.Language.Embedding.map_rel'._autoParam →
                L.Embedding M N
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_self_const_mul : ∀ {α : Type u_1} {S : Type u_17} [inst : NormedRing S] [NormMulClass S] {c : S},
  c ≠ 0 → ∀ (f : α → S) (l : Filter α), f =O[l] fun x => c * f x
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.pos_of_mem_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E}, x ∈ Metric.ball c f.rOut → 0 < ↑f x
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm_empty_apply : ∀ {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) (i : Fin (n + 1)),
  s.excenterWeightsUnnorm ∅ i = (s.height i)⁻¹
-- Lean.DocString.Extension
Lean.addMainModuleDoc : Lean.Environment → Lean.ModuleDoc → Lean.Environment
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.monodromy_toPermFiber : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {g : G} {x y : X}
  {γ : Path.Homotopic.Quotient x y} {e : ↑(p ⁻¹' {x})},
  ⋯.monodromy γ (((⋯.toPermFiber x) g) e) = ((⋯.toPermFiber y) g) (⋯.monodromy γ e)
-- Init.Control.Lawful.Instances
ExceptT.pure.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α),
  ExceptT.pure a = ExceptT.mk (pure (Except.ok a))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcHom_real_eq_restrict : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [T2Space A] {a : A} (ha : IsSelfAdjoint a),
  cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
-- Mathlib.Logic.IsEmpty.Basic
biTotal_empty : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] [IsEmpty β], Relator.BiTotal R
-- Mathlib.RingTheory.Algebraic.Pi
/-- This is not an instance for the same reasons as `Polynomial.hasSMulPi'`.  -/
Polynomial.algebraPi : (R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : CommSemiring T] → [Algebra R S] → [Algebra S T] → Algebra (Polynomial R) (S → T)
-- Mathlib.Data.Finset.Image
Finset.forall_mem_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop},
  (∀ y ∈ Finset.image f s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c) = 1 + sizeOf c
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- Version of `ContDiffWithinAt.congr` where `x` need not be contained in `s`,
but `f` and `f₁` are equal on a set containing both.  -/
ContDiffWithinAt.congr' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → (∀ y ∈ t, f₁ y = f y) → s ⊆ t → x ∈ t → ContDiffWithinAt 𝕜 n f₁ s x
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.toString : {β : Type u_1} → {α : Type u_2} → [ToString β] → [ToString α] → Std.Tactic.BVDecide.LRAT.Action β α → String
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.instModule : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type u_1} →
        [inst_2 : Ring R] →
          [CategoryTheory.Linear R C] →
            {F G : CochainComplex C ℤ} → {n : ℤ} → Module R (CochainComplex.HomComplex.Cocycle F G n)
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelSMul.le_of_smul_le_smul_left : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : SMul G P} [self : IsOrderedCancelSMul G P]
  (a : G) (b c : P), a • b ≤ a • c → b ≤ c
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricCoefficient.eq_1 : ∀ {𝕂 : Type u_1} [inst : Field 𝕂] (a b c : 𝕂) (n : ℕ),
  ordinaryHypergeometricCoefficient a b c n =
    (↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
      (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹
-- Mathlib.Data.List.Permutation
Prod.snd.eq_1 : ∀ (α : Type u) (β : Type v) (self : α × β), self.2 = self.2
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The value of `affineCombination`, where the given points take only two values.  -/
Finset.affineCombination_apply_eq_lineMap_sum : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (w : ι → k) (p : ι → P) (p₁ p₂ : P)
  (s' : Finset ι),
  ∑ i ∈ s, w i = 1 →
    (∀ i ∈ s ∩ s', p i = p₂) →
      (∀ i ∈ s \ s', p i = p₁) → (Finset.affineCombination k s p) w = (AffineMap.lineMap p₁ p₂) (∑ i ∈ s ∩ s', w i)
-- Lean.Expr
/-- Return `true` if the given expression is a metavariable.  -/
Lean.Expr.isMVar : Lean.Expr → Bool
-- Mathlib.Order.Max
IsMax.eq_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → a = b
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.toPolyN_Nonneg : ∀ (e : Lean.Grind.Linarith.Expr), e.toPolyN.NonnegCoeffs
-- Mathlib.Testing.Plausible.Functions
Plausible.Monotone.testable : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        (f : α → β) →
          [I :
              Plausible.Testable
                (Plausible.NamedBinder "x"
                  (∀ (x : α), Plausible.NamedBinder "y" (∀ (y : α), Plausible.NamedBinder "H" (x ≤ y → f x ≤ f y))))] →
            Plausible.Testable (Monotone f)
-- Mathlib.Algebra.Free
FreeAddMagma.toFreeAddSemigroup_comp_of : ∀ {α : Type u}, ⇑FreeAddMagma.toFreeAddSemigroup ∘ FreeAddMagma.of = FreeAddSemigroup.of
-- Mathlib.Algebra.Group.Defs
IsCancelAdd.toIsLeftCancelAdd : ∀ {G : Type u} {inst : Add G} [self : IsCancelAdd G], IsLeftCancelAdd G
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.logDeriv_cos : logDeriv Real.cos = -Real.tan
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzWith_iff_norm_div_le`. -/
LipschitzWith.norm_div_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F}
  {C : NNReal}, LipschitzWith C f → ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖
-- Mathlib.Algebra.Category.Grp.Shrink
GrpCat.shrinkFunctor_obj_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] (X : C),
  ↑((GrpCat.shrinkFunctor.{w, w', v, u} F).obj X) = Shrink.{w, w'} ↑(F.obj X)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.unit_aux : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) {r : R},
  r * x.leadingCoeff = 1 → ∀ (oinv : Γ), oinv + x.order = 0 → 0 < (1 - (HahnSeries.single oinv) r * x).orderTop
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.isClosedEmbedding_val : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R] [T1Space R], Topology.IsClosedEmbedding Subtype.val
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
/-- The variation of a `VectorMeasure` as a `Measure`.  -/
MeasureTheory.VectorMeasure.variation : {X : Type u_1} →
  {mX : MeasurableSpace X} →
    {V : Type u_2} →
      [inst : TopologicalSpace V] →
        [inst_1 : ENormedAddCommMonoid V] → [T2Space V] → MeasureTheory.VectorMeasure X V → MeasureTheory.Measure X
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.toPartialOrder : {α : Type u_4} → [self : ChainCompletePartialOrder α] → PartialOrder α
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Any hom in `G` can be made into a loop, by conjugating with `treeHom`s.  -/
IsFreeGroupoid.SpanningTree.loopOfHom : {G : Type u} →
  [inst : CategoryTheory.Groupoid G] →
    [inst_1 : IsFreeGroupoid G] →
      (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) →
        [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] →
          {a b : G} → (a ⟶ b) → CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {a : α} {h' : (t.getKey? a).isSome = true}, (t.getKey? a).get h' = t.getKey a ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.DHashMap.Raw.ofList l).getKeyD k' fallback = k
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFinitaryMapEquiv : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α ≃ β}, (M.mapEquiv f).Finitary
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C) {x y z : B} (f : x ⟶ y) (g : y ⟶ z),
  F.toStrictlyUnitaryLaxFunctor.mapComp f g = (F.mapComp f g).inv
-- Mathlib.Geometry.Manifold.Submersion
/-- `f : M → N` is a `C^n` submersion if around each point `x ∈ M`,
there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
such that in these charts, `f` looks like `(u, v) ↦ u`.

In other words, `f` is a submersion at each `x ∈ M`.

This definition has a fixed parameter `F`, which is a choice of complement of `E` in `E'`:
being a submersion at `x` includes a choice of linear isomorphism between `E` and `E'' × F`.  -/
Manifold.IsSubmersionOfComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    (F : Type u_5) →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              ModelWithCorners 𝕜 E H →
                                ModelWithCorners 𝕜 E'' G →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst : TopologicalSpace M] →
                                        [ChartedSpace H M] →
                                          [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → Prop
-- Mathlib.Algebra.Group.Defs
CancelCommMonoid.toLeftCancelMonoid : {M : Type u} → [self : CancelCommMonoid M] → LeftCancelMonoid M
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.join : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] [FaithfulSMul M X]
  {P Q : M}, IsLprojection X P → IsLprojection X Q → IsLprojection X (P + Q - P * Q)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basis
Basis.piTensorProduct.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  (b : (i : ι) → Module.Basis (κ i) R (M i)),
  Basis.piTensorProduct b =
    Finsupp.basisSingleOne.map
      (((PiTensorProduct.congr fun i => (b i).repr).trans PiTensorProduct.ofFinsuppEquiv).trans
          (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) ↑(PiTensorProduct.constantBaseRingEquiv ι R))).symm
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_of' : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)],
  (Monoid.CoprodI.lift fun i => Monoid.CoprodI.of) = MonoidHom.id (Monoid.CoprodI M)
-- Mathlib.Data.Option.NAry
Option.map₂_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {g : β → α → γ},
  (∀ (a : α) (b : β), f a b = g b a) → Option.map₂ f a b = Option.map₂ g b a