mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_comp_right : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃}, v ≈ v' → v ∘ₗ u ≈ v' ∘ₗ u
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.ι_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), CategoryTheory.CategoryStruct.comp Φ.ι Φ.π = 0
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_le_iff_le : ∀ {a b : ℤ} (ha₁ : Int32.minValue.toInt ≤ a) (ha₂ : a ≤ Int32.maxValue.toInt) (hb₁ : Int32.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int32.maxValue.toInt), Int32.ofIntLE a ha₁ ha₂ ≤ Int32.ofIntLE b hb₁ hb₂ ↔ a ≤ b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false →
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff m₂ ⋯) k fallback = fallback
-- Mathlib.Algebra.Lie.Basic
LieEquiv.map_lie : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x y : L₁), e ⁅x, y⁆ = ⁅e x, e y⁆
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongEpi.of_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) [h : CategoryTheory.StrongEpi f],
  CategoryTheory.StrongEpi g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.getKeyD k fallback =
    (Option.filter f (t.getKey? k)).getD fallback
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.vadd_toAffineMap : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q),
  ↑(f +ᵥ g) = ↑f +ᵥ ↑g
-- Init.Data.Dyadic.Basic
Dyadic.neg.eq_1 : Dyadic.zero.neg = Dyadic.zero
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context.mk.inj : ∀ {options : Lean.Options} {table : Lean.Parser.TokenTable} {options_1 : Lean.Options}
  {table_1 : Lean.Parser.TokenTable},
  { options := options, table := table } = { options := options_1, table := table_1 } →
    options = options_1 ∧ table = table_1
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.vadd_mem_of_set_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {g : G},
  s ∈ AddAction.fixedBy (Set α) g → ∀ {x : α}, g +ᵥ x ∈ s ↔ x ∈ s
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionClientCapabilities : Lean.ToJson Lean.Lsp.CodeActionClientCapabilities
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.mkPairs.loop : Array Lean.Term → ℕ → Lean.Term → Lean.MacroM Lean.Term
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.id_comp_lift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ],
  p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.id b))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE!_eq_get!_getEntryLE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.DTreeMap.Internal.Impl.getEntryLE! k t = (Std.DTreeMap.Internal.Impl.getEntryLE? k t).get!
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_eq_top_of_top_mem : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : OrderTop α] {f : ι → α},
  ⊤ ∈ Set.range f → iSup f = ⊤
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isInducing_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsInducing ⇑DomMulAct.mk.symm
-- Mathlib.Data.Sym.Sym2
Sym2.toRel_symm : ∀ {α : Type u_1} (s : Set (Sym2 α)), Std.Symm (Sym2.ToRel s)
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_add_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z
-- Mathlib.Topology.Algebra.Group.Basic
/-- Multiplication from the left in a topological group as a homeomorphism.  -/
Homeomorph.mulLeft : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : Group G] → [SeparatelyContinuousMul G] → G → G ≃ₜ G
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_xor_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x ^^^ y).sshiftRight n = x.sshiftRight n ^^^ y.sshiftRight n
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.zero_add : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S]
  (x : AddOreLocalization S R), 0 + x = x
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₁_obj_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C), (AlgebraicTopology.DoldKan.N₁.obj X).p = AlgebraicTopology.DoldKan.PInfty
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- The recurrence relation for the `convs'` of the continued fraction expansion
of an element `v` of `K` in terms of the convergents of the inverse of its fractional part.
 -/
GenContFract.convs'_succ : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ)
  [IsStrictOrderedRing K], (GenContFract.of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs' n
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.not_isSingular_succ : ∀ (c : Cardinal.{u_1}), ¬(Order.succ c).IsSingular
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_of_embedding.eq_1 : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] (n : ℕ) [inst_2 : DecidableEq α],
  Set.powersetCard.mulActionHom_of_embedding G α n = { toFun := Set.powersetCard.ofFinEmb n α, map_smul' := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs.inj : ∀ {c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {k : ℤ} {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {k_1 : ℤ},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs c₁ c₂ k =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs c₁_1 c₂_1 k_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1 ∧ k = k_1
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
/-- If `F` preserves pullbacks, then it preserves monomorphisms.  -/
CategoryTheory.preserves_mono_of_preservesLimit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f f) F] [CategoryTheory.Mono f],
  CategoryTheory.Mono (F.map f)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- If `K / E / F` is a ring extension tower, `L` is a submonoid of `K / F` which is generated by
`S` as an `F`-module, then `E[L]` is generated by `S` as an `E`-module.  -/
Submonoid.adjoin_eq_span_of_eq_span : ∀ (F : Type u_1) (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
  [inst_3 : Algebra E K] [inst_4 : Semiring F] [inst_5 : Module F K] [IsScalarTower F E K] (L : Submonoid K)
  {S : Set K}, ↑L = ↑(Submodule.span F S) → Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S
-- Mathlib.Order.Partition.Finpartition
/-- The part of the finpartition that `a` lies in.  -/
Finpartition.part : {α : Type u_1} → [inst : DecidableEq α] → {s : Finset α} → Finpartition s → α → Finset α
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.ext_iff : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : ↥(MeasureTheory.Lp E p μ)}, f = g ↔ ↑↑f =ᵐ[μ] ↑↑g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_eq_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.containsKey k l = true → Std.Internal.List.getKeyD k l fallback = k
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_comp_inl_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M × M₂ →ₗ[R] M₃), (f ∘ₗ LinearMap.inl R M M₂).coprod (f ∘ₗ LinearMap.inr R M M₂) = f
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_cons_key : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {acc : List α},
  Std.DHashMap.Raw.fold (fun acc k x => k :: acc) acc l =
    Std.Internal.List.keys (Std.DHashMap.Internal.toListModel l.buckets).reverse ++ acc
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_inter : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  t ∈ nhds x → (MDiffAt[s ∩ t] f x ↔ MDiffAt[s] f x)
-- Init.Data.Array.Find
Array.findIdx_extract : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {p : α → Bool}, Array.findIdx p (xs.extract 0 i) = min i (Array.findIdx p xs)
-- Mathlib.Algebra.Group.Nat.Units
Nat.addUnits_eq_zero : ∀ (u : AddUnits ℕ), u = 0
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- **Alias** of `MeasureTheory.measure_mono_ae`.

---

If `s ⊆ t` modulo a set of measure `0`, then `μ s ≤ μ t`.  -/
Filter.EventuallyLE.measure_le : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s ≤ᵐ[μ] t → μ s ≤ μ t
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.mk.sizeOf_spec : ∀ (f fType : Lean.Expr) (args mvars : Array Lean.Expr) (bInfos : Array Lean.BinderInfo) (forceRegularApp : Bool),
  sizeOf
      { f := f, fType := fType, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := forceRegularApp } =
    1 + sizeOf f + sizeOf fType + sizeOf args + sizeOf mvars + sizeOf bInfos + sizeOf forceRegularApp
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ↑1 = 1
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) {i : ι},
  (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom.app (Opposite.op (X i))))
      (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i) =
    CategoryTheory.yonedaEquiv (f i)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Makes the identity isomorphism from a proof two `NonUnitalSubring`s of a multiplicative
monoid are equal.  -/
RingEquiv.nonUnitalSubringCongr : {R : Type u} → [inst : NonUnitalRing R] → {s t : NonUnitalSubring R} → s = t → ↥s ≃+* ↥t
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.semilatticeInf : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : SemilatticeInf β] → [ContinuousInf β] → SemilatticeInf C(α, β)
-- Mathlib.RingTheory.Radical.Basic
/-- Radical is multiplicative for relatively prime elements.  -/
UniqueFactorizationMonoid.radical_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  IsRelPrime a b →
    UniqueFactorizationMonoid.radical (a * b) =
      UniqueFactorizationMonoid.radical a * UniqueFactorizationMonoid.radical b
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : TopologicalSpace.Opens X) (hs : Nonempty ↥s),
  s.openPartialHomeomorphSubtypeCoe hs = Topology.IsOpenEmbedding.toOpenPartialHomeomorph Subtype.val ⋯
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- The integral representation of the function `x ↦ x^p` (where `p ∈ (0, 1)`) .  -/
Real.rpow_eq_const_mul_integral : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → x ^ p = (∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x
-- Mathlib.Analysis.Convex.Function
ConcaveOn.sub_strictConvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, ConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s g → StrictConcaveOn 𝕜 s (f - g)
-- Init.Data.Nat.Basic
Nat.lt_of_lt_of_eq : ∀ {n m k : ℕ}, n < m → m = k → n < k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        k ∈ l → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKeyD k' fallback = k
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instAlgebraOfPolynomial : (K : Type u) →
  [inst : CommRing K] →
    [inst_1 : IsDomain K] →
      (R : Type u_1) → [inst_2 : CommSemiring R] → [Algebra R (Polynomial K)] → Algebra R (RatFunc K)
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.lift_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C}
  (k : CategoryTheory.IsKernelPair f a b) (p q : S ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (k.lift p q w) (CategoryTheory.CategoryStruct.comp b h) =
    CategoryTheory.CategoryStruct.comp q h
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_epi_of_isIso_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [S₂.HasLeftHomology] [CategoryTheory.Epi φ.τ₁]
  [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃], S₁.HasLeftHomology
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.quasiIso.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.CategoryWithHomology C],
  CochainComplex.Plus.quasiIso C =
    (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C)
-- Mathlib.Algebra.Group.Action.Prod
AddAction.prodOfVAddCommClass.eq_1 : ∀ (M : Type u_1) (N : Type u_2) (α : Type u_5) [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddAction M α]
  [inst_3 : AddAction N α] [inst_4 : VAddCommClass M N α],
  AddAction.prodOfVAddCommClass M N α = { vadd := fun mn a => mn.1 +ᵥ mn.2 +ᵥ a, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv_algebraMap : ∀ {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (h : A ≃+* B) (a : A),
  (IsFractionRing.ringEquivOfRingEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)
-- Mathlib.Data.Matrix.Mul
Matrix.nonAssocSemiring : {n : Type u_3} → {α : Type v} → [NonAssocSemiring α] → [Fintype n] → [DecidableEq n] → NonAssocSemiring (Matrix n n α)
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.normal_addSubgroupOf_addCommutator_sup : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), (⁅H₁, H₂⁆.addSubgroupOf (H₁ ⊔ H₂)).Normal
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
sup_div_inf_eq_mabs_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), (a ⊔ b) / (a ⊓ b) = |b / a|ₘ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonCompletionClientCapabilities.toJson : Lean.Lsp.CompletionClientCapabilities → Lean.Json
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_le' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : PartialOrder α]
  [OrderClosedTopology α] [SecondCountableTopology α], MeasurableSet {p | p.1 ≤ p.2}
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital ring homomorphism from a `CommRing` to a `SeminormedRing` induces a
`SeminormedCommRing` structure on the domain.

See note [reducible non-instances]  -/
SeminormedCommRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : CommRing R] → [inst_2 : SeminormedRing S] → [NonUnitalRingHomClass F R S] → F → SeminormedCommRing R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getElem_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂), t₁[k] = t₂[k]
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.liftOfRightInverse_comp : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : { g // f.ker ≤ g.ker }),
  ((f.liftOfRightInverse f_neg hf) g).comp f = ↑g
-- Init.ByCases
dif_eq_if : ∀ (c : Prop) {h : Decidable c} {α : Sort u} (t e : α), (if x : c then t else e) = if c then t else e
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mk : {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} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                (left : CategoryTheory.Functor A A') →
                                  (base : CategoryTheory.Functor B B') →
                                    (right : CategoryTheory.Functor C C') →
                                      autoParam (CategoryTheory.CatCommSq F left base F')
                                          CategoryTheory.Limits.CatCospanTransform.squareLeft._autoParam →
                                        autoParam (CategoryTheory.CatCommSq G right base G')
                                            CategoryTheory.Limits.CatCospanTransform.squareRight._autoParam →
                                          CategoryTheory.Limits.CatCospanTransform F G F' G'
-- Init.Data.List.Lemmas
List.forall_getElem : ∀ {α : Type u_1} {l : List α} {p : α → Prop}, (∀ (i : ℕ) (h : i < l.length), p l[i]) ↔ ∀ a ∈ l, p a
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instFormallyUnramified : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Etale f], AlgebraicGeometry.FormallyUnramified f
-- Mathlib.Data.Setoid.Basic
Setoid.sInf_iff : ∀ {α : Type u_1} {S : Set (Setoid α)} {x y : α}, (sInf S) x y ↔ ∀ s ∈ S, s x y
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Lean.Meta.Closure
/-- Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`.
 -/
Lean.Meta.mkAuxTheorem : Lean.Expr →
  Lean.Expr → optParam Bool false → optParam (Option Lean.Name) none → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.mk : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} {A : Set G},
  1 ∈ A → A⁻¹ = A → CovBySMul G K (A ^ 2) A → IsApproximateSubgroup K A
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (a : α), UniformContinuous fun x => f x + a
-- Init.Data.Slice.List.Lemmas
List.mkSlice_ric_eq_mkSlice_rio : ∀ {α : Type u_1} {xs : List α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
-- Mathlib.Algebra.Group.Defs
mul_left_cancel : ∀ {G : Type u_1} [inst : Mul G] [IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.Hom.hom.eq_1 : ∀ {X Y : AddCommGrpCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Init.Data.AC
Lean.Data.AC.EvalInformation.arbitrary : {α : Sort u} → {β : Sort v} → [self : Lean.Data.AC.EvalInformation α β] → α → β
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval.eq_1 : ∀ {R : Type u} [inst : Semiring R] (x : R) (p : Polynomial R), Polynomial.eval x p = Polynomial.eval₂ (RingHom.id R) x p
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiAlgebraFin_apply_const : ∀ {R : Type uR} {n : ℕ} [inst : CommSemiring R] {A : Type u_1} [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  ((MultilinearMap.mkPiAlgebraFin R n A) fun x => a) = a ^ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.mul_le_mul_iff_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Mul α] [IsMulCommutative α] [MulLeftMono α] {a b c : α},
  MulLECancellable a → (b * a ≤ c * a ↔ b ≤ c)
-- Mathlib.Data.Num.Basic
ZNum.zero.sizeOf_spec : sizeOf ZNum.zero = 1