mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.isMultiplyPreprimitive_iff : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] (n : ℕ),
  AddAction.IsMultiplyPreprimitive M α n ↔
    AddAction.IsMultiplyPretransitive M α n ∧
      ∀ {s : Set α},
        s.encard + 1 = ↑n → AddAction.IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.findAtSorted? : Array Lean.IR.Decl → Lean.Name → Option Lean.IR.Decl
-- Mathlib.NumberTheory.LSeries.Positivity
/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1`
is positive, and the L-series of `a` agrees with an entire function `f` on some open
right half-plane where it converges, then `f` is real and positive on `ℝ`.  -/
ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn : ∀ {a : ArithmeticFunction ℂ},
  (0 ≤ fun x => a x) →
    0 < a 1 →
      ∀ {f : ℂ → ℂ},
        Differentiable ℂ f →
          ∀ {x : ℝ}, LSeries.abscissaOfAbsConv ⇑a ≤ ↑x → Set.EqOn f (LSeries ⇑a) {s | x < s.re} → ∀ (y : ℝ), 0 < f ↑y
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa : {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
-- Aesop.Rule
Aesop.SafeRuleInfo.mk.injEq : ∀ (penalty : ℤ) (safety : Aesop.Safety) (penalty_1 : ℤ) (safety_1 : Aesop.Safety),
  ({ penalty := penalty, safety := safety } = { penalty := penalty_1, safety := safety_1 }) =
    (penalty = penalty_1 ∧ safety = safety_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.reverse.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k' : α) (v : β k') (l_1 r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l_1 r).reverse =
    Std.DTreeMap.Internal.Impl.inner size k' v r.reverse l_1.reverse
-- Init.Data.String.Basic
String.Pos.cast.congr_simp : ∀ {s t : String} (pos pos_1 : s.Pos), pos = pos_1 → ∀ (h : s = t), pos.cast h = pos_1.cast h
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.lift_symm_apply : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (F : TensorAlgebra R M →ₐ[R] A),
  (TensorAlgebra.lift R).symm F = F.toLinearMap ∘ₗ TensorAlgebra.ι R
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A morphism `f` satisfies `[WeakEquivalence f]` if it belongs to `weakEquivalences C`.  -/
HomotopicalAlgebra.WeakEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (X ⟶ Y) → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → Prop
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_notMem_affineSpan_face : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {fs : Finset (Fin (n + 1))}
  {m : ℕ} (hfs : fs.card = m + 1), m ≠ n → s.incenter ∉ affineSpan ℝ (Set.range (s.face hfs).points)
-- Mathlib.Tactic.CongrExclamation
/-- The transparency level to use when trying to close goals after no more congruence lemmas can
be applied. This includes trying to prove the goal by `rfl` and using the `assumption` tactic.
For backwards compatibility this is set to `.default`, which will be changed in the future to
`.reducible`.
 -/
Congr!.Config.postTransparency : Congr!.Config → Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.pageHomologyNatIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r r' : ℤ) (pq : κ)
  (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_1)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_3)
  (X : CategoryTheory.SpectralSequence C c r₀),
  (CategoryTheory.SpectralSequence.pageHomologyNatIso C c r₀ r r' pq hrr' hr).inv.app X = (X.iso r r' pq ⋯ ⋯).inv
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- Given a constant `K ∈ ℝ` (usually `0 < K ≤ 1`) and a finite subset `S ⊆ G`,
`expansion K S : Finset G → ℝ` measures the extent to which `S` extends the argument, compared
against the reference constant `K`. That is, given a finite `A ⊆ G` (possibly empty),
`expansion K S A` is defined as the value of `#(SA) - K#S`.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion : {G : Type u_1} → [Group G] → [DecidableEq G] → ℝ → Finset G → Finset G → ℝ
-- Mathlib.Order.Cofinal
isCofinal_iff_iUnion_Iio_eq_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] {s : Set α}, IsCofinal s ↔ ⋃ i ∈ s, Set.Iio i = Set.univ
-- Mathlib.Data.Seq.Defs
/-- A sequence has terminated at position `n` if the value at position `n` equals `none`.  -/
Stream'.Seq.TerminatedAt : {α : Type u} → Stream'.Seq α → ℕ → Prop
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : CategoryTheory.Functor C (Type w)} (h : Φ₁.fiber ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.CategoryStruct.comp f.hom h)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_const_lt_top_iff_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε'' : Type u_8} [inst : TopologicalSpace ε'']
  [inst_1 : ESeminormedAddMonoid ε''] {c : ε''},
  ‖c‖ₑ ≠ ⊤ → ∀ {p : ENNReal}, p ≠ 0 → p ≠ ⊤ → (MeasureTheory.eLpNorm (fun x => c) p μ < ⊤ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ⊤)
-- Mathlib.Data.Quot
/-- A version of `Quotient.inductionOn` taking `{s : Setoid α}` as an implicit argument instead
of an instance argument.  -/
Quotient.inductionOn' : ∀ {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁ → Prop} (q : Quotient s₁), (∀ (a : α), p (Quotient.mk'' a)) → p q
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_ciSup : ∀ {ι : Type u} (f : ι → Cardinal.{v}) [Nonempty ι],
  BddAbove (Set.range f) → ∀ (c : Cardinal.{v}), c + ⨆ i, f i = ⨆ i, c + f i
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- **Alias** of `OrthogonalFamily.norm_sq_sdiff_sum`. -/
OrthogonalFamily.norm_sq_diff_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ [inst_5 : DecidableEq ι] (f : (i : ι) → G i) (s₁ s₂ : Finset ι),
      ‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
-- Mathlib.Data.List.Lemmas
List.setOfPred_mem_eq_empty_iff : ∀ {α : Type u_1} {l : List α}, {x | x ∈ l} = ∅ ↔ l = []
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.Context.mk.injEq : ∀ (structId structId_1 : ℕ), ({ structId := structId } = { structId := structId_1 }) = (structId = structId_1)
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlEval.eval : {α : Type u} → [self : ProofWidgets.HtmlEval α] → α → Lean.Elab.Command.CommandElabM ProofWidgets.Html
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {y : E}, ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorUnit_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Arrow C) =
    CategoryTheory.Arrow.mk (CategoryTheory.Limits.initial.to (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toSubalgebra_le_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S₁ S₂ : StarSubalgebra R A},
  S₁.toSubalgebra ≤ S₂.toSubalgebra ↔ S₁ ≤ S₂
-- Init.Data.Float.Float32
/-- Computes the hyperbolic arc sine (inverse sine) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`asinhf`.
 -/
Float32.asinh : Float32 → Float32
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Array.of_findIdx?_eq_some.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNat_zero : Turing.PartrecToTM2.trNat 0 = []
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.intCast : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (n : ℤ), WittVector.mapFun ⇑f ↑n = ↑n
-- Lean.Parser.Tactic
Lean.Parser.Tactic.match.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Star.CHSH
TsirelsonInequality.sqrt_two_inv_mul_self : (√2)⁻¹ * (√2)⁻¹ = 2⁻¹
-- Mathlib.CategoryTheory.Sites.InducedTopology
/-- If `F` is continuous with the restricted topology, the restricted topology agrees with the
induced topology. This holds for example if `G` is locally faithful, locally full and cover dense.
 -/
CategoryTheory.Functor.restrictedTopology_eq_inducedTopology : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D}
  [F.IsContinuous (F.restrictedTopology K) K], F.restrictedTopology K = F.inducedTopology K
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The constant augmented simplicial object functor.  -/
CategoryTheory.SimplicialObject.Augmented.const : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.SimplicialObject.Augmented C)
-- Mathlib.Order.Concept
lowerPolar_swap : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α), lowerPolar (Function.swap r) s = upperPolar r s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).size =
        if k ∈ t ∧ (f (t.get? k)).isNone = true then t.size - 1
        else if k ∉ t ∧ (f (t.get? k)).isSome = true then t.size + 1 else t.size
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- Arbitrary witness of non-uniformity. `G.nonuniformWitness ε s t` and
`G.nonuniformWitness ε t s` form a pair of subsets witnessing the non-uniformity of `(s, t)`. If
`(s, t)` is uniform, returns `s`.  -/
SimpleGraph.nonuniformWitness : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Finset α → Finset α → Finset α
-- Mathlib.Topology.Filter
Filter.nhds_eq : ∀ {α : Type u_2} (l : Filter α), nhds l = l.lift' (Set.Iic ∘ Filter.principal)
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_real : ∀ {a : ℝ}, RCLike.sqrt a = √a
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_eq_refl_iff_eq_symm : ∀ {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α}, f.trans g = Equiv.refl α ↔ f = g.symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getInfo : Lean.Meta.Grind.Arith.Cutsat.ToIntM Lean.Meta.Grind.Arith.Cutsat.ToIntInfo
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_toSheafedSpace : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj R).toSheafedSpace = AlgebraicGeometry.Spec.sheafedSpaceObj R
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mk.sizeOf_spec : ∀ {V : Type u} {G : SimpleGraph V} [inst : SizeOf V] (verts : Set V) (Adj : V → V → Prop)
  (adj_sub : ∀ {v w : V}, Adj v w → G.Adj v w) (edge_vert : ∀ {v w : V}, Adj v w → v ∈ verts)
  (symm : autoParam (Std.Symm Adj) SimpleGraph.Subgraph.symm._autoParam),
  sizeOf { verts := verts, Adj := Adj, adj_sub := adj_sub, edge_vert := edge_vert, symm := symm } = 1 + sizeOf symm
-- Mathlib.Topology.Constructions
continuous_apply_apply : ∀ {ι : Type u_5} {κ : Type u_8} {ρ : κ → ι → Type u_9} [inst : (j : κ) → (i : ι) → TopologicalSpace (ρ j i)] (j : κ)
  (i : ι), Continuous fun p => p j i
-- Batteries.Data.MLList.Basic
/-- Construct a `MLList` recursively. Failures from `f` will result in `uncons` failing.   -/
MLList.fix : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → (α → m α) → α → MLList m α
-- Lean.Class
/-- Auxiliary function for collection the position class `outParams`, and
checking whether they are being correctly used.
A regular (i.e., non `outParam`) must not depend on an `outParam`.
Reason for this restriction:
When performing type class resolution, we replace arguments that
are `outParam`s with fresh metavariables. If regular parameters could
depend on `outParam`s, then we would also have to replace them with
fresh metavariables. Otherwise, the resulting expression could be type
incorrect. This transformation would be counterintuitive to users since
we would implicitly treat these regular parameters as `outParam`s.
 -/
_private.Lean.Class.0.Lean.checkOutParam : ℕ → Array Lean.FVarId → Array ℕ → Lean.Expr → Except Lean.MessageData (Array ℕ)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.tendsto_card_div_pow₂ : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Finite ι],
  Bornology.IsBounded s →
    (∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) →
      ∀ {x y : ℝ},
        0 < x →
          x ≤ y →
            Nat.card ↑(s ∩ x⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
              Nat.card ↑(s ∩ y⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
-- Mathlib.LinearAlgebra.TensorProduct.Defs
instZeroTensorProduct : (R : Type u_3) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      (N : Type u_2) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → Zero (TensorProduct R M N)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₂_D₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂), CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'') = 0
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.y_mul : ∀ {d : ℤ} (a b : Pell.Solution₁ d), (a * b).y = a.x * b.y + a.y * b.x
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformContinuousOn.comp_tendstoUniformlyOn_eventually : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] [inst_1 : UniformSpace γ]
  {p : Filter ι} {s : Set β} {F : ι → α → β} {f : α → β} {t : Set α},
  (∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s) →
    (∀ x ∈ t, f x ∈ s) →
      ∀ {g : β → γ},
        UniformContinuousOn g s →
          TendstoUniformlyOn F f p t → TendstoUniformlyOn (fun i x => g (F i x)) (fun x => g (f x)) p t
-- Init.Data.Float.Float
instDecidableEqFloat : DecidableEq Float
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.plus.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  HomotopyCategory.plus C = (CochainComplex.plus C).strictMap (HomotopyCategory.quotient C (ComplexShape.up ℤ))
-- Batteries.Data.List.Basic
List.takeD.eq_1 : ∀ {α : Type u_1} (x : List α) (x_1 : α), List.takeD 0 x x_1 = []
-- Mathlib.Algebra.Group.Units.Basic
eq_one_of_mul_left : ∀ {α : Type u} [inst : CommMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → b = 1
-- Mathlib.Data.List.Dedup
List.dedup_sublist : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.dedup.Sublist l
-- Lean.Expr
Lean.FVarId.mk.inj : ∀ {name name_1 : Lean.Name}, { name := name } = { name := name_1 } → name = name_1
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetInstance : Type
-- Lean.Elab.DefView
Lean.Elab.DefKind.isTheorem : Lean.Elab.DefKind → Bool
-- Batteries.Data.List.Basic
List.takeWhile₂TR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (R : α → β → Bool) (as : List α) (bs : List β),
  List.takeWhile₂TR R as bs = List.takeWhile₂TR.go R as bs [] []
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_mono : ∀ {α : Type u_1} (a : α) {k n : ℕ}, k ≤ n → Multiset.replicate k a ≤ Multiset.replicate n a
-- Mathlib.Data.Vector.Basic
List.Vector.map₂_cons : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (hd₁ : α) (tl₁ : List.Vector α n) (hd₂ : β)
  (tl₂ : List.Vector β n) (f : α → β → γ),
  List.Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ List.Vector.map₂ f tl₁ tl₂
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.injective_of_surjective_endomorphism : ∀ {R : Type u} [inst : Semiring R] [OrzechProperty R] {M : Type v} [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Finite R M] (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelUnitReal.instIsCondKernel : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel Unit (α × ℝ))
  [inst : ProbabilityTheory.IsFiniteKernel κ], κ.IsCondKernel κ.condKernelUnitReal
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed.below : {α : Type u_1} →
  {cmp : α → α → Ordering} →
    {β : Type u_2} →
      {motive : (a : Lean.PrefixTreeNode α β cmp) → Lean.PrefixTreeNode.WellFormed cmp a → Prop} →
        {a : Lean.PrefixTreeNode α β cmp} → Lean.PrefixTreeNode.WellFormed cmp a → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List α} {k : α}, k ∈ t → (t.insertManyIfNewUnit l).getKey! k = t.getKey! k
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compChangeOfVariables.congr_simp : ∀ (m m_1 : ℕ) (e_m : m = m_1) (M M_1 : ℕ) (e_M : M = M_1) (N N_1 : ℕ) (e_N : N = N_1) (i i_1 : (n : ℕ) × (Fin n → ℕ))
  (e_i : i = i_1) (hi : i ∈ FormalMultilinearSeries.compPartialSumSource m M N),
  FormalMultilinearSeries.compChangeOfVariables m M N i hi =
    FormalMultilinearSeries.compChangeOfVariables m_1 M_1 N_1 i_1 ⋯
-- Mathlib.Algebra.Category.ModuleCat.Basic
linearEquivIsoModuleIso_inv : ∀ {R : Type u} [inst : Ring R] {X Y : Type u} [inst_1 : AddCommGroup X] [inst_2 : AddCommGroup Y] [inst_3 : Module R X]
  [inst_4 : Module R Y], linearEquivIsoModuleIso.inv = TypeCat.ofHom fun i => i.toLinearEquiv
-- Mathlib.Topology.Constructions
/-- Homeomorphism between `X → Y → Z` and `X × Y → Z` with product topologies.  -/
Homeomorph.piCurry : {X : Type u_9} → {Y : Type u_10} → {Z : Type u_11} → [inst : TopologicalSpace Z] → (X × Y → Z) ≃ₜ (X → Y → Z)
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- Given a fully faithful functor `ι : C ⥤ A`, this structure contains the data
of a functor `F : A ⥤ C` and a functorial epimorphism
`π.app X : ι.obj (F.obj X) ⟶ X` for all `X : A`.  -/
CategoryTheory.Abelian.LeftResolution : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        CategoryTheory.Functor C A → Type (max (max (max u_1 u_2) v_1) v_2)
-- Lean.Setup
/-- Module data files used for an `import` statement.
This structure is designed for efficient JSON serialization.
 -/
Lean.ImportArtifacts : Type
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_of_one_lt : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], 1 < a → |a|ₘ = a
-- Aesop.Stats.Basic
Aesop.instToJsonForwardInstantiationStats : Lean.ToJson Aesop.ForwardInstantiationStats
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.differentiable_Gammaℂ_inv : Differentiable ℂ fun s => s.Gammaℂ⁻¹
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The Cartesian product of `C^n` functions at a point in a domain is `C^n`.  -/
ContDiffWithinAt.prodMk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {s : Set E} {f : E → F}
  {g : E → G}, ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => (f x, g x)) s x
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.getD_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.DHashMap.Const.getD (Std.DHashMap.filterMap f m) k fallback =
    ((Std.DHashMap.Const.get? m k).bind (f k)).getD fallback
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion_apply : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ι), MeasurableSet (s i)) →
      ∀ {t : Set α}, MeasurableSet t → (μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t
-- Mathlib.NumberTheory.Fermat
Nat.three_le_fermatNumber : ∀ (n : ℕ), 3 ≤ n.fermatNumber
-- Init.Data.String.Bootstrap
String.instOfNatRaw : OfNat String.Pos.Raw 0
-- Mathlib.LinearAlgebra.Quotient.Bilinear
/-- Lift a bilinear form from `M × N → P` to `(M ⧸ M') × (N ⧸ N') → P`.  -/
LinearMap.liftQ₂ : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S : Type u_3} →
      {S₂ : Type u_4} →
        {M : Type u_5} →
          {N : Type u_6} →
            {P : Type u_7} →
              [inst : Ring R] →
                [inst_1 : Ring R₂] →
                  [inst_2 : Ring S] →
                    [inst_3 : Ring S₂] →
                      [inst_4 : AddCommGroup M] →
                        [inst_5 : AddCommGroup N] →
                          [inst_6 : AddCommGroup P] →
                            [inst_7 : Module R M] →
                              [inst_8 : Module S N] →
                                [inst_9 : Module R₂ P] →
                                  [inst_10 : Module S₂ P] →
                                    [inst_11 : SMulCommClass R₂ S₂ P] →
                                      {ρ : R →+* R₂} →
                                        {σ : S →+* S₂} →
                                          (M' : Submodule R M) →
                                            (N' : Submodule S N) →
                                              (f : M →ₛₗ[ρ] N →ₛₗ[σ] P) →
                                                M' ≤ f.ker → N' ≤ f.flip.ker → M ⧸ M' →ₛₗ[ρ] N ⧸ N' →ₛₗ[σ] P
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : t[a]?.isSome = true}, t[a]?.get h = t[a]