mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Monotone
/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set.  -/
MonotoneOn.map_sInf_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousWithinAt f s (sInf s) → MonotoneOn f s → f ⊤ = ⊤ → f (sInf s) = sInf (f '' s)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects finite products, then `F.leftOp : Cᵒᵖ ⥤ D` reflects finite
coproducts.  -/
CategoryTheory.Limits.reflectsFiniteCoproducts_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteProducts F],
  CategoryTheory.Limits.ReflectsFiniteCoproducts F.leftOp
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical section”
`{a} × univ`, `a : α`, and is Lipschitz continuous on each “horizontal section”
`univ × {b}`, `b : β` with the same Lipschitz constant `K`. Then it is continuous.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space.  -/
continuous_prod_of_continuous_lipschitzWith : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal),
  (∀ (a : α), Continuous fun y => f (a, y)) → (∀ (b : β), LipschitzWith K fun x => f (x, b)) → Continuous f
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_map_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α) (b : β), b ∈ (PMF.map f p).support ↔ ∃ a ∈ p.support, f a = b
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineSubspace.closed_of_finiteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {P : Type u_1} [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  (s : AffineSubspace 𝕜 P) [FiniteDimensional 𝕜 ↥s.direction], IsClosed ↑s
-- Mathlib.Topology.MetricSpace.Pseudo.Real
Real.dist_le_of_mem_uIcc : ∀ {x y x' y' : ℝ}, x ∈ Set.uIcc x' y' → y ∈ Set.uIcc x' y' → dist x y ≤ dist x' y'
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, a ∈ m.erase k → a ∈ m
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.positional.sizeOf_spec : ∀ (name : Lean.Name) (type : Lean.Expr), sizeOf (Lean.Doc.ArgSpec.positional✝ name type) = 1 + sizeOf name + sizeOf type
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The L-function of a nontrivial Dirichlet character does not vanish at `s = 1`.  -/
DirichletCharacter.LFunction_apply_one_ne_zero : ∀ {N : ℕ} {χ : DirichletCharacter ℂ N} [inst : NeZero N], χ ≠ 1 → DirichletCharacter.LFunction χ 1 ≠ 0
-- Mathlib.Order.Defs.Prop
Pi.le_def : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → LE (π i)] {x y : (i : ι) → π i}, x ≤ y ↔ ∀ (i : ι), x i ≤ y i
-- Mathlib.Data.Vector.Basic
List.Vector.reverse.eq_1 : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), v.reverse = ⟨v.toList.reverse, ⋯⟩
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isoClosure_strictColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}, t.WF → k ∈ Std.DTreeMap.Raw.filterMap f t → k ∈ t
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [G.IsEquivalence], G.IsCoverDense J
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonneg.add : ∀ {d : ℕ} {a b : ℤ√↑d}, a.Nonneg → b.Nonneg → (a + b).Nonneg
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- Intermediate result of `CliffordAlgebraQuaternion.equiv`: clifford algebras over
`CliffordAlgebraQuaternion.Q` can be converted to `ℍ[R,c₁,c₂]`.  -/
CliffordAlgebraQuaternion.toQuaternion : {R : Type u_1} →
  [inst : CommRing R] →
    {c₁ c₂ : R} → CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂) →ₐ[R] QuaternionAlgebra R c₁ 0 c₂
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.instSmallStrictLimitsOfShapeOfSmallOfLocallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.ObjectProperty.Small.{w, v_1, u_1} P]
  [CategoryTheory.LocallySmall.{w, v_1, u_1} C] [Small.{w, u'} J] [CategoryTheory.LocallySmall.{w, v', u'} J],
  CategoryTheory.ObjectProperty.Small.{w, v_1, u_1} (P.strictLimitsOfShape J)
-- Lean.Meta.Tactic.Simp.Simproc
/-- Given a declaration name `declName`, store the discrimination tree keys and the actual procedure.

This method is invoked by the command `builtin_simproc_pattern%` elaborator.
 -/
Lean.Meta.Simp.registerBuiltinSimprocCore : Lean.Name → Array Lean.Meta.SimpTheoremKey → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc → IO Unit
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.instIsOverι : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), AlgebraicGeometry.Scheme.Hom.IsOver U.ι X
-- Mathlib.GroupTheory.Nilpotent
/-- Products of nilpotent additive groups are nilpotent if their nilpotency class is
bounded.  -/
AddGroup.isNilpotent_pi_of_bounded_class : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] [∀ (i : η), AddGroup.IsNilpotent (Gs i)]
  (n : ℕ), (∀ (i : η), AddGroup.nilpotencyClass (Gs i) ≤ n) → AddGroup.IsNilpotent ((i : η) → Gs i)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (size : ℕ) (k : α) (v : β k)
  (l : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntry! = ⟨k, v⟩
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Sieve.effectiveEpimorphic_family : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {α : Type u_1} (X : α → C) (π : (a : α) → X a ⟶ B),
  (CategoryTheory.Presieve.ofArrows X π).EffectiveEpimorphic ↔ CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.lowerCentralSeries_zero : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M], LieModule.lowerCentralSeries R L M 0 = ⊤
-- Mathlib.RingTheory.Coprime.Lemmas
pairwise_isRelPrime_iff_isRelPrime_prod : ∀ {α : Type u_2} {I : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {s : I → α} {t : Finset I}
  [inst_2 : DecidableEq I],
  Pairwise (Function.onFun IsRelPrime fun i => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
-- Batteries.Data.List.Basic
/-- Right-biased version of `List.zip`. `zipRight as bs` returns the list of pairs
`(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, the
remaining `bᵢ` are paired with `none`.
```
zipRight [1, 2] ['a'] = [(some 1, 'a')]
zipRight [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipRight = zipWithRight prod.mk
```
 -/
List.zipRight : {α : Type u_1} → {β : Type u_2} → List α → List β → List (Option α × β)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- There exists a bilinear form, depending continuously on the basepoint and defining the
inner product in the fibers. This is expressed as an existence statement so that it is Prop-valued
in terms of existing data, the inner product on the fibers and the fiber bundle structure.  -/
IsContinuousRiemannianBundle.exists_continuous : ∀ {B : Type u_1} {inst : TopologicalSpace B} {F : Type u_2} {inst_1 : NormedAddCommGroup F} {inst_2 : NormedSpace ℝ F}
  {E : B → Type u_3} {inst_3 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_4 : (x : B) → NormedAddCommGroup (E x)}
  {inst_5 : (x : B) → InnerProductSpace ℝ (E x)} {inst_6 : FiberBundle F E} {inst_7 : VectorBundle ℝ F E}
  [self : IsContinuousRiemannianBundle F E],
  ∃ g, (Continuous fun x => ⟨x, g x⟩) ∧ ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_mapDomain_index : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : CommMonoid N]
  {f : α → β} {s : α →₀ M} {h : β → M → N},
  (∀ (b : β), h b 0 = 1) →
    (∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂) →
      (Finsupp.mapDomain f s).prod h = s.prod fun a m => h (f a) m
-- Mathlib.Dynamics.FixedPoints.Support
Function.hasCompactFixedSupport_id : ∀ (X : Type u_1) [inst : TopologicalSpace X], Function.HasCompactFixedSupport id
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_node3R : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on `ℝ`, and `f''` is strictly negative on `ℝ`,
then `f` is strictly concave on `ℝ`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly negative, except at at most one point.  -/
strictConcaveOn_univ_of_deriv2_neg : ∀ {f : ℝ → ℝ}, Continuous f → (∀ (x : ℝ), deriv^[2] f x < 0) → StrictConcaveOn ℝ Set.univ f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {v : β k}, ⟨k, v⟩ ∈ (↑m).toList ↔ m.get? k = some v
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- The `tsub` version of `sub_sub_eq_add_sub`.  -/
tsub_tsub_eq_add_tsub_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ b → a - (b - c) = a + c - b
-- Mathlib.MeasureTheory.Function.EssSup
essSup_comp_le_essSup_map_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β},
  AEMeasurable f μ →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
        essSup_comp_le_essSup_map_measure._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
          essSup_comp_le_essSup_map_measure._auto_3 →
        essSup (g ∘ f) μ ≤ essSup g (MeasureTheory.Measure.map f μ)
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.instLawfulMonadAttachExceptTOfLawfulMonad.match_2.splitter : {ε α : Type (max u_1 u_2)} →
  {P : α → Prop} →
    (motive : Except ε (Subtype P) → Sort u_3) →
      (a : Except ε (Subtype P)) →
        ((a : Subtype P) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive a
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intAdicAbv.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b),
  v.intAdicAbv hb =
    { toFun := fun r => ↑(v.intAdicAbvDef hb r), map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.transitionMap_map_mul : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) (x : R ⧸ I ^ n • ⊤) (y : R ⧸ I ^ n • ⊤),
  (AdicCompletion.transitionMap I R hmn) (x * y) =
    (AdicCompletion.transitionMap I R hmn) x * (AdicCompletion.transitionMap I R hmn) y
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOnFilter.div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' → TendstoUniformlyOnFilter (f / f') (g / g') l l'
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.matrix_π : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
      (CategoryTheory.Limits.biproduct.π g k) =
    CategoryTheory.Limits.biproduct.desc fun j => m j k
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableOn.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → (∀ x ∈ s, f x ≠ 0) → DifferentiableOn ℝ (fun x => |f x|) s
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {S : AlgebraicGeometry.Scheme}, CategoryTheory.Limits.HasFiniteCoproducts (P.Over ⊤ S)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_ne_zero_of_nonempty : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] [h : Nonempty α], Ordinal.type r ≠ 0
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] (toEquiv : M ≃ N)
  (map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEquiv.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEquiv.toFun ∘ x))
      FirstOrder.Language.Equiv.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam),
  sizeOf { toEquiv := toEquiv, map_fun' := map_fun', map_rel' := map_rel' } = 1 + sizeOf toEquiv
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ), ⇑(ab.trans bc) = ⇑bc ∘ ⇑ab
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Any mono factorisation of `f` gives a mono factorisation of `g ≫ f`.  -/
CategoryTheory.Limits.MonoFactorisation.isoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        CategoryTheory.Limits.MonoFactorisation f →
          {X' : C} → (g : X' ⟶ X) → CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((bs : List β) → motive [] bs) →
            ((a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs) → motive x x_1
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.range_isAddCommutative : ∀ {G : Type u_7} [inst : AddGroup G] [IsAddCommutative G] {N : Type u_8} [inst_2 : AddGroup N] (f : G →+ N),
  IsAddCommutative ↥f.range
-- Mathlib.Logic.Encodable.Basic
Encodable.decodeSigma.eq_1 : ∀ {α : Type u_1} {γ : α → Type u_3} [inst : Encodable α] [inst_1 : (a : α) → Encodable (γ a)] (n : ℕ),
  Encodable.decodeSigma n =
    match Nat.unpair n with
    | (n₁, n₂) => (Encodable.decode n₁).bind fun a => Option.map (Sigma.mk a) (Encodable.decode n₂)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- `trace` distributes over `Matrix.kroneckerMapBilinear`.

This is primarily used with `R = ℕ` to prove `Matrix.trace_kronecker`.  -/
Matrix.trace_kroneckerMapBilinear : ∀ {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_5} {γ : Type u_7} {m : Type u_10} {n : Type u_11}
  [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : AddCommMonoid α]
  [inst_5 : AddCommMonoid β] [inst_6 : AddCommMonoid γ] [inst_7 : Module R α] [inst_8 : Module R γ]
  [inst_9 : Module S β] [inst_10 : Module S γ] [inst_11 : SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ)
  (A : Matrix m m α) (B : Matrix n n β), (((Matrix.kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instNeg : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → Neg W'.Point
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.inter_isBasis_closure_iff_subset_closure_inter : ∀ {α : Type u_2} {M : Matroid α} {I X : Set α}, M.Indep I → (M.IsBasis (X ∩ I) X ↔ X ⊆ M.closure (X ∩ I))
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (m = 0 → False) →
    (match Int.ofNat m, Int.ofNat n with
      | 0, x => h_1 x
      | Int.ofNat m, Int.ofNat n => h_2 m n
      | Int.ofNat m.succ, Int.negSucc n => h_3 m n
      | Int.negSucc a, 0 => h_4 a
      | Int.negSucc m, Int.ofNat n.succ => h_5 m n
      | Int.negSucc m, Int.negSucc n => h_6 m n) =
      h_2 m n
-- Mathlib.Order.OrderDual
OrderDual.instMaxOfMin : (α : Type u_2) → [h : Min α] → Max αᵒᵈ
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.State.mk : Array Lean.Lsp.ResolvableCompletionItem → Lean.Server.Completion.State✝
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_commonExtTangents_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s₁ s₂ : EuclideanGeometry.Sphere P},
  as ∈ s₁.commonExtTangents s₂ ↔ as ∈ s₁.commonTangents s₂ ∧ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_diff_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
various sanity checks on the parameter (is it even of inductive type etc).
 -/
Lean.Elab.Structural.getRecArgInfo : Lean.Name → Lean.Elab.FixedParamPerm → Array Lean.Expr → ℕ → Lean.MetaM Lean.Elab.Structural.RecArgInfo
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJNeZeroNF.a₃ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharTwoJNeZeroNF], W.a₃ = 0
-- Mathlib.Data.Finsupp.SMul
Finsupp.moduleIsTorsionFree : ∀ {M : Type u_3} {R : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_7}
  [Module.IsTorsionFree R M], Module.IsTorsionFree R (ι →₀ M)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.linearExt : Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.Arith.Linear.State
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.categoryStruct_comp_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y Z : CategoryTheory.Bicategory.InducedBicategory C F} (u : X.Hom Y) (v : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp u v).hom = CategoryTheory.CategoryStruct.comp u.hom v.hom
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.toSub : {R : Type u} → [self : AddGroupWithOne R] → Sub R
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.union : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D],
  D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n j = C
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.compare_right_not_beq_gt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
    (k k').isLE = true → ∀ p ∈ r.toListModel, ¬(k p.fst == Ordering.gt) = true
-- Mathlib.Data.List.Map2
List.zipLeft'_cons_nil : ∀ {α : Type u} {β : Type v} (a : α) (as : List α),
  (a :: as).zipLeft' [] = ((a, none) :: List.map (fun a => (a, none)) as, [])
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.copy.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_add' := ⋯ }
-- Mathlib.Data.List.InsertIdx
List.eraseIdx_pmap : ∀ {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl : ∀ a ∈ l, p a) (n : ℕ),
  (List.pmap f l hl).eraseIdx n = List.pmap f (l.eraseIdx n) ⋯
-- Init.Data.String.Basic
String.Slice.endPos_copy : ∀ {s : String.Slice}, s.copy.endPos = s.endPos.copy
-- Mathlib.Data.Set.Subset
Set.preimage_val_sUnion : ∀ {α : Type u_2} {A : Set α} {S : Set (Set α)}, Subtype.val ⁻¹' ⋃₀ S = ⋃₀ {x | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
AffineSubspace.shift_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (s : AffineSubspace k P) [h : Nonempty ↥s] (c : P),
  s.shift c 0 = AffineSubspace.mk' c s.direction
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instInhabited : {𝕜 : Type u_2} → {α : Type u_5} → [inst : Zero 𝕜] → [inst_1 : LE α] → Inhabited (IncidenceAlgebra 𝕜 α)
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.synthesizeSyntheticMVarsUsingDefault : Lean.Elab.TermElabM Unit
-- Mathlib.Order.BoundedOrder.Lattice
max_bot_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] (a : α), max ⊥ a = a
-- Mathlib.Analysis.Calculus.DSlope
eqOn_dslope_slope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜), Set.EqOn (dslope f a) (slope f a) {a}ᶜ
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.lift_symm_apply : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β] (f : AddMagma.FreeAddSemigroup α →ₙ+ β),
  AddMagma.FreeAddSemigroup.lift.symm f = f.comp AddMagma.FreeAddSemigroup.of
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.exists_comap_eq_of_mem_minimalPrimes : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {I : Ideal S} (f : R →+* S),
  ∀ p ∈ (Ideal.comap f I).minimalPrimes, ∃ p', p'.IsPrime ∧ I ≤ p' ∧ Ideal.comap f p' = p
-- Init.Data.SInt.Bitwise
ISize.neg_one_or : ∀ {a : ISize}, -1 ||| a = -1
-- Init.Data.List.Lemmas
List.concat_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, (a :: l).concat b = a :: l.concat b