mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftNatIso_hom : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
  (e : F₁ ≅ F₂),
  (CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).hom =
    CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' e.hom
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- A finite group `G` is a Z-group if and only if `G` is isomorphic to a semidirect product of two
cyclic subgroups of coprime order.  -/
isZGroup_iff_exists_mulEquiv : ∀ {G : Type u_1} [inst : Group G] [Finite G],
  IsZGroup G ↔ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X : C} {f : X ⟶ X}
  (hf : CategoryTheory.CategoryStruct.comp f f = f)
  {c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f} (i : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i).retraction =
    i.lift (CategoryTheory.Limits.Fork.ofι f ⋯)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_add : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Add γ] [inst_3 : ContinuousAdd γ] (f g : α →ₘ[μ] γ), ↑(f + g) =ᵐ[μ] ↑f + ↑g
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_mulSingle : ∀ {ι : Type u_2} {M : ι → Type u_6} [inst : (i : ι) → Monoid (M i)] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (x : (i : ι) → M i), Finset.univ.noncommProd (fun i => Pi.mulSingle i (x i)) ⋯ = x
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- This is the counit of the tilde-Gamma adjunction.  -/
AlgebraicGeometry.Scheme.Modules.fromTildeΓNatTrans : {R : CommRingCat} →
  AlgebraicGeometry.moduleSpecΓFunctor.comp (AlgebraicGeometry.tilde.functor R) ⟶
    CategoryTheory.Functor.id (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_intCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜) [inst_3 : IntCast F] (z : ℤ), derivWithin (↑z) s = 0
-- Mathlib.CategoryTheory.Limits.Pi
/-- Given a family of cocones over the `F ⋙ Pi.eval C i`,
we can assemble these together as a `Cocone F`.
 -/
CategoryTheory.pi.coconeOfCoconeCompEval : {I : Type v₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type v₁} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {F : CategoryTheory.Functor J ((i : I) → C i)} →
            ((i : I) → CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Pi.eval C i))) →
              CategoryTheory.Limits.Cocone F
-- ProofWidgets.Data.Html
ProofWidgets.LayoutKind.inline : ProofWidgets.LayoutKind
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rio : ∀ {n i : ℕ}, (*...n).toArray[i]? = if i < n then some i else none
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flip_smul : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (c : 𝕜₃) (f : E →SL[σ₁₃] F →SL[σ₂₃] G),
  (c • f).flip = c • f.flip
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.Commensurable.discreteTopology_iff : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {H K : AddSubgroup G}, H.Commensurable K → (DiscreteTopology ↥H ↔ DiscreteTopology ↥K)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.neg_one : ∀ {R : Type u_4} [inst : CommRing R] (p : ℕ) [Nontrivial R] [h : CharP R p], p ≠ 2 → IsPrimitiveRoot (-1) 2
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_prod : ∀ (α : Type u_3) (β : Type u_4), ENat.card (α × β) = ENat.card α * ENat.card β
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.liftOn.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (x : AddLocalization S) (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d),
  x.liftOn f H = AddLocalization.rec f ⋯ x
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mapInvariants_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (f : ContIntertwiningMap π π') (v : ↥π.invariants),
  ↑(f.mapInvariants v) = f ↑v
-- Mathlib.Analysis.Normed.Lp.lpHolder
/-- A uniformly bounded family of continuous linear maps, as a continuous linear map
on the `lp` space.  -/
lp.mapCLM : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : α → Type u_3} →
      {F : α → Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : α) → NormedAddCommGroup (E i)] →
            [inst_2 : (i : α) → NormedSpace 𝕜 (E i)] →
              [inst_3 : (i : α) → NormedAddCommGroup (F i)] →
                [inst_4 : (i : α) → NormedSpace 𝕜 (F i)] →
                  (p : ENNReal) →
                    [inst_5 : Fact (1 ≤ p)] →
                      (T : (i : α) → E i →L[𝕜] F i) →
                        {K : ℝ} → 0 ≤ K → (∀ (i : α), ‖T i‖ ≤ K) → ↥(lp E p) →L[𝕜] ↥(lp F p)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1}
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Init.Data.Rat.Basic
/-- Subtraction of rational numbers. (This definition is `@[irreducible]` because you don't want to
unfold it. Use `Rat.sub_def` instead.)
 -/
Rat.sub : ℚ → ℚ → ℚ
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ext_dual_iff : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [H : SeparatingDual 𝕜₂ F]
  {A B : E →SWOT[σ] F}, A = B ↔ ∀ (x : E) (y : StrongDual 𝕜₂ F), y (A x) = y (B x)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.move₂_ok : ∀ {p : Turing.PartrecToTM2.Γ' → Bool} {k₁ k₂ : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'}
  {s : Option Turing.PartrecToTM2.Γ'} {L₁ : List Turing.PartrecToTM2.Γ'} {o : Option Turing.PartrecToTM2.Γ'}
  {L₂ : List Turing.PartrecToTM2.Γ'} {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'},
  k₁ ≠ Turing.PartrecToTM2.K'.rev ∧ k₂ ≠ Turing.PartrecToTM2.K'.rev ∧ k₁ ≠ k₂ →
    S Turing.PartrecToTM2.K'.rev = [] →
      Turing.PartrecToTM2.splitAtPred p (S k₁) = (L₁, o, L₂) →
        StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
          { l := some (Turing.PartrecToTM2.move₂ p k₁ k₂ q), var := s, stk := S }
          { l := some q, var := none,
            stk := Function.update (Function.update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂) }
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (r : 𝕜) (f : E →L[𝕜] F),
  ContinuousLinearMap.lTensor G (r • f) = r • ContinuousLinearMap.lTensor G f
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.HasBasis.cauchySeq_iff : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [inst : SemilatticeSup β]
  {u : β → α} {p : γ → Prop} {s : γ → SetRel α α},
  (uniformity α).HasBasis p s →
    (CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ (X₁ ⊗ X₃) ⊗ X₂`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂.eq_1 : ∀ (z τ : ℂ), jacobiTheta₂ z τ = ∑' (n : ℤ), jacobiTheta₂_term n z τ
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.mem_lattice : ∀ {L : PeriodPair} {x : ℂ}, x ∈ L.lattice ↔ ∃ m n, ↑m * L.ω₁ + ↑n * L.ω₂ = x
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- A three-cycle is a cycle of length 3.  -/
Equiv.Perm.IsThreeCycle : {α : Type u_1} → [Fintype α] → [DecidableEq α] → Equiv.Perm α → Prop
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.acc_zero : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) → Acc (DFinsupp.Lex r s) 0
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.idIsPolyI' : ∀ (p : ℕ), WittVector.IsPoly p fun x x_1 a => a
-- Mathlib.Algebra.Torsor.Basic
Prod.instTorsor.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'],
  Prod.instTorsor =
    { smul := fun v p => (v.1 • p.1, v.2 • p.2), mul_smul := ⋯, one_smul := ⋯,
      sdiv := fun p₁ p₂ => (p₁.1 /ₛ p₂.1, p₁.2 /ₛ p₂.2), nonempty := ⋯, sdiv_smul' := ⋯, smul_sdiv' := ⋯ }
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.liftOfSurjective.eq_1 : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {C : Type u_4} [inst_5 : CommRing C] [inst_6 : Algebra R C]
  [inst_7 : Algebra.FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g)
  (hg' : IsNilpotent (RingHom.ker ↑g)),
  Algebra.FormallySmooth.liftOfSurjective f g hg hg' =
    Algebra.FormallySmooth.lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)
-- Init.Omega.IntList
Lean.Omega.IntList.dvd_gcd : ∀ (xs : Lean.Omega.IntList) (c : ℕ), (∀ {a : ℤ}, a ∈ xs → ↑c ∣ a) → c ∣ xs.gcd
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β} {h : k ∈ Std.ExtDHashMap.Const.modify m k f},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.modify m k f) k h = f (Std.ExtDHashMap.Const.get m k ⋯)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.desc.congr_simp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution solution_1 : relations.Solution M} (e_solution : solution = solution_1)
  (h : solution.IsPresentation) {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N]
  (s s_1 : relations.Solution N), s = s_1 → h.desc s = ⋯.desc s_1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termπ_3 : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKeyD_alter!_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t).maxKeyD fallback = k ↔
            (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
_private.Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal.0.IsCyclotomicExtension.Rat.«term𝒑» : Lean.ParserDescr
-- Batteries.Data.FloatArray
/-- `map f a` applies the function `f` to each element of the array.  -/
FloatArray.map : FloatArray → (Float → Float) → FloatArray
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                {M N : CategoryTheory.Mod D A} →
                  (hom : M.X ⟶ N.X) → [isModHom : CategoryTheory.IsModHom A hom] → M.Hom N
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.residuallyFinite_of_forall_exists_finite_addMonoidHom : ∀ {G : Type u_1} [inst : AddGroup G],
  (∀ (g : G), g ≠ 0 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 0) → AddGroup.ResiduallyFinite G
-- Mathlib.RingTheory.RingHom.Etale
/-- Helper lemma for the `algebraize` tactic  -/
RingHom.Etale.toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Etale → Algebra.Etale R S
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The product of `f` over `insert a s` is the same as
the product over `s`, as long as `a` is in `s` or `f a = 1`.  -/
Finset.prod_insert_of_eq_one_if_notMem : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (a ∉ s → f a = 1) → ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- Auxiliary definition for `LeftResolution.karoubi`.  -/
CategoryTheory.Abelian.LeftResolution.karoubi.π : {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 ι) →
            [inst_2 : CategoryTheory.Preadditive C] →
              [inst_3 : CategoryTheory.Preadditive A] →
                [ι.Additive] →
                  (CategoryTheory.Abelian.LeftResolution.karoubi.F Λ).comp
                      ((CategoryTheory.Idempotents.functorExtension₂ C A).obj ι) ⟶
                    CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi A)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.not_isCompleteMultipartite_iff_exists_isPathGraph3Compl : ∀ {α : Type u} {G : SimpleGraph α}, ¬G.IsCompleteMultipartite ↔ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
-- Mathlib.Data.Set.Countable
Set.Subsingleton.countable : ∀ {α : Type u} {s : Set α}, s.Subsingleton → s.Countable
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.range_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), (↑(p.projectionL q h)).range = p
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_re : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.re z⁻¹ = RCLike.re z / RCLike.normSq z
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- The identity isometry between equal quadratic forms.  -/
QuadraticMap.Isometry.ofEq : {R : Type u_1} →
  {M₁ : Type u_3} →
    {N : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M₁] → [inst_4 : Module R N] → {Q₁ Q₂ : QuadraticMap R M₁ N} → Q₁ = Q₂ → Q₁ →qᵢ Q₂
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ ν : MeasureTheory.Measure α},
  (μ₁ + μ₂).AbsolutelyContinuous ν ↔ μ₁.AbsolutelyContinuous ν ∧ μ₂.AbsolutelyContinuous ν
-- Mathlib.Data.Matrix.Composition
Matrix.comp_diagonal_diagonal : ∀ {I : Type u_1} {J : Type u_2} {R : Type u_5} [inst : DecidableEq I] [inst_1 : DecidableEq J] [inst_2 : Zero R]
  (d : I → J → R),
  (Matrix.comp I I J J R) (Matrix.diagonal fun i => Matrix.diagonal fun j => d i j) =
    Matrix.diagonal fun ij => d ij.1 ij.2
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.apply_mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α}, f x ∈ f.support ↔ x ∈ f.support
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- Eta-expanded form of `iteratedDerivWithin_id` -/
iteratedDerivWithin_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s → UniqueDiffOn 𝕜 s → iteratedDerivWithin n (fun x => x) s x = if n = 0 then x else if n = 1 then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept_def : ∀ (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ),
  L.derivWeierstrassPExcept (↑l₀) z = L.derivWeierstrassP z + 2 / (z - ↑l₀) ^ 3
-- Mathlib.Algebra.Free
/-- Length of an element of a free additive magma.  -/
FreeAddMagma.length : {α : Type u} → FreeAddMagma α → ℕ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product of two `C^n` functions within a set at a point is `C^n` within this set
at this point.  -/
ContDiffWithinAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {s : Set E} {f g : E → 𝔸},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.colimitPresheafOfModules_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [inst_3 : ∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] {x Y : Cᵒᵖ}
  (f : x ⟶ Y),
  (PresheafOfModules.colimitPresheafOfModules F).map f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimMap (F.whiskerLeft (PresheafOfModules.restriction R f)))
      (CategoryTheory.preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
          (F.comp (PresheafOfModules.evaluation R Y))).inv
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.isDecl : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Bool
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  (F : CategoryTheory.Functor C (Type w)) (X : C),
  (CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj F X).pt = F.obj X
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.StateT.wp_apply_eq : ∀ {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α σ : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] (x : StateT σ m α) (post : α → σ → Pred) (epost : EPred) (s : σ),
  Std.Internal.Do.wp x post epost s =
    Std.Internal.Do.wp (x.run s)
      (fun x =>
        match x with
        | (a, s) => post a s)
      epost
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), Monotone (CategoryTheory.Sieve.functorPullback F)
-- Mathlib.Order.KonigLemma
/-- The sequence given by Kőnig's lemma as an order embedding  -/
exists_orderEmbedding_covby_of_forall_covby_finite : ∀ {α : Type u_1} [inst : PartialOrder α] [IsStronglyAtomic α] {b : α},
  (∀ (a : α), {x | a ⋖ x}.Finite) → (Set.Ici b).Infinite → ∃ f, f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)
-- Mathlib.Order.Heyting.Basic
/-- `(p → q) ∧ p → q`  -/
himp_inf_le : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, (a ⇨ b) ⊓ a ≤ b
-- Mathlib.GroupTheory.OrderOfElement
isMulTorsionFree_iff_not_isOfFinOrder : ∀ {G : Type u_1} [inst : CommGroup G], IsMulTorsionFree G ↔ ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
-- Init.GetElem
GetElem.getElem.congr_simp : ∀ {coll : Type u} {idx : Type v} {elem : Type w} {valid : coll → idx → Prop} [self : GetElem coll idx elem valid]
  (xs xs_1 : coll) (e_xs : xs = xs_1) (i i_1 : idx) (e_i : i = i_1) (h : valid xs i), xs[i] = xs_1[i_1]
-- Aesop.Frontend.Saturate
Aesop.Frontend.evalSaturate? : Lean.Elab.Tactic.Tactic
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.fileMap : Lean.Elab.CommandContextInfo → Lean.FileMap
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Topology.IsLocallyConstructible s → Topology.IsOpenEmbedding f → Topology.IsLocallyConstructible (f ⁻¹' s)
-- Mathlib.Algebra.Order.Monoid.NatCast
zero_le_four : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : Preorder α] [ZeroLEOneClass α] [AddLeftMono α], 0 ≤ 4
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.forget₂_obj : ∀ {R : Type u} [inst : CommRing R] (X : CoalgCat R),
  (CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X.toModuleCat
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.mk : Aesop.Options' → Aesop.LocalRuleSet → Aesop.NormSimpContext → Aesop.NormM.Context
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_eq_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b = toIocMod hp 0 (b - a) + a
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_insert_zero : ∀ {M : Type u_1} (s : Set M) [inst : AddZeroClass M], SimpleGraph.addCayley (insert 0 s) = SimpleGraph.addCayley s
-- Mathlib.Topology.Inseparable
SpecializingMap.stableUnderSpecialization_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f → StableUnderSpecialization (Set.range f)
-- Mathlib.LinearAlgebra.Dimension.Free
/-- A rank `n` free module has a basis indexed by `Fin n`.  -/
Module.finBasisOfFinrankEq : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [Module.Free R M] →
            [StrongRankCondition R] → [Module.Finite R M] → {n : ℕ} → Module.finrank R M = n → Module.Basis (Fin n) R M