mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.mk.injEq : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (dpow : ℕ → A → A)
  (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1)
  (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I)
  (dpow_add :
    ∀ {n : ℕ} {x y : A},
      x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow k.1 x * dpow k.2 y)
  (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x)
  (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x)
  (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x)
  (dpow_1 : ℕ → A → A) (dpow_null_1 : ∀ {n : ℕ} {x : A}, x ∉ I → dpow_1 n x = 0)
  (dpow_zero_1 : ∀ {x : A}, x ∈ I → dpow_1 0 x = 1) (dpow_one_1 : ∀ {x : A}, x ∈ I → dpow_1 1 x = x)
  (dpow_mem_1 : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow_1 n x ∈ I)
  (dpow_add_1 :
    ∀ {n : ℕ} {x y : A},
      x ∈ I → y ∈ I → dpow_1 n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow_1 k.1 x * dpow_1 k.2 y)
  (dpow_mul_1 : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow_1 n (a * x) = a ^ n * dpow_1 n x)
  (mul_dpow_1 : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow_1 m x * dpow_1 n x = ↑((m + n).choose m) * dpow_1 (m + n) x)
  (dpow_comp_1 : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow_1 m (dpow_1 n x) = ↑(m.uniformBell n) * dpow_1 (m * n) x),
  ({ dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem,
        dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } =
      { dpow := dpow_1, dpow_null := dpow_null_1, dpow_zero := dpow_zero_1, dpow_one := dpow_one_1,
        dpow_mem := dpow_mem_1, dpow_add := dpow_add_1, dpow_mul := dpow_mul_1, mul_dpow := mul_dpow_1,
        dpow_comp := dpow_comp_1 }) =
    (dpow = dpow_1)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instIsCancelAddOfAddOpposite : ∀ {M : Type u_1} [inst : Add Mᵃᵒᵖ] [IsCancelAdd Mᵃᵒᵖ], IsCancelAdd Mᵈᵃᵃ
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.modify' : (Lean.Meta.Grind.AC.State → Lean.Meta.Grind.AC.State) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.toFun.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g g_1 : N →ₗ[R] P} (e_g : g = g_1) (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g), rTensor.toFun Q hfg = rTensor.toFun Q ⋯
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_mono_left : ∀ {α : Type u_1} {β : Type u_2} (t : Multiset β), Monotone fun s => s.disjSum t
-- Mathlib.Data.List.MinMax
List.not_lt_of_mem_argmax : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {l : List α} {a m : α},
  a ∈ l → m ∈ List.argmax f l → ¬f m < f a
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.subsingleton_orbit_iff_mem_fixedPoints : ∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {a : α},
  (MulAction.orbit M a).Subsingleton ↔ a ∈ MulAction.fixedPoints M α
-- Mathlib.Algebra.Group.Commute.Basic
Commute.conj_iff : ∀ {G : Type u_1} [inst : Group G] {a b : G} (h : G), Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressReport.kind : Lean.Lsp.WorkDoneProgressReport → String
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSub.eq_1 : ∀ {α : Type u_1} [inst : Sub α], Colex.instSub = inst
-- Lean.Language.Basic
_private.Lean.Language.Basic.0.Lean.Language.Snapshot.Diagnostics.mk : Lean.MessageLog → Option (IO.Ref (Option Dynamic)) → Lean.Language.Snapshot.Diagnostics
-- Init.Prelude
HSub.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HSub α β γ
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.all : Lean.Elab.Structural.IndGroupInfo → Array Lean.Name
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- The coherent sheaf condition on an essentially small site can be checked after precomposing with
the equivalence with a small category.
 -/
CategoryTheory.Equivalence.precoherent_isSheaf_iff_of_essentiallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] [inst_3 : CategoryTheory.EssentiallySmall.{u_4, v_1, u_1} C]
  (F : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology (CategoryTheory.SmallModel.{u_4, v_1, u_1} C))
      ((CategoryTheory.equivSmallModel C).inverse.op.comp F)
-- Lean.Compiler.IR.Basic
Lean.IR.JoinPointId.mk.sizeOf_spec : ∀ (idx : Lean.IR.Index), sizeOf { idx := idx } = 1 + sizeOf idx
-- Std.Data.DHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
Std.DHashMap.Const.getD : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → α → β → β
-- Mathlib.Data.FP.Basic
FP.Float.isFinite : [C : FP.FloatCfg] → FP.Float → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.instToString : ToString Std.Tactic.BVDecide.BVPred
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.inhabited : {T : Type u₃} →
  [inst : CategoryTheory.Category.{v₃, u₃} T] →
    [Inhabited T] → Inhabited (CategoryTheory.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.id T))
-- Mathlib.Data.Subtype
Subtype.coe_mk : ∀ {α : Sort u_1} {p : α → Prop} (a : α) (h : p a), ↑⟨a, h⟩ = a
-- Mathlib.RingTheory.Polynomial.Bernstein
/-- A certain linear combination of the previous three identities,
which we'll want later.
 -/
bernsteinPolynomial.variance : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  ∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial R n ν =
    n • Polynomial.X * (1 - Polynomial.X)
-- Mathlib.Tactic.SplitIfs
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition.hyp.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Mathlib.Tactic.SplitPosition.hyp✝ fvarId = Mathlib.Tactic.SplitPosition.hyp✝ fvarId_1 → fvarId = fvarId_1
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_tensorUnit_comon_counit : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofQuotient_π : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A),
  (Module.Relations.Solution.ofQuotient relations).π = (Submodule.span A (Set.range relations.relation)).mkQ
-- Init.Grind.ToInt
/-- The embedding takes negation to negation, wrapped into the range interval.  -/
Lean.Grind.ToInt.Neg.toInt_neg : ∀ {α : Type u} {inst : Neg α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Neg α I] (x : α), ↑(-x) = I.wrap (-↑x)
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.inclusionPathAux.match_1.eq_1 : ∀ {B : Type u_2} [inst : Quiver B] {a : B} (motive : (x : B) → Quiver.Path a x → Sort u_3)
  (h_1 : Unit → motive a Quiver.Path.nil) (h_2 : (x b : B) → (p : Quiver.Path a b) → (f : b ⟶ x) → motive x (p.cons f)),
  (match a, Quiver.Path.nil with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons f => h_2 x b p f) =
    h_1 ()
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.instToJsonMakeEditLinkProps.toJson : ProofWidgets.MakeEditLinkProps → Lean.Json
-- Mathlib.Data.List.Nodup
List.Nodup.insert : ∀ {α : Type u} {l : List α} {a : α} [inst : BEq α] [LawfulBEq α], l.Nodup → (List.insert a l).Nodup
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_pprod : ∀ {α : Sort u_1} {β : Sort u_2}, IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β
-- Mathlib.Order.RelIso.Basic
/-- A relation embedding is also a relation embedding between dual relations.  -/
RelEmbedding.swap : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → Function.swap r ↪r Function.swap s
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- If `M` and `M₂` are both `R`-modules and `S`-modules and `R`-module structures
are defined by an action of `R` on `S` (formally, we have two scalar towers), then any `S`-linear
map from `M` to `M₂` is `R`-linear.

See also `LinearMap.map_smul_of_tower`.  -/
LinearMap.restrictScalars : (R : Type u_1) →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module S M] →
                      [inst_7 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (M →ₗ[S] M₂) → M →ₗ[R] M₂
-- Mathlib.Logic.Equiv.Basic
/-- If a predicate `p : β → Prop` is true on the range of a map `f : α → β`, then
`Σ y : {y // p y}, {x // f x = y}` is equivalent to `α`.  -/
Equiv.sigmaSubtypeFiberEquiv : {α : Type u_9} →
  {β : Type u_10} → (f : α → β) → (p : β → Prop) → (∀ (x : α), p (f x)) → (y : Subtype p) × { x // f x = ↑y } ≃ α
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.ext : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {e e' : A ≃ₐc[R] B}, (∀ (x : A), e x = e' x) → e = e'
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- If a function is bounded on a discrete space, it is automatically continuous,
and therefore gives rise to an element of the type of bounded continuous functions.  -/
BoundedContinuousFunction.mkOfDiscrete : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        [DiscreteTopology α] →
          (f : α → β) → (C : ℝ) → (∀ (x y : α), dist (f x) (f y) ≤ C) → BoundedContinuousFunction α β
-- Mathlib.Algebra.Field.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
DivisionSemiring.zpow_succ' : ∀ {K : Type u_2} [self : DivisionSemiring K] (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l →
        ∀ {h' : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).contains k' = true},
          (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey k' h' = k
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.instCoeForallForallParenthesizerAliasValue : Coe (Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer)
  Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.equiv_iff_toList_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toList = t₂.toList)
-- Std.Do.PredTrans
/-- Transforming a conjunction of postconditions is the same as the conjunction of transformed
postconditions.
 -/
Std.Do.PredTrans.Conjunctive : {ps : Std.Do.PostShape} → {α : Type u} → (Std.Do.PostCond α ps → Std.Do.Assertion ps) → Prop
-- Lean.Data.KVMap
Lean.DataValue.ofString.inj : ∀ {v v_1 : String}, Lean.DataValue.ofString v = Lean.DataValue.ofString v_1 → v = v_1
-- Init.Simproc
/-- A builtin simplification procedure.
 -/
Lean.Parser.«command__Builtin_simproc__[_]_(_):=_» : Lean.ParserDescr
-- Mathlib.Data.Multiset.MapFold
Multiset.coe_foldl : ∀ {α : Type u_1} {β : Type v} (f : β → α → β) [inst : RightCommutative f] (b : β) (l : List α),
  Multiset.foldl f b ↑l = List.foldl f b l
-- Init.Data.UInt.Lemmas
UInt64.ofFin_mod : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a % b) = UInt64.ofFin a % UInt64.ofFin b
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cos_sq_sub_sin_sq : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.cos x ^ 2 - Real.sin x ^ 2 = Real.sin b * Real.cos b - Real.sin a * Real.cos a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapFst_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  (CategoryTheory.Comma.mapFst α β).inv.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
-- Mathlib.Analysis.Convex.EGauge
egauge_smul_left : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {c : 𝕜},
  c ≠ 0 → ∀ (s : Set E) (x : E), egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ
-- Mathlib.Algebra.Exact.Basic
/-- If two maps `f : M → N` and `g : N → P` are exact, then the induced maps
`Set.range f → N → Set.range g` are exact.

Note that if you already have an instance `[Zero (Set.range g)]` (which is unlikely) this lemma
may not apply if the zero of `Set.range g` is not definitionally equal to `⟨0, hg⟩`.  -/
Function.Exact.rangeFactorization : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : Zero P],
  Function.Exact f g → ∀ (hg : 0 ∈ Set.range g), Function.Exact Subtype.val (Set.rangeFactorization g)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Icc : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] (a b : R),
  f.measure (Set.Icc a b) = ENNReal.ofReal (↑f b - Function.leftLim (↑f) a)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- A coefficient of a product of finset-truncated power series equals the coefficient of the
untruncated product, with the two truncation finsets `s` and `t` allowed to differ.  -/
MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s t : Finset (σ →₀ ℕ)},
  IsLowerSet ↑s →
    IsLowerSet ↑t →
      ∀ {x : σ →₀ ℕ} (f g : MvPowerSeries σ R),
        x ∈ s →
          x ∈ t →
            MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) f * (MvPowerSeries.truncFinset R t) g) =
              (MvPowerSeries.coeff x) (f * g)
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- To check equality of two elements of `X(S)`, it suffices to check equality after composing with
each `X(S) → X(Sᵢ)`.
 -/
CompHausLike.LocallyConstant.presheaf_ext : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))}
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}]
  (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))))
  (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X]
  (x y : X.obj (Opposite.op S)) [CompHausLike.HasExplicitFiniteCoproducts P],
  (∀ (a : Function.Fiber ⇑f),
      (CategoryTheory.ConcreteCategory.hom (X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op)) x =
        (CategoryTheory.ConcreteCategory.hom (X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op)) y) →
    x = y
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.lift_unique : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {B : Type w'} [inst_4 : Semiring B]
  [inst_5 : Algebra R B] (maps : {i : I} → A i →ₐ[R] B) (f : LinearAlgebra.FreeProduct R A →ₐ[R] B),
  (∀ (i : I), f.comp (LinearAlgebra.FreeProduct.ι R A i) = maps) →
    f = (LinearAlgebra.FreeProduct.lift R A) fun {i} => maps
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.mk : {R : Type u} →
  [inst : CommRing R] →
    (weight : Type v) →
      [weightIsAddCommGroup : AddCommGroup weight] →
        [weightIsModule : Module R weight] →
          (coweight : Type v) →
            [coweightIsAddCommGroup : AddCommGroup coweight] →
              [coweightIsModule : Module R coweight] →
                (index : Type v) → RootPairing index R weight coweight → RootPairingCat R
-- Lean.Environment
/-- Resulting "main branch" environment. Accessing the kernel environment will block until
`PromiseCheckedResult.commitChecked` has been called.
 -/
Lean.Environment.PromiseCheckedResult.mainEnv : Lean.Environment.PromiseCheckedResult → Lean.Environment
-- Init.Data.BitVec.Lemmas
BitVec.or_allOnes : ∀ {w : ℕ} {x : BitVec w}, x ||| BitVec.allOnes w = BitVec.allOnes w
-- Mathlib.Data.UInt
UInt64.instCommMonoid : CommMonoid UInt64
-- Mathlib.Algebra.Quaternion
Quaternion.re_im : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a.im.re = 0
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_natCast_mul : ∀ {R : Type u} [inst : Semiring R] {n k : ℕ} {f : Polynomial R},
  (⇑Polynomial.derivative)^[k] (↑n * f) = ↑n * (⇑Polynomial.derivative)^[k] f
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- In a preprimitive action, stabilizers are maximal subgroups.  -/
AddAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive : ∀ (G : Type u_3) [inst : AddGroup G] {X : Type u_4} [inst_1 : AddAction G X] [Nontrivial X]
  [AddAction.IsPreprimitive G X] (a : X), IsCoatom (AddAction.stabilizer G a)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α}, f ≤ CauSeq.const abs x → f.lim ≤ x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.smul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f • g) μ
-- Init.Data.List.MapIdx
List.mapIdx_ne_nil_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α}, List.mapIdx f l ≠ [] ↔ l ≠ []
-- Mathlib.FieldTheory.Finite.Basic
ZMod.expand_card : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)), (Polynomial.expand (ZMod p) p) f = f ^ p
-- Init.Try
Lean.Try.Config.mk : Bool → Bool → Bool → ℕ → Bool → Bool → Bool → Bool → Bool → Lean.Try.Config
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits : ∀ {s : String.Slice} (p : s.Pos), p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).mop =
    CategoryTheory.MonoidalCategoryStruct.leftUnitor { unmop := X }
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `R` satisfies the strong rank condition,
then any linearly independent family `v : ι → M`
contained in the span of some finite `w : Set M`,
is itself finite.
 -/
LinearIndependent.finite_of_le_span_finite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} (v : ι → M),
  LinearIndependent R v → ∀ (w : Set M) [Finite ↑w], Set.range v ⊆ ↑(Submodule.span R w) → Finite ι
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalSub : ∀ {a b : Ordinal.{u}} {an bn rn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an →
    Mathlib.Meta.NormNum.IsNat b bn → an - bn = rn → Mathlib.Meta.NormNum.IsNat (a - b) rn
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `A`, this is
`(k[H] ⊗[k] A)_G` equipped with the `H`-representation defined by sending `h : H` and `⟦h₁ ⊗ₜ a⟧`
to `⟦h₁h⁻¹ ⊗ₜ a⟧`.  -/
Representation.ind : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            (φ : G →* H) →
              {A : Type u_4} →
                [inst_3 : AddCommGroup A] →
                  [inst_4 : Module k A] → (ρ : Representation k G A) → Representation k H (Representation.IndV φ ρ)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivWithinAt_insert : ∀ {𝕜 : 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 : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} {y : M}, HasMFDerivAt[insert y s] f x f' ↔ HasMFDerivAt[s] f x f'
-- Init.Data.List.Pairwise
List.Pairwise.imp_of_mem : ∀ {α : Type u_1} {l : List α} {R S : α → α → Prop},
  (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → List.Pairwise R l → List.Pairwise S l
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcRef.mk.injEq : ∀ (p p_1 : USize), ({ p := p } = { p := p_1 }) = (p = p_1)
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- A structure containing all the information from which one can build a nontrivial transvection.
This structure is easier to manipulate than transvections as one has a direct access to all the
relevant fields.  -/
Matrix.TransvectionStruct : Type u_1 → Type u₂ → Type (max u_1 u₂)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.τ_apply_infinity : ∀ {A B : GrpCat} (f : A ⟶ B),
  (GrpCat.SurjectiveOfEpiAuxs.tau f) GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_toList_perm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β},
  m₁.toList.Perm m₂.toList → m₁.Equiv m₂
-- Lean.Data.Lsp.Communication
/-- Returns true when the string is a Lean 3 request.
This means that the user is running a Lean 3 language client that
is not aware of Lean 4. In this case we should give a friendlier message.  -/
_private.Lean.Data.Lsp.Communication.0.Lean.IO.FS.Stream.isLean3Request : String → Bool
-- Init.PropLemmas
exists_prop_of_true : ∀ {p : Prop} {q : p → Prop} (h : p), (∃ (h' : p), q h') ↔ q h