mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpTrimToLpMeas_ae_eq : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  (f : ↥(MeasureTheory.Lp F p (μ.trim hm))), ↑↑↑(MeasureTheory.lpTrimToLpMeas F 𝕜 p μ hm f) =ᵐ[μ] ↑↑f
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.fixed.inj : ∀ {remaining remaining_1 : ℕ},
  Std.Http.Protocol.H1.Reader.BodyState.fixed remaining = Std.Http.Protocol.H1.Reader.BodyState.fixed remaining_1 →
    remaining = remaining_1
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.pow_equiv_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f1 f2 : CauSeq β abv},
  f1 ≈ f2 → ∀ (n : ℕ), f1 ^ n ≈ f2 ^ n
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkAtomCached.match_3.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (motive : Std.Sat.AIG α → Sort u_1)
  (decls : Array (Std.Sat.AIG.Decl α)) (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls)
  (hzero : 0 < decls.size) (hconst : decls[0] = Std.Sat.AIG.Decl.false)
  (h_1 :
    (decls : Array (Std.Sat.AIG.Decl α)) →
      (cache : Std.Sat.AIG.Cache α decls) →
        (hdag : Std.Sat.AIG.IsDAG α decls) →
          (hzero : 0 < decls.size) →
            (hconst : decls[0] = Std.Sat.AIG.Decl.false) →
              motive { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }),
  (match { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } with
    | { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =>
      h_1 decls cache hdag hzero hconst) =
    h_1 decls cache hdag hzero hconst
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals.append : Lean.Widget.InteractiveGoals → Lean.Widget.InteractiveGoals → Lean.Widget.InteractiveGoals
-- Mathlib.Analysis.Convex.Contractible
/-- A non-empty convex set is a contractible space.  -/
Convex.contractibleSpace : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {s : Set E}, Convex ℝ s → s.Nonempty → ContractibleSpace ↑s
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_mul_eq_mk_left : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a < MulArchimedeanClass.mk b → MulArchimedeanClass.mk (a * b) = MulArchimedeanClass.mk a
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.pre : Lean.Meta.SimpTheorems → Lean.Meta.SimpTheoremTree
-- Init.Data.Dyadic.Basic
Dyadic.mul_add : ∀ (x y z : Dyadic), x * (y + z) = x * y + x * z
-- Mathlib.Data.Finset.Pi
Finset.card_piDiag : ∀ {α : Type u_1} (s : Finset α) (ι : Type u_3) [inst : DecidableEq (ι → α)] [Nonempty ι], (s.piDiag ι).card = s.card
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_lid_comp_map_rid_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y')
  {Z : Type w} (h : P.obj X' Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.CategoryStruct.id X) g)
      (CategoryTheory.CategoryStruct.comp (P.map f (CategoryTheory.CategoryStruct.id Y)) h) =
    CategoryTheory.CategoryStruct.comp (P.map f g) h
-- Aesop.Rule
Aesop.NormRuleInfo : Type
-- Mathlib.Algebra.Field.Defs
/-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

Do not use this lemma directly. Use `NNRat.smul_def` instead.  -/
Field.nnqsmul_def : ∀ {K : Type u} [self : Field K] (q : ℚ≥0) (a : K), Field.nnqsmul q a = ↑q * a
-- Mathlib.Data.Set.Prod
Set.range_pair_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ),
  (Set.range fun x => (f x, g x)) ⊆ Set.range f ×ˢ Set.range g
-- Mathlib.Data.Real.Sign
/-- This lemma is useful for working with `ℝˣ`  -/
Real.sign_apply_eq_of_ne_zero : ∀ (r : ℝ), r ≠ 0 → r.sign = -1 ∨ r.sign = 1
-- Mathlib.Algebra.Ring.Basic
neg_div_neg_eq : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] (a b : R), -a / -b = a / b
-- Mathlib.Tactic.Linter.MinImports
Mathlib.Linter.instInhabitedImportState.default : Mathlib.Linter.ImportState✝
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.exists_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y),
  autoParam (CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
      CategoryTheory.Limits.weakPullback.exists_lift._auto_1 →
    ∃ l,
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.weakPullback.fst f g) = h ∧
        CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.weakPullback.snd f g) = k
-- Init.Data.Array.Count
Array.countP_eq_size_filter : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.countP p xs = (Array.filter p xs).size
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
          (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm'))
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.liftPostcompIso_inv_hom : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_7, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C E A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] (Φ : A → CategoryTheory.Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (a : A),
  (F.liftPostcompIso G Φ hΦ).inv.hom a = (hΦ a).inv
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_neg : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x : AddMonoidAlgebra R M), (-x).coeff = -x.coeff
-- Mathlib.RingTheory.Derivation.Basic
Derivation.congr_fun : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  {D1 D2 : Derivation R A M}, D1 = D2 → ∀ (a : A), D1 a = D2 a
-- Mathlib.Computability.Primrec.List
Primcodable.finArrow : {α : Type u_1} → [Primcodable α] → {n : ℕ} → Primcodable (Fin n → α)
-- Mathlib.LinearAlgebra.Complex.Module
realPart_idem : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, realPart ↑(realPart x) = realPart x
-- Mathlib.Order.RelSeries
/-- A relation `r` is said to be finite dimensional iff there is a relation series of `r` with the
maximum length.  -/
SetRel.FiniteDimensional.exists_longest_relSeries : ∀ {α : Type u_1} {r : SetRel α α} [self : r.FiniteDimensional], ∃ x, ∀ (y : RelSeries r), y.length ≤ x.length
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mk.congr_simp : ∀ {Γ : Type u_8} {R : Type u_9} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_7}
  (toFun toFun_1 : α → HahnSeries Γ R) (e_toFun : toFun = toFun_1)
  (isPWO_iUnion_support' : (⋃ a, (toFun a).support).IsPWO)
  (finite_co_support' : ∀ (g : Γ), {a | (toFun a).coeff g ≠ 0}.Finite),
  { toFun := toFun, isPWO_iUnion_support' := isPWO_iUnion_support', finite_co_support' := finite_co_support' } =
    { toFun := toFun_1, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
-- Mathlib.MeasureTheory.Measure.LevyConvergence
MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] {ι : Type u_2} {𝓕 : Filter ι} {μ₀ : MeasureTheory.ProbabilityMeasure E}
  {μ : ι → MeasureTheory.ProbabilityMeasure E},
  (∀ (t : E), Filter.Tendsto (fun n => MeasureTheory.charFun (↑(μ n)) t) 𝓕 (nhds (MeasureTheory.charFun (↑μ₀) t))) →
    ∀ {g : BoundedContinuousFunction E ℂ},
      g ∈ BoundedContinuousFunction.charPoly Real.continuous_probChar ⋯ →
        Filter.Tendsto (fun n => ∫ (x : E), g x ∂↑(μ n)) 𝓕 (nhds (∫ (x : E), g x ∂↑μ₀))
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of the forward direction of `Order.isSuccPrelimit_iff_isSuccLimit`. -/
Order.IsSuccPrelimit.isSuccLimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [NoMinOrder α], Order.IsSuccPrelimit a → Order.IsSuccLimit a
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- `totalDegree p` gives the maximum |s| over the monomials X^s in `p`  -/
MvPolynomial.totalDegree : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R → ℕ
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.mk.injEq : ∀ {β : Type u_1} {α : Type u_2} (toBallPackage : Besicovitch.BallPackage β α) (τ : ℝ) (one_lt_tau : 1 < τ)
  (toBallPackage_1 : Besicovitch.BallPackage β α) (τ_1 : ℝ) (one_lt_tau_1 : 1 < τ_1),
  ({ toBallPackage := toBallPackage, τ := τ, one_lt_tau := one_lt_tau } =
      { toBallPackage := toBallPackage_1, τ := τ_1, one_lt_tau := one_lt_tau_1 }) =
    (toBallPackage = toBallPackage_1 ∧ τ = τ_1)
-- Mathlib.Tactic.TacticAnalysis
/-- Specifies which analysis steps to take.

The overall design will have three user-supplied components:

* **trigger** on a piece of syntax (which could contain multiple tactic calls);
* **test** if a suggested change is indeed an improvement;
* **tell** the user where changes can be made.
 -/
Mathlib.TacticAnalysis.ComplexConfig : Type 1
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulAction' : {α : Type u_1} →
  {β : Type u_2} →
    {l : Filter α} → {M : Type u_5} → [inst : Monoid M] → [MulAction M β] → MulAction (l.Germ M) (l.Germ β)
-- Mathlib.RingTheory.RootsOfUnity.Lemmas
/-- If `μ` is a primitive `n`th root of unity in `R`, then `(-1)^(n-1) * ∏(1≤k<n) (μ^k-1) = n`.
(Stated with `n+1` in place of `n` to avoid the condition `n ≠ 0`.)  -/
IsPrimitiveRoot.prod_pow_sub_one_eq_order : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n : ℕ} {μ : R},
  IsPrimitiveRoot μ (n + 1) → (-1) ^ n * ∏ k ∈ Finset.range n, (μ ^ (k + 1) - 1) = ↑n + 1
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.decl.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.CasesTarget'.decl decl = Aesop.CasesTarget'.decl decl_1 → decl = decl_1
-- Mathlib.Analysis.Normed.Group.Uniform
Isometry.norm_map_of_map_zero : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F},
  Isometry f → f 0 = 0 → ∀ (x : E), ‖f x‖ = ‖x‖
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr.toJson : Lean.Lsp.RefIdent.RefIdentJsonRepr → Lean.Json
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The kernel of `δ : H^n(g) ⟶ H^{n+1}(f)`. In the documentation,
this may be shortened as `Z^n(f, g)`  -/
CategoryTheory.Abelian.SpectralObject.cycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι → {i j k : ι} → (i ⟶ j) → (j ⟶ k) → ℤ → C
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), Std.Internal.List.getKey a l h = Std.Internal.List.getKey! a l
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsLeft.iInf : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1}
  {W : ι → CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [∀ (i : ι), (W i).RespectsLeft Q],
  (⨅ i, W i).RespectsLeft Q
-- Lean.LocalContext
/-- A let-bound free variable, with a value `value : Expr`.
If `nondep := false`, then the variable is definitionally equal to its value.
If `nondep := true`, then the variable has an opaque value; we call these "have-bound free variables."
`Lean.LocalContext.mkBinding` creates let/have expressions from `ldecl`s.

**Important:** The `nondep := true` case is subtle; it is not merely an opaque `ldecl`!
- In most contexts, nondependent `ldecl`s should be treated like `cdecl`s.
  For example, suppose we have a tactic goal `x : α := v (nondep) ⊢ b`.
  It would be incorrect for `revert x` to produce the goal `⊢ have x : α := v; b`,
  since this would be saying "to prove `b` without knowledge of the value of `x`, it suffices to
  prove `have x : α := v; b` for this particular value of `x`."
  Instead, `revert x` *must* produce the goal `⊢ ∀ x : α, b`.
  Furthermore, given a goal `⊢ have x : α := v; b`, the `intro x` tactic should yield a *dependent* `ldecl`,
  since users expect to be able to make use of the value of `x`,
  plus, as discussed, if `intro` yielded a nondep `ldecl` then `intro x; revert x` would convert the goal into a forall, not a `have`.
- Also: `value` might not be type correct. Metaprograms may decide to pretend that all `nondep := true`
  `ldecl`s are `cdecl`s (for example, when reverting variables). As a consequence, nondep `ldecl`s may
  have type-incorrect values. This design decision allows metaprograms to not have to think about nondep `ldecl`s,
  so long as `LocalDecl` values are consumed through `LocalDecl.isLet` and `LocalDecl.value?` with `(allowNondep := false)`.
  **Rule:** never use `(generalizeNondepLet := false)` in `mkBinding`-family functions
  on a local context entry you did not create.
  See `LocalDecl.setNondep` for some additional discussion.
- Where then do nondep ldecls come from? Common functions are `Meta.mapLetDecl`, `Meta.withLetDecl`, and `Meta.letTelescope`.
  The `have` term syntax makes use of a nondep ldecl as well.

Therefore, `nondep := true` should be used with consideration.
Its primary use is in metaprograms that enter `let`/`have` telescopes and wish to reconstruct them.  -/
Lean.LocalDecl.ldecl : ℕ → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Bool → Lean.LocalDeclKind → Lean.LocalDecl
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.mapEquiv_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] (e : α ≃ᵤ β) (a : α),
  (UniformSpace.Completion.mapEquiv e) ↑a = ↑(e a)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.norm_comp_le_of_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂}
  {g : NormedAddGroupHom V₂ V₃} {C₁ C₂ : ℝ}, ‖g‖ ≤ C₂ → ‖f‖ ≤ C₁ → ‖g.comp f‖ ≤ C₂ * C₁
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
/-- Updates the old assignment of `l` to reflect the fact that `(l, false)` is now part of the formula.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The precomposition of functors with `toKaroubi C` is fully faithful.  -/
CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful : {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.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj
            (CategoryTheory.Idempotents.toKaroubi C)).FullyFaithful
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_1 : ∀ (x : Nat.Partrec.Code), Nat.Partrec.Code.evaln 0 x = fun x => none
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁)
  {Z : F.obj b₀ ⟶ F.obj b₁} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).hom (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom h)
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Icc_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : LocallyFiniteOrder R]
  [Archimedean R], Filter.Tendsto (fun n => Finset.Icc (-↑n) ↑n) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Being a colimiting cofan is stable under equivalences in the index type.  -/
CategoryTheory.Limits.Cofan.isColimitEquivOfEquiv : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {γ : Type w'} →
        (ε : β ≃ γ) →
          {f : γ → C} →
            (c : CategoryTheory.Limits.Cofan f) →
              CategoryTheory.Limits.IsColimit c ≃
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt fun i => c.inj (ε i))
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
group homomorphism `G/N →* M`.  -/
QuotientGroup.lift : {G : Type u_1} →
  {M : Type u_4} →
    [inst : Group G] → [inst_1 : Monoid M] → (N : Subgroup G) → [nN : N.Normal] → (φ : G →* M) → N ≤ φ.ker → G ⧸ N →* M
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_iInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {ι : Sort u_3} {S : ι → L.Substructure M} {x : M},
  x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : NumberField.RingOfIntegers K),
  (NumberField.IsCMField.complexConj K) ↑x = ↑x ↔
    ∃ y, (algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) K) y = ↑x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.insertMany_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {l : List α} {k : α},
  t.insertMany (k :: l) = (t.insert k).insertMany l
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- `M` is boundaryless if and only if its boundary is empty.  -/
ModelWithCorners.Boundaryless.iff_boundary_eq_empty : ∀ {𝕜 : 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], ModelWithCorners.boundary M = ∅ ↔ BoundarylessManifold I M
-- Mathlib.Data.Finset.Filter
Finset.filter_inj : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s t : Finset α},
  Finset.filter p s = Finset.filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList_eq_match_rcc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.Rxc.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.least? with
    | none => []
    | some least => (least...=r.upper).toList
-- Mathlib.Algebra.Group.Hom.Defs
instSubsingletonZeroHom : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] [Subsingleton M], Subsingleton (ZeroHom M N)
-- Aesop.Stats.File
Aesop.appendStatsToStatsFileIfEnabled : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.MonadOptions m] →
        [Lean.Elab.MonadParentDecl m] →
          [MonadLiftT IO m] → [MonadLiftT Lean.CoreM m] → Lean.Syntax → Aesop.Stats → Bool → m Unit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ofList_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  Std.ExtDTreeMap.Const.ofList l cmp = ∅ ↔ l = []
-- Mathlib.Analysis.Analytic.Composition
/-- Rewriting equality in the dependent type
`Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun i)` in
non-dependent terms with lists, requiring that the lists of blocks coincide.  -/
Composition.sigma_pi_composition_eq_iff : ∀ {n : ℕ} (u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))),
  u = v ↔ (List.ofFn fun i => (u.snd i).blocks) = List.ofFn fun i => (v.snd i).blocks
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_one : CartanMatrix.D 1 = CartanMatrix.A 1
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ}, HasFiniteFPowerSeriesAt f p x n → ∀ (m : ℕ), n ≤ m → p m = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul_three : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α] {a b c d e f : α},
  a ≤ d → b ≤ e → c ≤ f → a * b * c ≤ d * e * f
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousAt_iff_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β},
  ContinuousAt f b ↔ Filter.Tendsto (fun x => (f x.1, f x.2)) (nhds (b, b)) (uniformity α)
-- Lean.Syntax
Lean.Syntax.Traverser.idxs : Lean.Syntax.Traverser → Array ℕ
-- Init.Data.String.Lemmas.FindPos
String.Pos.ofSliceTo_prev : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).startPos},
  String.Pos.ofSliceTo (p.prev h) = (String.Pos.ofSliceTo p).prev ⋯
-- Std.Data.TreeSet.Basic
/-- Returns the `n`-th smallest element, or `fallback` if `n` is at least `t.size`.  -/
Std.TreeSet.atIdxD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → ℕ → α → α
-- Mathlib.Order.SymmDiff
compl_symmDiff : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), (symmDiff a b)ᶜ = bihimp a b
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.lift_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : Y ⨯ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) 0) h)
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.Subfunctor.equivalenceMonoOver F).unitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.eqToIso ⋯) ⋯