mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Sigma
Finset.sigmaLift_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  {f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b) →
    ∀ (a : (i : ι) × α i) (b : (i : ι) × β i), Finset.sigmaLift f a b ⊆ Finset.sigmaLift g a b
-- Mathlib.RingTheory.Polynomial.Tower
Polynomial.aeval_algebraMap_apply : ∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] (x : A) (p : Polynomial R),
  (Polynomial.aeval ((algebraMap A B) x)) p = (algebraMap A B) ((Polynomial.aeval x) p)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Truncated.instMonoidalTruncation : (n : ℕ) → (SSet.truncation n).Monoidal
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) (Z : CategoryTheory.Over X),
  (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).obj Z =
    CategoryTheory.Over.mk (CategoryTheory.MonoidalCategoryStruct.whiskerRight Z.hom Y)
-- Mathlib.Tactic.SplitIfs
/-- Collects a list of positions pointed to by `loc` and their types.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.getSplitCandidates : Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM (List (Mathlib.Tactic.SplitPosition✝ × Lean.Expr))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The diagram on the walking pair, sending the two points to `X` and `Y`.  -/
CategoryTheory.Limits.pair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    C → C → CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G} [inst_1 : DecidableEq G],
  IsOfFinAddOrder x →
    (y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x)))
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.ColimitCocone.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (cocone : CategoryTheory.Limits.Cocone F) →
            CategoryTheory.Limits.IsColimit cocone → CategoryTheory.Limits.ColimitCocone F
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk.inj : ∀ {R : Type u} {inst : NonUnitalNonAssocRing R} {toNonUnitalSubsemiring : NonUnitalSubsemiring R}
  {neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier}
  {toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R}
  {neg_mem'_1 : ∀ {x : R}, x ∈ toNonUnitalSubsemiring_1.carrier → -x ∈ toNonUnitalSubsemiring_1.carrier},
  { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := neg_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := neg_mem'_1 } →
    toNonUnitalSubsemiring = toNonUnitalSubsemiring_1
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_int64ToBitVec : ∀ (x : Int64), Int16.ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCastD k (Std.Internal.List.eraseKey k l) fallback = fallback
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.id_lift_eqToHom_domain : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} (hRS : R = S) {a : 𝒳},
  p.obj a = R → p.IsHomLift (CategoryTheory.eqToHom hRS) (CategoryTheory.CategoryStruct.id a)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A morphism is a generator if it is either a face or a degeneracy.  -/
SimplexCategoryGenRel.generators : CategoryTheory.MorphismProperty SimplexCategoryGenRel
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedRequest : {a : Type u_1} → [Inhabited a] → Inhabited (Lean.JsonRpc.Request a)
-- Mathlib.Data.Fin.Fin2
Fin2.equivFin_symm_apply : ∀ (n : ℕ) (i : Fin n), (Fin2.equivFin n).symm i = Fin2.ofFin i
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_toArray_rco : ∀ {a b : ℕ}, (a...b).toArray.size = b - a
-- Mathlib.Algebra.Category.Ring.Basic
CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom : ∀ {R S : CommRingCat} (e : R ≅ S), ↑e.commRingCatIsoToRingEquiv = CommRingCat.Hom.hom e.hom
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The natural inclusion of the `n`-cocycles `Zⁿ(G, A)` into the `n`-cochains `Cⁿ(G, A).`  -/
groupCohomology.iCocycles : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (n : ℕ) → groupCohomology.cocycles A n ⟶ (groupCohomology.inhomogeneousCochains A).X n
-- Mathlib.Data.Seq.Computation
/-- bind over a `Sum` of `Computation`  -/
Computation.Bind.g : {α : Type u} → {β : Type v} → β ⊕ Computation β → β ⊕ Computation α ⊕ Computation β
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.DTreeMap.entryAtIdxD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ℕ → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Star.Basic
StarRing.mk : {R : Type u} →
  [inst : NonUnitalNonAssocSemiring R] →
    [toStarMul : StarMul R] → (∀ (r s : R), star (r + s) = star r + star s) → StarRing R
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_pow : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) {n : ℕ},
  0 < n → X.basicOpen (f ^ n) = X.basicOpen f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union! m₂).getKey! k = m₂.getKey! k
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_rotateL : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rs : ℕ) (rk : α) (rv : β rk)
  (rl rr : Std.DTreeMap.Internal.Impl α β),
  l.Balanced →
    (Std.DTreeMap.Internal.Impl.inner rs rk rv rl rr).Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size rs ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond rs l.size →
        rs > Std.DTreeMap.Internal.delta * l.size → (Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr).Balanced
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.inv.match_1.eq_2 : ∀ {ι : Type u_1} {G : ι → Type u_2} [inst : (i : ι) → Group (G i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord G x x_1 → Sort u_3) (x x_1 j k : ι) (w₁ : Monoid.CoprodI.NeWord G x j)
  (h : j ≠ k) (w₂ : Monoid.CoprodI.NeWord G k x_1)
  (h_1 : (x : ι) → (x_2 : G x) → (h : x_2 ≠ 1) → motive x x (Monoid.CoprodI.NeWord.singleton x_2 h))
  (h_2 :
    (x x_2 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord G x j) →
        (h : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord G k x_2) → motive x x_2 (w₁.append h w₂)),
  (match x, x_1, w₁.append h w₂ with
    | x, .(x), Monoid.CoprodI.NeWord.singleton x_2 h => h_1 x x_2 h
    | x, x_2, w₁.append h w₂ => h_2 x x_2 j k w₁ h w₂) =
    h_2 x x_1 j k w₁ h w₂
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- The equalizer morphism `equalizerι` gives a split equalizer on `f,g`.  -/
CategoryTheory.HasSplitEqualizer.isSplitEqualizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.HasSplitEqualizer f g] →
          CategoryTheory.IsSplitEqualizer f g (CategoryTheory.HasSplitEqualizer.equalizerι f g)
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_lcm_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), a ∣ lcm a b
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars.orderIso_apply : ∀ {L : Type u_2} [inst : Field L] (F : Subfield L) (E : { E // F ≤ E }),
  (Subfield.extendScalars.orderIso F) E = Subfield.extendScalars ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instFaithfulGrpFunctorOppositeGrpCatYonedaGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaGrp.Faithful
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a `MulOneClass` under pointwise operations if `α` is.  -/
Set.mulOneClass : {α : Type u_2} → [MulOneClass α] → MulOneClass (Set α)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.run : {α : Type} → Lean.Meta.Simp.Arith.Nat.ToLinear.M α → Lean.MetaM (α × Array Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X},
  R = S ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f
-- Std.Async.Basic
Std.Async.Async.instMonadAsyncAsyncTask : Std.Async.MonadAsync Std.Async.AsyncTask Std.Async.Async
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_eq_size_beq_zero : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp}, t.isEmpty = (t.size == 0)
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `CommGroupWithZero` along an injective function.
See note [reducible non-instances].  -/
Function.Injective.commGroupWithZero : {G₀ : Type u_2} →
  {G₀' : Type u_4} →
    [inst : CommGroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    (f : G₀' → G₀) →
                      Function.Injective f →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : G₀'), f (x * y) = f x * f y) →
                              (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) →
                                (∀ (x y : G₀'), f (x / y) = f x / f y) →
                                  (∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) →
                                    (∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) → CommGroupWithZero G₀'
-- Mathlib.Data.Nat.Nth
/-- When `s` is an infinite set, `nth` agrees with `Nat.Subtype.orderIsoOfNat`.  -/
Nat.nth_eq_orderIsoOfNat : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Infinite), Nat.nth p = Subtype.val ∘ ⇑(Nat.Subtype.orderIsoOfNat (Set.ofPred p))
-- Lean.Meta.Tactic.Grind.Cases
_private.Lean.Meta.Tactic.Grind.Cases.0.Lean.Meta.Grind.cases.throwInductiveExpected : Lean.MVarId → Lean.Expr → {α : Type} → Lean.Expr → Lean.MetaM α
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_piEquivPiSubtypeProd : ∀ {δ : Type u_4} (X : δ → Type u_6) [inst : (a : δ) → MeasurableSpace (X a)] (p : δ → Prop) [inst_1 : DecidablePred p],
  Measurable ⇑(Equiv.piEquivPiSubtypeProd p X)
-- Init.Data.Bool
Bool.and_eq_false_imp : ∀ {x y : Bool}, (x && y) = false ↔ x = true → y = false
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.pointReflection_involutive : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (x : P₁), Function.Involutive ⇑(ContinuousAffineEquiv.pointReflection k x)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.BilinMap.isSymm_iff_eq_flip : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_20}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {B : LinearMap.BilinMap R M N},
  (∀ (x y : M), (B x) y = (B y) x) ↔ B = LinearMap.flip B
-- Mathlib.Data.Finset.Lattice.Pi
Finset.inf_sup : ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : BoundedOrder α] [inst_2 : DecidableEq ι]
  {κ : ι → Type u_3} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α),
  (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
-- Mathlib.Algebra.Lie.OfAssociative
LieSubmodule.coe_map_toEnd_le : ∀ {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]
  {N : LieSubmodule R L M} {x : L}, Submodule.map ((LieModule.toEnd R L M) x) ↑N ≤ ↑N
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hom_ofHom : ∀ {X Y : Type u} [inst : BooleanAlgebra X] [inst_1 : BooleanAlgebra Y] (f : BoundedLatticeHom X Y),
  BoolAlg.Hom.hom (BoolAlg.ofHom f) = f
-- Lean.Message
/-- Puts `MessageData` into a comma-separated list with `"and"` at the back (with the serial comma).

Best used on non-empty lists; returns `"– none –"` for an empty list.
 -/
Lean.MessageData.andList : List Lean.MessageData → Lean.MessageData
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁_hom_comp_i_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH1 A).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 1)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).hom h)
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- A magma is called a `PreValuationRing` provided that for any pair
of elements `a b : A`, either `a` divides `b` or vice versa.  -/
PreValuationRing : (A : Type u) → [Mul A] → Prop
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- A *subshift* on an alphabet `A` over a multiplicative monoid `G` is a closed,
shift-invariant subset of `G → A`, where the shift is given by left-multiplication.
Formally, it is composed of:
* `carrier`: the underlying set of allowed configurations.
* `isClosed`: the set is topologically closed in `A^G`.
* `mapsTo`: the set is invariant under all left-translation shifts
  `(mulShift g)`.  -/
SymbolicDynamics.FullShift.MulSubshift : (A : Type u_1) → [TopologicalSpace A] → (G : Type u_2) → [Monoid G] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.Final
/-- Initial functors preserve cofilteredness.

This can be seen as a generalization of `IsCofiltered.of_left_adjoint` (which states that left
adjoints preserve cofilteredness), as right adjoints are always initial,
see `initial_of_adjunction`.
 -/
CategoryTheory.IsCofilteredOrEmpty.of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] [CategoryTheory.IsCofilteredOrEmpty C],
  CategoryTheory.IsCofilteredOrEmpty D
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l → Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.insertMany m l) k' = v
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_setOfPred_le_im : ∀ (a : ℝ), interior {z | a ≤ z.im} = {z | a < z.im}
-- Mathlib.Tactic.Positivity.Core
/-- Run each registered `positivity` extension on an expression, returning a `NormNum.Result`.  -/
Mathlib.Meta.Positivity.core : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα? : Option Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap 0 = 0
-- Mathlib.Algebra.BigOperators.Expect
Finset.expectWith_congr : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s t : Finset ι} {f g : ι → M}
  {p q : ι → Prop} [inst_2 : DecidablePred p] [inst_3 : DecidablePred q],
  s = t →
    (∀ i ∈ t, p i ↔ q i) →
      (∀ i ∈ t, q i → f i = g i) → ({i ∈ s | p i}.expect fun i => f i) = {i ∈ t | q i}.expect fun i => g i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_toReal : ∀ (θ : Real.Angle), Real.sin θ.toReal = θ.sin
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff_extract : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat.isEmpty = false →
    (String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔
      s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The embedding of an `n`-independent set of an induced subgraph of the subgraph `G` is an
`n`-independent set in `G` and vice versa.  -/
SimpleGraph.isNIndepSet_induce : ∀ {α : Type u_1} (G : SimpleGraph α) {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ},
  (⊤.induce F).coe.IsNIndepSet n s ↔ G.IsNIndepSet n (Finset.map { toFun := Subtype.val, inj' := ⋯ } s)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportData.mk.inj : ∀ {errors errors_1 : IO.Ref (Array Lean.Meta.LazyDiscrTree.ImportFailure)},
  { errors := errors } = { errors := errors_1 } → errors = errors_1
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Circle integrability depends only on the restriction of the function to the sphere.
 -/
circleIntegrable_congr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E},
  Set.EqOn f₁ f₂ (Metric.sphere c |R|) → (CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R)
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- If an integral domain is Noetherian, and the localization at every nonzero prime is
a discrete valuation ring, then it is a Dedekind domain.  -/
IsDedekindDomainDvr.isDedekindDomain : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [IsDedekindDomainDvr A], IsDedekindDomain A
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The metric space structure on `L` induced by the spectral norm.  -/
spectralNorm.metricSpace : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → MetricSpace L
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.id_toFun : ∀ {R : Type u_3} [inst : Zero R] [inst_1 : TopologicalSpace R] (s : Set R) [inst_2 : Fact (0 ∈ s)] (a : ↑s),
  (ContinuousMapZero.id s) a = ↑a
-- Mathlib.Analysis.Analytic.Constructions
FormalMultilinearSeries.le_radius_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)] {r : ENNReal}
  {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  (∀ (i : ι), r ≤ (p i).radius) → r ≤ (FormalMultilinearSeries.pi p).radius
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.fiber_subset_ofLE : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) (a : Quotient A.toSetoid),
  A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {DiscreteQuotient.ofLE h a}
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.headD.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) (a : α) (x : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.headD le a x =
    match x with
    | Batteries.BinomialHeap.Imp.Heap.nil => a
    | Batteries.BinomialHeap.Imp.Heap.cons rank b node hs =>
      Batteries.BinomialHeap.Imp.Heap.headD le (if le a b = true then a else b) hs
-- Mathlib.FieldTheory.SeparableClosure
Field.insepDegree_top_le_insepDegree_of_isScalarTower : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K], Field.insepDegree E K ≤ Field.insepDegree F K
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} (n : ℕ),
  ¬MeasureTheory.VectorMeasure.restrict s
          (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k) ≤
        MeasureTheory.VectorMeasure.restrict 0
          (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k) →
    1 /
        (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s
              (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k)) +
          1) <
      s (MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n.succ)
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.lift_unique : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β] (f : WithOne α →* β),
  f = WithOne.lift ((↑f).comp WithOne.coeMulHom)
-- Mathlib.Order.Filter.IsBounded
/-- A bounded below function `u` is in particular eventually bounded below.  -/
BddBelow.isBoundedUnder_of_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α},
  BddBelow (Set.range u) → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.self_subset_toPlots_generateFrom : ∀ {X : Type u_1} (g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))), g ⊆ (DiffeologicalSpace.generateFrom g).toPlots
-- Mathlib.Data.Bool.Basic
Bool.true_eq_false_eq_False : ¬true = false
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.PreservesFiniteLimitsOfFlat.lift.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type v₁} [inst_2 : CategoryTheory.SmallCategory J] [inst_3 : CategoryTheory.FinCategory J]
  {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.RepresentablyFlat F]
  {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (K.comp F)),
  CategoryTheory.PreservesFiniteLimitsOfFlat.lift F hc s =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.IsCofiltered.cone (s.toStructuredArrow.comp (CategoryTheory.StructuredArrow.pre s.pt K F))).pt.hom
      (F.map
        (hc.lift
          ((CategoryTheory.Limits.Cone.postcompose
                {
                  app := fun x =>
                    CategoryTheory.CategoryStruct.id
                      (((s.toStructuredArrow.comp (CategoryTheory.StructuredArrow.pre s.pt K F)).comp
                            (CategoryTheory.StructuredArrow.proj s.pt F)).obj
                        x),
                  naturality := ⋯ }).obj
            ((CategoryTheory.StructuredArrow.proj s.pt F).mapCone
              (CategoryTheory.IsCofiltered.cone
                (s.toStructuredArrow.comp (CategoryTheory.StructuredArrow.pre s.pt K F)))))))