mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry.induct_unfolding : ∀ {α : Type u} {β : α → Type v}
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → (a : α) × β a → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β)
      (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false),
      (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x ⟨k, v⟩) →
    (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
        (l_1 r : Std.DTreeMap.Internal.Impl α β)
        (h :
          (Std.DTreeMap.Internal.Impl.inner size k v l
                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
            false),
        (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
            false →
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) ⋯
              ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              h ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry ⋯)) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β) (h : t.isEmpty = false), motive t h (t.maxEntry h)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurable_rnDeriv_right : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α),
  Measurable fun x => κ.rnDeriv η a x
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.insert.match_1.splitter : (motive : List ℕ → Sort u_1) →
  (x : List ℕ) → (Unit → motive []) → ((a : ℕ) → (as : List ℕ) → motive (a :: as)) → motive x
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Limits.PullbackCone.pasteHoriz.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₃ Y₁ Y₂ Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃}
  (t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃) {i₂ : t₂.pt ⟶ Y₂}
  (t₁ t₁_1 : CategoryTheory.Limits.PullbackCone g₁ i₂),
  t₁ = t₁_1 → ∀ (hi₂ : i₂ = t₂.fst), t₂.pasteHoriz t₁ hi₂ = t₂.pasteHoriz t₁_1 hi₂
-- Mathlib.Topology.ContinuousOn
IsOpen.continuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  IsOpen s → (ContinuousOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ContinuousAt f a)
-- Mathlib.Order.Compare
le_iff_le_of_cmp_eq_cmp : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} {β : Type u_3} [inst_1 : LinearOrder β] {x' y' : β},
  cmp x y = cmp x' y' → (x ≤ y ↔ x' ≤ y')
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Cofix.bisim' : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u_1} (Q : α → Prop) (u v : α → QPF.Cofix F),
  (∀ (x : α),
      Q x →
        ∃ a f f',
          (u x).dest = QPF.abs ⟨a, f⟩ ∧
            (v x).dest = QPF.abs ⟨a, f'⟩ ∧ ∀ (i : (QPF.P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') →
    ∀ (x : α), Q x → u x = v x
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.refl_source : ∀ (X : Type u_7) [inst : TopologicalSpace X], (PartialHomeomorph.refl X).source = Set.univ
-- Lean.Elab.Tactic.Omega.OmegaM
/-- User configurable options for `omega`.  -/
Lean.Elab.Tactic.Omega.Context.cfg : Lean.Elab.Tactic.Omega.Context → Lean.Meta.Omega.OmegaConfig
-- Mathlib.GroupTheory.CoprodI
/-- The list represented by a given `NeWord`  -/
Monoid.CoprodI.NeWord.toList : {ι : Type u_1} →
  {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i j : ι} → Monoid.CoprodI.NeWord M i j → List ((i : ι) × M i)
-- Init.Data.List.Sublist
List.prefix_or_prefix_of_prefix : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → l₁ <+: l₂ ∨ l₂ <+: l₁
-- Mathlib.Topology.UnitInterval
/-- Unit interval central symmetry.  -/
unitInterval.symm : ↑unitInterval → ↑unitInterval
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.isInduced_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {w : G.Walk u v}, w.toSubgraph.IsInduced ↔ w.IsChordless
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.lineCount_eq_pointCount : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.HasLines P L] [inst_2 : Fintype P]
  [inst_3 : Fintype L],
  Fintype.card P = Fintype.card L →
    ∀ {p : P} {l : L}, p ∉ l → Configuration.lineCount L p = Configuration.pointCount P l
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_zero_left : ∀ {y : NNReal}, NNReal.agm 0 y = 0
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.instReprConfig : Repr Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_one : ∀ {α : Type u_2} [inst : DecidableRel (Equiv.Perm.SameCycle 1)] (x : α), Equiv.Perm.cycleOf 1 x = 1
-- Mathlib.Data.Nat.ModEq
Nat.modEq_and_modEq_iff_modEq_mul : ∀ {a b m n : ℕ}, m.Coprime n → (a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n])
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
  (s s_1 : Set E), s = s_1 → ProperCone.innerDual s = ProperCone.innerDual s_1
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being left-unbounded right-closed.

The type of the resulting slices is `γ`.
 -/
Std.Ric.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If you're tempted to use this lemma "in the wild", you should probably
carefully consider whether you've made a mistake in allowing two
instances of `HasZeroMorphisms` to exist at all.

See, particularly, the note on `zeroMorphismsOfZeroObject` below.
 -/
CategoryTheory.Limits.HasZeroMorphisms.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I J : CategoryTheory.Limits.HasZeroMorphisms C), I = J
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
inf_sq_eq_mul_div_mabs_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), (a ⊓ b) ^ 2 = a * b / |b / a|ₘ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_def : ∀ {α : Type u_1} [inst : MeasurableSpace α] (r : ℝ) (j : MeasureTheory.JordanDecomposition α),
  r • j = if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instBaseSMul : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : PartialOrder Γ] →
      {V : Type u_6} →
        [inst_1 : Monoid R] → [inst_2 : AddMonoid V] → [inst_3 : DistribMulAction R V] → SMul R (HahnModule Γ R V)
-- Init.Data.List.Impl
List.replace.eq_def : ∀ {α : Type u} [inst : BEq α] (x : List α) (x_1 x_2 : α),
  x.replace x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, x_3 => []
    | a :: as, b, c =>
      match b == a with
      | true => c :: as
      | false => a :: as.replace b c
-- Mathlib.Order.Disjoint
IsCompl.of_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, x ⊓ y ≤ ⊥ → ⊤ ≤ x ⊔ y → IsCompl x y
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.transcendental : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsStronglyTranscendental R x → ∀ [FaithfulSMul R S], Transcendental R x
-- Mathlib.Probability.Kernel.Invariance
ProbabilityTheory.Kernel.Invariant.comp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {κ η : ProbabilityTheory.Kernel α α} {μ : MeasureTheory.Measure α},
  κ.Invariant μ → η.Invariant μ → (κ.comp η).Invariant μ
-- Mathlib.RingTheory.PowerSeries.Trunc
_private.Mathlib.RingTheory.PowerSeries.Trunc.0.PowerSeries.coeff_truncAux : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (φ : PowerSeries R),
  (PowerSeries.truncAux✝ n φ).coeff m = if m < n then (PowerSeries.coeff m) φ else 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map f)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape_le_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w),
  W.colimitsOfShape (CategoryTheory.Discrete J) ≤ CategoryTheory.MorphismProperty.coproducts.{w, v, u} W
-- Mathlib.NumberTheory.Primorial
primeFactors_primorial : ∀ (n : ℕ), (primorial n).primeFactors = n.primesLE
-- Batteries.Data.List.Basic
List.any.eq_1 : ∀ {α : Type u} (x : α → Bool), [].any x = false
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.prodComm_symm : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (Homeomorph.prodComm X Y).symm = Homeomorph.prodComm Y X
-- Init.Data.Vector.Erase
Vector.set_eraseIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {w : i < n} {j : ℕ} {a : α} (hj : j < n - 1),
  (xs.eraseIdx i w).set j a hj = if h' : i ≤ j then (xs.set (j + 1) a ⋯).eraseIdx i w else (xs.set j a ⋯).eraseIdx i w
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι'),
  AlternatingMap.domDomCongr σ 0 = 0
-- Mathlib.Order.Atoms
isAtomic_iff : ∀ (α : Type u_2) [inst : PartialOrder α] [inst_1 : OrderBot α], IsAtomic α ↔ ∀ (b : α), b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
-- Mathlib.Data.PFun
PFun.mem_restrict : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β} {s : Set α} (h : s ⊆ f.Dom) (a : α) (b : β),
  b ∈ f.restrict h a ↔ a ∈ s ∧ b ∈ f a
-- Init.Data.Array.Lemmas
Array.size_eq_one_iff : ∀ {α : Type u_1} {xs : Array α}, xs.size = 1 ↔ ∃ a, xs = #[a]
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurableSet_closedBall : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ℝ},
  MeasurableSet (Metric.closedBall x ε)
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - strict inequality condition**.
The condition is that not all elements of `z` are equal to their center of mass
`∑ i ∈ s, w i * z i`; see `geom_mean_lt_arith_mean_weighted_iff_of_pos` for a version that compares
the elements to each other instead.  -/
Real.geom_mean_lt_arith_mean_weighted_iff_of_pos' : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 < w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, z j ≠ ∑ i ∈ s, w i * z i)
-- Mathlib.Topology.Connected.Basic
IsPreconnected.transGen_of_iUnion : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {s : ι → Set α},
  IsPreconnected (⋃ n, s n) →
    (∀ (i : ι), IsOpen (s i)) →
      ∀ (i j : ι), (s i).Nonempty → (s j).Nonempty → Relation.TransGen (fun a b => (s a ∩ s b).Nonempty) i j
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCommGroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α],
  AddOpposite.instAddCommGroup = { toAddGroup := AddOpposite.instAddGroup, add_comm := ⋯ }
-- Mathlib.Topology.Algebra.Order.Group
comap_mabs_nhds_one : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G], Filter.comap mabs (nhds 1) = nhds 1
-- Mathlib.Analysis.Complex.Basic
RCLike.hasSum_ofReal : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → ℝ} {x : ℝ},
  HasSum (fun x => ↑(f x)) (↑x) L ↔ HasSum f x L
-- Std.Time.Format.Modifier
/-- Hour and minute without colon (e.g., "+0130")
 -/
Std.Time.OffsetX.hourMinute : Std.Time.OffsetX
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
differentiable_const_cpow_of_neZero : ∀ (z : ℂ) [NeZero z], Differentiable ℂ fun s => z ^ s
-- Mathlib.Algebra.Group.End
/-- See `Equiv.Perm.subtypePerm_inv`.  -/
Equiv.Perm.inv_subtypePerm : ∀ {α : Type u_4} {p : α → Prop} (f : Equiv.Perm α) (hf : ∀ (x : α), p (f x) ↔ p x),
  (f.subtypePerm hf)⁻¹ = f⁻¹.subtypePerm ⋯
-- Mathlib.Topology.Bases
TopologicalSpace.isTopologicalBasis_of_subbasis_of_finiteInter : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  t = TopologicalSpace.generateFrom s → FiniteInter s → TopologicalSpace.IsTopologicalBasis s
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι),
  CategoryTheory.CategoryStruct.comp (P.p.f n) (f.f.f n) = CategoryTheory.CategoryStruct.comp (f.f.f n) (Q.p.f n)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ}, (Std.HashSet.Raw.emptyWithCapacity c).get? a = none
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instNorm.eq_1 : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E],
  SeparationQuotient.instNorm = { norm := SeparationQuotient.lift norm ⋯ }
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.finite_periods : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s), (IsProperLinearSet.periods✝ hs).Finite
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- the counit morphism of a lax monoidal functor  -/
CategoryTheory.Functor.OplaxMonoidal.η : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {D : Type u₂} →
        {inst_2 : CategoryTheory.Category.{v₂, u₂} D} →
          {inst_3 : CategoryTheory.MonoidalCategory D} →
            (F : CategoryTheory.Functor C D) →
              [self : F.OplaxMonoidal] →
                F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D
-- Mathlib.Order.Antisymmetrization
Relation.SymmGen.of_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.kernelSequenceOpcycles f g fg h n).f = X.fromOpcycles f g fg h n
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instAddCommMonoidWithOne : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoidWithOne A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoidWithOne B] → [inst_4 : Module R B] → AddCommMonoidWithOne (TensorProduct R A B)
-- Init.Core
Quotient.exists_rep : ∀ {α : Sort u} {s : Setoid α} (q : Quotient s), ∃ a, ⟦a⟧ = q
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.hom_induction : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {motive : {x y : CategoryTheory.Cat.FreeRefl V} → (x ⟶ y) → Prop},
  (∀ (x : V), motive (CategoryTheory.Cat.FreeRefl.homMk (CategoryTheory.ReflQuiver.id x))) →
    (∀ {x y z : V} (f : CategoryTheory.Cat.FreeRefl.mk x ⟶ CategoryTheory.Cat.FreeRefl.mk y) (g : y ⟶ z),
        motive f → motive (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Cat.FreeRefl.homMk g))) →
      ∀ {x y : CategoryTheory.Cat.FreeRefl V} (f : x ⟶ y), motive f
-- Mathlib.RingTheory.Radical.Basic
/-- Relatively prime elements have disjoint prime factors (as finsets).  -/
UniqueFactorizationMonoid.disjoint_primeFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  IsRelPrime a b → Disjoint (UniqueFactorizationMonoid.primeFactors a) (UniqueFactorizationMonoid.primeFactors b)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotMk.eq_1 : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R),
  DoubleQuot.quotQuotMk I J = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk I)
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.instAlgebraLocalizationAtPrime : {R : Type u_1} →
  [inst : CommSemiring R] →
    (x : Ideal R) → [H : x.IsPrime] → [IsDomain R] → Algebra (Localization.AtPrime x) (Localization (nonZeroDivisors R))
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.isTheta_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → v =Θ[l] u
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`.  -/
Std.DTreeMap.Internal.Impl.get : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → [Std.LawfulEqOrd α] → (t : Std.DTreeMap.Internal.Impl α β) → (k : α) → k ∈ t → β k
-- Aesop.Forward.RuleInfo
Aesop.instHashableSlot : Hashable Aesop.Slot
-- Init.Data.Fin.Lemmas
Fin.castSucc_one : ∀ {n : ℕ}, Fin.castSucc 1 = 1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.equivCongr_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [inst : CommSemiring R]
  [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₁'] [inst_4 : Semiring A₂'] [inst_5 : Algebra R A₁]
  [inst_6 : Algebra R A₂] [inst_7 : Algebra R A₁'] [inst_8 : Algebra R A₂'] (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂')
  (ψ : A₁ ≃ₐ[R] A₁'), (e.equivCongr e') ψ = e.symm.trans (ψ.trans e')
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instUniqueOfSubsingleton : {G : Type u_1} → [inst : Group G] → [Subsingleton G] → Unique (Subgroup G)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse.  -/
EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₁ ≠ p₂ ∨ p₃ = p₂ → dist p₁ p₂ / Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₃
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.empty_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {n : ℕ}, n ≠ 0 → ∅ ^ n = ∅
-- Mathlib.Topology.EMetricSpace.Weak
/-- `EReal` is a weak extended metric space with its usual distance function.  -/
instWeakEMetricSpaceEReal : WeakEMetricSpace EReal
-- Mathlib.Order.Hom.PowersetCard
Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem : ∀ {n : ℕ} {I : Type u_1} [inst : LinearOrder I] (s : ↑(Set.powersetCard I n)) (i : I),
  i ∈ Set.range ⇑(Set.powersetCard.ofFinEmbEquiv.symm s) ↔ i ∈ s
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.nonempty_Iio : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsSuccLimit a → (Set.Iio a).Nonempty
-- Mathlib.Data.List.Flatten
List.Sublist.flatMap_right : ∀ {α : Type u_1} {β : Type u_2} (l : List α) {f g : α → List β},
  (∀ a ∈ l, (f a).Sublist (g a)) → (List.flatMap f l).Sublist (List.flatMap g l)
-- Lean.Expr
/-- Annotate `e` with the given annotation name `kind`.
It uses metadata to store the annotation.
 -/
Lean.mkAnnotation : Lean.Name → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.coe_lcs_eq : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) [LieModule R L M],
  ↑(I.lcs M k) = ↑(LieModule.lowerCentralSeries R (↥I) M k)
-- Mathlib.RingTheory.Ideal.Operations
/-- The radical of an ideal `I` consists of the elements `r` such that `r ^ n ∈ I` for some `n`.  -/
Ideal.radical : {R : Type u} → [inst : CommSemiring R] → Ideal R → Ideal R
-- Init.Data.Format.Basic
/-- Concatenates the given list after prepending `pre` to each element.

The list items are formatting using `ToFormat.format`.
 -/
Std.Format.prefixJoin : {α : Type u} → [Std.ToFormat α] → Std.Format → List α → Std.Format
-- Init.Data.Float.Model.Unpacked.Operations.Status
/-- Returns `true` if the float is `NaN`.
 -/
Float.Model.UnpackedFloat.isNaN : Float.Model.UnpackedFloat → Bool
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.instIsBalancedOfIsRootSystem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N]
  [inst_2 : CommRing R] [inst_3 : Module R M] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.IsRootSystem],
  P.IsBalanced
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- For an element in `HomogeneousLocalization x`, degree is the natural number `i` such that
`𝒜 i` contains both numerator and denominator.  -/
HomogeneousLocalization.deg : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] → [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization 𝒜 x → ι
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.trans_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasPullback P.p₁ P'.p₀],
  (P.trans P').p₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd P.p₁ P'.p₀) P'.p₁
-- Init.Data.List.Perm
/-- If two lists are sorted by an antisymmetric relation, and permutations of each other,
they must be equal.
 -/
List.Perm.eq_of_pairwise : ∀ {α : Type u_1} {le : α → α → Prop} {l₁ l₂ : List α},
  (∀ (a b : α), a ∈ l₁ → b ∈ l₂ → le a b → le b a → a = b) →
    List.Pairwise le l₁ → List.Pairwise le l₂ → l₁.Perm l₂ → l₁ = l₂
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory NonemptyFinLinOrd fun x1 x2 => ↑x1.toLinOrd →o ↑x2.toLinOrd