mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Divisible
/-- Any quotient group of a rootable group is rootable.  -/
QuotientGroup.rootableBy : {A : Type u_2} → [inst : CommGroup A] → (B : Subgroup A) → [RootableBy A ℕ] → RootableBy (A ⧸ B) ℕ
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.constantCoeff_expand : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R),
  PowerSeries.constantCoeff ((PowerSeries.expand p hp) φ) = PowerSeries.constantCoeff φ
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity from scaled positive distance. Backward direction of
`similar_iff_exists_pos_dist_eq`.  -/
Similar.of_exists_pos_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzOnWith_iff_norm_neg_add_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {s : Set E} {f : E → F}
  {C : NNReal}, LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖-f x + f y‖ ≤ ↑C * ‖-x + y‖
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'_d_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hi : ¬e.BoundaryGE i),
  (K.truncGE' e).d i j =
    CategoryTheory.CategoryStruct.comp (K.truncGE'XIso e hi' hi).hom
      (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.truncGE'XIso e hj' ⋯).inv)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKey! k' = k
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_X : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (i : σ), (MvPowerSeries.rename f) (MvPowerSeries.X i) = MvPowerSeries.X (f i)
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  {α : Type u_1} {β : Type u_2} (f : α → β) [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] [inst_4 : CategoryTheory.Limits.HasCoproduct fun x => R]
  (b : β) (hb : b ∉ Set.range f) {Z : C} (h : (∐ fun x => R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) b)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.sigmaConstCokernelCofork R f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) ⟨b, hb⟩) h
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The characteristic function of a Gaussian distribution with mean `μ` and variance `v`
is given by `t ↦ exp (t * μ - v * t ^ 2 / 2)`.  -/
ProbabilityTheory.charFun_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (t : ℝ),
  MeasureTheory.charFun (ProbabilityTheory.gaussianReal μ v) t = Complex.exp (↑t * ↑μ * Complex.I - ↑↑v * ↑t ^ 2 / 2)
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.mk.injEq : ∀ (visitedExpr : Lean.ExprSet) (fvarSet : Lean.FVarIdSet) (fvarIds : Array Lean.FVarId) (visitedExpr_1 : Lean.ExprSet)
  (fvarSet_1 : Lean.FVarIdSet) (fvarIds_1 : Array Lean.FVarId),
  ({ visitedExpr := visitedExpr, fvarSet := fvarSet, fvarIds := fvarIds } =
      { visitedExpr := visitedExpr_1, fvarSet := fvarSet_1, fvarIds := fvarIds_1 }) =
    (visitedExpr = visitedExpr_1 ∧ fvarSet = fvarSet_1 ∧ fvarIds = fvarIds_1)
-- Mathlib.Data.QPF.Multivariate.Constructions.Quot
MvQPF.Quot1.inhabited : {n : ℕ} →
  {F : TypeVec.{u} n → Type u} →
    (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) → {α : TypeVec.{u} n} → [Inhabited (F α)] → Inhabited (MvQPF.Quot1 R α)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.isStoppingTime_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m) (i : ι),
  MeasureTheory.IsStoppingTime f fun x => ↑i
-- Mathlib.Data.Nat.Choose.Multinomial
/-- The multinomial coefficients given by a list of natural numbers.

See also `Multiset.multinomial`  -/
List.multinomial : List ℕ → ℕ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_intervalIntegral_eq : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ)
  (μ : MeasureTheory.Measure ℝ), ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Set.uIoc a b, f x ∂μ‖
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.comparison_obj_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C),
  ((CategoryTheory.Comonad.comparison h).obj X).a = L.map (h.unit.app X)
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.smul_subset : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α} {x : α},
  IsLowerSet s → x ≤ 1 → x • s ⊆ s
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.downAddHom : (G : Type u) → [inst : Add G] → ULift.{u_1, u} G →ₙ+ G
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.norm_smul_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)), ‖c • f‖ = ‖f‖
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_mul : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f : SlashInvariantForm Γ k₁)
  (g : SlashInvariantForm Γ k₂), ⇑(f.mul g) = ⇑f * ⇑g
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_4.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_5 t ×' Lean.Doc.Block.below_4 t
-- Init.Data.SInt.Lemmas
ISize.add_mul : ∀ {a b c : ISize}, (a + b) * c = a * c + b * c
-- Mathlib.Tactic.MkIffOfInductiveProp
Mathlib.Tactic.MkIff.Shape.mk : List Bool → Option ℕ → Mathlib.Tactic.MkIff.Shape
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCastD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (fallback : β a)
  (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getCastD a fallback x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => fallback
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      if h : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.AssocList.getCastD a fallback es
-- Mathlib.Order.Monotone.Monovary
antivaryOn_toDual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f (⇑OrderDual.toDual ∘ g) s ↔ MonovaryOn f g s
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A `LinearMap` on a finite-dimensional space over a complete field
is injective iff it is anti-Lipschitz.  -/
LinearMap.injective_iff_antilipschitz : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F), Function.Injective ⇑f ↔ ∃ K > 0, AntilipschitzWith K ⇑f
-- Mathlib.Probability.Independence.BoundedContinuousFunction
process_indepFun_process_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  {F : T → Type u_5} [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)]
  [∀ (s : S), BorelSpace (E s)] [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : (t : T) → TopologicalSpace (F t)]
  [inst_5 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)] [∀ (t : T), HasOuterApproxClosed (F t)]
  {X : (s : S) → Ω → E s} {Y : (t : T) → Ω → F t} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (I : Finset S) (J : Finset T) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ)
          (g : (t : ↥J) → BoundedContinuousFunction (F ↑t) ℝ),
          ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P =
            (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.zero_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (m : M), 0 m = 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₁₀_comp_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 0 → G) →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).inv
      (CategoryTheory.CategoryStruct.comp
        (ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A))
          (fun n => groupHomology.inhomogeneousChains.d A n) 1 0)
        h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).inv h)
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- Twice the product of two Chebyshev `T` polynomials is the sum of two other Chebyshev `T`
polynomials.  -/
Polynomial.Chebyshev.T_mul_T : ∀ (R : Type u_1) [inst : CommRing R] (m k : ℤ),
  2 * Polynomial.Chebyshev.T R m * Polynomial.Chebyshev.T R k =
    Polynomial.Chebyshev.T R (m + k) + Polynomial.Chebyshev.T R (m - k)
-- Mathlib.Data.Num.ZNum
Num.mod.eq_1 : ∀ (x : Num), Num.zero.mod x = 0
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_sdiff_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.nonAssocSemiring : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [Module R M] → [Module Rᵐᵒᵖ M] → NonAssocSemiring (TrivSqZeroExt R M)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.State.mk : ℕ →
  Lean.Meta.Sym.Simp.Cache →
    Lean.Meta.Sym.Simp.Cache → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr → Lean.Meta.Sym.Simp.State
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- `AssocList α β` is "the same as" `List (α × β)`, but flattening the structure
leads to one fewer pointer indirection (in the current code generator).
 -/
Std.DHashMap.Internal.AssocList : (α : Type u) → (α → Type v) → Type (max u v)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.resRec.match_3.eq_2 : ∀ {w : ℕ} (motive : (s : ℕ) → s < w → 0 < s → Sort u_1) (s' : ℕ) (hs : s' + 1 < w) (hslt : 0 < s' + 1)
  (h_1 : (hs : 0 < w) → (hslt : 0 < 0) → s'.succ = 0 → motive 0 hs hslt)
  (h_2 : (s'_1 : ℕ) → (hs : s'_1 + 1 < w) → (hslt : 0 < s'_1 + 1) → s'.succ = s'_1.succ → motive s'_1.succ hs hslt),
  (match hs0 : s'.succ, hs, hslt with
    | 0, hs, hslt => h_1 hs hslt hs0
    | s'_1.succ, hs, hslt => h_2 s'_1 hs hslt hs0) =
    h_2 s' hs hslt ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_X₂ : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms], (S.map F).X₂ = F.obj S.X₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.ZSMul.eq_1 : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : Add α] [inst_2 : Neg α],
  Set.ZSMul = { smul := fun n s => zsmulRec nsmulRec n s }
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Data.Nat.Factorial.SuperFactorial
_private.Mathlib.Data.Nat.Factorial.SuperFactorial.0.Nat.factorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Topology.Separation.Basic
T0Space.of_open_cover : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (x : X), ∃ s, x ∈ s ∧ IsOpen s ∧ T0Space ↑s) → T0Space X
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.complOrderIso_symm_apply : ∀ (α : Type u_2) [inst : TopologicalSpace α] (a : (TopologicalSpace.Opens α)ᵒᵈ),
  (RelIso.symm (TopologicalSpace.Closeds.complOrderIso α)) a = (TopologicalSpace.Opens.compl ∘ ⇑OrderDual.ofDual) a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.contDiffAt_tan : ∀ {n : WithTop ℕ∞} {x : ℝ}, ContDiffAt ℝ n Real.tan x ↔ Real.cos x ≠ 0
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- Given `ι : C ⥤ A`, `Λ : LeftResolution ι`, `X : A`, this is a chain complex
which is a (functorial) resolution of `A` that is obtained inductively by using
the epimorphisms given by `Λ`.  -/
CategoryTheory.Abelian.LeftResolution.chainComplex : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          CategoryTheory.Abelian.LeftResolution ι →
            A →
              [ι.Full] →
                [ι.Faithful] →
                  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] → [CategoryTheory.Abelian A] → ChainComplex C ℕ
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.mem_span_integralBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x : K},
  x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.integralBasis K)) ↔
    x ∈ (algebraMap (NumberField.RingOfIntegers K) K).range
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightComp.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} (l : L₂ ⟶ L₁) (l' : L₃ ⟶ L₂),
  CategoryTheory.Comma.mapRightComp R l l' =
    CategoryTheory.NatIso.ofComponents'
      (fun X =>
        CategoryTheory.Comma.isoMk._to_dual_1
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Comma.mapRight R (CategoryTheory.CategoryStruct.comp l' l)).obj X).right)
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Comma.mapRight R (CategoryTheory.CategoryStruct.comp l' l)).obj X).left)
          ⋯)
      ⋯
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement.mk.injEq : ∀ (fvarId newFVarId fvarId_1 newFVarId_1 : Lean.FVarId),
  ({ fvarId := fvarId, newFVarId := newFVarId } = { fvarId := fvarId_1, newFVarId := newFVarId_1 }) =
    (fvarId = fvarId_1 ∧ newFVarId = newFVarId_1)
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanHalfSpace.ext_iff : ∀ {n : ℕ} [inst : NeZero n] {x y : EuclideanHalfSpace n}, x = y ↔ ↑x = ↑y
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.toNat_eq_iff_eq_natCast`. -/
ENat.toNat_eq_iff_eq_coe : ∀ (n : ℕ∞) (m : ℕ) [NeZero m], n.toNat = m ↔ n = ↑m
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.toUnder_comp_forget : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} S]
  (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y)
  (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z),
  (F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) = F
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.Nat.unaryCast.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseDayPeriod : String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.env : Lean.Elab.CommandContextInfo → Lean.Environment
-- Mathlib.Order.Partition.Basic
Partition.rel_comm : ∀ {α : Type u_1} {x y : α} {u : Set α} {P : Partition u}, P.Rel x y ↔ P.Rel y x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ρ_mul : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A : Rep.{w, u, v} k G} (g1 g2 : G),
  A.ρ (g1 * g2) = A.ρ g1 ∘ₗ A.ρ g2
-- Mathlib.Combinatorics.Graph.Basic
/-- The loopSet is included in the incidenceSet.  -/
Graph.loopSet_subset_incidenceSet : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α), Graph.loopSet x ⊆ Graph.incidenceSet x
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
`Π i, E →Lᵤ[𝕜, 𝔖] F i` and `E →Lᵤ[𝕜, 𝔖] Π i, F i`.  -/
UniformConvergenceCLM.piEquivL : (𝕜 : Type u_6) →
  [inst : NormedField 𝕜] →
    {E : Type u_7} →
      {ι : Type u_8} →
        (F : ι → Type u_9) →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : (i : ι) → AddCommGroup (F i)] →
                  [inst_5 : (i : ι) → Module 𝕜 (F i)] →
                    [inst_6 : (i : ι) → TopologicalSpace (F i)] →
                      [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] →
                        [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] →
                          (𝔖 : Set (Set E)) →
                            ((i : ι) → UniformConvergenceCLM (RingHom.id 𝕜) (F i) 𝔖) ≃L[𝕜]
                              UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖
-- Mathlib.Topology.VectorBundle.Basic
/-- Backwards map of `Bundle.Trivialization.continuousLinearEquivAt`, defined everywhere.  -/
Bundle.Trivialization.symmL : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                      [inst_7 : (x : B) → TopologicalSpace (E x)] →
                        [FiberBundle F E] →
                          (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                            [Bundle.Trivialization.IsLinear R e] → (b : B) → F →L[R] E b
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.mk.sizeOf_spec : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} [inst : SizeOf I₁]
  [inst_1 : SizeOf I₂] [inst_2 : SizeOf I₃] [inst_3 : SizeOf J] (I₁₂ : Type u_11) (p : I₁ × I₂ → I₁₂) (q : I₁₂ × I₃ → J)
  (hpq : ∀ (i : I₁ × I₂ × I₃), q (p (i.1, i.2.1), i.2.2) = r i),
  sizeOf { I₁₂ := I₁₂, p := p, q := q, hpq := hpq } = 1 + sizeOf I₁₂
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.finite_torsion_of_isSMulRegular_int : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) (n : ℤ), IsSMulRegular 𝕜 n → {x | n • x = 0}.Finite
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.add_fromLeftNeg : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg), ↑x + ↑(S.fromLeftNeg x) = 0
-- Mathlib.Data.Option.Basic
Option.Mem.leftUnique : ∀ {α : Type u_1}, Relator.LeftUnique fun x1 x2 => x1 ∈ x2
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.neg.inj : ∀ {a a_1 : Int.Internal.Linear.Expr}, a.neg = a_1.neg → a = a_1
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instVAddCommClassForall_2 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [inst : VAdd M α] [inst_1 : VAdd N α]
  [VAddCommClass M N α], VAddCommClass Mᵈᵃᵃ Nᵈᵃᵃ (α → β)