mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {fallback : β k} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getD k fallback = (f (t.get? k)).getD fallback
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_sub_Ico_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Multiset.Ico a b - Multiset.Ico a c = Multiset.Ico (max a c) b
-- Mathlib.Data.Sigma.Lex
Sigma.instSymmLex : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [Std.Symm r]
  [∀ (i : ι), Std.Symm (s i)], Std.Symm (Sigma.Lex r s)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {options? : Option Lean.Lsp.DeleteFile.Options} {annotationId? : Option String}
  {uri_1 : Lean.Lsp.DocumentUri} {options?_1 : Option Lean.Lsp.DeleteFile.Options} {annotationId?_1 : Option String},
  { uri := uri, options? := options?, annotationId? := annotationId? } =
      { uri := uri_1, options? := options?_1, annotationId? := annotationId?_1 } →
    uri = uri_1 ∧ options? = options?_1 ∧ annotationId? = annotationId?_1
-- Std.Data.DTreeMap.Raw.Basic
/-- Inserts multiple elements into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.DTreeMap.Raw.Const.insertManyIfNewUnit : {α : Type u} →
  {cmp : α → α → Ordering} →
    {ρ : Type u_1} →
      [ForIn Id ρ α] → Std.DTreeMap.Raw α (fun x => Unit) cmp → ρ → Std.DTreeMap.Raw α (fun x => Unit) cmp
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A category `HasBinaryCoproducts` if it has all colimit of shape `Discrete WalkingPair`,
i.e. if it has a coproduct for every pair of objects.  -/
CategoryTheory.Limits.HasBinaryCoproducts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula for the first order derivative**, assuming `f` is differentiable on
a closed ball.  -/
DifferentiableOn.deriv_eq_smul_circleIntegral : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ},
  0 < R →
    DifferentiableOn ℂ f (Metric.closedBall c R) →
      ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑Real.pi * Complex.I) • deriv f c
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- A map from the relations type to the variables type. Used to compute the differential.  -/
Algebra.PreSubmersivePresentation.map : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.PreSubmersivePresentation R S ι σ → σ → ι
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.DiscrInfo : Type
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ`. -/
Topology.CWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ),
  ↑(Topology.RelCWComplex.skeleton C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell (n + 1) j =
    ↑(Topology.RelCWComplex.skeleton C (↑n + 1))
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeleton.congr_simp : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n n_1 : ℕ∞),
  n = n_1 → Topology.RelCWComplex.skeleton C n = Topology.RelCWComplex.skeleton C n_1
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_nonUnitalStarSubalgebra : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s : Set A),
  StarAlgebra.adjoin R ↑(NonUnitalStarAlgebra.adjoin R s) = StarAlgebra.adjoin R s
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The full set is a fixed block.  -/
AddAction.IsFixedBlock.univ : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X], AddAction.IsFixedBlock G Set.univ
-- Aesop.Tree.Data
Aesop.Iteration.none : Aesop.Iteration
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_inv_naturality_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} (n a a' : M) (ha' : n + a = a')
  (f : X ⟶ Y) {Z : A} (h : (F.shift a).obj ((CategoryTheory.shiftFunctor C n).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.shift a').map f)
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X)
      (CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f)) h)
-- Plausible.DeriveShrinkable
/-- Returns `(argument_name, argument_type)` pairs for a constructor,
skipping the inductive's type parameters. Freshens names to avoid macro scopes.  -/
_private.Plausible.DeriveShrinkable.0.Plausible.getCtorArgsNamesAndTypes : Lean.InductiveVal → Lean.Name → Lean.MetaM (Array (Lean.Name × Lean.Expr))
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) thickening is an open set.  -/
Metric.isOpen_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {E : Set α}, IsOpen (Metric.thickening δ E)
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIio.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {b x : α} [inst_1 : Decidable (x < b)], Set.decidableMemIio = inst_1
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumCompl_apply_inl : ∀ {α : Type u} (s : Set α) [inst : DecidablePred fun x => x ∈ s] (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
-- Mathlib.Analysis.Convex.Between
not_sbtw_self : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (x y : P), ¬Sbtw R x y x
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_finsetSum : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  {ε''' : Type u_9} [inst_2 : TopologicalSpace ε'''] [inst_3 : ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε''']
  {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''},
  (∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) → MeasureTheory.LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ
-- Mathlib.Order.PropInstances
Prop.decidableRelBot : {α : Type u} → DecidableRel ⊥
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.map_fst : ∀ {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] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D) (i : J.L),
  (d.map F).fst i = F.map (d.fst i)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec.congr_simp : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X], X.isoSpec = X.isoSpec
-- Mathlib.Algebra.Order.Group.PosPart
posPart_mono : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α], Monotone fun x => x⁺
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.congr_map_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {X Y : Cᵒᵖ} {f g : X ⟶ Y},
  f = g →
    ∀ (m : ↑(M.obj X)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) m = (CategoryTheory.ConcreteCategory.hom (M.map g)) m
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.comp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {X Y Z : CategoryTheory.SpectralSequence C c r₀} (f : X.Hom Y) (g : Y.Hom Z) (r : ℤ)
  (hr : r₀ ≤ r),
  (CategoryTheory.CategoryStruct.comp f g).hom r hr = CategoryTheory.CategoryStruct.comp (f.hom r ⋯) (g.hom r ⋯)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_top : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G], ↑⊤ = ⊤
-- Mathlib.Algebra.Opposites
MulOpposite.instSMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β],
  MulOpposite.instSMul = { smul := fun c x => MulOpposite.op (c • MulOpposite.unop x) }
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The underlying morphism of a partial map.  -/
AlgebraicGeometry.Scheme.PartialMap.hom : {X Y : AlgebraicGeometry.Scheme} → (self : X.PartialMap Y) → ↑self.domain ⟶ Y
-- Lean.Linter.UnusedVariables
/-- Enables or disables all unused variable linter warnings  -/
Lean.Linter.linter.unusedVariables : Lean.Option Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {f g : E.Hom F} (hs : f.s₀ = g.s₀),
  (∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)) → f = g
-- Init.Data.List.MinMaxOn
List.min_map_eq_min : ∀ {α : Type u_1} {β : Type u_2} [inst : Min α] [inst_1 : LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α]
  [inst_4 : Min β] [inst_5 : LE β] [DecidableLE β] [Std.IsLinearPreorder β] [Std.LawfulOrderLeftLeaningMin β]
  {f : α → β}, (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → ∀ {l : List α} {h : l ≠ []}, (List.map f l).min ⋯ = f (l.min h)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Weights for expressing a single point as an affine combination.  -/
Finset.affineCombinationSingleWeights : (k : Type u_1) → [Ring k] → {ι : Type u_4} → [DecidableEq ι] → ι → ι → k
-- Mathlib.RingTheory.Derivation.Basic
/-- If adjoin of a set is the whole algebra, then any two derivations equal on this set are equal
on the whole algebra.  -/
Derivation.ext_of_adjoin_eq_top : ∀ {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]
  {D1 D2 : Derivation R A M} (s : Set A), Algebra.adjoin R s = ⊤ → Set.EqOn (⇑D1) (⇑D2) s → D1 = D2
-- Init.Data.String.Lemmas.FindPos
String.Pos.posGT_offset : ∀ {s : String} {p : s.Pos} {h : p.offset < s.rawEndPos}, s.posGT p.offset h = p.next ⋯
-- Mathlib.Probability.HasLaw
MeasureTheory.MeasurePreserving.fun_comp_hasLaw : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} {𝓨 : Type u_3} {m𝓨 : MeasurableSpace 𝓨}
  {ν : MeasureTheory.Measure 𝓨} {Y : 𝓧 → 𝓨},
  MeasureTheory.MeasurePreserving Y μ ν →
    ProbabilityTheory.HasLaw X μ P → ProbabilityTheory.HasLaw (fun ω => Y (X ω)) ν P
-- Mathlib.Topology.Order.MonotoneConvergence
iSup_eq_iSup_subseq_of_antitone : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : Preorder ι₂] [inst_1 : CompleteLattice α] {l : Filter ι₁}
  [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂}, Antitone f → Filter.Tendsto φ l Filter.atBot → ⨆ i, f i = ⨆ i, f (φ i)
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt'_nonempty : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M), (Archimedean.ratLt' x).Nonempty
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'} {f' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt% f z f' → HasMFDerivAt% (-f) z (-f')
-- Batteries.Data.List.Lemmas
List.take_succ_drop : ∀ {α : Type u_1} {l : List α} {n stop : ℕ} (h : n < l.length - stop),
  List.take (n + 1) (List.drop stop l) = List.take n (List.drop stop l) ++ [l[stop + n]]
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.compClosure.congruence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C),
  CategoryTheory.Congruence fun X Y => Relation.EqvGen (CategoryTheory.HomRel.CompClosure r)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.val_mulMap'_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (a : ↥A) (b : ↥B), ↑((A.mulMap' B) (a ⊗ₜ[R] b)) = ↑a * ↑b
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.inv_add_inv_eq_one : ∀ {p q : ℝ}, p.HolderConjugate q → p⁻¹ + q⁻¹ = 1
-- Mathlib.Algebra.Algebra.Unitization
Unitization.lift_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] (φ : A →ₙₐ[R] C), Unitization.lift φ = φ.toAlgHom
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_two : bernoulli' 2 = 1 / 6
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_inv₀`. -/
Antivary.of_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {f : ι → α} {g : ι → β},
  StrongLT 0 f → StrongLT 0 g → Antivary f⁻¹ g⁻¹ → Antivary f g
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Fact.mk.injEq : ∀ (coeffs : Lean.Omega.Coeffs) (constraint : Lean.Omega.Constraint)
  (justification : Lean.Elab.Tactic.Omega.Justification constraint coeffs) (coeffs_1 : Lean.Omega.Coeffs)
  (constraint_1 : Lean.Omega.Constraint) (justification_1 : Lean.Elab.Tactic.Omega.Justification constraint_1 coeffs_1),
  ({ coeffs := coeffs, constraint := constraint, justification := justification } =
      { coeffs := coeffs_1, constraint := constraint_1, justification := justification_1 }) =
    (coeffs = coeffs_1 ∧ constraint = constraint_1 ∧ justification ≍ justification_1)
-- Mathlib.NumberTheory.Cyclotomic.Gal
/-- `IsCyclotomicExtension.autEquivPow` repackaged in terms of `Gal`.
Asserts that the Galois group of `cyclotomic n K` is equivalent to `(ZMod n)ˣ`
if `cyclotomic n K` is irreducible in the base field.  -/
galCyclotomicEquivUnitsZMod : {n : ℕ} →
  [NeZero n] →
    {K : Type u_1} →
      [inst : Field K] →
        {L : Type u_2} →
          [inst_1 : Field L] →
            [inst_2 : Algebra K L] →
              [IsCyclotomicExtension {n} K L] →
                Irreducible (Polynomial.cyclotomic n K) → (Polynomial.cyclotomic n K).Gal ≃* (ZMod n)ˣ
-- Mathlib.Topology.MetricSpace.Defs
dist_le_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y ≤ 0 ↔ x = y
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.linear_inv_isBigO_left : ∀ (d : ℤ) {z : ℂ}, z ≠ 0 → (fun c => (↑c * z + ↑d)⁻¹) =O[Filter.cofinite] fun n => (↑n)⁻¹
-- Mathlib.Topology.Inseparable
SeparationQuotient.instZero : {X : Type u_1} → [inst : TopologicalSpace X] → [Zero X] → Zero (SeparationQuotient X)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} (hom : R₁.X ⟶ R₂.X)
  [isRingHom : CategoryTheory.IsRingHom hom] (hom_1 : R₁.X ⟶ R₂.X) (isRingHom_1 : CategoryTheory.IsRingHom hom_1),
  ({ hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := isRingHom_1 }) = (hom = hom_1)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.inst : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → OmegaCompletePartialOrder (α →𝒄 β)
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.isGrindOnly : Lean.TSyntax `tactic → Bool
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.ofAdd_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Multiplicative.ofAdd a < Multiplicative.ofAdd b ↔ a < b
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The sine of the angle between `x` and `x + y`.  -/
InnerProductGeometry.sin_angle_add : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 →
    x + y ≠ 0 →
      Real.sin (InnerProductGeometry.angle x (x + y)) =
        √(inner ℝ x x * inner ℝ y y - inner ℝ x y * inner ℝ x y) / (‖x‖ * ‖x + y‖)
-- Mathlib.Algebra.Field.Basic
sub_div' : ∀ {K : Type u_1} [inst : Field K] {a b c : K}, c ≠ 0 → b - a / c = (b * c - a) / c
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_inclusion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {U V : TopologicalSpace.Opens M}
  (h : U ≤ V), ContMDiff I I n (TopologicalSpace.Opens.inclusion h)
-- Mathlib.Algebra.Order.ToIntervalMod
left_lt_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), a < toIocMod hp a b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_comap_eq_self_of_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ (t : Subring S), Subring.map f (Subring.comap f t) = t
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.ofNat_arg : ∀ {n : ℕ} [inst : n.AtLeastTwo], (OfNat.ofNat n).arg = 0
-- Init.Data.Nat.Lemmas
Nat.div_eq_iff_eq_of_dvd_dvd : ∀ {n a b : ℕ}, n ≠ 0 → a ∣ n → b ∣ n → (n / a = n / b ↔ a = b)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.adic_exact : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type}
  (f : (ι → R) →ₗ[R] M),
  Function.Surjective ⇑f →
    ∀ [IsNoetherianRing R] [Finite ι], Function.Exact ⇑(AdicCompletion.map I f.ker.subtype) ⇑(AdicCompletion.map I f)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lsub_lt_ord_lift : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Ordinal.{max u v}},
  Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof → (∀ (i : ι), f i < c) → Ordinal.lsub f < c
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_nat_atTop_induction : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] {f : ℕ → E''}
  {g : ℕ → F''},
  (∀ᶠ (n : ℕ) in Filter.atTop, g n = 0 → f n = 0) →
    (∀ᶠ (n₀ : ℕ) in Filter.atTop,
        ∃ C₀, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖) →
      f =O[Filter.atTop] g
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformlyOn.summable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  SummableLocallyUniformlyOn f s → x ∈ s → Summable fun x_1 => f x_1 x
-- Lean.Parser.Term.Basic
Lean.Parser.Term.omission.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- For `h : S.RightHomologyData`, this is a restatement of `h.hι`, saying that
`ι : h.H ⟶ h.Q` is a kernel of `h.g' : h.Q ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.RightHomologyData.hι' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι h.ι ⋯)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_rightUnitor_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C) {Z : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.ε F))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h))
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the right by a positive element preserves strict antitonicity.  -/
StrictAnti.smul_const : ∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosStrictMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → α},
  StrictAnti f → 0 < b → StrictAnti fun x => f x • b
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- append arrows of a polynomial functor application  -/
MvPFunctor.appendContents : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {β : Type u_1} → {a : P.A} → (P.drop.B a).Arrow α → (P.last.B a → β) → (P.B a).Arrow (α ::: β)
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.toLinearPMap_domain : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (g : Submodule R (E × F)),
  g.toLinearPMap.domain = Submodule.map (LinearMap.fst R E F) g
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.coe_negPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(α →₁ₛ[μ] ℝ)),
  ↑(MeasureTheory.L1.SimpleFunc.negPart f) = MeasureTheory.Lp.negPart ↑f
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h