mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.Field
Lean.Grind.Field.zpow_neg_one : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α), a ^ (-1) = a⁻¹
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.getElem?_toList_eq : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  r.toList[i]? = Option.filter (fun x => decide (x < r.upper)) (Std.PRange.succMany? (i + 1) r.lower)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isSymm_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.BilinForm.IsSymm 0
-- Mathlib.Topology.Separation.Basic
instR0SpaceSubtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {p : X → Prop}, R0Space { x // p x }
-- Init.Data.String.Iterate
String.Slice.ByteIterator.instIteratorUInt8OfPure : {m : Type → Type u_1} → [Pure m] → Std.Iterator String.Slice.ByteIterator m UInt8
-- Mathlib.Data.Seq.Basic
Stream'.Seq.all_coind_drop_motive : ∀ {α : Type u} {s : Stream'.Seq α} (motive : Stream'.Seq α → Prop),
  motive s →
    (∀ (hd : α) (tl : Stream'.Seq α), motive (Stream'.Seq.cons hd tl) → motive tl) → ∀ (n : ℕ), motive (s.drop n)
-- Mathlib.Topology.Constructions.SumProd
continuous_sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.zero_lt_orderTop_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R},
  x ≠ 0 → (0 < x.orderTop ↔ 0 < x.order)
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.IsNilpotent.mk_int : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M],
  (∃ k, LieModule.lowerCentralSeries ℤ L M k = ⊥) → LieModule.IsNilpotent L M
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.lipschitzWith_compLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g : E → F} {c : NNReal} [inst_2 : Fact (1 ≤ p)]
  (hg : LipschitzWith c g) (g0 : g 0 = 0), LipschitzWith c (hg.compLp g0)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectR : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel (α × β) γ}
  [∀ (b : α), ProbabilityTheory.IsMarkovKernel (κ.sectR b)], ProbabilityTheory.IsMarkovKernel κ
-- Mathlib.Algebra.Polynomial.Taylor
/-- The Taylor expansion of a polynomial `f` at `r`.  -/
Polynomial.taylor : {R : Type u_1} → [inst : Semiring R] → R → Polynomial R →ₗ[R] Polynomial R
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C)
  (f : (i : Y.I) × (X ⟶ Y.obj i)) (x : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I),
  ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y).symm f).φ x = f.snd
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.self_trans_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  h.trans h.symm = Diffeomorph.refl I M n
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instPartialOrder : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [PartialOrder β] → PartialOrder (MeasureTheory.SimpleFunc α β)
-- Mathlib.Algebra.Star.TransferInstance
/-- Transfer `StarAddMonoid` across an `Equiv`. See note [reducible non-instances].  -/
Equiv.starAddMonoid : {R : Type u_1} → {S : Type u_2} → (e : R ≃ S) → [inst : AddMonoid S] → [StarAddMonoid S] → StarAddMonoid R
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.iff_of_equiv : ∀ {R : Type u_2} {R' : Type u_3} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] {σ : R →+* R'}
  {σ' : R' →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e₂ : M ≃ₛₗ[σ] M'),
  Module.Free R M ↔ Module.Free R' M'
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_union : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s t : Set R),
  NonUnitalSubsemiring.closure (s ∪ t) = NonUnitalSubsemiring.closure s ⊔ NonUnitalSubsemiring.closure t
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0.injEq : ∀ (k : ℕ) (c₁ c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k_1 : ℕ)
  (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0 k c₁ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0 k_1 c₁_1 c₂_1) =
    (k = k_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.sin_sq_le_sq : ∀ {x : ℝ}, Real.sin x ^ 2 ≤ x ^ 2
-- Mathlib.CategoryTheory.Functor.OfSequence
/-- Constructor for natural transformations `F ⟶ G` in `ℕᵒᵖ ⥤ C` which takes as inputs
the morphisms `F.obj ⟨n⟩ ⟶ G.obj ⟨n⟩` for all `n : ℕ` and the naturality condition only
for morphisms of the form `n ⟶ n + 1`.  -/
CategoryTheory.NatTrans.ofOpSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.Functor ℕᵒᵖ C} →
      (app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n)) →
        (∀ (n : ℕ),
            CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯).op) (app n) =
              CategoryTheory.CategoryStruct.comp (app (n + 1)) (G.map (CategoryTheory.homOfLE ⋯).op)) →
          (F ⟶ G)
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hyp.injEq : ∀ (a a_1 : Lean.FVarId), (Lean.SubExpr.GoalLocation.hyp a = Lean.SubExpr.GoalLocation.hyp a_1) = (a = a_1)
-- Init.Meta.Defs
Lean.Option.hasQuote : {α : Type} → [Lean.Quote α] → Lean.Quote (Option α)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ext_iff : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] {f g : M₁ ≃SL[σ₁₂] M₂}, f = g ↔ ⇑f = ⇑g
-- Lean.Parser.Basic
Lean.Parser.symbol : String → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Elements
/-- The equivalence of categories `costructuredArrowULiftYonedaEquivalence`
commutes with the projections.  -/
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v))) →
      (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).functor.comp
          (CategoryTheory.CostructuredArrow.proj CategoryTheory.uliftYoneda.{w, v, u} F) ≅
        (CategoryTheory.CategoryOfElements.π F).leftOp
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurry_curryLeft : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G),
  f.curryLeft.uncurryLeft = f
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.generate_discretePresieve_mem : ∀ (α : Type u),
  CategoryTheory.Sieve.generate (CategoryTheory.discretePresieve α) ∈ CategoryTheory.typesGrothendieckTopology α
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.dist_lt_add_of_nonempty_ball_inter_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  (Metric.ball x ε₁ ∩ Metric.ball y ε₂).Nonempty → dist x y < ε₁ + ε₂
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.logTaylor_succ : ∀ (n : ℕ), Complex.logTaylor (n + 1) = Complex.logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt8 = OfNat.ofNat n
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
IsLocalHom.of_comap_surjective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Function.Surjective (PrimeSpectrum.comap f) → IsLocalHom f
-- Mathlib.Data.Fintype.Sum
Fintype.card_subtype_or_disjoint : ∀ {α : Type u_1} (p q : α → Prop),
  Disjoint p q →
    ∀ [inst : Fintype { x // p x }] [inst_1 : Fintype { x // q x }] [inst_2 : Fintype { x // p x ∨ q x }],
      Fintype.card { x // p x ∨ q x } = Fintype.card { x // p x } + Fintype.card { x // q x }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀)
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').hom.app X_1).snd.app x =
    CategoryTheory.CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X_1.snd.obj x)))
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_iff_finset : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ ↔ ∀ (s : Finset ι), ProbabilityTheory.iIndepFun (s.restrict f) μ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res.eq_1 : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X : C}
  {X₀ Y₀ : C₀} {f : F.obj X₀ ⟶ X} {g : Y₀ ⟶ X₀} (h : (data X).SieveStruct f g),
  CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res data G₀ h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X h.i₀)
      (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ h.q)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.terminatedAt_ofList : ∀ {α : Type u} (l : List α), (↑l).TerminatedAt l.length
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.mk : Lean.Grind.CommRing.Poly →
  Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof → Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr
-- Init.Data.String.TakeDrop
String.Slice.dropRightWhile : String.Slice → (Char → Bool) → String.Slice
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_trunc : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R),
  MvPolynomial.coeff m ((MvPowerSeries.trunc R n) φ) = if m < n then (MvPowerSeries.coeff m) φ else 0
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : ENNReal) (s : Set X),
  Metric.IsSeparated ε s = s.Pairwise fun x1 x2 => ε < edist x1 x2
-- Mathlib.Geometry.Manifold.VectorBundle.Pullback
/-- For a `C^n` vector bundle `E` over a manifold `B` and a `C^n` map `f : B' → B`, the pullback
vector bundle `f *ᵖ E` is a `C^n` vector bundle.  -/
ContMDiffVectorBundle.pullback : ∀ {𝕜 : Type u_1} {B : Type u_2} {B' : Type u_3} (F : Type u_4) (E : B → Type u_5) {n : WithTop ℕ∞}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module 𝕜 (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_6 : (x : B) → TopologicalSpace (E x)] {EB : Type u_6} [inst_7 : NormedAddCommGroup EB]
  [inst_8 : NormedSpace 𝕜 EB] {HB : Type u_7} [inst_9 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_10 : TopologicalSpace B] [inst_11 : ChartedSpace HB B] {EB' : Type u_8} [inst_12 : NormedAddCommGroup EB']
  [inst_13 : NormedSpace 𝕜 EB'] {HB' : Type u_9} [inst_14 : TopologicalSpace HB'] (IB' : ModelWithCorners 𝕜 EB' HB')
  [inst_15 : TopologicalSpace B'] [inst_16 : ChartedSpace HB' B'] [inst_17 : FiberBundle F E]
  [inst_18 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (f : ContMDiffMap IB' IB B' B n),
  ContMDiffVectorBundle n F (⇑f *ᵖ E) IB'
-- Mathlib.Util.FormatTable
Alignment.center : Alignment
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_div : ∀ {S : Type u_5} [inst : Semifield S] [inst_1 : LinearOrder S] {R : Type u_6} [inst_2 : DivisionSemiring R]
  (abv : R → S) [IsAbsoluteValue abv] (a b : R), abv (a / b) = abv a / abv b
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.lam : Mathlib.Meta.FunProp.LambdaTheorem → Mathlib.Meta.FunProp.Theorem
-- Mathlib.GroupTheory.Perm.List
List.formPerm_eq_head_iff_eq_getLast : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y : α), (y :: l).formPerm x = y ↔ x = (y :: l).getLast ⋯
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A predicate that holds for the return value(s) of the `m`-monadic operation.
 -/
Std.Iterators.HetT.Property : {m : Type w → Type w'} → {α : Type v} → Std.Iterators.HetT m α → α → Prop
-- Mathlib.Algebra.Category.Ring.Instances
isLocalHom_of_iso : ∀ {R S : CommRingCat} (f : R ≅ S), IsLocalHom (CommRingCat.Hom.hom f.hom)
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
LinearMap.liftQ₂.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7}
  [inst : Ring R] [inst_1 : Ring R₂] [inst_2 : Ring S] [inst_3 : Ring S₂] [inst_4 : AddCommGroup M]
  [inst_5 : AddCommGroup N] [inst_6 : AddCommGroup P] [inst_7 : Module R M] [inst_8 : Module S N] [inst_9 : Module R₂ P]
  [inst_10 : Module S₂ P] [inst_11 : SMulCommClass R₂ S₂ P] {ρ : R →+* R₂} {σ : S →+* S₂} (M' : Submodule R M)
  (N' : Submodule S N) (f f_1 : M →ₛₗ[ρ] N →ₛₗ[σ] P) (e_f : f = f_1) (hM' : M' ≤ f.ker) (hN' : N' ≤ f.flip.ker),
  LinearMap.liftQ₂ M' N' f hM' hN' = LinearMap.liftQ₂ M' N' f_1 ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_int_mul_two_pi : ∀ (n : ℤ), Real.cos (↑n * (2 * Real.pi)) = 1
-- Init.Data.Ord.String
Char.instTransOrd : Std.TransOrd Char
-- Mathlib.Data.Set.Lattice.Image
/-- Analogue of `biSup_prod` for sets.  -/
Set.biUnion_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set β) (t : Set γ) (f : β × γ → Set α),
  ⋃ x ∈ s ×ˢ t, f x = ⋃ i ∈ s, ⋃ j ∈ t, f (i, j)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
spectrum.hasDerivAt_resolvent_const_right : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField A]
  [inst_2 : NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜},
  k ∈ resolventSet 𝕜 a → HasDerivAt (fun x => resolvent x k) (resolvent a k ^ 2) a
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.left_pos : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < p
-- Init.Data.UInt.Lemmas
USize.toNat_toUInt16 : ∀ (x : USize), x.toUInt16.toNat = x.toNat % 2 ^ 16
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.trans_refl : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), e.trans (AffineEquiv.refl k P₂) = e
-- Init.Data.UInt.Lemmas
USize.mul_assoc : ∀ (a b c : USize), a * b * c = a * (b * c)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `max j j'` is an arbitrary choice of object to the right of both `j` and `j'`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.max : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.IsFilteredOrEmpty C] → C → C → C
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.is_generator : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] {v : Valuation K Γ}
  [hv : v.IsRankOneDiscrete] (π : v.Uniformizer), IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {π.val}
-- Std.Time.Format.Modifier
Std.Time.instInhabitedZoneId : Inhabited Std.Time.ZoneId
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : Option β → Option β} {hc : k ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k hc =
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get ⋯
-- Init.Data.Array.MapIdx
Array.mapIdx_ne_empty_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Array α}, Array.mapIdx f xs ≠ #[] ↔ xs ≠ #[]
-- Mathlib.Logic.Function.Basic
Function.IsPartialInv.get_eq : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α},
  Function.IsPartialInv f g → ∀ (x : β) (h : (g x).isSome = true), f ((g x).get h) = x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.fold.eq_1 : ∀ {σ : Sort u_1} {α : Type u_2} (v₀ : σ) (f : σ → α → σ → σ), RBTree.RBNode.fold v₀ f RBTree.RBNode.nil = v₀
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The relations between elements of the direct sum of the `F.obj j` given by the
morphisms in the diagram `J`.
 -/
AddCommGrpCat.Colimits.Relations : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) → [DecidableEq J] → AddSubgroup (Π₀ (j : J), ↑(F.obj j))
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
Continuous.map_eq_borel : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [PolishSpace X] [inst_2 : MeasurableSpace X] [BorelSpace X]
  [inst_4 : TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y] {f : X → Y},
  Continuous f → Function.Surjective f → MeasurableSpace.map f inst_2 = borel Y
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The functor between bounded below homotopy categories that is induced
by an additive functor.  -/
CategoryTheory.Functor.mapHomotopyCategoryPlus : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [F.Additive] → CategoryTheory.Functor (HomotopyCategory.Plus C) (HomotopyCategory.Plus D)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.hom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F] {X : C}
  {f g : CategoryTheory.Limits.coend F ⟶ X},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) g) →
    f = g
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift_bot : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E),
  IntermediateField.lift ⊥ = ⊥
-- Init.Data.Float.Float32
/-- Computes the hyperbolic sine of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`sinhf`.
 -/
Float32.sinh : Float32 → Float32
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Context.mk.injEq : ∀ (config config_1 : Lean.Meta.Sym.DSimp.Config), ({ config := config } = { config := config_1 }) = (config = config_1)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.shift_unit_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a).obj (G.obj (F.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X)) h =
    CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G a).hom.app (F.obj X)) h))
-- Mathlib.CategoryTheory.Equivalence
/-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it
to a refined natural isomorphism `adjointifyη η : 𝟭 C ≅ F ⋙ G` which exhibits the properties
required for a half-adjoint equivalence. See `Equivalence.mk`.  -/
CategoryTheory.Equivalence.adjointifyη : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (CategoryTheory.Functor.id C ≅ F.comp G) →
              (G.comp F ≅ CategoryTheory.Functor.id D) → (CategoryTheory.Functor.id C ≅ F.comp G)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.div_pf : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Div α], a₁ = b₁ → a₂ = b₂ → a₁ / a₂ = b₁ / b₂
-- Mathlib.GroupTheory.Index
Subgroup.index_prod : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (K : Subgroup G'),
  (H.prod K).index = H.index * K.index