mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Prod
/-- Swaps the elements in a pair.

Examples:
* `(1, 2).swap = (2, 1)`
* `("orange", -87).swap = (-87, "orange")`
 -/
Prod.swap : {α : Type u_1} → {β : Type u_2} → α × β → β × α
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_le_iff : ∀ {u : ℕ → ENNReal} {a : EReal}, ExpGrowth.expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ (b * ↑n).exp
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.termρ_ : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The volume form on an oriented real inner product space can be evaluated as the determinant with
respect to any orthonormal basis of the space compatible with the orientation.  -/
Orientation.volumeForm_robust : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (b : OrthonormalBasis (Fin n) ℝ E),
  b.toBasis.orientation = o → o.volumeForm = b.toBasis.det
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_iso_hom : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).iso.hom = S.iso.hom.app x
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_const : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] [hι : Nonempty ι] {a : α}, ⨆ x, a = a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.quasiCoherentData_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [inst_3 : q.IsLocallyFreeData], q.quasiCoherentData.I = q.I
-- Mathlib.LinearAlgebra.InvariantBasisNumber
Module.Finite.exists_nat_not_surjective : ∀ (R : Type u) [inst : Semiring R] [RankCondition R] (M : Type u_1) [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Finite R M], ∃ n, ∀ (f : M →ₗ[R] Fin n → R), ¬Function.Surjective ⇑f
-- Batteries.Control.AlternativeMonad
mapConst_failure : ∀ {m : Type u_1 → Type u_2} {β α : Type u_1} [inst : Alternative m] [LawfulAlternative m] (y : β),
  Functor.mapConst y failure = failure
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Ideal.isCancelMulZero : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], IsCancelMulZero (Ideal A)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Infinite.of_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α}, (a +ᵥ s).Infinite → s.Infinite
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.eq_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) {x : β} {y : α}, y = e.symm x ↔ e y = x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforward_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (i : E.I₀), (CategoryTheory.PreZeroHypercover.pushforward f E).X i = E.X i
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.neg_ofNat_smul : ∀ {n : ℕ} {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {a : A}
  [inst_3 : n.AtLeastTwo], -OfNat.ofNat n • a = -OfNat.ofNat n * a
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isClosed_iff_iSup : ∀ {s : Set Ordinal.{u}},
  IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
-- Mathlib.Data.Set.Insert
Set.disjoint_singleton_right : ∀ {α : Type u_1} {s : Set α} {a : α}, Disjoint s {a} ↔ a ∉ s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion_id : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData),
  AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯ = CategoryTheory.CategoryStruct.id I.subscheme
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_whisker_left : ∀ {B : Type u} [inst : Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c}
  (η : CategoryTheory.FreeBicategory.Hom₂ g h),
  (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η).mk = CategoryTheory.Bicategory.whiskerLeft f η.mk
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integral_deriv_comp_mul_deriv : ∀ {a b : ℝ} {f f' g g' : ℝ → ℝ},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt g (g' (f x)) (f x)) →
      ContinuousOn f' (Set.uIcc a b) → Continuous g' → ∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
-- Init.Data.Int.Lemmas
Int.sub_eq_iff_eq_add : ∀ {b a c : ℤ}, a - b = c ↔ a = c + b
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.le_trans : ∀ {α : Type u} (self : Std.Packages.PreorderOfLEArgs α),
  let this := self.le;
  ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.PreprocessorToGlobalBranchingPreprocessor : Coe Mathlib.Tactic.Linarith.Preprocessor Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.constOfIsEmpty_toMultilinearMap : ∀ (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : IsEmpty ι] (m : M₂),
  (ContinuousMultilinearMap.constOfIsEmpty R M₁ m).toMultilinearMap = MultilinearMap.constOfIsEmpty R M₁ m
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.prodMk_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {E'' : Type u_8} [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {x : M}
  {f : M → E'} {g : M → E''}, MDiffAt f x → MDiffAt g x → (MDiffAt fun x => (f x, g x)) x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Auxiliary lemma for `hasStrictFDerivAt_multiset_prod`.

For `NormedCommRing 𝔸'`, can rewrite as `Multiset` using `Multiset.prod_coe`.
 -/
hasStrictFDerivAt_list_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] [inst_3 : DecidableEq ι] [Finite ι] {l : List ι} {x : ι → 𝔸'},
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (List.map (fun i => (List.map x (l.erase i)).prod • ContinuousLinearMap.proj i) l).sum x
-- Mathlib.Algebra.Module.Projective
/-- Free modules are projective.  -/
Module.Projective.of_basis : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {ι : Type u_8}
  (b : Module.Basis ι R P), Module.Projective R P
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.continuousOn_sin : ∀ {s : Set ℂ}, ContinuousOn Complex.sin s
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.instDecidableRelR : {V : Type u_1} →
  [inst : Fintype V] →
    {G : SimpleGraph V} → [inst_1 : DecidableRel G.Adj] → {r : ℕ} → (h : G.IsTuranMaximal r) → DecidableRel ⇑h.setoid
-- Init.Data.List.Find
List.isSome_find? : ∀ {α : Type u_1} {xs : List α} {f : α → Bool}, (List.find? f xs).isSome = xs.any fun x => f x
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.bijective_of_isScalarTower : ∀ {K : Type u_1} {L : Type u_2} {R : Type u_3} [inst : CommRing K] [IsDomain K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [Module.IsTorsionFree K L] [Algebra.IsAlgebraic K L] [inst_6 : DivisionRing R]
  [inst_7 : Algebra K R] [inst_8 : Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L), Function.Bijective ⇑f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k : α} {fallback : β k},
      (List.map Sigma.fst l).contains k = false → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [T1Space E] {y : E},
  HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.pre.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A),
  CategoryTheory.MonoidalClosed.pre f =
    (CategoryTheory.conjugateEquiv (CategoryTheory.ihom.adjunction A) (CategoryTheory.ihom.adjunction B))
      ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f)
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_apply_le : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0] (n : ℕ),
  l.length ≤ n → l.toFinsupp n = 0
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Technical lemma which will give us differentiability of Hurwitz zeta at `s = 0`.  -/
HurwitzZeta.differentiableAt_update_of_residue : ∀ {Λ : ℂ → ℂ},
  (∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s) →
    ∀ {L : ℂ},
      Filter.Tendsto (fun s => s * Λ s) (nhdsWithin 0 {0}ᶜ) (nhds L) →
        ∀ (s : ℂ), s ≠ 1 → DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_skipSuffixWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String.Slice} {h : s.skipSuffixWhile p ≠ s.startPos},
  p (((s.skipSuffixWhile p).prev h).get ⋯) = false
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_smul_ofReal_right : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) {t : ℝ}, inner 𝕜 x (↑t • y) = inner 𝕜 x y * ↑t
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- A presheaf `P` is a sheaf for the Grothendieck topology generated by a pretopology `K`
iff for every covering presieve `R` of `K`, the natural cone associated to `P` and
`Sieve.generate R` is a limit cone.  -/
CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (P : CategoryTheory.Functor Cᵒᵖ A) [inst_2 : CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C),
  CategoryTheory.Presheaf.IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄,
      ∀ R ∈ K.coverings X,
        Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprCPUInfo.repr : Std.Internal.UV.System.CPUInfo → ℕ → Std.Format
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.coe_moebius_mul_coe_zeta : ∀ {R : Type u_1} [inst : Ring R], ↑ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta = 1
-- Mathlib.Tactic.Widget.Calc
instRpcEncodableCalcParams : Lean.Server.RpcEncodable CalcParams
-- Mathlib.CategoryTheory.Filtered.Basic
/-- An arbitrary choice of object "to the right"
of a finite collection of objects `O` and morphisms `H`,
making all the triangles commute.
 -/
CategoryTheory.IsFiltered.sup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFiltered C] →
      (O : Finset C) → Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) → C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.eraseMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List α), (t₁.eraseMany l).Equiv (t₂.eraseMany l)
-- Init.Data.SInt.Lemmas
Int32.not_lt_minValue : ∀ {a : Int32}, ¬a < Int32.minValue
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofIntClamp : ∀ {n : ℤ}, Int16.minValue.toInt ≤ n → n ≤ Int16.maxValue.toInt → (Int16.ofIntClamp n).toBitVec = BitVec.ofInt 16 n
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.toAddEquiv : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} → [inst_1 : TopologicalSpace H] → [inst_2 : Add G] → [inst_3 : Add H] → G ≃ₜ+ H → G ≃+ H
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_zero_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sqrt_eq_zero_iff._auto_1 → (CFC.sqrt a = 0 ↔ a = 0)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
LiouvilleNumber.partialSum.eq_1 : ∀ (m : ℝ) (k : ℕ), LiouvilleNumber.partialSum m k = ∑ i ∈ Finset.range (k + 1), 1 / m ^ i.factorial
-- Mathlib.Data.Nat.Find
Nat.find_le : ∀ {n : ℕ} {p : ℕ → Prop} [inst : DecidablePred p] {h : ∃ n, p n}, p n → Nat.find h ≤ n
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The comap of the identity is the identity. In this variant of the lemma, two open subsets `U` and
`V` are given as arguments, together with a proof that `U = V`. This is useful when `U` and `V`
are not definitionally equal.
 -/
AlgebraicGeometry.StructureSheaf.comap_id : ∀ {R : Type u} [inst : CommRing R] {U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)}
  (hUV : U = V),
  AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (CategoryTheory.eqToHom ⋯)
-- Init.Data.Nat.Fold
Nat.foldRev_congr : ∀ {α : Type u} {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → α → α) (init : α),
  n.foldRev f init = m.foldRev (fun i h => f i ⋯) init
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.xor.eq_1 : Nat.xor = Nat.bitwise bne
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Icc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.rev (Finset.Icc i j) = Finset.Icc j.rev i.rev
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The initial state for the TM2 emulator, given an initial TM2 state. All stacks start out empty
except for the input stack, and the stack bottom mark is set at the head.  -/
Turing.TM2to1.trInit : {K : Type u_1} → {Γ : K → Type u_2} → [DecidableEq K] → (k : K) → List (Γ k) → List (Turing.TM2to1.Γ' K Γ)
-- Mathlib.Order.LiminfLimsup
Filter.liminf.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] (u : β → α) (f : Filter β),
  Filter.liminf u f = (Filter.map u f).limsInf
-- Init.Data.List.Nat.TakeDrop
List.take_append_of_le_length : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, i ≤ l₁.length → List.take i (l₁ ++ l₂) = List.take i l₁
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.unop_epi_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : Cᵒᵖ} (f : A ⟶ B) [CategoryTheory.Mono f],
  CategoryTheory.Epi f.unop
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.ext : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {n : ℕ} {M : ModuleCat k}
  {x y : (groupHomology.inhomogeneousChains A).X n ⟶ M},
  (∀ (g : Fin n → G),
      CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) x =
        CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) y) →
    x = y
-- Mathlib.RingTheory.Congruence.Hom
RingCon.mkₐ_comp_factorₐ_comp_mkₐ : ∀ {M : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c ≤ d), (RingCon.factorₐ R h).comp (RingCon.mkₐ R c) = RingCon.mkₐ R d
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentItem.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (languageId : String) (version : ℕ) (text : String) (uri_1 : Lean.Lsp.DocumentUri)
  (languageId_1 : String) (version_1 : ℕ) (text_1 : String),
  ({ uri := uri, languageId := languageId, version := version, text := text } =
      { uri := uri_1, languageId := languageId_1, version := version_1, text := text_1 }) =
    (uri = uri_1 ∧ languageId = languageId_1 ∧ version = version_1 ∧ text = text_1)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.inf_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S T : NonUnitalSubalgebra R A),
  (S ⊓ T).toSubmodule = S.toSubmodule ⊓ T.toSubmodule
-- Std.Http.Data.URI.Basic
/-- Optional authority component (user info, host, and port).
 -/
Std.Http.URI.authority : Std.Http.URI → Option Std.Http.URI.Authority
-- Mathlib.Order.Cover
denselyOrdered_iff_forall_not_covBy : ∀ {α : Type u_1} [inst : LT α], DenselyOrdered α ↔ ∀ (a b : α), ¬a ⋖ b
-- Init.Data.List.Lemmas
List.filterMap_some : ∀ {α : Type u_1} {l : List α}, List.filterMap some l = l
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.Prime.le_or_le : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : Associates M},
  Prime p → ∀ {a b : Associates M}, p ≤ a * b → p ≤ a ∨ p ≤ b
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.brecOn : ∀ {α : Type u_2} {g : Set (Set α)} {motive : (a : Set α) → Filter.CountableGenerateSets g a → Prop} {a : Set α}
  (t : Filter.CountableGenerateSets g a),
  (∀ (a : Set α) (t : Filter.CountableGenerateSets g a), Filter.CountableGenerateSets.below t → motive a t) → motive a t
-- Init.Prelude
/-- Specifies the interpretation of a `Syntax.node` value. An abbreviation for `Name`.

Node kinds may be any name, and do not need to refer to declarations in the environment.
Conventionally, however, a node's kind corresponds to the `Parser` or `ParserDesc` declaration that
produces it. There are also a number of built-in node kinds that are used by the parsing
infrastructure, such as `nullKind` and `choiceKind`; these do not correspond to parser declarations.
 -/
Lean.SyntaxNodeKind : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.coe_star : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : ↥(spinGroup Q)}, ↑(star x) = star ↑x
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `lt_tsub_iff_right` for a stronger statement in a linear order.  -/
lt_tsub_iff_right_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ b → (a < b - c ↔ a + c < b)
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.sub_eq_add_neg : ∀ {G : Type u} [self : SubNegMonoid G] (a b : G), a - b = a + -b
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.inv_prod : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Group (G i)] {i j : ι} (w : Monoid.CoprodI.NeWord G i j),
  w.inv.prod = w.prod⁻¹
-- Mathlib.GroupTheory.Complement
/-- The collection of left transversals of a subgroup.  -/
AddSubgroup.LeftTransversal : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → Type (max 0 u_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.pairFunction_left : ∀ {C : Type u} (X Y : C), CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.left = X
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_eq_indicator : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
  ⇑(Finsupp.filter p f) = {x | p x}.indicator ⇑f
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInlCompAssociator_hom_app_down_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D),
  ((CategoryTheory.sum.inrCompInlCompAssociator C D E).hom.app X).down.down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inr (Sum.inl X))).down.down
      (CategoryTheory.CategoryStruct.id (Sum.inr (Sum.inl X))).down.down
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.haus' : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_4} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : IsHausdorff I M] (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- A set of vectors `v` is orthogonal with respect to some bilinear form `B` if and only
if for all `i ≠ j`, `B (v i) (v j) = 0`.  -/
LinearMap.BilinForm.iIsOrtho : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {n : Type w} → LinearMap.BilinForm R M → (n → M) → Prop
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.closure.eq_1 : ∀ (R : Type u_1) {M : Type u_2} [inst : VAdd R M] (s : Set M), SubAddAction.closure R s = sInf {p | s ⊆ ↑p}
-- Mathlib.Data.Fin.Tuple.Basic
Fin.consCases.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} {motive : ((i : Fin n.succ) → α i) → Sort v}
  (cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)) (x : (i : Fin n.succ) → α i),
  Fin.consCases cons x = cast ⋯ (cons (x 0) (Fin.tail x))
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Power asymptotic for `f - f₀` as `x → 0`.  -/
WeakFEPair.hf_zero' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  (fun x => P.f x - P.f₀) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-P.k)
-- Mathlib.Algebra.Module.Submodule.Map
LinearEquiv.submoduleMap_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂)
  (p : Submodule R M) (x : ↥p), ↑((e.submoduleMap p) x) = e ↑x
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the reverse direction of `Submodule.projectionOnto_apply_eq_zero_iff`. -/
Submodule.projectionOnto_apply_of_mem_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) {x : E}, x ∈ q → (p.projectionOnto q h) x = 0
-- Mathlib.Analysis.Normed.Module.FiniteDimension
LinearIsometry.coe_toLinearIsometryEquiv : ∀ {F : Type u_1} {E₁ : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedAddCommGroup E₁] {R₁ : Type u_3}
  [inst_2 : Field R₁] [inst_3 : Module R₁ E₁] [inst_4 : Module R₁ F] [inst_5 : FiniteDimensional R₁ E₁]
  [inst_6 : FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : Module.finrank R₁ E₁ = Module.finrank R₁ F),
  ⇑(li.toLinearIsometryEquiv h) = ⇑li