mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the image under the natural morphism to the quotient.  -/
quotient_norm_mk_eq : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M),
  ‖(QuotientAddGroup.mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
-- Std.Http.Data.Status
/-- 409 Conflict
 -/
Std.Http.Status.conflict : Std.Http.Status
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_apply_eq : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {x : A₂} {y : A₁}, e.symm x = y ↔ x = e y
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for indexed supremum  -/
Filter.Realizer.iSup : {α : Type u_1} → {β : Type u_2} → {f : α → Filter β} → ((i : α) → (f i).Realizer) → (⨆ i, f i).Realizer
-- Mathlib.Topology.ClusterPt
mem_interior_iff_not_clusterPt_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ interior s ↔ ¬ClusterPt x (Filter.principal sᶜ)
-- Mathlib.Data.NNRat.Defs
NNRat.coe_mk : ∀ (q : ℚ) (hq : 0 ≤ q), ↑⟨q, hq⟩ = q
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.IsInitial.isPrincipal_mul`. -/
Ordinal.IsInitial.principal_mul : ∀ {o : Ordinal.{u_1}}, o.IsInitial → Ordinal.omega0 ≤ o → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (j : C),
  ((t.eTriangleLTGE.obj i).obj j).obj₁ = (t.eTruncLT.obj i).obj j
-- Init.Core
/-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop  -/
DoResultSBC.continue : {α σ : Type u} → σ → DoResultSBC α σ
-- Mathlib.Topology.DiscreteSubset
mem_codiscrete_subtype_iff_mem_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X} {U : Set ↑S},
  U ∈ Filter.codiscrete ↑S ↔ Subtype.val '' U ∈ Filter.codiscreteWithin S
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_eq_posLT : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h = s.posLT p.offset ⋯
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.getElem_eq_getLsbD : ∀ {w : ℕ} (a : BitVec w) (i : ℕ) (h : i < w), a[i] = a.getLsbD i
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag_commute : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i₀ : ι) (D : ι → F)
  (hD : (Matrix.diagonal D).det = 1),
  (↑{i | i ≠ i₀}).Pairwise
    (Function.onFun Commute fun i => if hi : i ≠ i₀ then Matrix.SpecialLinearGroup.diag2n hi (D i) ⋯ else 1)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- The set of finite `ℝ≥0∞` numbers is `MeasurableEquiv` to `ℝ≥0`.  -/
MeasurableEquiv.ennrealEquivNNReal : ↑{r | r ≠ ⊤} ≃ᵐ NNReal
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.instHasLeftHomologyOppositeOpOfHasRightHomology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasRightHomology], S.op.HasLeftHomology
-- Mathlib.Topology.Connected.Basic
instPreconnectedSpaceProd : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [PreconnectedSpace α]
  [PreconnectedSpace β], PreconnectedSpace (α × β)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.one_sub_sq_div_two_le_cos : ∀ {x : ℝ}, 1 - x ^ 2 / 2 ≤ Real.cos x
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry : Type
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_opcyclesMap' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (hr₁ : S₁.RightHomologyData) (hr₂ : S₂.RightHomologyData) (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : hr₁.IsPreservedBy F] [inst_6 : hr₂.IsPreservedBy F],
  F.map (CategoryTheory.ShortComplex.opcyclesMap' φ hr₁ hr₂) =
    CategoryTheory.ShortComplex.opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
-- Lean.Meta.Sym.Pattern
/-- Returns `true` if the `i`th argument / pattern variable is a proof.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.Pattern.isProof : Lean.Meta.Sym.Pattern → ℕ → Bool
-- Mathlib.Topology.SeparatedMap
isSeparatedMap_iff_disjoint_nhds : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → Disjoint (nhds x₁) (nhds x₂)
-- Lean.DefEqAttrib
Lean.backward.defeqAttrib.useBackward : Lean.Option Bool
-- Mathlib.Algebra.GCDMonoid.Basic
associatesEquivOfUniqueUnits_apply : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : Subsingleton αˣ] (a : Associates α),
  associatesEquivOfUniqueUnits a = a.out
-- Mathlib.Topology.Algebra.Monoid
LocallyFinite.exists_finset_mulSupport : ∀ {ι : Type u_1} {X : Type u_5} [inst : TopologicalSpace X] {M : Type u_6} [inst_1 : One M] {f : ι → X → M},
  (LocallyFinite fun i => Function.mulSupport (f i)) →
    ∀ (x₀ : X), ∃ I, ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun i => f i x) ⊆ ↑I
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- Rotate a vector whose product is 1.  -/
Equiv.Perm.VectorsProdEqOne.rotate : {G : Type u_2} →
  [inst : Group G] → {n : ℕ} → ↑(Equiv.Perm.vectorsProdEqOne G n) → ℕ → ↑(Equiv.Perm.vectorsProdEqOne G n)
-- Init.Data.String.Basic
String.Pos.Raw.isValid_iff_isUTF8FirstByte : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.tsupport_subset : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n), tsupport ⇑f ⊆ ↑Ω
-- Lean.Util.LeanOptions
Lean.LeanOptions.values : Lean.LeanOptions → Lean.NameMap Lean.LeanOptionValue
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isAtomic : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (r : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)),
  (r.boundedFormula ts).IsAtomic
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.findDiscrRefinementPath.checkCompatibleApps : Lean.Expr → Lean.Expr → OptionT Lean.MetaM Unit
-- Mathlib.Tactic.TermCongr
/-- If `lhs` or `rhs` is a congruence hole, then process it.
Only process ones that are at least as new as `mvarCounterSaved`
since nothing prevents congruence holes from leaking into the local context.  -/
Mathlib.Tactic.TermCongr.mkCongrOfCHole? : ℕ → Lean.Expr → Lean.Expr → Lean.MetaM (Option Mathlib.Tactic.TermCongr.CongrResult)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfDom_comp_symm : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {k : P ≃* M}
  (H : Submonoid.map k.toMonoidHom T = S) (x : M), (f.ofMulEquivOfDom H) (k.symm x) = f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) = true},
  (m₁.diff m₂ ⋯).get k h_contains = m₁.get k ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum, as an affine map on the points involved.  -/
AffineMap.weightedVSubOfPoint : {k : Type u_1} →
  {V : Type u_2} →
    (P : Type u_3) →
      [inst : CommRing k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → k) → (ι → P) × P →ᵃ[k] V
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.pushChoice : Lean.Meta.Grind.EMatch.Choice → Lean.Meta.Grind.EMatch.M Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α}, (m₁.inter m₂ ⋯).get? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.get? k else none
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for `map m f` given a realizer for `f`  -/
Filter.Realizer.map : {α : Type u_1} → {β : Type u_2} → (m : α → β) → {f : Filter α} → f.Realizer → (Filter.map m f).Realizer
-- Init.Data.Array.Basic
Array.usize.eq_1 : ∀ {α : Type u} (xs : Array α), xs.usize = xs.size.toUSize
-- Init.Data.List.Range
List.getElem_zipIdx : ∀ {α : Type u_1} {i j : ℕ} {l : List α} (h : i < (l.zipIdx j).length), (l.zipIdx j)[i] = (l[i], j + i)
-- Mathlib.Data.Option.NAry
Option.map₂_none_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α), Option.map₂ f a none = none
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than the given key.
 -/
Std.TreeMap.getEntryLT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α × β
-- Lean.Data.KVMap
Lean.instReprKVMap.repr : Lean.KVMap → ℕ → Std.Format
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G},
  1 ∈ T → ∀ (hg : g ∈ S), (hST.equiv g).1 = ⟨g, hg⟩
-- Mathlib.Data.List.Fold
/-- **Alias** of `List.foldl_cons_eq_apply_foldl`. -/
List.foldl_eq_of_comm_of_assoc : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v],
  List.foldl v b (a :: l) = v (List.foldl v b l) a
-- Init.Data.UInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.complement : UInt32 → UInt32
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b}, curveIntegralFun (ω₁ + ω₂) γ = curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_add : ∀ {n : ℕ} {x y : BitVec n}, BitVec.Signed.rotate✝ (x + y) = BitVec.Signed.rotate✝ x + y
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.ae_ae_of_ae_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {a : α} {p : γ → Prop},
  (∀ᵐ (z : γ) ∂(η.comp κ) a, p z) → ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z
-- Mathlib.Data.ENat.Basic
ENat.lift_lt_iff : ∀ {x : ℕ∞} {h : x < ⊤} {n : ℕ}, x.lift h < n ↔ x < ↑n
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_mem_Icc_right_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (n : ℕ) (x : X),
  Urysohns.CU.approx n c x ∈ Set.Icc (Urysohns.CU.approx n c.right x) (Urysohns.CU.approx n c.left x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k fallback : α},
  (Std.ExtDHashMap.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  {S : Type u_3} [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] [inst_6 : IsScalarTower S R R],
  IsScalarTower S (R ⧸ I) ↥(Submodule.torsionBySet R M ↑I)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofComp_toAlgHom_monomial_sumElim : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (v₁ : ι' →₀ ℕ)
  (v₂ : ι →₀ ℕ) (a : R),
  (Q.ofComp P).toAlgHom ((MvPolynomial.monomial (v₁.sumElim v₂)) a) =
    (MvPolynomial.monomial v₁) ((MvPolynomial.aeval P.val) ((MvPolynomial.monomial v₂) a))
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_mem : ∀ {α : Type u_1} {s : Set α} [inst : MeasurableSpace α], (Measurable fun x => x ∈ s) ↔ MeasurableSet s
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Zero loci of minimal prime ideals of `R` are irreducible components in `Spec R` and any
irreducible component is a zero locus of some minimal prime ideal.  -/
minimalPrimes.equivIrreducibleComponents : (R : Type u) → [inst : CommSemiring R] → ↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.iIndepFun.integral_fun_prod_eq_prod_integral : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3}
  [inst_1 : Fintype ι] {X : ι → Ω → 𝕜},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (X i) μ) → ∫ (ω : Ω), ∏ i, X i ω ∂μ = ∏ i, ∫ (x : Ω), X i x ∂μ
-- Mathlib.Algebra.RingQuot
RingQuot.ringQuot_ext_iff : ∀ {R : Type uR} [inst : Semiring R] {T : Type uT} [inst_1 : NonAssocSemiring T] {r : R → R → Prop}
  {f g : RingQuot r →+* T}, f = g ↔ f.comp (RingQuot.mkRingHom r) = g.comp (RingQuot.mkRingHom r)
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or
underflow.

This function is overridden at runtime with an efficient implementation.
 -/
Int.toISize : ℤ → ISize
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.npow.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.npow = { pow := fun a n => ⟨↑a ^ n, ⋯⟩ }
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.toSubspace.eq_1 : ∀ {η : Type u_1} {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line (η → α) ι),
  l.toSubspace = { idxFun := fun ie => (l.idxFun ie.1).elim (Sum.inr ie.2) fun f => Sum.inl (f ie.2), proper := ⋯ }
-- Lean.HeadIndex
/-- Datastructure for representing the "head symbol" of an expression.
It is the key of `KExprMap`.
Examples:
- The head of `f a` is `.const f`
- The head of `let x := 1; f x` is `.const f`
- The head of `fun x => fun` is `.lam`

`HeadIndex` is a very simple index, and is used in situations where
we want to find definitionally equal terms, but we want to minimize
the search by checking only pairs of terms that have the same
`HeadIndex`.
 -/
Lean.HeadIndex : Type
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinsert_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.ndinsert a 0 = {a}
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- Given measures `μ`, `ν` where `ν ≤ μ`, `FiniteSpanningSetsIn.ofLe` provides the induced
`FiniteSpanningSet` with respect to `ν` from a `FiniteSpanningSet` with respect to `μ`.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE : {α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ ν : MeasureTheory.Measure α} → ν ≤ μ → {C : Set (Set α)} → μ.FiniteSpanningSetsIn C → ν.FiniteSpanningSetsIn C
-- Mathlib.Geometry.Euclidean.Projection
/-- The square of the distance between two points constructed by
adding multiples of the same orthogonal vector to points in the same
subspace.  -/
EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  {p₁ p₂ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      ∀ (r₁ r₂ : 𝕜) {v : V},
        v ∈ s.directionᗮ →
          dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
            dist p₁ p₂ * dist p₁ p₂ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Cfg.mk.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Γ] (q : Λ) (Tape : Turing.Tape Γ) (q_1 : Λ) (Tape_1 : Turing.Tape Γ),
  ({ q := q, Tape := Tape } = { q := q_1, Tape := Tape_1 }) = (q = q_1 ∧ Tape = Tape_1)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A product of meromorphic functions in normal form is in normal form if at most one of the factors
vanishes.
 -/
meromorphicNFOn_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜},
  (∀ i ∈ s, MeromorphicNFOn (f i) U) →
    (∀ x ∈ U, {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton) → MeromorphicNFOn (∏ i ∈ s, f i) U
-- Mathlib.RepresentationTheory.Action
Representation.linearize_single : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X : Action (Type w) G} (g : G) (x : X.V),
  ((Representation.linearize k G X) g) (MonoidAlgebra.single x 1) =
    MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) x) 1
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_erase_one : ∀ {M : Type u_1} (s : Set M) [inst : MulOneClass M], SimpleGraph.mulCayley (s \ {1}) = SimpleGraph.mulCayley s
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of `n + 1` points in an indexed family has
dimension at most `n`.  -/
finrank_vectorSpan_image_finset_le : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] (p : ι → P) (s : Finset ι) {n : ℕ},
  s.card = n + 1 → Module.finrank k ↥(vectorSpan k ↑(Finset.image p s)) ≤ n
-- Init.Data.UInt.Lemmas
UInt64.toNat_mul : ∀ (a b : UInt64), (a * b).toNat = a.toNat * b.toNat % 2 ^ 64
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  I.subschemeObjIso U =
    CategoryTheory.Functor.mapIso I.subscheme.presheaf (CategoryTheory.eqToIso ⋯).op ≪≫
      AlgebraicGeometry.Scheme.Hom.appIso (I.subschemeCover.f U) ⊤ ≪≫
        AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U))
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.congr_iff : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X Y : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E},
  X =ᵐ[ℙ] Y → (MeasureTheory.HasPDF X ℙ μ ↔ MeasureTheory.HasPDF Y ℙ μ)
-- Lean.Widget.Diff
/-- Add a tag at the given position to the `changesBefore` dict.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.insertBeforeChange : Lean.SubExpr.Pos →
  optParam Lean.Widget.ExprDiffTag✝ Lean.Widget.ExprDiffTag.change✝ → Lean.Widget.ExprDiff✝ → Lean.Widget.ExprDiff✝
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_eq_bot_of_bot_mem : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : OrderBot α] {s : Set α}, ⊥ ∈ s → sInf s = ⊥
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.inv_toFun : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → m.inv.toFun basis =ᶠ[Filter.atTop] (m.toFun basis)⁻¹
-- Mathlib.Algebra.Group.Action.Units
Units.val_smul : ∀ {G : Type u_1} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulAction G M]
  [inst_3 : SMulCommClass G M M] [inst_4 : IsScalarTower G M M] (g : G) (m : Mˣ), ↑(g • m) = g • ↑m
-- Mathlib.Data.Int.Order.Lemmas
Int.abs_le_sqrt : ∀ {a b : ℤ}, 0 ≤ b → (|a| ≤ Int.sqrt b ↔ a * a ≤ b)
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.offset : String.Slice.RevByteIterator → String.Pos.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} [inst_1 : SizeOf C]
  (f : Y ⟶ h.pullback)
  (f_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam)
  (f_p₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam)
  (f_p :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam),
  sizeOf { f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p } = 1 + sizeOf f + sizeOf f_p₁ + sizeOf f_p₂ + sizeOf f_p
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_mul_snd : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g g₁ : G) (a : ↑A) (s : ↥S),
  (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)
-- Init.Data.Nat.Basic
Nat.pow_left_inj : ∀ {a b n : ℕ}, n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.mk.sizeOf_spec : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : SizeOf X]
  [inst_3 : SizeOf Y] (toFun : X → Y)
  (continuous_toFun : autoParam (Continuous toFun) ContinuousMap.continuous_toFun._autoParam),
  sizeOf { toFun := toFun, continuous_toFun := continuous_toFun } = 1 + sizeOf continuous_toFun
-- Mathlib.Data.Seq.Parallel
Computation.mem_parallel : ∀ {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α},
  (∀ s ∈ S, s.Promises a) → ∀ {c : Computation α}, c ∈ S → a ∈ c → a ∈ Computation.parallel S
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_add : ∀ {α : Type u} {β : Type v} [inst : Add α] {F : Type u_1} [inst_1 : Add β] [inst_2 : FunLike F α β] [AddHomClass F α β]
  (f : F) (a b : WithBot α), WithBot.map (⇑f) (a + b) = WithBot.map (⇑f) a + WithBot.map (⇑f) b
-- Mathlib.Logic.Unique
uniqueElim_const : ∀ {ι : Sort u_2} {β : Sort u_4} {x : Unique ι} (x_1 : β) (i : ι), uniqueElim x_1 i = x_1
-- Mathlib.Algebra.MonoidAlgebra.Lift
/-- A non-commutative version of `AddMonoidAlgebra.lift`: given an additive homomorphism
`f : k →+ R` and a map `g : Multiplicative G → R`, returns the additive
homomorphism from `k[G]` such that `liftNC f g (single a b) = f b * g a`. If `f`
is a ring homomorphism and the range of either `f` or `g` is in center of `R`, then the result is a
ring homomorphism.  If `R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra
homomorphism called `AddMonoidAlgebra.lift`.  -/
AddMonoidAlgebra.liftNC : {k : Type u₁} →
  {G : Type u₂} →
    {R : Type u_2} →
      [inst : Semiring k] →
        [inst_1 : NonUnitalNonAssocSemiring R] → (k →+ R) → (Multiplicative G → R) → AddMonoidAlgebra k G →+ R