mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Hom
Algebra.ofId_apply : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (Algebra.ofId R A) r = (algebraMap R A) r
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.congr_linearEquiv_coe_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommGroup W] [inst_4 : Module R W] (e : V ≃ₗ[R] W) (f : SpecialLinearGroup R V),
  ↑((SpecialLinearGroup.congr_linearEquiv e) f) = e.symm ≪≫ₗ ↑f ≪≫ₗ e
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.mem_selfAdjointSubmodule : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} (f : Module.End R M),
  f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint ⇑f
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
OpenPartialHomeomorph.contMDiffOn_writtenInExtend_iff : ∀ {𝕜 : 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_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_7} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_8}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M}
  {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G},
  φ ∈ IsManifold.maximalAtlas I n M →
    ψ ∈ IsManifold.maximalAtlas J n N →
      s ⊆ φ.source →
        Set.MapsTo f s ψ.source →
          (ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm)
              (↑(φ.extend I) '' s) ↔
            ContMDiffOn I J n f s)
-- Mathlib.Algebra.Group.ULift
ULift.pow.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Pow α β], ULift.pow = { pow := fun x n => { down := x.down ^ n } }
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- A subgraph as a graph has equivalent neighbor sets.  -/
SimpleGraph.Subgraph.coeNeighborSetEquiv : {V : Type u} →
  {G : SimpleGraph V} → {G' : G.Subgraph} → (v : ↑G'.verts) → ↑(G'.coe.neighborSet v) ≃ ↑(G'.neighborSet ↑v)
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.sec_spec : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [inst_3 : IsLocalization.Away x S] (s : S),
  s * (algebraMap R S) (x ^ (IsLocalization.Away.sec x s).2) = (algebraMap R S) (IsLocalization.Away.sec x s).1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (n : ℕ), SimpleGraph.Walk.nil.take n = SimpleGraph.Walk.nil
-- Mathlib.Data.Nat.Factorization.Defs
/-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b`  -/
Nat.factorization_mul_of_coprime : ∀ {a b : ℕ}, a.Coprime b → (a * b).factorization = a.factorization + b.factorization
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
HomotopyCategory.instLinearIntUpSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (R : Type u_1) [inst_3 : Ring R] [inst_4 : CategoryTheory.Linear R C]
  (n : ℤ), CategoryTheory.Functor.Linear R (HomotopyCategory.singleFunctor C n)
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The cusps of `SL(2, ℤ)` are precisely the `SL(2, ℤ)` orbit of `∞`.  -/
isCusp_SL2Z_iff' : ∀ {c : OnePoint ℝ},
  IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range ↔ ∃ g, c = (Matrix.SpecialLinearGroup.mapGL ℝ) g • OnePoint.infty
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.mk : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ},
  (∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass v).valueGroup ∧ γ < 1) → v.IsRankOneDiscrete
-- Mathlib.Data.List.Chain
List.IsChain.cons : ∀ {α : Type u_1} {R : α → α → Prop} {x : α} {l : List α},
  List.IsChain R l → (∀ y ∈ l.head?, R x y) → List.IsChain R (x :: l)
-- Init.Data.UInt.Lemmas
USize.toNat_mod : ∀ (a b : USize), (a % b).toNat = a.toNat % b.toNat
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.mem_polarSubmodule : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {S : Type u_6} [inst_4 : SetLike S E]
  [inst_5 : SMulMemClass S 𝕜 E] (m : S) (y : StrongDual 𝕜 E), y ∈ StrongDual.polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.instCoeContinuousLinearEquivId : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → Coe (A ≃A[R] B) (A ≃L[R] B)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- This instance is needed to create an instance for `AddCommMonoid (MultiseriesExpansion basis)`,
which is necessary for using the `abel` tactic in our proofs.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.instZero : {basis : Tactic.ComputeAsymptotics.Basis} → Zero (Tactic.ComputeAsymptotics.MultiseriesExpansion basis)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension₂ : ∀ (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] [CategoryTheory.IsIdempotentComplete D],
  (CategoryTheory.Idempotents.functorExtension₂ C D).IsEquivalence
-- Std.Tactic.Do.ProofMode
Std.Tactic.Do.mgoalStx : Lean.ParserDescr
-- Mathlib.Topology.Order.IntermediateValue
isConnected_uIoo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, a ≠ b → IsConnected (Set.uIoo a b)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prime_pow_le_iff_le_bcount : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] {m p : Associates α},
  m ≠ 0 → ∀ (h₂ : Irreducible p) {k : ℕ}, p ^ k ≤ m ↔ k ≤ Associates.bcount ⟨p, h₂⟩ m.factors
-- Lean.Message
/-- Lifted `Format.nest`  -/
Lean.MessageData.nest : ℕ → Lean.MessageData → Lean.MessageData
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.copy_eq : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A) (s : Set A)
  (hs : s = ↑S), S.copy s hs = S
-- Mathlib.SetTheory.Ordinal.Exponential
/-- `opow b` and `log b` (almost) form a Galois connection.

See `opow_le_iff_le_log'` for a variant assuming `c ≠ 0` rather than `x ≠ 0`. See also
`le_log_of_opow_le` and `opow_le_of_le_log`, which are both separate implications under weaker
assumptions.  -/
Ordinal.opow_le_iff_le_log : ∀ {b x c : Ordinal.{u_1}}, 1 < b → x ≠ 0 → (b ^ c ≤ x ↔ c ≤ Ordinal.log b x)
-- Mathlib.Topology.PartitionOfUnity
/-- A continuous partition of unity on a set `s : Set X` is a collection of continuous functions
`f i` such that

* the supports of `f i` form a locally finite family of sets, i.e., for every point `x : X` there
  exists a neighborhood `U ∋ x` such that all but finitely many functions `f i` are zero on `U`;
* the functions `f i` are nonnegative;
* the sum `∑ᶠ i, f i x` is equal to one for every `x ∈ s` and is less than or equal to one
  otherwise.

If `X` is a normal paracompact space, then `PartitionOfUnity.exists_isSubordinate` guarantees
that for every open covering `U : Set (Set X)` of `s` there exists a partition of unity that is
subordinate to `U`.
 -/
PartitionOfUnity : Type u_1 → (X : Type u_2) → [TopologicalSpace X] → optParam (Set X) Set.univ → Type (max u_1 u_2)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.cons : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ g ∈ basis, (Real.log ∘ g) =o[Filter.atTop] (Real.log ∘ f)) →
        Tactic.ComputeAsymptotics.WellFormedBasis (f :: basis)
-- Init.Data.Rat.Lemmas
Rat.mul_inv_cancel : ∀ (a : ℚ), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Data.Nat.Choose.Lucas
/-- **Alias** of `Choose.choose_modEq_prod_range_choose`.

---

**Lucas's Theorem**: For primes `p`, `choose n k` is congruent to the product of
`choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p)` over `i` modulo `p`.  -/
Choose.lucas_theorem : ∀ {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ},
  n < p ^ a → k < p ^ a → ↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.prodMap_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  {V4 : Type u_8} {P4 : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2]
  [inst_7 : AddCommGroup V3] [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] [inst_10 : AddCommGroup V4]
  [inst_11 : Module k V4] [inst_12 : AddTorsor V4 P4] (f : P1 →ᵃ[k] P2) (g : P3 →ᵃ[k] P4),
  (f.prodMap g).linear = f.linear.prodMap g.linear
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosedTypeComp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.UniversallyClosed f]
  [hg : AlgebraicGeometry.UniversallyClosed g],
  AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.mk.inj : ∀ {G : Type u_6} {inst : AddGroup G} {toAddGroupSeminorm : AddGroupSeminorm G}
  {eq_zero_of_map_eq_zero' : ∀ (x : G), toAddGroupSeminorm.toFun x = 0 → x = 0}
  {toAddGroupSeminorm_1 : AddGroupSeminorm G}
  {eq_zero_of_map_eq_zero'_1 : ∀ (x : G), toAddGroupSeminorm_1.toFun x = 0 → x = 0},
  { toAddGroupSeminorm := toAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 } →
    toAddGroupSeminorm = toAddGroupSeminorm_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `f` is a periodic function with period `T`, then its integral over `[t, t + T]` does not
depend on `t`.  -/
Function.Periodic.intervalIntegral_add_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
  Function.Periodic f T → ∀ (t s : ℝ), ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
-- Init.Grind.Lemmas
Lean.Grind.ne_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : LawfulBEq α} {a b : α}, (a == b) = false → (a = b) = False
-- Mathlib.Algebra.Group.Action.Opposite
/-- With `open scoped RightActions`, an alternative symbol for left actions, `r • m`.

In lemma names this is still called `smul`.  -/
RightActions.«term_•>_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Group.Abs
sub_le_of_abs_sub_le_left : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  |a - b| ≤ c → b - c ≤ a
-- Init.Data.Option.Lemmas
Option.not_lt_filter : ∀ {α : Type u_1} [inst : LT α], (∀ (x : α), ¬x < x) → ∀ {o : Option α} {p : α → Bool}, ¬o < Option.filter p o
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.biSup_finset : ∀ {G : Type u_3} [inst : Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G),
  (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Init.Data.SInt.Bitwise
Int32.shiftLeft_and : ∀ {a b c : Int32}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algEquiv_apply : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (v : AbsoluteValue T S) (x : WithAbs v),
  (WithAbs.algEquiv R v) x = x.ofAbs
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {Y : AlgebraicGeometry.Scheme}
  (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒰.f i)
      (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphismsOfLocallyDirected g ⋯) h_1) =
    CategoryTheory.CategoryStruct.comp (g i) h_1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms in `ComposableArrows C 4`.  -/
CategoryTheory.ComposableArrows.homMk₄ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 4} →
      (app₀ : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) →
        (app₁ : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝) →
          (app₂ : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) →
            (app₃ : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝) →
              (app₄ : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝) →
                autoParam
                    (CategoryTheory.CategoryStruct.comp
                        (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝) app₁ =
                      CategoryTheory.CategoryStruct.comp app₀
                        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
                    _auto_353✝ →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
                        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
                      _auto_355✝ →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
                          CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
                        _auto_357✝ →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
                            CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝))
                          _auto_359✝ →
                        (f ⟶ g)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_id : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom ⋯ U = CategoryTheory.CategoryStruct.id (I.glueDataObj U)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.coev_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X Y : CategoryTheory.Over J} (g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp g ((CategoryTheory.ExponentiableMorphism.coev f).app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ExponentiableMorphism.coev f).app X)
      ((CategoryTheory.ExponentiableMorphism.pushforward f).map
        ((CategoryTheory.ChosenPullbacksAlong.pullback f).map g))
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_sdiv_right : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, (s /ₛ t).Nonempty → t.Nonempty
-- Mathlib.Data.Setoid.Partition
/-- A complete lattice instance for partitions; there is more infrastructure for the
equivalent complete lattice on equivalence relations.  -/
Setoid.Partition.completeLattice : {α : Type u_1} → CompleteLattice (Setoid.Partitions α)
-- Mathlib.Algebra.Group.Action.Defs
MulDistribMulAction.mk : {M : Type u_9} →
  {N : Type u_10} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] →
        [toMulAction : MulAction M N] →
          (∀ (r : M), r • 1 = 1) → (∀ (r : M) (x y : N), r • (x * y) = r • x * r • y) → MulDistribMulAction M N
-- Mathlib.Logic.Relation
Relation.reflTransGen_eq_transGen : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], Relation.ReflTransGen r = Relation.TransGen r
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.prod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : SMul M α] [inst_1 : SMul N γ]
  [inst_2 : SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ),
  f.prod g = { toFun := fun x => (f x, g x), map_smul' := ⋯ }
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.mk_coe : ∀ (z : Complex.UnitDisc) (hz : optParam (‖↑z‖ < 1) ⋯), Complex.UnitDisc.mk (↑z) hz = z
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.neZero_partSize : ∀ {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length), NeZero (c.partSize i)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {a fallback : α}, ∅.getD a fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- A group object is a monoid object.  -/
CategoryTheory.Grp.toMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Grp C → CategoryTheory.Mon C
-- Lean.Parser.Syntax
Lean.Parser.Command.syntaxCat.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Computability.Language
Language.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (l : Language α),
  (Language.map g) ((Language.map f) l) = (Language.map (g ∘ f)) l
-- Lean.Elab.Tactic.Conv.Basic
/-- Removes the hypothesis referred to by `fvarId` from the context of the currently focused `conv`
goal, provided that `fvarId` is not referenced by another hypothesis or the current `conv`-focused
target.
 -/
Lean.Elab.Tactic.Conv.convClear : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ),
  (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ n).r = (CochainComplex.mappingCone.snd φ).v n n ⋯
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `{ n_i }` is an `R`-basis of `N`, which is also `M`-linearly independent,
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_basis_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {ι : Type u_1} (n : Module.Basis ι R ↥N), (M.mulRightMap ⇑n).ker = ⊥ → M.LinearDisjoint N
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_fstX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j) {Z : C} (h : F.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex cotangent function, defined as `cos z / sin z`  -/
Complex.cot : ℂ → ℂ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_tensorδ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂) h) =
    h
-- Init.Data.ToString.Basic
instToStringUInt32 : ToString UInt32
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_dite : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (p : Prop) [inst_2 : Decidable p] (a : p → α) (b : ¬p → α),
  |if h : p then a h else b h| = if h : p then |a h| else |b h|
-- Init.Data.SInt.Lemmas
ISize.lt_or_eq_of_le : ∀ {a b : ISize}, a ≤ b → a < b ∨ a = b
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.b₄ = 0
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.InfiniteAdeleRing K),
  (NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) x =
    (fun v => (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal ⋯) (x ↑v), fun v =>
      (NumberField.InfinitePlace.Completion.extensionEmbedding ↑v) (x ↑v))
-- Lean.DocString.Parser
Lean.Doc.Parser.instInhabitedInlineCtxt : Inhabited Lean.Doc.Parser.InlineCtxt
-- Mathlib.GroupTheory.Torsion
/-- A module whose scalars are torsion is torsion.  -/
IsAddTorsion.module_of_torsion : ∀ (R : Type u_3) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [Module R M],
  IsAddTorsion R → IsAddTorsion M
-- Mathlib.RingTheory.MvPolynomial.Groebner
MonomialOrder.degree_sub_LTerm_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f : MvPolynomial σ R),
  m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f)
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
/-- Any module isomorphism induces a quadratic isomorphism between the corresponding `dual_prod.`  -/
QuadraticForm.dualProdIsometry : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (M ≃ₗ[R] N) → QuadraticMap.IsometryEquiv (QuadraticForm.dualProd R M) (QuadraticForm.dualProd R N)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_le : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((∀ (k' : α), Std.Internal.List.maxKey? l = some k' → (compare k' k).isLE = true) ↔
      ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f},
  (t.modify k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ⋯ (f (t.get k ⋯)) else t.get k' ⋯
-- Mathlib.LinearAlgebra.Pi
LinearMap.single_apply : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] {i : ι} (v : φ i),
  (LinearMap.single R φ i) v = Pi.single i v
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.zsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
  Function.Periodic f c → ∀ (n : ℤ), f (n • c) = f 0
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremsArray.isLetDeclToUnfold : Lean.Meta.SimpTheoremsArray → Lean.FVarId → Bool