mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.coe_splitLower : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, ↑(I.splitLower i x) = ↑I ∩ {y | y i ≤ x}
-- Mathlib.Data.Set.Basic
Set.union_congr_left : ∀ {α : Type u} {s t u : Set α}, t ⊆ s ∪ u → u ⊆ s ∪ t → s ∪ t = s ∪ u
-- Init.Data.UInt.Lemmas
UInt16.mul_neg : ∀ (a b : UInt16), a * -b = -(a * b)
-- Mathlib.Analysis.InnerProductSpace.Basic
parallelogram_law_with_nnnorm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E),
  ‖x + y‖₊ ^ 2 + ‖x - y‖₊ ^ 2 = 2 * (‖x‖₊ ^ 2 + ‖y‖₊ ^ 2)
-- Mathlib.Topology.Sheaves.Over
/-- `overPullback` and `sheafRestrict` are isomorphic under `sheafEquivOver`.  -/
TopologicalSpace.Opens.overPullbackSheafEquivOver : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {X : TopCat} →
      (U : TopologicalSpace.Opens ↑X) →
        ((Opens.grothendieckTopology ↑X).overPullback A U).comp U.sheafEquivOver.functor ≅ U.sheafRestrict
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.mem_domChart_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), x ∈ h.domChart.source
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instLeftIdentityJoinBot : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l],
  Std.LeftIdentity (fun x1 x2 => Lean.Order.join x1 x2) Lean.Order.bot
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instMulOneClass.eq_1 : ∀ {α : Type u_1} [inst : MulOneClass α],
  OrderDual.instMulOneClass = { toOne := OrderDual.instOne, toMul := OrderDual.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.biUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β},
  s.Countable → (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋃ b ∈ s, f b)
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_zero : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ}, Finsupp.embSigma 0 = 0
-- Mathlib.Data.List.Lattice
List.mem_bagInter : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l₁ l₂ : List α}, a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- A point `c` belongs the perpendicular bisector of `[p₁, p₂]` iff `p₂ -ᵥ p₁` is orthogonal to
`c -ᵥ midpoint ℝ p₁ p₂`.  -/
AffineSubspace.mem_perpBisector_iff_inner_eq_zero' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
  c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ inner ℝ (p₂ -ᵥ p₁) (c -ᵥ midpoint ℝ p₁ p₂) = 0
-- Mathlib.Data.Int.Order.Lemmas
Int.natAbs_lt_iff_mul_self_lt : ∀ {a b : ℤ}, a.natAbs < b.natAbs ↔ a * a < b * b
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_3.eq_3 : ∀ (motive : List String → List String → Sort u_1) (pre : String) (l s' : List String) (h_1 : Unit → motive [] [])
  (h_2 : (x : String) → (s : List String) → motive [] (x :: s))
  (h_3 : (pre : String) → (l s' : List String) → motive (pre :: l) s'),
  (match pre :: l, s' with
    | [], [] => h_1 ()
    | [], x :: s => h_2 x s
    | pre :: l, s' => h_3 pre l s') =
    h_3 pre l s'
-- Mathlib.Tactic.Linter.TextBased
/-- Determine whether a `new` `ErrorContext` is covered by an `existing` exception,
and, if it is, if we prefer replacing the new exception or keeping the previous one.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.compare : Mathlib.Linter.TextBased.ErrorContext✝ →
  Mathlib.Linter.TextBased.ErrorContext✝ → Mathlib.Linter.TextBased.ComparisonResult✝
-- Lean.Elab.Do.Control
/-- The body's elaboration type, `stM dec.resultType`.  -/
Lean.Elab.Do.EffectForwarder.liftedDoBlockResultType : Lean.Elab.Do.EffectForwarder → Lean.Expr
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedRing R] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : Module R E'] [IsBoundedSMul R E'],
  f' =o[l] g → ∀ (c : R), (c • f') =o[l] g
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot' : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι)
  (π₀ : BoxIntegral.Prepartition I), (l.toFilterDistortioniUnion I (max π₀.distortion π₀.compl.distortion) π₀).NeBot
-- Init.Data.UInt.Lemmas
UInt16.zero_def : 0 = { toBitVec := 0 }
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.yoneda_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C), (J.yoneda.obj X).obj = CategoryTheory.yoneda.obj X
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_prod_apply : ∀ (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : DecidableLE α] [inst_4 : DecidableLE β] (a b : α × β),
  (IncidenceAlgebra.zeta 𝕜) a b = (IncidenceAlgebra.zeta 𝕜) a.1 b.1 * (IncidenceAlgebra.zeta 𝕜) a.2 b.2
-- Mathlib.Analysis.Normed.Affine.AsymptoticCone
AffineSpace.asymptoticNhds_le_cobounded : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {v : V}, v ≠ 0 → AffineSpace.asymptoticNhds ℝ P v ≤ Bornology.cobounded P
-- Mathlib.NumberTheory.FLT.Three
/-- We have that `S.Solution'_descent.multiplicity = S.multiplicity - 1`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution'.multiplicity✝ (FermatLastTheoremForThreeGen.Solution.Solution'_descent✝ S) =
    FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.MeasurePreserving (⇑(NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K)) MeasureTheory.volume
    MeasureTheory.volume
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instRing : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Ring Y] → Ring (LocallyConstant X Y)
-- Qq.MetaM
Qq.synthInstanceQ : {u : Lean.Level} → (α : Q(Sort u)) → Lean.MetaM Q(«$α»)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertManyIfNew_eq_insertListIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (l : List ((a : α) × β a)), ↑(m.insertManyIfNew l) = m.insertListIfNewₘ l
-- Lean.Level
Lean.instInhabitedLevelMVarId : Inhabited Lean.LevelMVarId
-- Mathlib.Tactic.NormNum.Ineq
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLE.core.ratArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LE «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b →
            have e := q(«$a» ≤ «$b»);
            Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- If a function coincides with a measurable function outside of a countable set, it is
measurable.  -/
Measurable.measurable_of_countable_ne : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSingletonClass α], Measurable f → {x | f x ≠ g x}.Countable → Measurable g
-- Mathlib.RingTheory.WittVector.MulCoeff
/-- Produces the "remainder function" of the `n+1`st coefficient, which does not depend on the `n+1`st
coefficients of the inputs.  -/
WittVector.nthRemainder : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} → [inst : CommRing k] → [CharP k p] → (n : ℕ) → (Fin (n + 1) → k) → (Fin (n + 1) → k) → k
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_const_smul_le : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)],
  p ≠ 0 → ∀ (c : 𝕜) (f : ↥(lp E p)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero' : ∀ {w : ℕ} {c : Bool} {a t : BitVec w}, (a * bif c then t else 0#w) = bif c then a * t else 0#w
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) (x : ↥seed.baseEmbedding.domain)
  (c : FiniteArchimedeanClass M),
  toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range
-- Mathlib.Algebra.Group.ULift
ULift.cancelMonoid : {α : Type u} → [CancelMonoid α] → CancelMonoid (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmop_injective : ∀ {C : Type u₁}, Function.Injective CategoryTheory.MonoidalOpposite.unmop
-- Mathlib.Order.Hom.Basic
/-- Bundled monotone (aka, increasing) function  -/
OrderHom : (α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → Type (max u_6 u_7)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_map : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M),
  ↑(LieSubmodule.map f N) = Submodule.map ↑f ↑N
-- Init.Data.SInt.Lemmas
Int16.le_iff_lt_or_eq : ∀ {a b : Int16}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Data.List.AList
/-- The list of keys of an association list.  -/
AList.keys : {α : Type u} → {β : α → Type v} → AList β → List α
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.isEmbedding_coe : Topology.IsEmbedding Complex.UnitClosedDisc.coe
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.comap_C_surjective : ∀ {R : Type u_1} [inst : CommRing R], Function.Surjective (PrimeSpectrum.comap Polynomial.C)
-- Mathlib.Algebra.Order.Hom.Basic
map_eq_zero_iff_eq_one : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [GroupNormClass F α β] (f : F) {x : α}, f x = 0 ↔ x = 1
-- Mathlib.AlgebraicGeometry.Birational.Dominant
/-- If a restriction of `f` is dominant, then `f` is dominant.  -/
AlgebraicGeometry.Scheme.PartialMap.isDominant_hom_of_isDominant_restrict_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain)
  [H : AlgebraicGeometry.IsDominant (f.restrict U hU hU').hom], AlgebraicGeometry.IsDominant f.hom
-- Mathlib.Order.Bounded
Set.unbounded_gt_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoBotOrder α], Set.Unbounded (fun x1 x2 => x1 > x2) Set.univ
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- A submodule `N` an `R`-module `M` is fully invariant if `N` is mapped into itself by all
`R`-linear endomorphisms of `M`.

If `M` is semisimple, this is equivalent to `N` being a sum of isotypic components of `M`:
see `isFullyInvariant_iff_sSup_isotypicComponents`.  -/
Submodule.IsFullyInvariant : {R : Type u_5} →
  {M : Type u_6} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Prop
-- Mathlib.Algebra.Group.Action.TypeTags
Additive.vaddCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  VAddCommClass (Additive α) (Additive β) γ
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instIsCancelMulZero : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [IsCancelMulZero 𝕜] [inst_2 : NormOneClass 𝕜],
  IsCancelMulZero ↑(Metric.closedBall 0 1)
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The canonical map from the restriction to the subspace.  -/
AlgebraicGeometry.Scheme.ofRestrict : {U : TopCat} →
  (X : AlgebraicGeometry.Scheme) →
    {f : U ⟶ TopCat.of ↥X} → (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) → X.restrict h ⟶ X
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_int_mod : ∀ {ι : Type u_1} (s : Finset ι) (n : ℤ) (f : ι → ℤ), (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n
-- Mathlib.Order.Category.Frm
Frm.coe_comp : ∀ {X Y Z : Frm} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.map f).obj X).left = X.left
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.congr_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} {α β : X ⟶ Y}
  (h : α = β) (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ),
  α.hom.c.app U = CategoryTheory.CategoryStruct.comp (β.hom.c.app U) (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.Inf.adjDecidable : (V : Type u_2) → (G H : Digraph V) → [DecidableRel G.Adj] → [DecidableRel H.Adj] → DecidableRel (G ⊓ H).Adj
-- Mathlib.Algebra.Order.Ring.Units
Units.posSubgroup.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R],
  Units.posSubgroup R = Units.posSubgroup R
-- Lean.ProjFns
/-- The field index associated with the auxiliary projection function.  -/
Lean.ProjectionFunctionInfo.i : Lean.ProjectionFunctionInfo → ℕ
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₃ = (⋯.iso ⋯).inv
-- Mathlib.Analysis.Matrix.Spectrum
/-- The `ℝ`-spectrum of a Hermitian matrix over `RCLike` field is the range of the eigenvalue
function.  -/
Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), spectrum ℝ A = Set.range hA.eigenvalues
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_sInf : ∀ {G : Type u_2} [inst : Group G] (S : Set (Subgroup Gᵐᵒᵖ)), (sInf S).unop = sInf (Subgroup.op ⁻¹' S)
-- Mathlib.Data.Set.Prod
Set.univ_prod_univ : ∀ {α : Type u_1} {β : Type u_2}, Set.univ ×ˢ Set.univ = Set.univ
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.instInhabitedSimpHaveResult : Inhabited Lean.Meta.SimpHaveResult✝
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- An alternative constructor to `QuadraticMap.mk`, for rings where `polar` can be used.  -/
QuadraticMap.ofPolar : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (toFun : M → N) →
                  (∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x) →
                    (∀ (x x' y : M),
                        QuadraticMap.polar toFun (x + x') y =
                          QuadraticMap.polar toFun x y + QuadraticMap.polar toFun x' y) →
                      (∀ (a : R) (x y : M), QuadraticMap.polar toFun (a • x) y = a • QuadraticMap.polar toFun x y) →
                        QuadraticMap R M N
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (f f_1 : A.A ⟶ B.A) (e_f : f = f_1)
  (h : CategoryTheory.CategoryStruct.comp A.a (G.map f) = CategoryTheory.CategoryStruct.comp f B.a),
  { f := f, h := h } = { f := f_1, h := ⋯ }
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIioIci_apply_inl : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Iio x)), (OrderIso.sumLexIioIci x) (toLex (Sum.inl a)) = ↑a
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_range : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : Fintype β] (f : β → α) (h : (Set.range f).Finite),
  h.toFinset = Finset.image f Finset.univ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.AtomIso.mk.injEq : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr)
  (src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  ({ e := e, src := src, tgt := tgt } = { e := e_1, src := src_1, tgt := tgt_1 }) =
    (e = e_1 ∧ src = src_1 ∧ tgt = tgt_1)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ AddGrpCat AddMonCat)
      (AddMonCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)))
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (a : ε) → motive (Except.error a)),
  (match Except.error a with
    | Except.ok a => h_1 a
    | Except.error a => h_2 a) =
    h_2 a
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Every functor out of `WalkingReflexivePair` is isomorphic to the `reflexivePair` given by
its components  -/
CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) →
      F ≅
        CategoryTheory.Limits.reflexivePair (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
          (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
          (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) ⋯ ⋯
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eq_conj_eqToHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_of_notMem : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {s : Finset ι} {i : ι},
  i ∉ s → ∀ (f : (i : ι) → i ∈ s → α), (Finsupp.indicator s f) i = 0
-- Std.Time.Date.Unit.Month
Std.Time.Month.instOrdQuarter : Ord Std.Time.Month.Quarter
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_prod : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {ι : Type u_4} [inst_3 : Fintype ι] (f : ι → ↥S), ↑(∏ i, f i) = ∏ i, ↑(f i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm.injEq : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly) (c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
  (e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (p_1 : Lean.Grind.CommRing.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm c_1 e_1 p_1) =
    (c = c_1 ∧ e = e_1 ∧ p = p_1)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.BisimO.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s')))
  (h_3 : (x x_1 : Option (Stream'.Seq1 α)) → motive x x_1),
  (match none, none with
    | none, none => h_1 ()
    | some (a, s), some (a', s') => h_2 a s a' s'
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.funUnique_apply : ∀ (α : Type u_2) (M : Type u_4) [inst : Add M] [inst_1 : Unique α] (f : (i : α) → (fun a => M) i),
  (AddEquiv.funUnique α M) f = f default
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, t.WF → (t.modify k f).minKey? = t.minKey?
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The composition of copies is a copy.  -/
SimpleGraph.Copy.comp : {α : Type u_4} →
  {β : Type u_5} →
    {γ : Type u_6} → {A : SimpleGraph α} → {B : SimpleGraph β} → {C : SimpleGraph γ} → B.Copy C → A.Copy B → A.Copy C
-- Lean.Elab.Tactic.Basic
/-- Return the main goal tag.  -/
Lean.Elab.Tactic.getMainTag : Lean.Elab.Tactic.TacticM Lean.Name
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff m₂ ⋯) k = default
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.instZero : (K : Type u_1) →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → Zero (ConjRootClass K L)
-- Init.Data.UInt.Lemmas
USize.toUInt8_mod : ∀ (a b : USize), a < 256 → b < 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.differenceFunctor_map : ∀ {G : Type u} [inst : Group G] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C] (f : C → G) {x y : C}
  (x_1 : x ⟶ y), (CategoryTheory.SingleObj.differenceFunctor f).map x_1 = f y * (f x)⁻¹
-- Mathlib.Data.Sym.Basic
instDecidableEqSym : (α : Type u_1) → (n : ℕ) → [DecidableEq α] → DecidableEq (Sym α n)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Closure of a `NonUnitalSubring` `S` equals `S`.  -/
NonUnitalSubring.closure_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), NonUnitalSubring.closure ↑s = s