mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.flip_hasTotal_iff : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c], K.flip.HasTotal c ↔ K.HasTotal c
-- Init.Internal.Order.Basic
Lean.Order.iterates.sup : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} {c : α → Prop} (hc : Lean.Order.chain c),
  (∀ (x : α), c x → Lean.Order.iterates f x) → Lean.Order.iterates f (Lean.Order.CCPO.csup hc)
-- Mathlib.Topology.Algebra.UniformMulAction
IsUniformAddGroup.instUniformContinuousConstVAdd : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G], UniformContinuousConstVAdd G G
-- Mathlib.Topology.LocallyFinite
/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F : Π a, β a` such that for any `x`, we have `f n x = F x` on the product of an infinite
interval `[N, +∞)` and a neighbourhood of `x`.

We formulate the conclusion in terms of the product of filter `Filter.atTop` and `𝓝 x`.  -/
LocallyFinite.exists_forall_eventually_eq_prod : ∀ {X : Type u_4} [inst : TopologicalSpace X] {π : X → Sort u_6} {f : ℕ → (x : X) → π x},
  (LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) →
    ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in Filter.atTop ×ˢ nhds x, f p.1 p.2 = F p.2
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.smul_sup : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (m : M)
  (S T : AddSubmonoid A), m • (S ⊔ T) = m • S ⊔ m • T
-- Mathlib.Data.Sigma.Interval
Sigma.Icc_mk_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i),
  Finset.Icc ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Icc a b)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.match_1.eq_1 : ∀ (n : ℕ) (motive : (x : ℕ) → x ≤ n → Sort u_1) (h : 0 ≤ n) (h_1 : (h : 0 ≤ n) → motive 0 h)
  (h_2 : (m : ℕ) → (h : m.succ ≤ n) → motive m.succ h),
  (match 0, h with
    | 0, h => h_1 h
    | m.succ, h => h_2 m h) =
    h_1 h
-- Mathlib.Topology.SmallInductiveDimension
/-- **Alias** of `hasSmallInductiveDimensionLT_zero_iff`. -/
HasSmallInductiveDimensionLT_zero_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X], HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- `Finsupp.mapRange` as a `LinearMap`.  -/
Finsupp.mapRange.linearMap : {α : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {R : Type u_5} →
        {R₂ : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring R₂] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : Module R M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R₂ N] → {σ₁₂ : R →+* R₂} → (M →ₛₗ[σ₁₂] N) → (α →₀ M) →ₛₗ[σ₁₂] α →₀ N
-- Mathlib.Data.Real.ConjExponents
Real.holderConjugate_one_div : ∀ {a b : ℝ}, 0 < a → 0 < b → a + b = 1 → (1 / a).HolderConjugate (1 / b)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- `free I` is the colimit of copies of `unit R` indexed by `I`.  -/
SheafOfModules.isColimitFreeCofan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            (I : Type u) → CategoryTheory.Limits.IsColimit (SheafOfModules.freeCofan I)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_sub : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x y : WithVal v), (x - y).ofVal = x.ofVal - y.ofVal
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.Hom.fst : {J : CategoryTheory.Limits.MultispanShape} →
  (a : J.L) →
    (CategoryTheory.Limits.WalkingMultispan.left a).Hom (CategoryTheory.Limits.WalkingMultispan.right (J.fst a))
-- Mathlib.Algebra.Group.Units.Basic
eq_divp_iff_mul_eq : ∀ {α : Type u} [inst : Monoid α] {x : α} {u : αˣ} {y : α}, x = y /ₚ u ↔ x * ↑u = y
-- Init.Data.Slice.Array.Lemmas
Subarray.sliceFoldlM_eq_foldlM : ∀ {β : Type u_1} {init : β} {m : Type u_1 → Type u_2} [inst : Monad m] {α : Type u} {s : Subarray α} {f : β → α → m β},
  Std.Slice.foldlM f init s = Std.Slice.foldlM f init s
-- Mathlib.CategoryTheory.Monad.Limits
/-- The reflector always preserves terminal objects. Note this in general doesn't apply to any other
limit.
 -/
CategoryTheory.leftAdjoint_preservesTerminal_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.Reflective R],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{v + 1})
    (CategoryTheory.monadicLeftAdjoint R)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharTwoJNeZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2], W.c₆ = 1
-- Mathlib.Data.List.Shortlex
List.Shortlex.append_left : ∀ {α : Type u_1} {r : α → α → Prop} {t₁ t₂ : List α},
  List.Shortlex r t₁ t₂ → ∀ (s : List α), List.Shortlex r (s ++ t₁) (s ++ t₂)
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv_add : ∀ {α : Type u_1} [inst : DecidableEq α] (P Q : RegularExpression α) (a : α), (P + Q).deriv a = P.deriv a + Q.deriv a
-- Mathlib.Algebra.Field.ModEq
AddCommGroup.div_modEq_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b c p : K}, c ≠ 0 → (a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c])
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureInt_rename : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] {σ : Type u_3} (Φ : MvPolynomial idx ℤ) (f : idx → σ) (n : ℕ),
  wittStructureInt p ((MvPolynomial.rename f) Φ) n = (MvPolynomial.rename (Prod.map f id)) (wittStructureInt p Φ n)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Collects all semantic tokens that can be deduced purely from `Syntax`
without elaboration information.
 -/
Lean.Server.FileWorker.collectSyntaxBasedSemanticTokens : Lean.FileMap → Lean.Syntax → Array Lean.Server.FileWorker.LeanSemanticToken
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.realize_symmetric : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
  M ⊨ r.symmetric ↔ Std.Symm fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.opEquiv_apply : ∀ {M : Type u_2} [inst : MulOneClass M] (x : Submonoid M), Submonoid.opEquiv x = x.op
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_lt_zero : ∀ {x : ℝ}, Real.arctan x < 0 ↔ x < 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a multilinear map `f` satisfies a boundedness property around `0`,
one can deduce a bound on `f m₁ - f m₂` using the multilinearity.
Here, we give a precise but hard to use version.
See `norm_image_sub_le_of_bound` for a less precise but more usable version.
The bound reads
`‖f m - f m'‖ ≤
  C * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
where the other terms in the sum are the same products where `1` is replaced by any `i`.  -/
MultilinearMap.norm_image_sub_le_of_bound' : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (f : MultilinearMap 𝕜 E G) {C : ℝ},
  0 ≤ C →
    (∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
      ∀ (m₁ m₂ : (i : ι) → E i), ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.minD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            (inl : N →+ E) →
              (rightHom : E →+ G) →
                Function.Injective ⇑inl →
                  inl.range = rightHom.ker → Function.Surjective ⇑rightHom → AddGroupExtension N E G
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Matrices with entries in a C⋆-algebra form a C⋆-algebra.  -/
CStarMatrix.instCStarRing : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {n : Type u_3}
  [inst_3 : Fintype n], CStarRing (CStarMatrix n n A)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_smul_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance X (c • Y) μ = c * ProbabilityTheory.covariance X Y μ
-- Mathlib.Algebra.Category.BoolRing
BoolRing.Hom.ext : ∀ {R : BoolRing} {S : BoolRing} {x y : R.Hom S}, x.hom' = y.hom' → x = y
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntryIfNew_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = false → Std.Internal.List.insertEntryIfNew k v l = ⟨k, v⟩ :: l
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
left_le_lineMap_iff_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k}, 0 < r → (a ≤ (AffineMap.lineMap a b) r ↔ a ≤ b)
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.degree_eq_of_mem_mem : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [DirectSum.Decomposition ℳ] {x : M} {i j : ι},
  x ∈ ℳ i → x ∈ ℳ j → x ≠ 0 → i = j
-- Init.Omega.IntList
Lean.Omega.IntList.cons_add_cons : ∀ (x : ℤ) (xs : Lean.Omega.IntList) (y : ℤ) (ys : Lean.Omega.IntList), x :: xs + y :: ys = (x + y) :: (xs + ys)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.negY_negY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y : R), W'.negY x (W'.negY x y) = y
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.constInsertMany : ∀ {α : Type u} [inst : Ord α] {β : Type v} {ρ : Type u_1} [inst_1 : ForIn Id ρ (α × β)]
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {l : ρ} {h : t.Balanced},
  t.WF → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l h)).WF
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k k' : α} {v : β},
      Array.find? (fun a => a.1 == k) m.toArray = some (k', v) ↔ m.getKey? k = some k' ∧ m[k]? = some v
-- Init.Data.BitVec.Lemmas
/-- Sign extending to a larger bitwidth depends on the msb.
If the msb is false, then the result equals the original value.
If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension.  -/
BitVec.toNat_signExtend : ∀ {w : ℕ} (x : BitVec w) {v : ℕ},
  (BitVec.signExtend v x).toNat = (BitVec.setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- A finite Hilbert basis is an orthonormal basis.  -/
HilbertBasis.toOrthonormalBasis : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : Fintype ι] → HilbertBasis ι 𝕜 E → OrthonormalBasis ι 𝕜 E
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.freeHomEquiv_symm_apply : ∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R} (ψ : X ⟶ ↑M),
  ModuleCat.freeHomEquiv.symm ψ = ModuleCat.freeDesc (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom ψ))
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- If a derivation `D` is in the Killing orthogonal of the range of the adjoint action, then, for
any `x : L`, `ad (D x)` is also in this orthogonal.  -/
LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal : ∀ {R : Type u_1} {L : Type u_2} [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {D : LieDerivation R L L},
  D ∈ (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule →
    ∀ (x : L),
      (LieDerivation.ad R L) (D x) ∈
        (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instDistribMulAction' : {G₀ : Type u_1} →
  {M₀ : Type u_2} →
    [inst : Monoid G₀] → [inst_1 : AddMonoid M₀] → [DistribMulAction G₀ M₀] → DistribMulAction G₀ (Lex M₀)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- The canonical map from `ℝ` to the quotient `Angle`.  -/
Real.Angle.coe : ℝ → Real.Angle
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- The projection from a trivial fiber bundle to its base is open.  -/
IsHomeomorphicTrivialFiberBundle.isOpenMap_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B}, IsHomeomorphicTrivialFiberBundle F proj → IsOpenMap proj
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.mk.injEq : ∀ {β : Type u_4} (filter filter_1 : Filter (Finset β)),
  ({ filter := filter } = { filter := filter_1 }) = (filter = filter_1)
-- Mathlib.Data.Multiset.AddSub
Multiset.mem_of_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, a ∈ s.erase b → a ∈ s
-- Mathlib.LinearAlgebra.Prod
Submodule.fstEquiv_symm_apply_coe : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (m : M), ↑((Submodule.fstEquiv R M M₂).symm m) = (m, 0)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instIsDomainOfIsCancelAdd : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] [IsCancelAdd R] [IsDomain R], IsDomain (HahnSeries Γ R)
-- Mathlib.Topology.EMetricSpace.Defs
WeakEMetricSpace.mk : {α : Type u} →
  [inst : TopologicalSpace α] →
    [toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α] → (∀ {x y : α}, edist x y = 0 → x = y) → WeakEMetricSpace α
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.leftUnitor_inv_apply : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (X : CategoryTheory.GradedObject I C) (i : I),
  (CategoryTheory.GradedObject.Monoidal.leftUnitor X).inv i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv (X i))
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X 0 i i ⋯))
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
IsFractionRing.map.congr_simp : ∀ {A : Type u_8} {B : Type u_9} {K : Type u_10} {L : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : IsDomain B] [inst_3 : CommRing K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] [inst_6 : CommRing L]
  [inst_7 : Algebra B L] [inst_8 : IsFractionRing B L] {j j_1 : A →+* B} (e_j : j = j_1) (hj : Function.Injective ⇑j),
  IsFractionRing.map hj = IsFractionRing.map ⋯
-- Init.Data.List.Lemmas
List.headD.eq_1 : ∀ {α : Type u} (x : α), [].headD x = x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.neg.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J CommRingCat}
  {a a_1 : CommRingCat.Colimits.Prequotient F}, a.neg = a_1.neg → a = a_1
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (τ₁ τ₁_1 : sq₁.X₁ ⟶ sq₂.X₁)
  (e_τ₁ : τ₁ = τ₁_1) (τ₂ τ₂_1 : sq₁.X₂ ⟶ sq₂.X₂) (e_τ₂ : τ₂ = τ₂_1) (τ₃ τ₃_1 : sq₁.X₃ ⟶ sq₂.X₃) (e_τ₃ : τ₃ = τ₃_1)
  (τ₄ τ₄_1 : sq₁.X₄ ⟶ sq₂.X₄) (e_τ₄ : τ₄ = τ₄_1)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂)
  (comm₁₃ : CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃)
  (comm₂₄ : CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄)
  (comm₃₄ : CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄),
  { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, τ₄ := τ₄, comm₁₂ := comm₁₂, comm₁₃ := comm₁₃, comm₂₄ := comm₂₄, comm₃₄ := comm₃₄ } =
    { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, τ₄ := τ₄_1, comm₁₂ := ⋯, comm₁₃ := ⋯, comm₂₄ := ⋯, comm₃₄ := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- Weak rank functions for `h : A.PairingCore` correspond to
weak rank functions for `h.pairing : A.Pairing`.  -/
SSet.Subcomplex.PairingCore.weakRankFunctionEquiv : {X : SSet} →
  {A : X.Subcomplex} →
    (h : A.PairingCore) → (α : Type v) → [inst : PartialOrder α] → h.WeakRankFunction α ≃ h.pairing.WeakRankFunction α
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubring.instIsTopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalRing R] [IsTopologicalRing R] (S : NonUnitalSubring R),
  IsTopologicalRing ↥S
-- Mathlib.Combinatorics.Graph.Simple
Graph.not_adj_self : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] (x : α), ¬G.Adj x x
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.BasicMeasure.toTerminationMeasure : Lean.Elab.WF.GuessLex.BasicMeasure → Lean.Elab.TerminationMeasure
-- Mathlib.Data.Set.Equitable
Set.equitableOn_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : LE β] [inst_1 : Add β] [inst_2 : One β] (f : α → β), ∅.EquitableOn f
-- Mathlib.NumberTheory.SumTwoSquares
/-- **Fermat's theorem on the sum of two squares**. Every prime not congruent to 3 mod 4 is the sum
of two squares. Also known as **Fermat's Christmas theorem**.  -/
Nat.Prime.sq_add_sq : ∀ {p : ℕ} [Fact (Nat.Prime p)], p % 4 ≠ 3 → ∃ a b, a ^ 2 + b ^ 2 = p
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.merge_aux₁ : ∀ {α : Type u_1} [inst : Preorder α] {o₁ : WithBot α} {o₂ : WithTop α} {ls : ℕ} {ll : Ordnode α} {lx : α}
  {lr : Ordnode α} {rs : ℕ} {rl : Ordnode α} {rx : α} {rr t : Ordnode α},
  Ordnode.Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
    Ordnode.Valid' o₁ (Ordnode.node rs rl rx rr) o₂ →
      Ordnode.delta * ls < rs →
        Ordnode.Valid' o₁ t ↑rx →
          t.size = ls + rl.size → Ordnode.Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateSsetImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu →
    Lean.FVarId → ℕ → ℕ → Lean.FVarId → Lean.Expr → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.containsThenInsertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α} {b : β},
  t.WF → (t.containsThenInsertIfNew a b).2.WF
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` is `C^1` at `x`, then `f` is Lipschitz in a neighborhood of `x`.  -/
ContDiffAt.exists_lipschitzOnWith : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {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'},
  ContDiffAt 𝕂 1 f x → ∃ K, ∃ t ∈ nhds x, LipschitzOnWith K f t
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toLinearOrder_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [inst_1 : LinearOrder ι]
  (j : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L), I.toLinearOrder.left j = I.left ↑j
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : InfTopHom α β)
  (hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)), ⇑{ toInfTopHom := f, map_sSup' := hf } = ⇑f
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [P.IsStableUnderShift ℤ], P.rightOrthogonal.IsTriangulated
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
_private.Mathlib.MeasureTheory.Measure.Haar.Quotient.0.termπ_1 : Lean.ParserDescr
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.addEmptyCaseSound : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    ∀ (rupHints : Array ℕ),
      (Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f Std.Tactic.BVDecide.LRAT.Internal.Clause.empty
              rupHints).2 =
          true →
        Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F : C ⥤ D` commutes with shifts, this is the 2-commutative square of categories
`CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor`.
 -/
CategoryTheory.Functor.instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                CategoryTheory.CatCommSq F.mapTriangle.op
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence D).functor F.op.mapTriangle