mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_predAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (x : Fin (n + 2)),
  SimplexCategory.II.map' { toFun := i.predAbove, monotone' := ⋯ } x = i.succ.castSucc.succAbove x
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Sleep.ofNative.sizeOf_spec : ∀ (native : Std.Internal.UV.Timer), sizeOf { native := native } = 1 + sizeOf native
-- Init.Data.Int.Bitwise.Basic
/-- Bitwise not, usually accessed via the `~~~` prefix operator.

Interprets the integer as an infinite sequence of bits in two's complement and complements each bit.

Examples:
* `~~~(0 : Int) = -1`
* `~~~(1 : Int) = -2`
* `~~~(-1 : Int) = 0`
 -/
Int.not : ℤ → ℤ
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.le_comap_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G),
  H ≤ AddSubgroup.comap f (AddSubgroup.map f H)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Note: This function assumes that the provided `clauses` Array is indexed according to the `clauses`
field invariant described in the DefaultFormula doc comment.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray : {n : ℕ} →
  Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instInhabitedHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (A B : HomologicalComplex V c) → Inhabited (A.Hom B)
-- Init.System.IOError
IO.Error.otherErrorToString : String → UInt32 → Option String → String
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- Comparison test of convergence of `ℝ≥0`-valued series.  -/
NNReal.summable_of_le : ∀ {β : Type u_2} {f g : β → NNReal}, (∀ (b : β), g b ≤ f b) → Summable f → Summable g
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult.mk.injEq : ∀ (res? : Except Lean.Exception Dynamic) (snap? : Option Lean.Language.SnapshotTree)
  (res?_1 : Except Lean.Exception Dynamic) (snap?_1 : Option Lean.Language.SnapshotTree),
  ({ res? := res?, snap? := snap? } = { res? := res?_1, snap? := snap?_1 }) = (res? = res?_1 ∧ snap? = snap?_1)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_inv_comp_tensorHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  (f : X ⟶ Y) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y g) h))
-- Mathlib.SetTheory.Cardinal.Regular
/-- If `c` is a regular cardinal, then `c.ord.ToType` has a least element.  -/
Cardinal.IsRegular.ne_zero : ∀ {c : Cardinal.{u_1}}, c.IsRegular → c ≠ 0
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ n` is integrable for all nonnegative `p : ℝ`.  -/
ProbabilityTheory.integrable_rpow_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => X ω ^ p) μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_two_nsmul : ∀ (θ : Real.Angle), (2 • θ).sin = 2 • (θ.sin * θ.cos)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If two functions differ only on a discrete set of an open, then they induce the same divisors.
 -/
MeromorphicOn.divisor_congr_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E},
  f₁ =ᶠ[Filter.codiscreteWithin U] f₂ → IsOpen U → MeromorphicOn.divisor f₁ U = MeromorphicOn.divisor f₂ U
-- Mathlib.Order.CompleteLattice.Basic
isGLB_biInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, IsGLB (f '' s) (⨅ x ∈ s, f x)
-- Mathlib.Computability.Encoding
/-- A unary encoding function of `ℕ` in `Bool`.  -/
Computability.unaryEncodeNat : ℕ → List Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : β k → β k}, m.WF → (k' ∈ m.modify k f ↔ k' ∈ m)
-- Mathlib.Topology.Separation.Basic
IsCompact.closure_of_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {s K : Set X}, IsCompact K → s ⊆ K → IsCompact (closure s)
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedAddGroup : {E : Type u_2} → [SeminormedAddGroup E] → SeminormedAddGroup Eᵒᵈ
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.zero.injEq : ∀ (sign sign_1 : Float.Model.UnpackedFloat.Sign),
  (Float.Model.UnpackedFloat.zero sign = Float.Model.UnpackedFloat.zero sign_1) = (sign = sign_1)
-- Aesop.Search.SearchM
Aesop.SearchM.Context : Type
-- Mathlib.Analysis.Convex.Piecewise
/-- The piecewise function `(Set.Ici e).piecewise f g` of a function `f` increasing and convex on
`Set.Ici e` and a function `g` decreasing and convex on `Set.Iic e`, such that `f e = g e`, is
convex on the universal set.  -/
convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] [inst_7 : AddCommGroup β]
  [inst_8 : PartialOrder β] [IsOrderedAddMonoid β] [inst_10 : Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β},
  ConvexOn 𝕜 (Set.Ici e) f →
    ConvexOn 𝕜 (Set.Iic e) g →
      MonotoneOn f (Set.Ici e) → AntitoneOn g (Set.Iic e) → f e = g e → ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise f g)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionSemiHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {φ : outParam (M → N)}
  {A : outParam (Type u_13)} {B : outParam (Type u_14)} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid A]
  [inst_3 : Monoid B] [inst_4 : MulDistribMulAction M A] [inst_5 : MulDistribMulAction N B] [inst_6 : FunLike F A B]
  [toMulActionSemiHomClass : MulActionSemiHomClass F φ A B] [toMonoidHomClass : MonoidHomClass F A B],
  MulDistribMulActionSemiHomClass F φ A B
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂},
  Std.DHashMap.Const.get (m₁.diff m₂) k h_mem = Std.DHashMap.Const.get m₁ k ⋯
-- Mathlib.Analysis.Analytic.Uniqueness
/-- If a formal multilinear series `p` represents the zero function at `x : E`, then the
terms `p n (fun i ↦ y)` appearing in the sum are zero for any `n : ℕ`, `y : E`.  -/
HasFPowerSeriesAt.apply_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt 0 p x → ∀ (n : ℕ) (y : E), ((p n) fun x => y) = 0
-- Mathlib.Computability.NFA
NFA.stepSet_union : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S T : Set σ} {a : α}, M.stepSet (S ∪ T) a = M.stepSet S a ∪ M.stepSet T a
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.fromOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)),
  f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_mul' := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g y` is invertible for all `y : S`, the homomorphism induced from
`N` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : M, y ∈ S`.  -/
Submonoid.LocalizationMap.lift_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M) (y : ↥S),
  (f.lift hg) (f.mk' x y) = g x * ↑((IsUnit.liftRight (g.domRestrict S) hg) y)⁻¹
-- Std.Data.DTreeMap.Raw.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.DTreeMap.Raw.Const.forInUncurried : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} →
      {m : Type w → Type w₂} →
        [Monad m] → {β : Type v} → (α × β → δ → m (ForInStep δ)) → δ → Std.DTreeMap.Raw α (fun x => β) cmp → m δ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for absolute value of `BitVec`s.  -/
BitVec.reduceAbs : Lean.Meta.Simp.DSimproc
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.natCastFn? : Lean.Meta.Sym.Arith.Semiring → Option Lean.Expr
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_continuousLinearMap_apply : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℝ F] {f : V → F →L[ℝ] E} {a : F} {v : V},
  MeasureTheory.Integrable f MeasureTheory.volume →
    (FourierTransform.fourier f v) a = FourierTransform.fourier (fun x => (f x) a) v
-- Lean.Elab.Tactic.Conv.Basic
/-- `⊢ lhs = rhs` ~~> `⊢ lhs' = rhs` using `h : lhs = lhs'`.  -/
Lean.Elab.Tactic.Conv.updateLhs : Lean.Expr → Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Data.List.Sym
List.sym_sublist_sym_cons : ∀ {α : Type u_1} {xs : List α} {n : ℕ} {a : α}, (List.sym n xs).Sublist (List.sym n (a :: xs))
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X))
      CategoryTheory.MonObj.mul
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.DTreeMap.Const.unitOfList l cmp).getKey? k' = some k
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrRight_symm_apply : ∀ {α : Sort u_1} {β₁ : α → Sort u_9} {β₂ : α → Sort u_10} (F : (a : α) → β₁ a ≃ β₂ a) (a : (i : α) → β₂ i) (i : α),
  (Equiv.piCongrRight F).symm a i = Pi.map (fun a => ⇑(F a).symm) a i
-- Mathlib.Logic.Relation
Relation.TransGen.to_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.TransGen r a b → Relation.ReflTransGen r a b
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderivWithin_smul` -/
mvfderivWithin_fun_smul : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {x : M} {a : M → 𝕜},
  MDiffAt[s] a x →
    ∀ {g : M → F},
      MDiffAt[s] g x → UniqueMDiffAt[s] x → (d[s] fun i => a i • g i) x = a x • d[s] g x + (d[s] a x).smulRight (g x)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_le_iff : ∀ {M : Type u_2} [inst : Mul M] {S₁ : Subsemigroup M} {S₂ : Subsemigroup Mᵐᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.mk.sizeOf_spec : ∀ (tempMark doneMark : Lean.FVarIdHashSet) (newDecls : Array Lean.LocalDecl) (newArgs : Array Lean.Expr),
  sizeOf { tempMark := tempMark, doneMark := doneMark, newDecls := newDecls, newArgs := newArgs } =
    1 + sizeOf tempMark + sizeOf doneMark + sizeOf newDecls + sizeOf newArgs
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.map_neg₂ : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommGroup E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F),
  (f (-x)) y = -(f x) y
-- Mathlib.Order.Hom.Lattice
SupHom.subtypeVal_coe : ∀ {β : Type u_3} [inst : SemilatticeSup β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)),
  ⇑(SupHom.subtypeVal Psup) = Subtype.val
-- Mathlib.Data.FunLike.Group
FunLike.mulOneClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : MulOneClass β] [inst_4 : IsOneApply F α β] [inst_5 : IsMulApply F α β],
  FunLike.mulOneClass = Function.Injective.mulOneClass (fun f => ⇑f) ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.instAddMonoidHomClassAddHom_2 : ∀ {M : Type u_10} {N : Type u_11} [inst : AddMonoid M] [inst_1 : AddCancelMonoid N], AddMonoidHomClass (M →ₙ+ N) M N
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_lt_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s : Finset ι} [MulLeftStrictMono M], (∀ i ∈ s, f i < 1) → s.Nonempty → ∏ i ∈ s, f i < 1
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.ofAlgEquiv_comp_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m),
  (↑(AdicCompletion.ofAlgEquiv I)).comp (IsAdicComplete.liftRingHom I f ⋯) = AdicCompletion.liftRingHom I f ⋯
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_1 : Std.Time.Weekday.monday.toOrdinal = 1
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- `gramSchmidtNormed` produces linearly independent vectors when given linearly independent
vectors.  -/
InnerProductSpace.gramSchmidtNormed_linearIndependent : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E},
  LinearIndependent 𝕜 f → LinearIndependent 𝕜 (InnerProductSpace.gramSchmidtNormed 𝕜 f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β k}, (cmp (t.insert k v).minKey! k).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_transpose_mul_diag : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : NonAssocSemiring R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {e : Sym2 α} [inst_3 : Fintype α] [inst_4 : Decidable (e ∈ G.edgeSet)],
  ((SimpleGraph.incMatrix R G).transpose * SimpleGraph.incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_toInfHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β),
  ⇑f.toInfHom = ⇑f
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.le_of_lt : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a < b → a' + b ≤ b' + a → a' ≤ b'
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).inv
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv Y) h
-- Batteries.Data.UInt
UInt32.ext_iff : ∀ {x y : UInt32}, x = y ↔ x.toNat = y.toNat
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.exists_of_mem_bind : ∀ {α : Type u} {β : Type v} {s : Stream'.WSeq α} {f : α → Stream'.WSeq β} {b : β}, b ∈ s.bind f → ∃ a ∈ s, b ∈ f a
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_sSup_of_directedOn : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.Util.Notation3
/-- Evaluate `f` with the given variable's value as the `SubExpr` and within that subexpression's
saved context. Fails if the variable has no value.  -/
Mathlib.Notation3.MatchState.withVar : {α : Type} →
  Mathlib.Notation3.MatchState →
    Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
iSupIndep_range_lsingle : ∀ (ι : Type u') (R : Type u_2) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  iSupIndep fun i => (Finsupp.lsingle i).range
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowRight_id : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom),
  sq₁₂.mapArrowRight sq₁₂ (CategoryTheory.CategoryStruct.id f₂) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk sq₁₂.ι)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.pi_ne_zero : ↑Real.pi ≠ 0
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_inter_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioo a b ∩ Set.Iio c = Set.Ioo a (min b c)
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.coe_toLinearMap : ∀ {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₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂), ⇑f.toLinearMap = ⇑f
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsDownInt_χ : ∀ (n : ℤ), ComplexShape.EulerCharSigns.χ (ComplexShape.down ℤ) n = n.negOnePow
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁),
  CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.iCycles f₁ f₂ n₁) = X.δ f₂ f₃ n₀ n₁ hn₁
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedSimpTheorem : Inhabited Lean.Meta.SimpTheorem
-- Mathlib.Order.Filter.CountableInter
instCountableInterFilterComap : ∀ {α : Type u_2} {β : Type u_3} (l : Filter β) [CountableInterFilter l] (f : α → β),
  CountableInterFilter (Filter.comap f l)
-- Mathlib.Topology.VectorBundle.Basic
/-- A fiberwise linear inverse to `e`.  -/
Bundle.Trivialization.symmₗ : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
                [inst_4 : AddCommMonoid F] →
                  [inst_5 : Module R F] →
                    [inst_6 : (x : B) → AddCommMonoid (E x)] →
                      [inst_7 : (x : B) → Module R (E x)] →
                        (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                          [Bundle.Trivialization.IsLinear R e] → (b : B) → F →ₗ[R] E b
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match Lean.Grind.Linarith.Expr.zero with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X}
  (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) {Z : C} (h : X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hc.lift d) (CategoryTheory.CategoryStruct.comp (c.proj i) h) =
    CategoryTheory.CategoryStruct.comp (d.proj i) h
-- Mathlib.Data.Set.BooleanAlgebra
Set.instCompleteAtomicBooleanAlgebra : {α : Type u_1} → CompleteAtomicBooleanAlgebra (Set α)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.instFintypeSymbolsRing : Fintype FirstOrder.Language.ring.Symbols
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_dblX : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblX (⇑f ∘ P) = f ((W'.baseChange A).dblX P)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.comp_init : ∀ {n : ℕ} {α : Sort u_2} {β : Sort u_3} (g : α → β) (q : Fin n.succ → α), g ∘ Fin.init q = Fin.init (g ∘ q)