mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.coe_mk' : ∀ {R : Type u_2} [inst : CommRing R] {P : Set R} {add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P}
  {mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P} {sq : ∀ (x : R), x * x ∈ P} {neg_one : -1 ∉ P},
  ↑(RingPreordering.mk' P add mul sq neg_one) = P
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.instCoeOutSet : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → {ps : DiscreteTiling.Protoset G X ιₚ} → CoeOut (DiscreteTiling.PlacedTile ps) (Set X)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A continuous function whose support is contained in a compact set is strongly
measurable.  -/
Continuous.stronglyMeasurable_of_support_subset_isCompact : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : Zero β] {f : α → β},
  Continuous f → ∀ {k : Set α}, IsCompact k → Function.support f ⊆ k → MeasureTheory.StronglyMeasurable f
-- Mathlib.Order.Hom.Bounded
TopHom.instOrderTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : LE β] [inst_2 : OrderTop β],
  TopHom.instOrderTop = { top := { toFun := ⊤, map_top' := ⋯ }, le_top := ⋯ }
-- Aesop.Percent
Aesop.Percent.fifty : Aesop.Percent
-- Init.Data.Slice.Notation
Std.Rci.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Rci β → γ) → Std.Rci.Sliceable α β γ
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldl.match_1.eq_1 : ∀ {σ : Sort u_3} {α : Type u_1} (motive : σ → RBTree.RBNode α → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive b RBTree.RBNode.nil)
  (h_2 :
    (b : σ) →
      (c : RBTree.RBColor) →
        (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive b (RBTree.RBNode.node c l v r)),
  (match b, RBTree.RBNode.nil with
    | b, RBTree.RBNode.nil => h_1 b
    | b, RBTree.RBNode.node c l v r => h_2 b c l v r) =
    h_1 b
-- Mathlib.FieldTheory.Galois.Basic
/-- Let $E$ be a field. Let $G$ be a finite group acting on $E$.
Then the extension $E / E^G$ is Galois.  -/
IsGalois.of_fixed_field : ∀ (E : Type u_2) [inst : Field E] (G : Type u_3) [inst_1 : Group G] [Finite G] [inst_3 : MulSemiringAction G E],
  IsGalois (↥(FixedPoints.subfield G E)) E
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Limits.isoZeroOfMonoEqZero.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f f_1 : X ⟶ Y} (e_f : f = f_1)
  [inst_3 : CategoryTheory.Mono f] (h : f = 0),
  CategoryTheory.Limits.isoZeroOfMonoEqZero h = CategoryTheory.Limits.isoZeroOfMonoEqZero ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsLeft.inf : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P₁ P₂ Q : CategoryTheory.MorphismProperty C)
  [P₁.RespectsLeft Q] [P₂.RespectsLeft Q], (P₁ ⊓ P₂).RespectsLeft Q
-- Mathlib.RingTheory.Multiplicity
multiplicity_sub_of_gt : ∀ {α : Type u_1} [inst : Ring α] {p a b : α},
  multiplicity p b < multiplicity p a → FiniteMultiplicity p b → multiplicity p (a - b) = multiplicity p b
-- Mathlib.Data.Nat.Factorial.SuperFactorial
_private.Mathlib.Data.Nat.Factorial.SuperFactorial.0.Nat.superFactorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.Directed
SemilatticeInf.instIsCodirectedOrder : ∀ {α : Type u_1} [inst : SemilatticeInf α], IsCodirectedOrder α
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t)
  {i : J} (x y : F.obj i),
  (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y ↔
    ∃ j f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeRule : Aesop.UnsafeRule → Aesop.BaseRuleSetMember
-- Mathlib.GroupTheory.Index
Subgroup.index_dvd_card : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.index ∣ Nat.card G
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- `F.mapCocone s` being colimiting is the same as the induced binary cofan being colimiting.  -/
CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : C} →
            {s : CategoryTheory.Limits.BinaryCofan X Y} →
              CategoryTheory.Limits.IsColimit (F.mapCocone s) ≃
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.map F s)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G}
  {x : AddAction.orbitRel.Quotient G α} {a b : ↑x.orbit}, ↑a ∈ AddAction.orbit ↥H ↑b ↔ a ∈ AddAction.orbit (↥H) b
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_eq_add_of_root_eq_add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j k l : ι},
  P.root k = P.root i + P.root j → P.pairing k l = P.pairing i l + P.pairing j l
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.essFiniteType_iff : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.EssFiniteType R S ↔ ∃ σ, ∀ (s : S), ∃ t ∈ Algebra.adjoin R ↑σ, IsUnit t ∧ s * t ∈ Algebra.adjoin R ↑σ
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.mapEdgeSet.eq_1 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑G.edgeSet),
  f.mapEdgeSet e = ⟨Sym2.map ⇑f ↑e, ⋯⟩
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapWhiskerLeft_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ⟶ Gᵣ) (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapWhiskerLeft H α).app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (H.obj x))
    | CategoryTheory.Join.right x => (CategoryTheory.Join.inclRight E E').map (α.app x)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instBEqOfEquivBEqOfLawfulHashable : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → BEq (Std.ExtHashSet α)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstInfo.mk.injEq : ∀ (argsInfo argsInfo_1 : Array Lean.Meta.Sym.ProofInstArgInfo),
  ({ argsInfo := argsInfo } = { argsInfo := argsInfo_1 }) = (argsInfo = argsInfo_1)
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_one : ∀ {α : Type u_1} [inst : One α], ofLex 1 = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_insertMany_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ} {k : α}, k ∈ m → k ∈ Std.DHashMap.Raw.Const.insertMany m l
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Equation (11.3.8) from Cohn's proof, where we view `Q` as a univariate polynomial.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₂_mul_Φ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  Polynomial.map Polynomial.C (RatFunc.Luroth.Q₂✝ h) * RatFunc.Luroth.Φ✝ E = RatFunc.Luroth.θ✝ E
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousLinearEquiv.coe_continuousAlternatingMapCongr : ∀ {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup E']
  [inst_5 : Module 𝕜 E'] [inst_6 : TopologicalSpace E'] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜 F]
  [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousConstSMul 𝕜 F]
  [inst_12 : AddCommGroup G] [inst_13 : Module 𝕜 G] [inst_14 : TopologicalSpace G] [inst_15 : IsTopologicalAddGroup G]
  [inst_16 : ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] G),
  ↑(e.continuousAlternatingMapCongr e') =
    (ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 E' F G ι) ↑e' ∘SL
      ContinuousAlternatingMap.compContinuousLinearMapCLM ↑e.symm
-- Mathlib.Algebra.Group.Basic
neg_inj : ∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, -a = -b ↔ a = b
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- Evidence that the proposed colimit is the colimit.  -/
MonCat.Colimits.colimitIsColimit : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → CategoryTheory.Limits.IsColimit (MonCat.Colimits.colimitCocone F)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b ⊆ Set.Iic b
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- To show that a locally ringed space is a scheme, it suffices to show that it has a jointly
surjective family of open immersions from affine schemes.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme : (X : AlgebraicGeometry.LocallyRingedSpace) →
  (∀ (x : ↑X.toTopCat),
      ∃ R f,
        x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ∧
          AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f) →
    AlgebraicGeometry.Scheme
-- Lean.Server.References
/-- Name of the parent declaration.  -/
Lean.Server.References.ParentDecl.name : Lean.Server.References.ParentDecl → String
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.withRingM : {α : Type} → Lean.Meta.Grind.Arith.CommRing.RingM α → Lean.Meta.Grind.Arith.Linear.LinearM α
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with the general mean value form of the remainder.

We assume that `f` is `n`-times continuously differentiable in the closed set `uIcc x₀ x` and
`n+1`-times differentiable on the open set `uIoo x₀ x`, and `g` is a differentiable function on
`uIoo x₀ x` and continuous on `uIcc x₀ x`. Then there exists an `x' ∈ uIoo x₀ x` such that
$$f(x) - (P_n f)(x₀, x) = \frac{(x - x')^n}{n!} \frac{g(x) - g(x₀)}{g' x'},$$
where $P_n f$ denotes the Taylor polynomial of degree $n$.  -/
taylor_mean_remainder : ∀ {f g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  x₀ ≠ x →
    ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x) →
      DifferentiableOn ℝ (iteratedDerivWithin n f (Set.uIcc x₀ x)) (Set.uIoo x₀ x) →
        ContinuousOn g (Set.uIcc x₀ x) →
          (∀ x_1 ∈ Set.uIoo x₀ x, HasDerivAt g (g' x_1) x_1) →
            (∀ x_1 ∈ Set.uIoo x₀ x, g' x_1 ≠ 0) →
              ∃ x' ∈ Set.uIoo x₀ x,
                f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
                  ((x - x') ^ n / ↑n.factorial * (g x - g x₀) / g' x') •
                    iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) x'
-- Mathlib.RingTheory.Polynomial.GaussLemma
IsLocalization.integerNormalization.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (M M_1 : Submonoid R) (e_M : M = M_1) {S : Type u_2} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (p p_1 : Polynomial S),
  p = p_1 → IsLocalization.integerNormalization M p = IsLocalization.integerNormalization M_1 p_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_singleton_append_iff : ∀ {xs : Array ℕ} {m n a : ℕ}, (m<...=n).toArray = #[a] ++ xs ↔ m + 1 = a ∧ m < n ∧ ((m + 1)<...=n).toArray = xs
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Icc a b).OrdConnected
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)] {b : β a}, (m.insert a b).get! a = b
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongr_single : ∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e : G ≃* H}
  (he : ∀ (a : G) (x : A), a • x = e a • x) (g : G) (a : A),
  (SkewMonoidAlgebra.domCongrAlg k A he) (SkewMonoidAlgebra.single g a) = SkewMonoidAlgebra.single (e g) a
-- Mathlib.Tactic.Linter.Header
/-- The "header" style linter checks that a file starts with
```
/-
Copyright ...
Apache ...
Authors ...
-/

import statements*
module doc-string*
remaining file
```
It emits a warning if
* the copyright statement is malformed;
* `Mathlib.Tactic` is imported;
* any import in `Lake` is present;
* the first non-`import` command is not a module doc-string.

The linter allows `import`-only files and does not require a copyright statement in `Mathlib.Init`.
 -/
Mathlib.Linter.linter.style.header : Lean.Option Bool
-- Mathlib.Algebra.Notation.Defs
/-- `a +ᵥ b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent,
but it is intended to be used for left actions.  -/
VAdd.vadd : {G : Type u} → {P : Type v} → [self : VAdd G P] → G → P → P
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.Iso.girth_eq : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β} (f : G ≃g G'), G.girth = G'.girth
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
RingCon.liftₐ.congr_simp : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M) (f f_1 : M →ₐ[R] P) (e_f : f = f_1)
  (H : c ≤ RingCon.ker f.toRingHom), c.liftₐ f H = c.liftₐ f_1 ⋯
-- Mathlib.Order.SetDissipate
Set.mem_dissipate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α} {z : β}, z ∈ Set.dissipate s x ↔ ∀ y ≤ x, z ∈ s y
-- Std.Data.Internal.List.Defs
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.DistinctKeys.distinct : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → List.Pairwise (fun a b => (a == b) = false) (Std.Internal.List.keys l)
-- Mathlib.Algebra.Prime.Defs
Prime.ne_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → p ≠ 0
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- We can only lose at most one sign changes if we drop the leading coefficient.  -/
Polynomial.signVariations_le_eraseLead_succ : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] (P : Polynomial R),
  P.signVariations ≤ P.eraseLead.signVariations + 1
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.tsum_logDeriv_eta_q : ∀ (z : ℂ),
  ∑' (n : ℕ), logDeriv (fun x => 1 - ModularForm.eta_q n x) z =
    2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), (↑n + 1) * -ModularForm.eta_q n z / (1 - ModularForm.eta_q n z)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (t.insert k v).minKey? = some k
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
SeminormedAddCommGroup.dist_eq : ∀ {E : Type u_8} [self : SeminormedAddCommGroup E] (x y : E), dist x y = ‖-x + y‖
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  (X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ),
  ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj X).snd =
    CategoryTheory.yonedaEquiv.toFun (Opposite.unop X).hom
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.of_eq_zero_of_mul_self_of_eq_zero_of_add : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R],
  (∀ {a : R}, a * a = 0 → a = 0) → (∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0) → IsFormallyReal R
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- The solid closure of a subset `s` is the smallest superset of `s` that is solid.  -/
LatticeOrderedAddCommGroup.solidClosure : {α : Type u_1} → [Lattice α] → [AddCommGroup α] → Set α → Set α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {a : α} {fallback : β a}, m.contains a = true → m.get? a = some (m.getD a fallback)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.skeletonEquivalence_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.skeletonEquivalence C).inverse = CategoryTheory.toSkeletonFunctor C
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R) (y : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk x y = 0 ↔ x ≤ᵥ 0
-- Mathlib.Topology.Instances.ENat
ENat.instContinuousMul : ContinuousMul ℕ∞
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.decidableLE.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α}
  [inst_3 : DecidableLE α] (a b : Localization s),
  a.decidableLE b = a.recOnSubsingleton₂ b fun x x_1 x_2 x_3 => decidable_of_iff' (↑x_3 * x ≤ ↑x_2 * x_1) ⋯
-- Mathlib.GroupTheory.Perm.List
List.formPerm_nil : ∀ {α : Type u_1} [inst : DecidableEq α], [].formPerm = 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Vertical composition of strong transformations.  -/
CategoryTheory.Pseudofunctor.StrongTrans.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.Pseudofunctor B C} → F.StrongTrans G → G.StrongTrans H → F.StrongTrans H
-- Mathlib.Order.Heyting.Boundary
Coheyting.inf_hnot_self : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), a ⊓ ￢a = Coheyting.boundary a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k fallback : α},
  k ∉ m → l.contains k = false → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKeyD k fallback = fallback
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv : ∀ {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]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv._auto_3),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.center_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S],
  NonUnitalSubsemiring.center (R × S) = (NonUnitalSubsemiring.center R).prod (NonUnitalSubsemiring.center S)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.resNatTrans_app : ∀ (k : Type u) {G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (f : G →* H) (n : ℕ)
  (X : Rep.{u, u, u} k H),
  (groupCohomology.resNatTrans k f n).app X = groupCohomology.map f (CategoryTheory.CategoryStruct.id (Rep.res f X)) n
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.instFiniteToSSet : ∀ (X : SSet) [X.Finite] (A : X.Subcomplex), A.toSSet.Finite
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G], (groupCohomology.cochainsFunctor k G).PreservesZeroMorphisms
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.p : Lean.Meta.Grind.Arith.Linear.EqCnstr → Lean.Grind.Linarith.Poly
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair_ε : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k],
  (ModularForm.weakFEPair hk f).ε = Complex.I ^ k
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ne_endPos_of_sliceTo_ne_endPos : ∀ {s : String.Slice} {p p₀ : s.Pos} {h₀ : p ≤ p₀}, p₀.sliceTo p h₀ ≠ (s.sliceTo p₀).endPos → p ≠ s.endPos
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone_pt_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C) {X Y : D} (f : X ⟶ Y),
  (CategoryTheory.Limits.pointwiseBinaryBicone F G).pt.map f = CategoryTheory.Limits.biprod.map (F.map f) (G.map f)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roo_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toList[i]? = none ↔ (n - (m + 1)).toNat ≤ i
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β]
  (f g : SupBotHom α β), ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ι), MeasurableSet (s i)) → μ.restrict (⋃ i, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s i)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticWithinAt.pow`

---

Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticWithinAt.fun_pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A} {z : E}
  {s : Set E}, AnalyticWithinAt 𝕜 f s z → ∀ (n : ℕ), AnalyticWithinAt 𝕜 (fun i => f i ^ n) s z
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.coe_iSup_of_directed : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} [Nonempty ι], Directed (fun x1 x2 => x1 ≤ x2) t → ↑(iSup t) = ⋃ i, ↑(t i)