mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.ofHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsMonHom f], CategoryTheory.Grp.ofHom f = CategoryTheory.Grp.homMk f
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.deriv_ne_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    (Polynomial.aeval a) (Polynomial.derivative F) ≠ 0
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_inj : ∀ {m n : ℕ∞}, ↑m = ↑n ↔ m = n
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_toReal : ∀ {a : ENNReal}, a ≠ ⊤ → Filter.Tendsto ENNReal.toReal (nhds a) (nhds a.toReal)
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryFinFinset_apply_const : ∀ {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [inst : CommSemiring R] [inst_1 : AddCommMonoid M']
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M'] [inst_4 : Module R M₂] {k l n : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') M₂) (x y : M'),
  ((((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)
-- Mathlib.Geometry.Manifold.Instances.Sphere
isOpenEmbedding_stereographic_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  Topology.IsOpenEmbedding ↑(stereographic hv).symm
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.InvariantCardinalRank.forall_card_isBasis_diff : ∀ {α : Type u} {M : Matroid α} [self : M.InvariantCardinalRank] ⦃I J X : Set α⦄,
  M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)
-- Mathlib.Data.Set.Pairwise.Lattice
Pairwise.biUnion_injective : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) → (∀ (i : ι), (f i).Nonempty) → Function.Injective fun s => ⋃ i ∈ s, f i
-- Lean.Data.SMap
Lean.SMap.insert' : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → α → β → Lean.SMap α β
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.none.sizeOf_spec : sizeOf Lean.Elab.Tactic.ElabSimpArgResult.none = 1
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.fac : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsHomLift f φ],
  f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (p.map φ) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.toInner : {𝕜 : Type u_4} →
  {E : Type u_5} → {inst : RCLike 𝕜} → {inst_1 : SeminormedAddCommGroup E} → [self : InnerProductSpace 𝕜 E] → Inner 𝕜 E
-- Init.Data.List.Nat.Range
List.count_range_1' : ∀ {a s n : ℕ}, List.count a (List.range' s n) = if s ≤ a ∧ a < s + n then 1 else 0
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.lift_obj_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {Y : D}
  (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X))
  (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom)
  (f : CategoryTheory.MonoOver Y),
  ((CategoryTheory.MonoOver.lift F h).obj f).arrow = (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_const : ∀ (X : Type u_1) {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (r : NNReal) (c : Y),
  eHolderNorm r (Function.const X c) = 0
-- Mathlib.Algebra.Group.Basic
mul_rotate : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c : G), a * b * c = b * c * a
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_of_lt_pred : ∀ {α : Type u_1} {b : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  (∀ (a : α), b < a → b < Order.pred a) → Order.IsPredPrelimit b
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.toPrefunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (a : C), F.toPrefunctor.obj a = F.obj a
-- Init.Data.Array.MinMax
Array.min?_toList : ∀ {α : Type u_1} [inst : Min α] {xs : Array α}, xs.toList.min? = xs.min?
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.posPart_add_negPart : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (IsSelfAdjoint a) CFC.posPart_add_negPart._auto_1 → a⁺ + a⁻ = CFC.abs a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_some_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.min? = some (t.minD fallback)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.deflate_inflate : ∀ {α : Type v} {x : Std.Internal.Small α} {x_1 : Std.Internal.USquash α}, Std.Internal.USquash.deflate x_1.inflate = x_1
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveTelescopeInfo.mk.injEq : ∀ (haveInfo : Array Lean.Meta.HaveInfo) (bodyDeps bodyTypeDeps : Std.HashSet ℕ) (body bodyType : Lean.Expr)
  (level : Lean.Level) (haveInfo_1 : Array Lean.Meta.HaveInfo) (bodyDeps_1 bodyTypeDeps_1 : Std.HashSet ℕ)
  (body_1 bodyType_1 : Lean.Expr) (level_1 : Lean.Level),
  ({ haveInfo := haveInfo, bodyDeps := bodyDeps, bodyTypeDeps := bodyTypeDeps, body := body, bodyType := bodyType,
        level := level } =
      { haveInfo := haveInfo_1, bodyDeps := bodyDeps_1, bodyTypeDeps := bodyTypeDeps_1, body := body_1,
        bodyType := bodyType_1, level := level_1 }) =
    (haveInfo = haveInfo_1 ∧
      bodyDeps = bodyDeps_1 ∧ bodyTypeDeps = bodyTypeDeps_1 ∧ body = body_1 ∧ bodyType = bodyType_1 ∧ level = level_1)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeInverse_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C),
  (e.changeInverse iso).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_C_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.Monic (MvPolynomial.C 1)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.snd : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : N → M × M'}, ContMDiff J (I.prod I') n f → ContMDiff J I' n fun x => (f x).2
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Shows the inferred termination measure to the user, and implements `termination_by?`
 -/
Lean.Elab.WF.GuessLex.reportTerminationMeasures : Array Lean.Elab.PreDefinition → Lean.Elab.TerminationMeasures → Lean.MetaM Unit
-- Init.Data.SInt.Lemmas
Int32.toInt_toInt16 : ∀ (x : Int32), x.toInt16.toInt = x.toInt.bmod (2 ^ 16)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_sliceFrom_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p ≤ p₀.sliceFrom q h ↔ String.Slice.Pos.ofSliceFrom p ≤ q
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (weight : Type v) [weightIsAddCommGroup : AddCommGroup weight]
  [weightIsModule : Module R weight] (coweight : Type v) [coweightIsAddCommGroup : AddCommGroup coweight]
  [coweightIsModule : Module R coweight] (index : Type v) (pairing : RootPairing index R weight coweight)
  (weight_1 : Type v) (weightIsAddCommGroup_1 : AddCommGroup weight_1) (weightIsModule_1 : Module R weight_1)
  (coweight_1 : Type v) (coweightIsAddCommGroup_1 : AddCommGroup coweight_1) (coweightIsModule_1 : Module R coweight_1)
  (index_1 : Type v) (pairing_1 : RootPairing index_1 R weight_1 coweight_1),
  ({ weight := weight, weightIsAddCommGroup := weightIsAddCommGroup, weightIsModule := weightIsModule,
        coweight := coweight, coweightIsAddCommGroup := coweightIsAddCommGroup, coweightIsModule := coweightIsModule,
        index := index, pairing := pairing } =
      { weight := weight_1, weightIsAddCommGroup := weightIsAddCommGroup_1, weightIsModule := weightIsModule_1,
        coweight := coweight_1, coweightIsAddCommGroup := coweightIsAddCommGroup_1,
        coweightIsModule := coweightIsModule_1, index := index_1, pairing := pairing_1 }) =
    (weight = weight_1 ∧
      weightIsAddCommGroup ≍ weightIsAddCommGroup_1 ∧
        weightIsModule ≍ weightIsModule_1 ∧
          coweight = coweight_1 ∧
            coweightIsAddCommGroup ≍ coweightIsAddCommGroup_1 ∧
              coweightIsModule ≍ coweightIsModule_1 ∧ index = index_1 ∧ pairing ≍ pairing_1)
-- Mathlib.GroupTheory.Exponent
AddMonoid.ExponentExists.of_finite : ∀ {G : Type u} [inst : AddLeftCancelMonoid G] [Finite G], AddMonoid.ExponentExists G
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
LowerSemicontinuousWithinAt.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f g : α → γ},
  LowerSemicontinuousWithinAt f s x →
    LowerSemicontinuousWithinAt g s x → LowerSemicontinuousWithinAt (fun z => f z + g z) s x
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.Context.mk.sizeOf_spec : ∀ (offset : ℕ), sizeOf { offset := offset } = 1 + sizeOf offset
-- Init.Data.Option.Attach
Option.toList_pbind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  (o.pbind f).toList =
    List.flatMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x h).toList)
      o.attach.toList
-- Mathlib.Topology.Constructible
IsRetrocompact.isConstructible : ∀ {X : Type u_2} [inst : TopologicalSpace X] {U : Set X}, IsOpen U → IsRetrocompact U → Topology.IsConstructible U
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from rings to semirings preserves all limits.
 -/
RingCat.forget₂SemiRing_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ RingCat SemiRingCat)
-- Mathlib.Order.Lattice
Prod.fst_inf : ∀ (α : Type u) (β : Type v) [inst : Min α] [inst_1 : Min β] (p q : α × β), (p ⊓ q).1 = p.1 ⊓ q.1
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), x.gcd y = 1 → 0 < z → h.IsPrimitiveClassified
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.instInhabitedState.default : Aesop.RuleTac.ForwardM.State
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R], HahnSeries.C 1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d),
  (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).inverse = I.ofSigmaCoforkFunctor hc
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaForget.eq_1 : CommMonCat.coyonedaForget =
  CategoryTheory.NatIso.ofComponents
    (fun X =>
      CategoryTheory.NatIso.ofComponents
        (fun Y =>
          { hom := TypeCat.ofHom fun f => CommMonCat.ofHom f, inv := TypeCat.ofHom fun f => CommMonCat.Hom.hom f,
            hom_inv_id := ⋯, inv_hom_id := ⋯ })
        ⋯)
    @CommMonCat.coyonedaForget._proof_4
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- Given a t-structure `t` on a pretriangulated category `C` and `n : ℤ`, this
is the `> n`-truncation functor. See also the natural transformation `truncGTπ`.  -/
CategoryTheory.Triangulated.TStructure.truncGT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → ℤ → CategoryTheory.Functor C C
-- Mathlib.Topology.Instances.ENNReal.Lemmas
tendsto_iff_edist_tendsto_0 : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] {l : Filter β} {f : β → α} {y : α},
  Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (fun x => edist (f x) y) l (nhds 0)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsIsHomotopyInvariant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι}, (TopPair.HomologyPretheory.isHomotopyInvariant C c).IsClosedUnderIsomorphisms
-- Mathlib.GroupTheory.CoprodI
/-- The last letter of a `NeWord`  -/
Monoid.CoprodI.NeWord.last : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i j : ι} → Monoid.CoprodI.NeWord M i j → M j
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instRightCancelSemigroupOfMulOpposite : {M : Type u_1} → [RightCancelSemigroup Mᵐᵒᵖ] → RightCancelSemigroup Mᵈᵐᵃ
-- Lean.Elab.App
/-- Cached from `NamedArg.numImplicitParams`. This is the prefix of parameters whose explicitness
should be overridden to become implicit.  -/
Lean.Elab.Term.ElabAppArgs.Context.numImplicitParams : Lean.Elab.Term.ElabAppArgs.Context → ℕ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
      (List.map Prod.fst l).contains k = false → (t.insertMany l)[k]! = t.get! k
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.hasProjectiveDimensionLT_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [inst_2 : CategoryTheory.HasExt C],
  CategoryTheory.HasProjectiveDimensionLT X n ↔
    ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : CategoryTheory.Abelian.Ext X Y i), e = 0
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_bot : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K]
  [inst_6 : IsFractionRing R K], FractionalIdeal.absNorm ⊥ = 0
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioo_sub_one_left_eq_Ioc_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a : α}, ¬IsMin a → ∀ (b : α), Finset.Ioo (a - 1) b = Finset.Ico a b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast aig { lhs := lhs, rhs := rhs } =
    Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs 0 ⋯ (aig.mkConstCached false)
      (Std.Sat.AIG.RefVec.emptyWithCapacity w)
-- Mathlib.Data.Sum.Order
/-- `Equiv.sumAssoc` promoted to an order isomorphism.  -/
OrderIso.sumLexAssoc : (α : Type u_10) →
  (β : Type u_11) → (γ : Type u_12) → [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → (α ⊕ₗ β) ⊕ₗ γ ≃o α ⊕ₗ β ⊕ₗ γ
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.left_id : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveTermGoal.mk.inj : ∀ {toInteractiveGoalCore : Lean.Widget.InteractiveGoalCore} {range : Lean.Lsp.Range}
  {term : Lean.Server.WithRpcRef Lean.Elab.TermInfo} {toInteractiveGoalCore_1 : Lean.Widget.InteractiveGoalCore}
  {range_1 : Lean.Lsp.Range} {term_1 : Lean.Server.WithRpcRef Lean.Elab.TermInfo},
  { toInteractiveGoalCore := toInteractiveGoalCore, range := range, term := term } =
      { toInteractiveGoalCore := toInteractiveGoalCore_1, range := range_1, term := term_1 } →
    toInteractiveGoalCore = toInteractiveGoalCore_1 ∧ range = range_1 ∧ term = term_1
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiff_of_contDiffOn_iUnion_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞}
  {ι : Type u_5} {s : ι → Set E},
  (∀ (i : ι), ContDiffOn 𝕜 n f (s i)) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → ContDiff 𝕜 n f
-- ProofWidgets.Cancellable
ProofWidgets.cancellableSuffix : Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.middle_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.actLeft B.X)
      self.actRight =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X self.X B.X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.actRight)
        self.actLeft)
-- Mathlib.LinearAlgebra.RootSystem.Basic
RootPairing.equiv_of_mapsTo_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M)
  (coroot : ι ↪ N) (i : ι)
  (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root))
  (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2) (j : ι), (RootPairing.equiv_of_mapsTo p root coroot i h hp) j = ⋯.choose
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F], F.rightDerivedZeroIsoSelf.inv = F.toRightDerivedZero
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of `-x` is the same as that of `x`.  -/
Height.logHeight₁_neg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.logHeight₁ (-x) = Height.logHeight₁ x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproduct.bicone_inr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inr = CategoryTheory.Limits.biprod.inr
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.surjective_pullbackFst_of_surjective : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T), Function.Surjective ⇑g → Function.Surjective ⇑(f.pullbackFst g)
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- The constant in the (upper) height bound on values of `p`.  -/
Height.mulHeightBound : {K : Type u_4} →
  [inst : Field K] → {ι : Type u_5} → {ι' : Type u_6} → [Height.AdmissibleAbsValues K] → (ι' → MvPolynomial ι K) → ℝ
-- Std.Data.HashMap.Lemmas
Std.HashMap.isSome_getElem?_eq_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m[a]?.isSome = m.contains a
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- `A.IsTotallyUnimodular` means that every square submatrix of `A` (not necessarily contiguous)
has determinant `0` or `1` or `-1`; that is, the determinant is in the range of `SignType.cast`.  -/
Matrix.IsTotallyUnimodular : {m : Type u_1} → {n : Type u_3} → {R : Type u_5} → [CommRing R] → Matrix m n R → Prop
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.comap_map_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  Submodule.comap p.mkQ (Submodule.map p.mkQ p') = p ⊔ p'
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instInhabitedUnitVal : {a : ℚ} → Inhabited (Std.Time.Internal.UnitVal a)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_smul : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ),
  (c • μ).transpose B = c • μ.transpose B
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.updateBucket.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (self self_1 : Array (Std.DHashMap.Internal.AssocList α β))
  (e_self : self = self_1) (h : 0 < self.size) (k k_1 : α),
  k = k_1 →
    ∀ (f f_1 : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β),
      f = f_1 → Std.DHashMap.Internal.updateBucket self h k f = Std.DHashMap.Internal.updateBucket self_1 ⋯ k_1 f_1
-- Mathlib.Order.Atoms
IsSimpleOrder.eq_top_of_lt : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a b : α}, a < b → b = ⊤
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSumLocallyUniformly_derivWeierstrassP : ∀ (L : PeriodPair), HasSumLocallyUniformly (fun l z => -2 / (z - ↑l) ^ 3) L.derivWeierstrassP
-- Lean.Elab.Match
Lean.Elab.Term.elabNoFun : Lean.Elab.Term.TermElab