mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
/-- If `H' : D' ⥤ V` is a pointwise left Kan extension along `L : D ⥤ D'`,
and if tensoring right with an object preserves colimits in `V`
then `H' ⊠ K : D' × E ⥤ V` is a pointwise left Kan extension along `L × (𝟭 E)`.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitLeft : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (α : H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            [∀ (d : D') (e : E),
                                  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow L d)
                                    (CategoryTheory.MonoidalCategory.tensorRight (K.obj e))] →
                              (CategoryTheory.Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension →
                                (CategoryTheory.Functor.LeftExtension.mk
                                    (CategoryTheory.MonoidalCategory.externalProduct H' K)
                                    (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft H' α
                                      K)).IsPointwiseLeftKanExtension
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocMod hp (a + ↑m * p) b = toIocMod hp a b + ↑m * p
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.symm_mk_inv : ∀ {M : Type u_1} [inst : Inv M] (a : Mᵈᵐᵃ), DomMulAct.mk.symm a⁻¹ = (DomMulAct.mk.symm a)⁻¹
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) An open cover on `S`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰S : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} → AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f → S.OpenCover
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.copy_eq : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (s : Set L) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CategoryTheory.Cat) →
      CategoryTheory.Category.{v, v} (CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects))
-- Init.Data.Array.Int
Array.sum_append_int : ∀ {as₁ as₂ : Array ℤ}, (as₁ ++ as₂).sum = as₁.sum + as₂.sum
-- Mathlib.Topology.Category.Profinite.Basic
instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite : ∀ (X : FintypeCat), Finite ↑(FintypeCat.toProfinite.obj X).toTop
-- Mathlib.Order.Filter.SmallSets
Filter.eventually_smallSets_eventually : ∀ {α : Type u_1} {l l' : Filter α} {p : α → Prop},
  (∀ᶠ (s : Set α) in l.smallSets, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
-- Mathlib.Order.WellFounded
Function.argminOn_mem : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LT β] [inst_1 : WellFoundedLT β] (s : Set α) (hs : s.Nonempty),
  Function.argminOn f s hs ∈ s
-- Init.Control.Lawful.Basic
LawfulMonad.mk : ∀ {m : Type u → Type v} [inst : Monad m] [toLawfulApplicative : LawfulApplicative m],
  (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let a ← x
          pure (f a)) =
        f <$> x) →
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
        (do
            let x_1 ← f
            x_1 <$> x) =
          f <*> x) →
      (∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) →
        (∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
          LawfulMonad m
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.match_1.eq_4 : ∀ (motive : Lean.Expr → List Lean.Expr → Sort u_1) (data : Lean.MData) (b : Lean.Expr) (args : List Lean.Expr)
  (h_1 : (f : Lean.Expr) → motive f [])
  (h_2 :
    (binderName : Lean.Name) →
      (binderType b : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) →
          (a : Lean.Expr) → (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as))
  (h_3 :
    (n : Lean.Name) →
      (t v b : Lean.Expr) → (nondep : Bool) → (args : List Lean.Expr) → motive (Lean.Expr.letE n t v b nondep) args)
  (h_4 : (data : Lean.MData) → (b : Lean.Expr) → (args : List Lean.Expr) → motive (Lean.Expr.mdata data b) args)
  (h_5 : (f : Lean.Expr) → (args : List Lean.Expr) → motive f args),
  (args = [] → False) →
    (match Lean.Expr.mdata data b, args with
      | f, [] => h_1 f
      | Lean.Expr.lam binderName binderType b binderInfo, a :: as => h_2 binderName binderType b binderInfo a as
      | Lean.Expr.letE n t v b nondep, args => h_3 n t v b nondep args
      | Lean.Expr.mdata data b, args => h_4 data b args
      | f, args => h_5 f args) =
      h_4 data b args
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α],
  t ≠ ∅ → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Logic.Equiv.Basic
/-- Subtype of the quotient is equivalent to the quotient of the subtype. Let `α` be a setoid with
equivalence relation `~`. Let `p₂` be a predicate on the quotient type `α/~`, and `p₁` be the lift
of this predicate to `α`: `p₁ a ↔ p₂ ⟦a⟧`. Let `~₂` be the restriction of `~` to `{x // p₁ x}`.
Then `{x // p₂ x}` is equivalent to the quotient of `{x // p₁ x}` by `~₂`.  -/
Equiv.subtypeQuotientEquivQuotientSubtype : {α : Sort u_1} →
  (p₁ : α → Prop) →
    {s₁ : Setoid α} →
      {s₂ : Setoid (Subtype p₁)} →
        (p₂ : Quotient s₁ → Prop) →
          (∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) → (∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y) → { x // p₂ x } ≃ Quotient s₂
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toSubsemigroup_strictMono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], StrictMono NonUnitalSubring.toSubsemigroup
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Convert a multiseries in an empty basis to a real number.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.toReal : Tactic.ComputeAsymptotics.MultiseriesExpansion [] → ℝ
-- Mathlib.Tactic.DepRewrite
/-- Apply `rw!` to a local declaration.  -/
Mathlib.Tactic.DepRewrite.depRwLocalDecl : Lean.Syntax → Bool → Lean.FVarId → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instT3Space : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F],
  T3Space (E [⋀^ι]→L[𝕜] F)
-- ProofWidgets.Cancellable
ProofWidgets.CheckRequestResponse.done.inj : ∀ {result result_1 : ProofWidgets.LazyEncodable Lean.Json},
  ProofWidgets.CheckRequestResponse.done result = ProofWidgets.CheckRequestResponse.done result_1 → result = result_1
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.inhabited : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) →
                        (f : M →ₗ[R] Q) → [Fact (Function.Injective ⇑i)] → Inhabited (Module.Baer.ExtensionOf i f)
-- Mathlib.Topology.MetricSpace.Isometry
/-- The natural isometry `∀ i, Y i ≃ᵢ ∀ j, Y (e.symm j)` obtained from a bijection `ι ≃ ι'` of
fintypes. `Equiv.piCongrLeft'` as an `IsometryEquiv`.  -/
IsometryEquiv.piCongrLeft' : {ι : Type u_2} →
  {ι' : Type u_3} →
    [inst : Fintype ι] →
      [inst_1 : Fintype ι'] →
        {Y : ι → Type u_4} →
          [inst_2 : (j : ι) → PseudoEMetricSpace (Y j)] → (e : ι ≃ ι') → ((i : ι) → Y i) ≃ᵢ ((j : ι') → Y (e.symm j))
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_fst : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β], ⇑LatticeHom.fst = Prod.fst
-- Mathlib.Algebra.Lie.Rank
LieModule.rank_eq_natTrailingDegree : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M]
  [inst_6 : Module R M] [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] [inst_11 : Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] [inst_13 : DecidableEq ι],
  LieModule.rank R L M = ((↑(LieModule.toEnd R L M)).polyCharpoly b).natTrailingDegree
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Hom.addCommGroup.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G X : C}
  [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.IsCommAddMonObj G],
  CategoryTheory.Hom.addCommGroup = { toAddGroup := CategoryTheory.Hom.addGroup, add_comm := ⋯ }
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAdd.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G]
  [toIsManifold : IsManifold I n G], (ContMDiff (I.prod I) I n fun p => p.1 + p.2) → ContMDiffAdd I n G
-- Batteries.Data.Array.Scan
Array.scanr_push : ∀ {α : Type u_1} {β : Type u_2} {a : α} {init : β} {f : α → β → β} {as : Array α},
  Array.scanr f init (as.push a) = (Array.scanr f (f a init) as).push init
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k a : α},
  Std.DHashMap.Const.get? (m.erase k) a = if (k == a) = true then none else Std.DHashMap.Const.get? m a
-- Mathlib.Order.Sublattice
Sublattice.comap_iInf : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β)
  (s : ι → Sublattice β), Sublattice.comap f (iInf s) = ⨅ i, Sublattice.comap f (s i)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.instFunLikeHomSubtypeX : (X : Bipointed) → (Y : Bipointed) → FunLike (X.HomSubtype Y) X.X Y.X
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.isZero_trivial : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Limits.IsZero (CategoryTheory.AddGrp.trivial C)
-- Mathlib.Algebra.Group.Hom.Defs
AddHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Add M] [inst_1 : Add N]
  [inst_2 : FunLike F M N], (∀ (f : F) (x y : M), f (x + y) = f x + f y) → AddHomClass F M N
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.integrable_coeFn : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α →ₘ[μ] ε}, MeasureTheory.Integrable (↑f) μ ↔ f.Integrable
-- Mathlib.Algebra.Homology.Localization
/-- The condition on a complex shape `c` saying that homotopic maps become equal in
the localized category with respect to quasi-isomorphisms.  -/
ComplexShape.QFactorsThroughHomotopy : {ι : Type u_3} →
  ComplexShape ι →
    (C : Type u_4) →
      [inst : CategoryTheory.Category.{v_2, u_4} C] →
        [inst_1 : CategoryTheory.Preadditive C] → [CategoryTheory.CategoryWithHomology C] → Prop
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- If a set is bounded below and above, and nonempty, its infimum is less than or equal to
its supremum.  -/
csInf_le_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  s.Nonempty →
    autoParam (BddBelow s) csInf_le_csSup._auto_1 → autoParam (BddAbove s) csInf_le_csSup._auto_3 → sInf s ≤ sSup s
-- Init.Data.Int.Gcd
Int.gcd_dvd_natAbs_left : ∀ (a b : ℤ), a.gcd b ∣ a.natAbs
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (h : A = B),
  (CategoryTheory.eqToHom h).hom₂ = CategoryTheory.eqToHom ⋯
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_eq_get!_get? : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.get! a = (m.get? a).get!
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_eq_one_iff_nonempty_unique : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α = 1 ↔ Nonempty (Unique α)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is nonzero, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y ≠ 0 → x ≠ 0
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.Small.productIso_inv_comp_π : ∀ {J : Type v} (F : J → Type u) [inst : Small.{u, v} J] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Small.productIso F).inv
      (CategoryTheory.Limits.Pi.π F j) =
    TypeCat.ofHom fun f => (equivShrink ((j : J) → F j)).symm f j
-- Mathlib.RingTheory.Ideal.Colon
Submodule.instIsTwoSidedColonCoe : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (P : Submodule R M), (N.colon ↑P).IsTwoSided
-- Lean.Parser.Do
Lean.Parser.Term.doNested.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.WithOne.Map
/-- Lift a map `f : α → β` to `WithOne α → WithOne β`. Implemented using `Option.map`.

Note: the definition previously known as `WithOne.map` is now called `WithOne.mapMulHom`.  -/
WithOne.map : {α : Type u_1} → {β : Type u_2} → (α → β) → WithOne α → WithOne β
-- Mathlib.Order.Max
IsTop.prodMk : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsTop a → IsTop b → IsTop (a, b)
-- Lean.Meta.HaveTelescope
/-- Information about each `have` in the telescope.  -/
Lean.Meta.HaveTelescopeInfo.haveInfo : Lean.Meta.HaveTelescopeInfo → Array Lean.Meta.HaveInfo
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_induce_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (s : Set α) (t : Finset ↑s) (n : ℕ),
  (SimpleGraph.induce s G).IsNClique n t ↔ G.IsNClique n (Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_yield : ∀ {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} {it : α} {out : β},
  Std.IterStep.mapIterator f (Std.IterStep.yield it out) = Std.IterStep.yield (f it) out
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.aleph0_le_card : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph0 ≤ o.card ↔ Ordinal.omega0 ≤ o
-- Mathlib.RingTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of ring commutes.  -/
RingCon.lift_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (H : c ≤ RingCon.ker f) (x : M), (c.lift f H) (c.mk' x) = f x
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.inter_ae_eq_left_of_ae_eq_univ : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, t =ᵐ[μ] Set.univ → s ∩ t =ᵐ[μ] s
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ematch.sizeOf_spec : ∀ (thm : Lean.Meta.Grind.EMatchTheorem), sizeOf (Lean.Meta.Grind.Entry.ematch thm) = 1 + sizeOf thm
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx?_eq_entryAtIdx? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {i : ℕ},
  t.keyAtIdx? i = Option.map (fun x => x.fst) (t.entryAtIdx? i)
-- Mathlib.Order.ModularLattice
isModularLattice_iff_inf_sup_inf_assoc : ∀ {α : Type u_1} [inst : Lattice α], IsModularLattice α ↔ ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- Two quadratic forms over a ring `R` are equivalent
if there exists an isometric equivalence between them:
a linear equivalence that transforms one quadratic form into the other.  -/
QuadraticMap.Equivalent : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R N] → QuadraticMap R M₁ N → QuadraticMap R M₂ N → Prop
-- Init.Data.List.Pairwise
List.pairwise_of_forall_mem_list : ∀ {α : Type u_1} {l : List α} {r : α → α → Prop}, (∀ a ∈ l, ∀ b ∈ l, r a b) → List.Pairwise r l
-- Mathlib.AlgebraicGeometry.Birational.Dominant
AlgebraicGeometry.Scheme.RationalMap.IsDominant.out : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X.RationalMap Y} [self : f.IsDominant],
  Quotient.liftOn f (fun g => AlgebraicGeometry.IsDominant g.hom) ⋯
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ},
  CategoryTheory.Limits.coconeUnopOfConeEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Right action for the tensor product of two bimodules.  -/
Bimod.TensorBimod.actRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        {R S T : CategoryTheory.Mon C} →
          (P : Bimod R S) →
            (Q : Bimod S T) →
              [∀ (X : C),
                    CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                      (CategoryTheory.MonoidalCategory.tensorRight X)] →
                CategoryTheory.MonoidalCategoryStruct.tensorObj (Bimod.TensorBimod.X P Q) T.X ⟶ Bimod.TensorBimod.X P Q
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  (m.alter k f).getKey? k = if (f m[k]?).isSome = true then some k else none
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
/-- `equiv` bundled as an algebra isomorphism with `Unitization 𝕜 A`.  -/
WithLp.unitizationAlgEquiv : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] →
              (R : Type u_3) →
                [inst_5 : CommSemiring R] →
                  [inst_6 : Algebra R 𝕜] →
                    [inst_7 : DistribMulAction R A] →
                      [inst_8 : IsScalarTower R 𝕜 A] → WithLp 1 (Unitization 𝕜 A) ≃ₐ[R] Unitization 𝕜 A
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the forward direction of `contMDiffWithinAt_iff_contDiffWithinAt`. -/
ContMDiffWithinAt.contDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E},
  ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x → ContDiffWithinAt 𝕜 n f s x
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitBackward_counitForward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A),
  CategoryTheory.OverPresheafAux.counitBackward F s ∘ CategoryTheory.OverPresheafAux.counitForward F s = id
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C}
  (h : V₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd i₁ i₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
        h)
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F)
  (α β : A₁ ⟶ A₂), (α - β).f = α.f - β.f
-- Std.Do.SPred.SVal
/-- Auxiliary type class used by `SVal.getThe` to construct a projection from a list of state types to
one of the component states.
 -/
Std.Do.SVal.GetTy : Type u → List (Type u) → Type u
-- Std.Http.Data.Headers
Std.Http.instInhabitedHeaders.default : Std.Http.Headers
-- Mathlib.Condensed.Functors
/-- The yoneda presheaf as a condensed set, restricted to Stonean spaces.  -/
stoneanToCondensed : CategoryTheory.Functor Stonean CondensedSet