mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.mk.injEq : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
  (δ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map = f.map)
      SSet.PtSimplex.RelStruct.δ_castSucc_map._autoParam)
  (δ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map = g.map)
      SSet.PtSimplex.RelStruct.δ_succ_map._autoParam)
  (δ_map_of_lt :
    autoParam (∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)), i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_gt._autoParam)
  (map_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
  (δ_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map_1 = f.map)
      SSet.PtSimplex.RelStruct.δ_castSucc_map._autoParam)
  (δ_succ_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map_1 = g.map)
      SSet.PtSimplex.RelStruct.δ_succ_map._autoParam)
  (δ_map_of_lt_1 :
    autoParam (∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt_1 :
    autoParam
      (∀ (j : Fin (n + 2)), i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_gt._autoParam),
  ({ map := map, δ_castSucc_map := δ_castSucc_map, δ_succ_map := δ_succ_map, δ_map_of_lt := δ_map_of_lt,
        δ_map_of_gt := δ_map_of_gt } =
      { map := map_1, δ_castSucc_map := δ_castSucc_map_1, δ_succ_map := δ_succ_map_1, δ_map_of_lt := δ_map_of_lt_1,
        δ_map_of_gt := δ_map_of_gt_1 }) =
    (map = map_1)
-- Std.Do.SPred.SPred
Std.Do.SPred.and_nil : ∀ {P Q : Std.Do.SPred []}, spred(P ∧ Q) = { down := P.down ∧ Q.down }
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_28 : HAdd Std.Time.Hour.Offset Std.Time.Day.Offset Std.Time.Hour.Offset
-- Mathlib.Algebra.Quandle
/-- Free generators of the enveloping group.
 -/
Rack.PreEnvelGroup : Type u → Type u
-- Mathlib.Analysis.Fourier.Notation
FourierInvAdd.fourierInv_add : ∀ {E : Type u_5} {F : outParam (Type u_6)} {inst : Add E} {inst_1 : Add F} {inst_2 : FourierTransformInv E F}
  [self : FourierInvAdd E F] (f g : E),
  FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)],
  ∅.get! a = default
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  ProbabilityTheory.HasSubgaussianMGF 0 0 μ
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.mk.sizeOf_spec : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [inst : SizeOf α] [inst_1 : (a : Type u) → SizeOf (m a)]
  [inst_2 : (a : Type (max u v)) → SizeOf (n a)] [inst_3 : SizeOf β] (inner : Std.IterM m β),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.setInvOn_digitsAppend_ofDigits : ∀ {b : ℕ},
  1 < b → ∀ (l : ℕ), Set.InvOn (b.digitsAppend l) (Nat.ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} {n | n < b ^ l}
-- Init.Data.Vector.Lemmas
Vector.forall_cons_iff : ∀ {α : Type u_1} {n : ℕ} {P : Vector α (n + 1) → Prop},
  (∀ (xs : Vector α (n + 1)), P xs) ↔ ∀ (x : α) (xs : Vector α n), P (xs.push x)
-- Mathlib.Algebra.FiveLemma
/-- A special case of the five lemma in terms of groups. For a diagram explaining the
variables, see the module docstring.  -/
MonoidHom.bijective_of_bijective_of_injective_of_left_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : Group M₁]
  [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group N₁] [inst_4 : Group N₂] [inst_5 : Group N₃] (f₁ : M₁ →* M₂)
  (f₂ : M₂ →* M₃) (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.MulExact ⇑f₁ ⇑f₂ →
        Function.MulExact ⇑g₁ ⇑g₂ →
          Function.Bijective ⇑i₂ →
            Function.Injective ⇑i₃ → Function.Injective ⇑f₁ → Function.Injective ⇑g₁ → Function.Bijective ⇑i₁
-- Mathlib.Algebra.Opposites
AddOpposite.instVAdd : {α : Type u_1} → {β : Type u_2} → [VAdd α β] → VAdd α βᵃᵒᵖ
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E}, IsBoundedLinearMap 𝕜 f → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics.  -/
Polynomial.eq_neg_mul_add_of_roots_quadratic_eq_pair : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {a b c x1 x2 : R},
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2} →
    b = -a * (x1 + x2)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ι_postcompose : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g f' g' : X ⟶ Y}
  {α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'}
  {c : CategoryTheory.Limits.Fork f g},
  CategoryTheory.Limits.Fork.ι ((CategoryTheory.Limits.Cone.postcompose α).obj c) =
    CategoryTheory.CategoryStruct.comp c.ι (α.app CategoryTheory.Limits.WalkingParallelPair.zero)
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionOfComplement.of_opens : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
  (s : TopologicalSpace.Opens M), Manifold.IsImmersionOfComplement PUnit.{u_15 + 1} I I n Subtype.val
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_inter_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a b ∩ Set.Iio c = Set.Ico a (min b c)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keys_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → Bool},
  t.WF → (Std.TreeMap.Raw.filter (fun k x => f k) t).keys = List.filter f t.keys
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYonedaEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {X : C},
  PresheafOfModules.freeYonedaEquiv = PresheafOfModules.freeHomEquiv.trans CategoryTheory.yonedaEquiv
-- Lean.Meta.Tactic.Congr
/-- Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ f as ≍ f bs`, try to apply congruence.
It takes proof irrelevance into account, and the fact that `Decidable p` is a subsingleton.

* Applies `congr` recursively up to depth `depth`.
* If `closePre := true`, it will attempt to close new goals
  using `Eq.refl`, `HEq.refl`, and `assumption` with reducible transparency.
* If `closePost := true`, it will try again on goals on which `congr` failed to make progress
  with default transparency.
 -/
Lean.MVarId.congrN : Lean.MVarId → optParam ℕ 1000000 → optParam Bool true → optParam Bool true → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_distrib`. -/
Set.union_diff_distrib : ∀ {α : Type u_1} {s t u : Set α}, (s ∪ t) \ u = s \ u ∪ t \ u
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ),
  (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).Additive
-- Mathlib.Tactic.Rename
/-- `rename' h => hnew` renames the hypothesis named `h` to `hnew`.
To rename several hypothesis, use `rename' h₁ => h₁new, h₂ => h₂new`.
You can use `rename' a => b, b => a` to swap two variables.  -/
Mathlib.Tactic.rename' : Lean.ParserDescr
-- Mathlib.Order.Category.Frm
Frm.instCoeSortType : CoeSort Frm (Type u_1)
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.bot_isMaximal : ∀ {K : Type u} [inst : DivisionSemiring K], ⊥.IsMaximal
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkSyntaxAbbrev : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.Order.Hom.Basic
OrderHom.apply_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : α →o β} {x y : α},
  f ≤ g → x ≤ y → f x ≤ g y
-- Mathlib.Data.Finset.NAry
Finset.image₂_right_comm : ∀ {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [inst : DecidableEq δ']
  [inst_1 : DecidableEq ε] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {γ : Type u_14} {u : Finset γ}
  {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) →
    Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ g' (Finset.image₂ f' s u) t
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAddMonoid : {α : Type u} → [AddSemigroup α] → AddMonoid (WithZero α)
-- Lean.Data.NameMap.Basic
Lean.NameSSet.insert : Lean.NameSSet → Lean.Name → Lean.NameSSet
-- Mathlib.Data.Option.NAry
Option.map₂_coe_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) (b : β),
  Option.map₂ f a (some b) = Option.map (fun a => f a b) a
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opEquivalence_counitIso : CategoryTheory.Cat.opEquivalence.counitIso =
  CategoryTheory.NatIso.ofComponents
    (fun x =>
      { hom := (CategoryTheory.unopUnop ↑x).toCatHom, inv := (CategoryTheory.opOp ↑x).toCatHom, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    @CategoryTheory.Cat.opEquivalence._proof_4
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β},
  ⇑e₁ = ⇑e₂ → e₁ = e₂
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.isEmpty_functions_constantsOn_succ : ∀ {α : Type u'} {n : ℕ}, IsEmpty ((FirstOrder.Language.constantsOn α).Functions (n + 1))
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.mem_centeredArc_div : ∀ {z : Circle} {s : ℝ} {n : ℕ},
  s ≤ Real.pi → z ∈ Circle.centeredArc (Real.pi / ↑n) → z ^ n ∈ Circle.centeredArc s → z ∈ Circle.centeredArc (s / ↑n)
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.instComp_id : ∀ {N : Type u_1} {P : Type u_2} {φ : N → N} [CompTriple.IsId φ] {ψ : N → P}, CompTriple φ ψ ψ
-- Mathlib.Computability.TuringMachine.Config
/-- Evaluating `c : Code` in a continuation `k : Cont` and input `v : List ℕ`. This goes by
recursion on `c`, building an augmented continuation and a value to pass to it.

* `zero' v = 0 :: v` evaluates immediately, so we return it to the parent continuation
* `succ v = [v.headI.succ]` evaluates immediately, so we return it to the parent continuation
* `tail v = v.tail` evaluates immediately, so we return it to the parent continuation
* `cons f fs v = (f v).headI :: fs v` requires two sub-evaluations, so we evaluate
  `f v` in the continuation `k (_.headI :: fs v)` (called `Cont.cons₁ fs v k`)
* `comp f g v = f (g v)` requires two sub-evaluations, so we evaluate
  `g v` in the continuation `k (f _)` (called `Cont.comp f k`)
* `case f g v = v.head.casesOn (f v.tail) (fun n => g (n :: v.tail))` has the information needed
  to evaluate the case statement, so we do that and transition to either
  `f v` or `g (n :: v.tail)`.
* `fix f v = let v' := f v; if v'.headI = 0 then k v'.tail else fix f v'.tail`
  needs to first evaluate `f v`, so we do that and leave the rest for the continuation (called
  `Cont.fix f k`)
 -/
Turing.ToPartrec.stepNormal : Turing.ToPartrec.Code → Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (CategoryTheory.CategoryStruct.comp (F.map f₁₂) (F.map f₂₃)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) h) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom h))
-- Mathlib.Algebra.Algebra.Defs
Algebra.coe_linearMap : ∀ (R : Type u) (A : Type w) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ⇑(Algebra.linearMap R A) = ⇑(algebraMap R A)
-- Mathlib.Topology.Order.LiminfLimsup
/-- If the liminf and the limsup of a function coincide, then the limit of the function
exists and has the same value.  -/
tendsto_of_liminf_eq_limsup : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {f : Filter β} {u : β → α} {a : α},
  Filter.liminf u f = a →
    Filter.limsup u f = a →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) tendsto_of_liminf_eq_limsup._auto_1 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) tendsto_of_liminf_eq_limsup._auto_3 →
          Filter.Tendsto u f (nhds a)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` fixes `(j • h) +ᵥ x` iff `g` fixes `x`.  -/
AddAction.vadd_zsmul_fixedBy_eq_of_addCommute : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g h : G},
  AddCommute g h → ∀ (j : ℤ), j • h +ᵥ AddAction.fixedBy α g = AddAction.fixedBy α g
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_of_source_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0), f = 0
-- Std.Data.HashSet.Basic
/-- Computes the difference of the given hash sets.

This function always iterates through the smaller set, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashSet.diff : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → Std.HashSet α → Std.HashSet α
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_shiftRight : ∀ (a b : UInt16), (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 16)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toEventualRanges_finite : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [inst_1 : CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Finite (F.obj j)] (j : J),
  Finite (F.toEventualRanges.obj j)
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.sub_nonpos_of_le : ∀ {α : Type u} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α}, a ≤ b → a - b ≤ 0
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.Substructure.inclusion.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S T : L.Substructure M} (h : S ≤ T),
  FirstOrder.Language.Substructure.inclusion h = FirstOrder.Language.Substructure.inclusion h
-- Mathlib.LinearAlgebra.QuadraticForm.Real
/-- **Sylvester's law of inertia**: A real quadratic form is equivalent to a weighted
sum of squares with the weights being ±1 or 0.  -/
QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M),
  ∃ w,
    (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧
      QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply : ∀ {X : AlgebraicGeometry.LocallyRingedSpace} {R : CommRingCatᵒᵖ}
  (f : AlgebraicGeometry.LocallyRingedSpace.Γ.rightOp.obj X ⟶ R),
  (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X R) f =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.identityToΓSpec.app X)
      (AlgebraicGeometry.Spec.locallyRingedSpaceMap f.unop)
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Non-unital convolution semiring structure on linear maps from a coalgebra to a
non-unital algebra.  -/
LinearMap.convNonUnitalSemiring : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : AddCommMonoid C] →
                  [inst_6 : Module R C] → [Coalgebra R C] → NonUnitalSemiring (WithConv (C →ₗ[R] A))
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- The locally discrete bicategory on a category is a bicategory in which the objects and the
1-morphisms are the same as those in the underlying category, and the 2-morphisms are the
equalities between 1-morphisms.
 -/
CategoryTheory.locallyDiscreteBicategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Bicategory (CategoryTheory.LocallyDiscrete C)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.toFun_eq_rTensor_φ_toFun' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type v} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N) {t : TensorProduct R S M} {s : Finset S} {p : TensorProduct R (MvPolynomial (Fin s.card) R) M},
  PolynomialLaw.π R M S ⟨s, p⟩ = t →
    PolynomialLaw.toFun S f t =
      (LinearMap.rTensor N (PolynomialLaw.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instAlt : List Lean.Name →
  List Lean.Level →
    Lean.Compiler.LCNF.Alt Lean.Compiler.LCNF.Purity.pure → Lean.Compiler.LCNF.Alt Lean.Compiler.LCNF.Purity.pure
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Products distribute over sums as measurable spaces.  -/
MeasurableEquiv.sumProdSum : (α : Type u_6) →
  (β : Type u_7) →
    (γ : Type u_8) →
      (δ : Type u_9) →
        [inst : MeasurableSpace α] →
          [inst_1 : MeasurableSpace β] →
            [inst_2 : MeasurableSpace γ] →
              [inst_3 : MeasurableSpace δ] → (α ⊕ β) × (γ ⊕ δ) ≃ᵐ (α × γ ⊕ α × δ) ⊕ β × γ ⊕ β × δ
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algebraMap_eq_inlHom : ∀ (R' : Type u) (M : Type v) [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M],
  algebraMap R' (TrivSqZeroExt R' M) = TrivSqZeroExt.inlHom R' M
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_copy : ∀ {K : Type u} [inst : DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.Algebra.Category.ModuleCat.Ext.Basic
/-- `r • 𝟙 M` induces a monomorphism in `Ext M N n` if and only if scalar multiplication by `r`
is faithful on `Ext M N n`.  -/
CategoryTheory.Abelian.Ext.postcomp_smul_id_mono_iff : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] {M N : ModuleCat R} (r : R) (i : ℕ),
  CategoryTheory.Mono
      (AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ (r • CategoryTheory.CategoryStruct.id M)).postcomp N ⋯)) ↔
    IsSMulRegular (CategoryTheory.Abelian.Ext N M i) r
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.nonempty_iff_nontrivial : ∀ {R : Type u} [inst : CommSemiring R], Nonempty (PrimeSpectrum R) ↔ Nontrivial R
-- Mathlib.Algebra.Order.Hom.Monoid
/-- See Note [custom simps projection]  -/
OrderMonoidIso.Simps.symm_apply : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → (α ≃*o β) → β → α
-- Mathlib.Algebra.Category.CommBialgCat
/-- Turn an unbundled `R`-bialgebra into the corresponding object in the category of `R`-bialgebras.

This is the preferred way to construct a term of `CommBialgCat R`.  -/
CommBialgCat.of : (R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : CommRing X] → [Bialgebra R X] → CommBialgCat R
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.lTensorBot_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (a : ↥A), A.lTensorBot.symm a = 1 ⊗ₜ[R] a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorHom_left_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X S U : C} {R T : CategoryTheory.Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ CategoryTheory.Over.mk fS)
  (g : T ⟶ CategoryTheory.Over.mk fU),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.Limits.pullback.fst fS fU) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom T.hom) (CategoryTheory.Over.Hom.left f)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.eq_false_of_isUnsat : ∀ (ctx : Nat.Internal.Linear.Context) {c : Nat.Internal.Linear.PolyCnstr},
  c.isUnsat = true → Nat.Internal.Linear.PolyCnstr.denote ctx c = False
-- Mathlib.Topology.Algebra.Affine
eventually_homothety_image_subset_of_finite_subset_interior : ∀ (R : Type u_1) {W : Type u_4} {Q : Type u_5} [inst : AddCommGroup W] [inst_1 : TopologicalSpace W]
  [inst_2 : AddTorsor W Q] [inst_3 : TopologicalSpace Q] [IsTopologicalAddTorsor Q] [inst_5 : CommRing R]
  [inst_6 : TopologicalSpace R] [inst_7 : Module R W] [ContinuousSMul R W] (x : Q) {s t : Set Q},
  t.Finite → t ⊆ interior s → ∀ᶠ (δ : R) in nhds 1, ⇑(AffineMap.homothety x δ) '' t ⊆ s
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.one : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : One β], HasCompactMulSupport 1
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.of_not_isSingular : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → ¬c.IsSingular → c.IsRegular
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.takeEndWhile_prop_eq_takeEndWhile_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.takeEndWhile p = s.takeEndWhile fun x => decide (p x)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_false_iff_exists_isSome_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)},
  l.isEmpty = false ↔ ∃ a, (Std.Internal.List.getEntry? a l).isSome = true