mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f : C ≌ D} {α β : e ⟶ f}, CategoryTheory.Equivalence.asNatTrans α = CategoryTheory.Equivalence.asNatTrans β → α = β
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (toContinuousMap : C(α, β))
  (map_bounded' : ∃ C, ∀ (x y : α), dist (toContinuousMap.toFun x) (toContinuousMap.toFun y) ≤ C)
  (toContinuousMap_1 : C(α, β))
  (map_bounded'_1 : ∃ C, ∀ (x y : α), dist (toContinuousMap_1.toFun x) (toContinuousMap_1.toFun y) ≤ C),
  ({ toContinuousMap := toContinuousMap, map_bounded' := map_bounded' } =
      { toContinuousMap := toContinuousMap_1, map_bounded' := map_bounded'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_map_of_gt_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i) (j : Fin (n + 2)),
  i.succ < j →
    ∀ {Z : SSet} (h : X ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) =
        CategoryTheory.CategoryStruct.comp (SSet.const x) h
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_strictMonoOn : StrictMonoOn Nat.fib (Set.Ici 2)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_succ_pow : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (m : ℕ) (x : K),
  PerfectClosure.mk K p (m + 1, x ^ p) = PerfectClosure.mk K p (m, x)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Backward direction of the unit.  -/
CategoryTheory.OverPresheafAux.unitBackward : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (η : F ⟶ A) →
        (X : C) →
          F.obj (Opposite.op X) →
            CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKey!_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, k ∈ t → (cmp k t.maxKey!).isLE = true
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqBoth : Bool → Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Order.UpperLower.Prod
LowerSet.Ici_prod_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a : α) (b : β),
  LowerSet.Iic a ×ˢ LowerSet.Iic b = LowerSet.Iic (a, b)
-- Lean.Elab.DefView
/-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation.  -/
Lean.Elab.HeaderProcessedSnapshot.moreSnaps : Lean.Elab.HeaderProcessedSnapshot → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v),
  ∃ b ∈ nonZeroDivisors R, a * ↑b ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v
-- Mathlib.Data.PFun
PFun.mem_dom : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α), x ∈ f.Dom ↔ ∃ y, y ∈ f x
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.normal.sizeOf_spec : ∀ (promise : IO.Promise Unit), sizeOf (Std.CancellationToken.Consumer.normal promise) = 1 + sizeOf promise
-- Mathlib.Topology.NhdsWithin
inter_mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) {t : Set α} {a : α}, t ∈ nhds a → s ∩ t ∈ nhdsWithin a s
-- Mathlib.Data.Fintype.Sets
/-- Given `Fintype α`, `finsetEquivSet` is the equiv between `Finset α` and `Set α`. (All
sets on a finite type are finite.)  -/
Fintype.finsetEquivSet : {α : Type u_1} → [Fintype α] → Finset α ≃ Set α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_filter : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_6 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β}
  {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)},
  forIn (Std.IterM.filter f it) init g =
    forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc)
-- Mathlib.Algebra.Order.Group.Unbundled.Int
/-- **Alias** of `Int.natAbs_le_self_sq`. -/
Int.natAbs_le_self_pow_two : ∀ (a : ℤ), ↑a.natAbs ≤ a ^ 2
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative multiplicatively bounded function and `x : R` is a unit with
`f x ≠ 0`, then for every `n : ℕ`, we have `f (x ^ n) ≠ 0`.  -/
map_pow_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → ∀ {x : R}, IsUnit x → f x ≠ 0 → ∀ (n : ℕ), (∀ (x y : R), f (x * y) ≤ c * f x * f y) → f (x ^ n) ≠ 0
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Suppose we have a cofiltered diagram of nonempty quasi-compact schemes,
whose transition maps are affine. Then the limit is also nonempty.
 -/
AlgebraicGeometry.Scheme.nonempty_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), Nonempty ↥(D.obj i)]
  [∀ (i : I), CompactSpace ↥(D.obj i)], Nonempty ↥c.pt
-- Mathlib.RingTheory.Coprime.Lemmas
Int.isCoprime_gcdA : ∀ {x y : ℤ}, IsCoprime x y → IsCoprime (x.gcdA y) y
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- An isometry between two bilinear spaces `M₁, B₁` and `M₂, B₂` over a ring `R`,
is a linear map between `M₁` and `M₂` that commutes with the bilinear forms.  -/
LinearMap.BilinForm.Isometry : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] → LinearMap.BilinForm R M₁ → LinearMap.BilinForm R M₂ → Type (max u_3 u_4)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.equivAdjoin_toAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), ↑(minpoly.equivAdjoin hx) = AdjoinRoot.Minpoly.toAdjoin R x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.QuasiCompact f
-- Batteries.Data.Vector.Lemmas
Vector.scanlM_reverse : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : β → α → m β} {as : Vector α n},
  Vector.scanlM f init as.reverse = Vector.reverse <$> Vector.scanrM (flip f) init as
-- Mathlib.Data.Finset.Card
Finset.card_le_card_sdiff_add_card : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s.card ≤ (s \ t).card + t.card
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k k' : α} {f : Option β → Option β}
  (hc : (Std.DHashMap.Internal.Raw₀.Const.alter m k f).contains k' = true),
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k' hc =
    if heq : (k == k') = true then (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get ⋯
    else Std.DHashMap.Internal.Raw₀.Const.get m k' ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordered_keys_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a.1 b.1 = Ordering.lt) t.toList
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalM.runCore : {α : Type} → Lean.Meta.Grind.Goal → Lean.Meta.Grind.GoalM α → Lean.Meta.Grind.GrindM (α × Lean.Meta.Grind.Goal)
-- Lean.Compiler.IR.CompilerM
Lean.IR.Log : Type
-- Init.Data.BitVec.Bitblast
BitVec.toInt_bmod_cancel : ∀ {w : ℕ} (b : BitVec w), b.toInt.bmod (2 ^ w) = b.toInt
-- Mathlib.Order.SuccPred.Limit
PredOrder.colimitRecOn_pred : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : WellFoundedGT α]
  (isMax : (a : α) → IsMax a → motive a) (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) [inst_3 : NoMinOrder α]
  (b : α),
  PredOrder.colimitRecOn (Order.pred b) isMax pred isPredLimit =
    pred b ⋯ (PredOrder.colimitRecOn b isMax pred isPredLimit)
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_of_forall_isSymm : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  (∀ V ∈ uniformity α, SetRel.IsSymm V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, UniformSpace.ball y V) → TotallyBounded s
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
/-- If `r > 0`, then `OpenPartialHomeomorph.univBall c r` is a smooth open partial homeomorphism
with `source = Set.univ` and `target = Metric.ball c r`.
Otherwise, it is the translation by `c`.
Thus in all cases, it sends `0` to `c`, see `OpenPartialHomeomorph.univBall_apply_zero`.  -/
OpenPartialHomeomorph.univBall : {E : Type u_1} →
  [inst : SeminormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      {P : Type u_2} → [inst_2 : PseudoMetricSpace P] → [NormedAddTorsor E P] → P → ℝ → OpenPartialHomeomorph E P
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.eq_zero_imp : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {l : Filter α}, f'' =O[l] g'' → ∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0
-- Mathlib.Data.List.Duplicate
List.Duplicate.of_duplicate_cons : ∀ {α : Type u_1} {l : List α} {x y : α}, List.Duplicate x (y :: l) → x ≠ y → List.Duplicate x l
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMulOneClass : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [MulOneClass Y] → MulOneClass (LocallyConstant X Y)
-- Mathlib.Order.SymmDiff
bihimp_iff_iff : ∀ {p q : Prop}, bihimp p q ↔ (p ↔ q)
-- Mathlib.Data.Rat.Cast.Lemmas
NNRat.cast_pow : ∀ {K : Type u_1} [inst : DivisionSemiring K] (q : ℚ≥0) (n : ℕ), ↑(q ^ n) = ↑q ^ n
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentCoordChange_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {x z : M} {v : E},
  z ∈ (extChartAt I x).source → (tangentCoordChange I x x z) v = v
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMapM_cons.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive __do_lift
-- Mathlib.GroupTheory.Commutator.Basic
image_addCommutatorSet_closureAddCommutatorRepresentatives : ∀ (G : Type u_1) [inst : AddGroup G],
  ⇑(closureAddCommutatorRepresentatives G).subtype '' addCommutatorSet ↥(closureAddCommutatorRepresentatives G) =
    addCommutatorSet G
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The restriction of `f - μ • 1` to the generalized `μ`-eigenspace is nilpotent.  -/
Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M) (μ : R)
  (h :
    optParam (Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)) ⋯),
  IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_mul_isBoundedUnder_le : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l g →
    Filter.Tendsto (fun x => f x * g x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Lean.Meta.Tactic.Simp.Simproc
/-- Try to retrieve the simproc set using the `simp` or `simproc` attribute names.
Recall that when we declare a `simp` set using `register_simp_attr`, an associated
`simproc` set is automatically created. We use the function `simpAttrNameToSimprocAttrName` to
find the `simproc` associated with the `simp` attribute.
 -/
Lean.Meta.Simp.getSimprocExtension? : Lean.Name → IO (Option Lean.Meta.Simp.SimprocExtension)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiffWithinAt.subtypeVal_comp_iff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M']
  (U : TopologicalSpace.Opens M') (f : M → ↥U) (s : Set M) (x : M),
  ContMDiffWithinAt I I' (↑⊤) (Subtype.val ∘ f) s x ↔ ContMDiffWithinAt I I' (↑⊤) f s x
-- Init.Data.Range.Polymorphic.Fin
Fin.rxcHasSize_eq : ∀ {n : ℕ}, Std.Rxc.HasSize.size = fun lo hi => ↑hi + 1 - ↑lo
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.obj₀Equiv_symm_apply : ∀ {n : ℕ} (i : Fin (n + 1)), SSet.stdSimplex.obj₀Equiv.symm i = SSet.stdSimplex.const n i (Opposite.op { len := 0 })
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_rootMultiplicity_map : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {p : Polynomial A} {f : A →+* B},
  Function.Injective ⇑f →
    ∀ (a : A), Polynomial.rootMultiplicity a p = Polynomial.rootMultiplicity (f a) (Polynomial.map f p)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- That $\operatorname{im}(q^* : (V/W)^* \to V^*) = \operatorname{ann}(W)$.  -/
Submodule.range_dualMap_mkQ_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (W : Submodule R M),
  W.mkQ.dualMap.range = W.dualAnnihilator
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_seq.match_1.eq_1 : ∀ {ε σ α β : Type u_1} (motive : EStateM.Result ε σ (α → β) → Sort u_2) (g : α → β) (s : σ)
  (h_1 : (g : α → β) → (s : σ) → motive (EStateM.Result.ok g s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok g s with
    | EStateM.Result.ok g s => h_1 g s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 g s
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.instCommMonoid.eq_1 : ∀ {M : Type u_2} [inst : Monoid M] [inst_1 : IsMulCommutative M],
  IsMulCommutative.instCommMonoid = { toMonoid := inst, mul_comm := ⋯ }
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.map_self : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.map f = 0
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.nonempty_Icc`. -/
Finset.Aesop.nonempty_Icc_of_le : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a ≤ b → (Finset.Icc a b).Nonempty
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
coe_basisOfLinearIndependentOfCardEqFinrank' : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [inst_4 : FiniteDimensional K V] (b : ι → V) (hb : LinearIndependent K b)
  (hι : Fintype.card ι = Module.finrank K V), ⇑(basisOfLinearIndependentOfCardEqFinrank' b hb hι) = b
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_c₄_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).c₄ = W.c₄
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.power_lt_aleph0 : ∀ {a b : Cardinal.{u_1}}, a < Cardinal.aleph0 → b < Cardinal.aleph0 → a ^ b < Cardinal.aleph0
-- Batteries.Data.Fin.Fold
Fin.dfoldlM_loop_lt : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1) → Type u_1} {i : ℕ} [inst : Monad m]
  (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (h : i < n) (x : α ⟨i, ⋯⟩),
  Fin.dfoldlM.loop n α f i ⋯ x = f ⟨i, h⟩ x >>= Fin.dfoldlM.loop n α f (i + 1) ⋯
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germToPullbackStalk.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U),
  TopCat.Presheaf.germToPullbackStalk C f F U x hx = TopCat.Presheaf.germToPullbackStalk C f F U x hx
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_eq_Ioo_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico b a = Set.Ioo b a ↔ ¬b < a
-- Init.Data.List.Lemmas
List.mem_of_getLast? : ∀ {α : Type u_1} {l : List α} {a : α}, l.getLast? = some a → a ∈ l
-- Lean.Meta.Match.Match
/-- Does any alternative have a pattern that can be independently handled (variable, inaccessible,
as-pattern) before any refutable pattern?
 -/
Lean.Meta.Match.hasIndependentPatterns : Lean.Meta.Match.Problem → Bool
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.MonoOver.factors_congr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} {Y : C}
  (h : Y ⟶ X) (e : f ≅ g), f.Factors h ↔ g.Factors h
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
/-- A morphism of schemes `X ⟶ Y` is affine if
the preimage of any affine open subset of `Y` is affine.  -/
AlgebraicGeometry.IsAffineHom : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Init.Data.Nat.Power2.Basic
Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo : ∀ {n : ℕ}, n.isPowerOfTwo → (n * 2).isPowerOfTwo
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_one_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom f
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- Bound for iterated forward differences of a continuous function from a compact space to a
nonarchimedean seminormed group.  -/
IsUltrametricDist.norm_fwdDiff_iter_apply_le : ∀ {M : Type u_1} {G : Type u_2} [inst : TopologicalSpace M] [inst_1 : CompactSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : SeminormedAddCommGroup G] [IsUltrametricDist G] (h : M) (f : C(M, G)) (m : M) (n : ℕ),
  ‖(fwdDiff h)^[n] (⇑f) m‖ ≤ ‖f‖
-- Mathlib.RingTheory.LaurentSeries
/-- The localization map from power series to Laurent series.  -/
LaurentSeries.of_powerSeries_localization : ∀ {R : Type u_1} [inst : CommRing R], IsLocalization (Submonoid.powers PowerSeries.X) (LaurentSeries R)
-- Mathlib.Data.Set.Function
Set.LeftInvOn.right_prodMk : ∀ {α : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s : Set α} {f₁ : α → β₁} {f₂ : α → β₂} {g₂ : β₂ → α},
  Set.LeftInvOn g₂ f₂ s → Set.LeftInvOn (fun x => g₂ x.2) (fun x => (f₁ x, f₂ x)) s
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConcaveOn.condExp_map_le_trim_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mE : MeasurableSpace E} [BorelSpace E]
  (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConcaveOn ℝ Set.univ φ →
    UpperSemicontinuous φ →
      MeasureTheory.StronglyMeasurable φ →
        MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m]
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_sum : ∀ {R : Type u} {ι : Type y} [inst : Semiring R] {s : Finset ι} {f : ι → Polynomial R},
  Polynomial.derivative (∑ b ∈ s, f b) = ∑ b ∈ s, Polynomial.derivative (f b)
-- Mathlib.Data.Rat.Lemmas
Rat.forall : ∀ {p : ℚ → Prop}, (∀ (r : ℚ), p r) ↔ ∀ (a b : ℤ), b ≠ 0 → p (↑a / ↑b)
-- Mathlib.Algebra.Colimit.Ring
Field.DirectLimit.mul_inv_cancel : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  [inst_3 : (i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) {p : Ring.DirectLimit G f},
  p ≠ 0 → p * Field.DirectLimit.inv G f p = 1
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.lastVar : Lean.Grind.AC.Seq → Lean.Grind.AC.Var
-- Mathlib.Data.NNRat.Defs
NNRat.toNNRat_coe : ∀ (q : ℚ≥0), (↑q).toNNRat = q
-- Aesop.Options.Public
Aesop.instInhabitedStrategy.default : Aesop.Strategy
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.mul_ι_mul_ι_mul_comm_of_isOrtho : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q) {a b : M},
  QuadraticMap.IsOrtho Q a b →
    ∀ (y : CliffordAlgebra Q),
      x * (CliffordAlgebra.ι Q) a * ((CliffordAlgebra.ι Q) b * y) =
        -(x * (CliffordAlgebra.ι Q) b * ((CliffordAlgebra.ι Q) a * y))
-- Mathlib.RingTheory.Ideal.Operations
Ideal.bot_mul : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R), ⊥ * I = ⊥
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).inv
      (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).pOpcycles j) h)
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeMemFinset : {α : Type u} → (s : Finset α) → Fintype ↑{a | a ∈ s}
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- `Fintype.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.

This map is linear in `v` if `R` is commutative, and always linear in `f`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
 -/
Fintype.bilinearCombination : {α : Type u_1} →
  {M : Type u_2} →
    (R : Type u_3) →
      [Fintype α] →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              (S : Type u_4) →
                [inst_3 : Semiring S] →
                  [inst_4 : Module S M] → [inst_5 : SMulCommClass R S M] → (α → M) →ₗ[S] (α → R) →ₗ[R] M