mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_filterMap_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  m.WF → ((Std.HashMap.Raw.filterMap f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = none)
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.mk.inj : ∀ {sysname release version machine sysname_1 release_1 version_1 machine_1 : String},
  { sysname := sysname, release := release, version := version, machine := machine } =
      { sysname := sysname_1, release := release_1, version := version_1, machine := machine_1 } →
    sysname = sysname_1 ∧ release = release_1 ∧ version = version_1 ∧ machine = machine_1
-- Mathlib.CategoryTheory.EffectiveEpi.Coproduct
/-- Given an `EffectiveEpiFamily X π` and a corresponding coproduct cocone, the family descends to an
`EffectiveEpi` from the coproduct.
 -/
CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        (X : α → C) →
          (c : CategoryTheory.Limits.Cofan X) →
            (hc : CategoryTheory.Limits.IsColimit c) →
              (π : (a : α) → X a ⟶ B) →
                [CategoryTheory.EffectiveEpiFamily X π] →
                  CategoryTheory.EffectiveEpiStruct (hc.desc (CategoryTheory.Limits.Cofan.mk B π))
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.H1Cotangent.map.congr_simp : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (S' : Type u_2)
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (T : Type w) [inst_5 : CommRing T] [inst_6 : Algebra R T]
  [inst_7 : Algebra S T] [inst_8 : IsScalarTower R S T] [inst_9 : Algebra S' T] [inst_10 : IsScalarTower R S' T],
  Algebra.H1Cotangent.map R S S' T = Algebra.H1Cotangent.map R S S' T
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
hasDerivAt_of_tendstoUniformly : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g : 𝕜 → G} {f' : ι → 𝕜 → G} {g' : 𝕜 → G}
  [IsRCLikeNormedField 𝕜] [l.NeBot],
  TendstoUniformly f' g' l →
    (∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x) →
      (∀ (x : 𝕜), Filter.Tendsto (fun n => f n x) l (nhds (g x))) → ∀ (x : 𝕜), HasDerivAt g (g' x) x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.toCloseds_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (x : α), {x}.toCloseds = {x}
-- Mathlib.Order.Disjoint
Disjoint.mono : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
  a ≤ b → c ≤ d → Disjoint b d → Disjoint a c
-- Mathlib.Analysis.Convex.Between
sbtw_add_const_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R (x + v) (y + v) (z + v) ↔ Sbtw R x y z
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅} {km : α},
  t.max he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaCongrRight_symm : ∀ {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a),
  (Equiv.sigmaCongrRight F).symm = Equiv.sigmaCongrRight fun a => (F a).symm
-- Mathlib.RingTheory.LocalRing.Basic
/-- A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.  -/
IsLocalRing.of_nonunits_add : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R],
  (∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) → IsLocalRing R
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_symm_C_C : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (r : R),
  (MvPolynomial.sumAlgEquiv R S₁ S₂).symm (MvPolynomial.C (MvPolynomial.C r)) = MvPolynomial.C r
-- Mathlib.RingTheory.Etale.Weakly
Algebra.WeaklyEtale.mk : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  autoParam (Module.Flat R S) Algebra.WeaklyEtale.flat._autoParam →
    (Algebra.TensorProduct.lmul' R).Flat → Algebra.WeaklyEtale R S
-- Init.Data.SInt.Bitwise
Int16.xor_neg_one : ∀ {a : Int16}, a ^^^ -1 = ~~~a
-- Mathlib.RingTheory.HopfAlgebra.Quotient
Ideal.IsHopfIdeal.toIsCoideal : ∀ {R : Type u_1} {A : Type u_2} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : HopfAlgebraStruct R A} {I : Ideal A}
  [self : Ideal.IsHopfIdeal R I], (Submodule.restrictScalars R I).IsCoideal
-- Init.Grind.ToInt
/-- The embedding into the integers takes division to division, wrapped into the range interval.
 -/
Lean.Grind.ToInt.Div : (α : Type u) → [Div α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.Γ_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  AlgebraicGeometry.SheafedSpace.Γ =
    AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op.comp AlgebraicGeometry.PresheafedSpace.Γ
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis_of_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {I J X C : Set α},
  M.IsBasis I X → M.IsBasis' J C → M.Indep (I \ C ∪ J) → (M.contract C).IsBasis (I \ C) (X \ C)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The proof that `c.subject = c.norm`  -/
Mathlib.Tactic.Determinant.Cert.proof : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      (c : Mathlib.Tactic.Determinant.Cert rα) →
        have a := c.norm;
        have a_1 := c.subject;
        Q(«$a_1» = «$a»)
-- Qq.Macro
Qq.Impl.MVarSynth.type.injEq : ∀ (unquotedMVar unquotedMVar_1 : Lean.MVarId),
  (Qq.Impl.MVarSynth.type unquotedMVar = Qq.Impl.MVarSynth.type unquotedMVar_1) = (unquotedMVar = unquotedMVar_1)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
/-- A morphism of schemes `f : X ⟶ Y` is universally closed if the base change `X ×[Y] Y' ⟶ Y'`
along any morphism `Y' ⟶ Y` is (topologically) a closed map.
 -/
AlgebraicGeometry.UniversallyClosed : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter! m₂).get! k = m₁.get! k
-- Init.Data.Vector.Zip
Vector.map_prod_right_eq_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β},
  Vector.map (fun x => (f x, x)) xs = (Vector.map f xs).zip xs
-- Init.Data.UInt.Bitwise
UInt32.toUSize_and : ∀ (a b : UInt32), (a &&& b).toUSize = a.toUSize &&& b.toUSize
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- A variant of `finsuppTensorFinsupp` where both modules are the ground ring.  -/
finsuppTensorFinsupp' : (R : Type u_1) →
  (ι : Type u_5) → (κ : Type u_6) → [inst : CommSemiring R] → TensorProduct R (ι →₀ R) (κ →₀ R) ≃ₗ[R] ι × κ →₀ R
-- Mathlib.Algebra.Group.AddChar
AddChar.neg_apply : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : CommMonoid M] (ψ : AddChar A M) (a : A),
  (-ψ) a = ψ (-a)
-- Mathlib.Order.Filter.Extr
IsMinFilter.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → ∀ {g : β → γ}, Antitone g → IsMaxFilter (g ∘ f) l a
-- Mathlib.NumberTheory.WellApproximable
_private.Mathlib.NumberTheory.WellApproximable.0.AddCircle.term𝕊 : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.keyAtIdx!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {i : ℕ}, t₁.Equiv t₂ → t₁.keyAtIdx! i = t₂.keyAtIdx! i
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.Int.castDef.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.zoom.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → RBTree.RBNode.Path α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : RBTree.RBNode.Path α) →
        ((path : RBTree.RBNode.Path α) → motive RBTree.RBNode.nil path) →
          ((c : RBTree.RBColor) →
              (a : RBTree.RBNode α) →
                (y : α) →
                  (b : RBTree.RBNode α) → (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a y b) path) →
            motive x x_1
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Computes all semantic tokens for the document.  -/
Lean.Server.FileWorker.handleSemanticTokensFull : Lean.Lsp.SemanticTokensParams →
  Lean.Server.FileWorker.SemanticTokensState →
    Lean.Server.RequestM (Lean.Server.LspResponse Lean.Lsp.SemanticTokens × Lean.Server.FileWorker.SemanticTokensState)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E}, (∀ (i : ι), AnalyticOn 𝕜 (f i) s) → AnalyticOn 𝕜 (fun x x_1 => f x_1 x) s
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β), f.toFun = ⇑f
-- Mathlib.Util.Export
Lean.Export.Entry.defn.injEq : ∀ (n n_1 : Lean.Name), (Lean.Export.Entry.defn n = Lean.Export.Entry.defn n_1) = (n = n_1)
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_le_replicate : ∀ {α : Type u_1} (a : α) {k n : ℕ}, Multiset.replicate k a ≤ Multiset.replicate n a ↔ k ≤ n
-- Mathlib.Algebra.Lie.Abelian
/-- The kernel of the action of a Lie algebra `L` on a Lie module `M` as a Lie ideal in `L`.  -/
LieModule.ker : (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 R L M] → LieIdeal R L
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trContStack.eq_1 : ∀ (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.trContStack k = Turing.PartrecToTM2.trLList (Turing.PartrecToTM2.contStack k)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        (∀ a ∈ t, l.contains a = false) → (t.insertMany l).size = t.size + l.length
-- Lean.Elab.Do.Control
Lean.Elab.Do.EffectForwarder.mk.sizeOf_spec : ∀ (origCont : Lean.Elab.Do.DoElemCont) (returnBase? breakBase? continueBase? : Option Lean.Elab.Do.ControlStack)
  (liftedStack : Lean.Elab.Do.ControlStack) (liftedDoBlockResultType : Lean.Expr),
  sizeOf
      { origCont := origCont, returnBase? := returnBase?, breakBase? := breakBase?, continueBase? := continueBase?,
        liftedStack := liftedStack, liftedDoBlockResultType := liftedDoBlockResultType } =
    1 + sizeOf origCont + sizeOf returnBase? + sizeOf breakBase? + sizeOf continueBase? + sizeOf liftedStack +
      sizeOf liftedDoBlockResultType
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.RingObjCat C} (hom hom_1 : R₁.X ⟶ R₂.X)
  (e_hom : hom = hom_1) [isRingHom : CategoryTheory.IsRingHom hom],
  { hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Abelian
/-- In the category of modules, every monomorphism is normal.  -/
ModuleCat.normalMono : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (f : M ⟶ N) → CategoryTheory.Mono f → CategoryTheory.NormalMono f
-- Init.Guard
/-- Tactic to check that a named hypothesis has a given type and/or value.

* `guard_hyp h : t` checks the type up to reducible defeq,
* `guard_hyp h :~ t` checks the type up to default defeq,
* `guard_hyp h :ₛ t` checks the type up to syntactic equality,
* `guard_hyp h :ₐ t` checks the type up to alpha equality.
* `guard_hyp h := v` checks value up to reducible defeq,
* `guard_hyp h :=~ v` checks value up to default defeq,
* `guard_hyp h :=ₛ v` checks value up to syntactic equality,
* `guard_hyp h :=ₐ v` checks the value up to alpha equality.

The value `v` is elaborated using the type of `h` as the expected type.
 -/
Lean.Parser.Tactic.guardHyp : Lean.ParserDescr
-- Mathlib.Data.List.Lookmap
List.lookmap.go.eq_2 : ∀ {α : Type u_1} (f : α → Option α) (a : Array α) (x_2 : α) (xs : List α),
  List.lookmap.go f (x_2 :: xs) a =
    match f x_2 with
    | some b => a.toListAppend (b :: xs)
    | none => List.lookmap.go f xs (a.push x_2)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_mul_closure_one : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : Group G]
  [IsTopologicalGroup G] (s : Set G) (μ : MeasureTheory.Measure G), μ (s * closure {1}) = μ s
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.of_measurable_inverse : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β} {g : β → α},
  Measurable f → MeasurableSet (Set.range f) → Measurable g → Function.LeftInverse g f → MeasurableEmbedding f
-- Mathlib.Analysis.Convex.Slope
/-- A function `f : 𝕜 → 𝕜` is concave iff for any three points `x < y < z` the slope of the secant
line of `f` on `[x, y]` is greater than the slope of the secant line of `f` on `[y, z]`.  -/
concaveOn_iff_slope_anti_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) {Z : C}
  (h_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv h_1)
-- Mathlib.Data.Nat.Hyperoperation
_private.Mathlib.Data.Nat.Hyperoperation.0.hyperoperation.match_1.eq_3 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x k : ℕ) → motive 0 x k) (h_2 : (m : ℕ) → motive 1 m 0)
  (h_3 : (x : ℕ) → motive 2 x 0) (h_4 : (n x : ℕ) → motive n.succ.succ.succ x 0)
  (h_5 : (n m k : ℕ) → motive n.succ m k.succ),
  (match 2, x, 0 with
    | 0, x, k => h_1 x k
    | 1, m, 0 => h_2 m
    | 2, x, 0 => h_3 x
    | n.succ.succ.succ, x, 0 => h_4 n x
    | n.succ, m, k.succ => h_5 n m k) =
    h_3 x
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_cast : ∀ {w v : ℕ} (h : w = v) (x : BitVec w), (BitVec.cast h x).toNat = x.toNat
-- Std.Time.Format.Modifier
Std.Time.ZoneId.short.sizeOf_spec : sizeOf Std.Time.ZoneId.short = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.inter m₂).get? k = none
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Month.Ordinal
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go : {α : Type u} → {β : Type v} → [Ord α] → α → Option (α × β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.add.eq_1 : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M), S.add = { add := fun a b => ⟨↑a + ↑b, ⋯⟩ }
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
/-- The underlying type of the bundled type  -/
CategoryTheory.Bundled.α : {c : Type u → Type v} → CategoryTheory.Bundled c → Type u
-- Mathlib.GroupTheory.Transfer
AddSubgroup.leftTransversals.diff_add_diff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  (R S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  AddSubgroup.leftTransversals.diff ϕ R S + AddSubgroup.leftTransversals.diff ϕ S T =
    AddSubgroup.leftTransversals.diff ϕ R T
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_toUInt32 : ∀ (n : UInt64), n.toUInt32.toUInt8 = n.toUInt8
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eq_get_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {he : l.isEmpty = false},
  Std.Internal.List.maxKey l he = (Std.Internal.List.maxKey? l).get ⋯
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.uncurry.match_3.splitter : {α : Type u_1} →
  (motive : (σs : List (Type u_1)) → Std.Do.SVal σs α → Sort u_2) →
    (σs : List (Type u_1)) →
      (f : Std.Do.SVal σs α) →
        ((f : Std.Do.SVal [] α) → motive [] f) →
          ((head : Type u_1) →
              (tail : List (Type u_1)) → (f : Std.Do.SVal (head :: tail) α) → motive (head :: tail) f) →
            motive σs f
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instIsOpenImmersionToImageOfQuasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsImmersion f] [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.Hom.toImage f)
-- Init.Prelude
instTransEq : {α : Sort u_1} → {γ : Sort u_2} → (r : α → γ → Sort u) → Trans Eq r r
-- Mathlib.Data.Set.Function
Set.InjOn.invFunOn_image : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β} [inst : Nonempty α],
  Set.InjOn f s₂ → s₁ ⊆ s₂ → Function.invFunOn f s₂ '' f '' s₁ = s₁
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.end_mem_verts_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), v ∈ p.toSubgraph.verts
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.objAsTypeToAsType_map : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  {x x_1 : CategoryTheory.FinCategory.ObjAsType α} (a : x ⟶ x_1),
  (CategoryTheory.FinCategory.objAsTypeToAsType α).map a = (Fintype.equivFin (x ⟶ x_1)) a
-- Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Finset.sum_eq_sum_range_intervalGapsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommGroup β] (F : Finset (α × α)) {k : ℕ}
  (h : F.card = k) {a b : α} (f : α → α → β),
  ∑ z ∈ F, f z.1 z.2 = ∑ i ∈ Finset.range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1
-- Mathlib.Algebra.BigOperators.Group.Finset.Pi
/-- Taking a sum over `univ.pi t` is the same as taking the sum over
`Fintype.piFinset t`. `univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`,
but differ in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
`Fintype.piFinset t` is a `Finset (Π a, t a)`.  -/
Finset.sum_univ_pi : ∀ {ι : Type u_1} {β : Type u_2} [inst : AddCommMonoid β] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {κ : ι → Type u_3} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β),
  ∑ x ∈ Finset.univ.pi t, f x = ∑ x ∈ Fintype.piFinset t, f fun a x_1 => x a
-- Mathlib.Data.Set.Inclusion
Set.inclusion_injective : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t), Function.Injective (Set.inclusion h)
-- Init.Data.BitVec.Basic
/-- Shifts a bitvector to the left. The low bits are filled with zeros. As a numeric operation, this is
equivalent to `x * 2^s`, modulo `2^n`.

SMT-LIB name: `bvshl` except this operator uses a `Nat` shift value.
 -/
BitVec.shiftLeft : {n : ℕ} → BitVec n → ℕ → BitVec n
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.mul_vlt_mul_right`.

---

**Alias** of the reverse direction of `ValuativeRel.mul_vlt_mul_iff_right`. -/
ValuativeRel.vlt_mul_left : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ x → y <ᵥ z → x * y <ᵥ x * z
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.mk : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position → Option ℕ → Option Lean.Lsp.CompletionIdentifier → Lean.Lsp.ResolvableCompletionItemData
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrLemma.mk.injEq : ∀ (keys : List Mathlib.Tactic.GCongr.GCongrKey) (declName : Lean.Name)
  (mainSubgoals : Array Mathlib.Tactic.GCongr.GCongrHyp) (numHyps prio numVarying : ℕ) (forGrw : Bool)
  (keys_1 : List Mathlib.Tactic.GCongr.GCongrKey) (declName_1 : Lean.Name)
  (mainSubgoals_1 : Array Mathlib.Tactic.GCongr.GCongrHyp) (numHyps_1 prio_1 numVarying_1 : ℕ) (forGrw_1 : Bool),
  ({ keys := keys, declName := declName, mainSubgoals := mainSubgoals, numHyps := numHyps, prio := prio,
        numVarying := numVarying, forGrw := forGrw } =
      { keys := keys_1, declName := declName_1, mainSubgoals := mainSubgoals_1, numHyps := numHyps_1, prio := prio_1,
        numVarying := numVarying_1, forGrw := forGrw_1 }) =
    (keys = keys_1 ∧
      declName = declName_1 ∧
        mainSubgoals = mainSubgoals_1 ∧
          numHyps = numHyps_1 ∧ prio = prio_1 ∧ numVarying = numVarying_1 ∧ forGrw = forGrw_1)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pell_eq : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xn a1 n * Pell.xn a1 n - Pell.d✝ a1 * Pell.yn a1 n * Pell.yn a1 n = 1
-- Mathlib.Topology.Order.MonotoneConvergence
isGLB_of_tendsto_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsCodirectedOrder β] [Nonempty β] {f : β → α} {a : α},
  Monotone f → Filter.Tendsto f Filter.atBot (nhds a) → IsGLB (Set.range f) a
-- Mathlib.Tactic.Have
Mathlib.Tactic.haveIdLhs'.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_int16ToBitVec : ∀ (x : Int16), Int32.ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.instSMulH1CotangentOfIsScalarTowerCotangent : {R : Type u_3} →
  {S : Type u_4} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R₀ : Type u_1} →
              [inst_3 : CommRing R₀] →
                [inst_4 : Algebra R₀ S] →
                  [inst_5 : Module R₀ P.Cotangent] → [IsScalarTower R₀ S P.Cotangent] → SMul R₀ P.H1Cotangent
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.erase k ≠ ∅ → ∀ {fallback : α}, (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true