mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffWithinAt.change_section_trivialization : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {s : Set M} {x : M} {f : M → Bundle.TotalSpace F E},
  ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x →
    ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun y => (↑e (f y)).2) s x →
      f x ∈ e.source → f x ∈ e'.source → ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun y => (↑e' (f y)).2) s x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_zero' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], ⇑(MvPolynomial.monomial 0) = ⇑MvPolynomial.C
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- The opposite of a profunctor.  -/
CategoryTheory.Profunctor.op : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D → CategoryTheory.Profunctor.{w, v₂, v₁, u₂, u₁} Dᵒᵖ Cᵒᵖ
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_inv_dvd : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x ≠ 0 → x⁻¹.num ∣ x.denom
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.succNthValUnits.congr_simp : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ) (a a_1 : kˣ),
  a = a_1 →
    ∀ (A A_1 : WittVector p k),
      A = A_1 →
        ∀ (bs bs_1 : Fin (n + 1) → k),
          bs = bs_1 → WittVector.succNthValUnits n a A bs = WittVector.succNthValUnits n a_1 A_1 bs_1
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_lift_of_infinite' : ∀ (α : Type u) (β : Type v) [Nonempty α] [inst : Zero β] [Infinite β],
  Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))
-- Batteries.Data.PairingHeap
/-- `O(1)`. Returns the smallest element in the heap, or `default` if the heap is empty.  -/
Batteries.PairingHeap.headI : {α : Type u} → {le : α → α → Bool} → [Inhabited α] → Batteries.PairingHeap α le → α
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
Finset.measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (s : Finset α) (μ : MeasureTheory.Measure α)
  [MeasureTheory.NullSingletonClass μ], μ ↑s = 0
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.instStar : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Star β] → [ContinuousStar β] → Star C(α, β)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A bound variable, from a lambda or forall binder.
It stores the De Bruijn index and the arity.  -/
Lean.Meta.RefinedDiscrTree.Key.bvar : ℕ → ℕ → Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Algebra.Order.SuccPred
antitoneOn_of_le_sub_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_rhs_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Lean.ReducibilityAttrs
Lean.isInstanceReducibleCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.ofLE_apply : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂) (v : V), (SimpleGraph.Hom.ofLE h) v = v
-- Mathlib.GroupTheory.Congruence.Hom
/-- The homomorphism on the quotient of a monoid by a congruence relation `c` induced by a
homomorphism constant on `c`'s equivalence classes.  -/
Con.lift : {M : Type u_1} →
  {P : Type u_3} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass P] → (c : Con M) → (f : M →* P) → c ≤ Con.ker f → c.Quotient →* P
-- Mathlib.NumberTheory.NumberField.Basic
/-- The quotient of `ℚ[X]` by the ideal generated by an irreducible polynomial of `ℚ[X]`
is a number field.  -/
AdjoinRoot.instNumberFieldRat : ∀ {f : Polynomial ℚ} [hf : Fact (Irreducible f)], NumberField (AdjoinRoot f)
-- Mathlib.Data.Finsupp.Ext
Finsupp.add_closure_setOfPred_eq_single : ∀ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M], AddSubmonoid.closure {f | ∃ a b, f = fun₀ | a => b} = ⊤
-- Init.Data.Int.Order
Int.le_add_of_sub_left_le : ∀ {a b c : ℤ}, a - b ≤ c → a ≤ b + c
-- Lean.ResolveName
Lean.ResolveName.resolveNamespaceUsingOpenDecls : Lean.Environment → Lean.Name → List Lean.OpenDecl → List Lean.Name
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.map_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.PrepathObject X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).p₁ = F.map P.p₁
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fmod_right : ∀ (a b : ℤ), (a * b).fmod a = 0
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- A `k`-algebra homomorphism from `SkewMonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`.  -/
SkewMonoidAlgebra.algHom_ext : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : CommSemiring k] {A : Type u_3} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  ⦃φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A⦄,
  (∀ (x : G), φ₁ (SkewMonoidAlgebra.single x 1) = φ₂ (SkewMonoidAlgebra.single x 1)) → φ₁ = φ₂
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.alterₘ.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (b : β a) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.RingTheory.Unramified.Basic
/-- This actually does not need the localization instance, and is stated here again for
consistency. See `Algebra.FormallyUnramified.of_comp` instead.

The intended use is for copying proofs between `Formally{Unramified, Smooth, Etale}`
without the need to change anything (including removing redundant arguments).  -/
Algebra.FormallyUnramified.localization_base : ∀ {R : Type u_1} {Rₘ : Type u_3} {Sₘ : Type u_4} [inst : CommRing R] [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ]
  (M : Submonoid R) [inst_3 : Algebra R Sₘ] [inst_4 : Algebra R Rₘ] [inst_5 : Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
  [Algebra.FormallyUnramified R Sₘ], Algebra.FormallyUnramified Rₘ Sₘ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.getKey! a = m.getKeyD a default
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.specImpl : (m : Type u_1 → Type u_1) → MLList.Spec✝ m
-- Init.Omega.LinearCombo
/-- Implementation of subtraction on `LinearCombo`.  -/
Lean.Omega.LinearCombo.sub : Lean.Omega.LinearCombo → Lean.Omega.LinearCombo → Lean.Omega.LinearCombo
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_eq_iff : ∀ (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] [inst_6 : LieModule R L M]
  [LieModule.IsFaithful R L M] {x y : L}, (LieModule.toEnd R L M) x = (LieModule.toEnd R L M) y ↔ x = y
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The colimit of `F ⋙ forget₂ AddCommMonCat AddMonCat` in the category `AddMonCat`. In the
following, we will show that this has the structure of a _commutative_ additive monoid.  -/
AddCommMonCat.FilteredColimits.M : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J AddCommMonCat → AddMonCat
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.toCommGrp_obj_grp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  ((CategoryTheory.Preadditive.toCommGrp C).obj X).grp = CategoryTheory.Preadditive.instGrpObj X
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- the corresponding type (II) simplex is the `1`-codimensional
face given by this index  -/
SSet.Subcomplex.PairingCore.index : {X : SSet} → {A : X.Subcomplex} → (self : A.PairingCore) → (s : self.ι) → Fin (self.dim s + 2)
-- Mathlib.Algebra.Ring.Int.Parity
Int.two_dvd_mul_add_one : ∀ (k : ℤ), 2 ∣ k * (k + 1)
-- Plausible.Gen
/-- Picks one of the generators in `gs` at random, returning the `default` generator
if `gs` is empty.

(This is a more ergonomic version of Plausible's `Gen.oneOf` which doesn't
require the caller to supply a proof that the list index is in bounds.)  -/
Plausible.Gen.oneOfWithDefault : {α : Type} → Plausible.Gen α → List (Plausible.Gen α) → Plausible.Gen α
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- The "identity" functor from `ObjAsType α` to `AsType α`.  -/
CategoryTheory.FinCategory.objAsTypeToAsType : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [inst_2 : CategoryTheory.FinCategory α] →
        CategoryTheory.Functor (CategoryTheory.FinCategory.ObjAsType α) (CategoryTheory.FinCategory.AsType α)
-- Mathlib.Algebra.Order.Group.Cone
LinearOrder.mkOfAddGroupCone.eq_1 : ∀ {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : AddGroupConeClass S G]
  [inst_3 : HasMemOrNegMem C] [inst_4 : DecidablePred fun x => x ∈ C],
  LinearOrder.mkOfAddGroupCone C =
    { toPartialOrder := PartialOrder.mkOfAddGroupCone C, min := fun a b => if a ≤ b then a else b,
      max := fun a b => if a ≤ b then b else a, compare := fun a b => compareOfLessAndEq a b, le_total := ⋯,
      toDecidableLE := fun x b => inst_4 (b - x), toDecidableEq := decidableEqOfDecidableLE,
      toDecidableLT := decidableLTOfDecidableLE, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }
-- Mathlib.Data.PEquiv
PEquiv.trans_assoc : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ),
  (f.trans g).trans h = f.trans (g.trans h)
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.proj.eq_1 : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i} (i : ι)
  (p : Path.Homotopic.Quotient as bs), Path.Homotopic.proj i p = p.map { toFun := fun p => p i, continuous_toFun := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.ofInt_one : UInt16.ofInt 1 = 1
-- Mathlib.Order.KrullDimension
/-- A definition of krullDim for nonempty `α` that avoids `WithBot`  -/
Order.krullDim_eq_iSup_length : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim α = ↑(⨆ p, ↑p.length)
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.toCentralizer_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) (x : α), ↑(a.toCentralizer τ) x = a.ofPermHomFun τ x
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.setRoot.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) →
            (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)) →
          motive x
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.liftCompleteLattice.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : CompleteLattice α]
  (gi : GaloisCoinsertion u l),
  gi.liftCompleteLattice =
    { toLattice := gi.liftLattice, sSup := fun s => gi.choice (sSup (u '' s)) ⋯, isLUB_sSup := ⋯,
      sInf := fun s => l (sInf (u '' s)), isGLB_sInf := ⋯, toBoundedOrder := gi.liftBoundedOrder }
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.lift_symm_injective_of_injective : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β] {f : WithOne α →* β},
  Function.Injective ⇑f → Function.Injective ⇑(WithOne.lift.symm f)
-- Batteries.Recycling.RBTree.Basic
/-- Fold a function in tree order along the nodes. `v₀` is used at `nil` nodes and
`f` is used to combine results at branching nodes.
 -/
RBTree.RBNode.fold : {σ : Sort u_1} → {α : Type u_2} → σ → (σ → α → σ → σ) → RBTree.RBNode α → σ
-- Init.Data.Vector.Find
Vector.getElem_zero_flatten : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n} (h : 0 < n * m),
  xss.flatten[0] = (Vector.findSome? (fun xs => xs[0]?) xss).get ⋯
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coeToMulHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N],
  MonoidHom.coeToMulHom = { coe := MonoidHom.toMulHom }
-- Init.Data.String.Basic
String.Pos.lt_of_lt_of_le : ∀ {s : String} {p q r : s.Pos}, p < q → q ≤ r → p < r
-- Lean.Meta.InferType
/-- `isProofQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to
`n` arguments is a proof.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isProofQuickApp : Lean.Expr → ℕ → Lean.MetaM Lean.LBool
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.instPretriangulatedIntUp : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          CategoryTheory.Pretriangulated (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.ext_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] {s t : ClopenUpperSet α}, s = t ↔ ↑s = ↑t
-- Mathlib.Logic.Equiv.Defs
Equiv.ext_iff : ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g ↔ ∀ (x : α), f x = g x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.blast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Topology.Algebra.InfiniteSum.Real
summable_sigma_of_nonneg : ∀ {α : Type u_4} {β : α → Type u_3} {f : (x : α) × β x → ℝ},
  (∀ (x : (x : α) × β x), 0 ≤ f x) →
    (Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKeyD_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k fallback : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (Std.Internal.List.Const.modifyKey k f l) fallback =
      if Std.Internal.List.containsKey k l = true then k else fallback
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher : {pat : String.Slice} → String.Slice.Pattern.ToForwardSearcher pat String.Slice.Pattern.ForwardSliceSearcher
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.cocycle : ∀ (self : TopCat.GlueData.MkCore) (i j k : self.J) (x : ↥(self.V i j)) (h : ↑x ∈ self.V i k),
  ↑((CategoryTheory.ConcreteCategory.hom (self.t j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (self.t i j)) x), ⋯⟩) =
    ↑((CategoryTheory.ConcreteCategory.hom (self.t i k)) ⟨↑x, h⟩)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_empty : ∀ {α : Type u_1} [inst : Fintype ↑∅], ∅.toFinset = ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.innerAnodyneExtensions_eq_llp_rlp : SSet.innerAnodyneExtensions = SSet.innerHornInclusions.rlp.llp
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.toAddMonoidHomClass : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
  AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
/-- The type of closed subgroups of an additive topological group.  -/
ClosedAddSubgroup : (G : Type u) → [AddGroup G] → [TopologicalSpace G] → Type u
-- Mathlib.Data.W.Basic
/-- `WType` is encodable when `α` is an encodable fintype and for every `a : α`, `β a` is
encodable.  -/
WType.instEncodable : {α : Type u_1} →
  {β : α → Type u_2} → [(a : α) → Fintype (β a)] → [(a : α) → Encodable (β a)] → [Encodable α] → Encodable (WType β)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        {aig : Std.Sat.AIG α} →
          {w : ℕ} → aig.RefVec w → ℕ → (curr : ℕ) → curr ≤ newWidth → aig.RefVec curr → aig.RefVec newWidth
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Commute.tsum_left : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] (a : α),
  (∀ (i : ι), Commute (f i) a) → Commute (∑'[L] (i : ι), f i) a
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The `dualAnnihilator` of a submodule of the dual space pulled back along the evaluation map
`Module.Dual.eval`.  -/
Submodule.dualCoannihilator : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R (Module.Dual R M) → Submodule R M
-- Mathlib.Order.SuccPred.Basic
/-- A constructor for `PredOrder α` usable when `α` has no minimal element.  -/
PredOrder.ofPredLeIff : {α : Type u_1} → [inst : Preorder α] → (pred : α → α) → (∀ {a b : α}, b ≤ pred a ↔ b < a) → PredOrder α
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_le_of_surjective : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  Function.Surjective ⇑f → Module.supportDim R N ≤ Module.supportDim R M
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_range : ∀ {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : Std.Legacy.Range}
  {init : β} {f : ℕ → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List ℕ) (cur : ℕ) (suff : List ℕ) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_map_eq : ∀ {α β : Type u} {f : α → β} {X : Set β} (M : Matroid α) (hf : Set.InjOn f M.E), (M.map f hf).cRk X = M.cRk (f ⁻¹' X)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurableSet_range : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → MeasurableSet (Set.range f)
-- Init.Data.Array.Subarray
Subarray.size_le_array_size : ∀ {α : Type u_1} {s : Subarray α}, Std.Slice.size s ≤ s.array.size
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.instFintypePairwise.match_5.eq_2 : ∀ (ι : Type u_1) (motive : CategoryTheory.Pairwise ι → Sort u_2) (a a_1 : ι)
  (h_1 : (a : ι) → motive (CategoryTheory.Pairwise.single a))
  (h_2 : (a a_2 : ι) → motive (CategoryTheory.Pairwise.pair a a_2)),
  (match CategoryTheory.Pairwise.pair a a_1 with
    | CategoryTheory.Pairwise.single a => h_1 a
    | CategoryTheory.Pairwise.pair a a_2 => h_2 a a_2) =
    h_2 a a_1
-- Mathlib.Data.Option.Basic
Option.mem_pmem : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (x : Option α) {a : α} (h : ∀ a ∈ x, p a)
  (ha : a ∈ x), f a ⋯ ∈ Option.pmap f x h
-- Mathlib.Logic.Equiv.Sum
Equiv.sumSigmaDistrib_symm_apply : ∀ {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) (a : (i : α) × t (Sum.inl i) ⊕ (i : β) × t (Sum.inr i)),
  (Equiv.sumSigmaDistrib t).symm a = Sum.elim (fun a => ⟨Sum.inl a.fst, a.snd⟩) (fun b => ⟨Sum.inr b.fst, b.snd⟩) a
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
hasFPowerSeriesAt_clog_one : HasFPowerSeriesAt Complex.log (FormalMultilinearSeries.ofScalars ℂ fun n => -(-1) ^ n / ↑n) 1
-- Mathlib.Algebra.Order.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : LinearOrderedCommGroupWithZero B] {f : A →*₀ B},
  IsOrderedMonoid f.ValueGroup₀
-- Mathlib.Order.IsNormal
Order.IsNormal.exists_map_le_lt_map_succ_of_exists_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : SuccOrder α] [inst_3 : LinearOrder β]
  [NoMaxOrder α] [inst_5 : OrderBot α] [WellFoundedLT β] {f : α → β} {x : β},
  Order.IsNormal f → (∃ y, x ≤ f y) → f ⊥ ≤ x → ∃ a, f a ≤ x ∧ x < f (Order.succ a)
-- Init.Data.Int.Order
Int.sub_lt_self : ∀ (a : ℤ) {b : ℤ}, 0 < b → a - b < a
-- Mathlib.Topology.Constructible
/-- If `f` is continuous and is such that preimages of open retrocompact sets are retrocompact,
then preimages of constructible sets are constructible.  -/
Topology.IsConstructible.preimage : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Continuous f →
    (∀ (s : Set Y), IsOpen s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)) →
      Topology.IsConstructible s → Topology.IsConstructible (f ⁻¹' s)
-- Mathlib.Algebra.Group.Commute.Defs
/-- Equality behind `Commute a b`; useful for rewriting.  -/
Commute.eq : ∀ {S : Type u_3} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC_nc.go : ℕ → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple.0.RootPairing.GeckConstruction.instIsIrreducible_aux₂ : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : CharZero K]
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] [inst_4 : AddCommGroup M] [inst_5 : Module K M]
  [inst_6 : AddCommGroup N] [inst_7 : Module K N] {P : RootPairing ι K M N} [inst_8 : P.IsCrystallographic] {b : P.Base}
  [P.IsReduced] [P.IsIrreducible]
  {U : LieSubmodule K (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → K)} {i : ι},
  RootPairing.GeckConstruction.v b i ∈ U → U = ⊤