mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Closure
/-- Every Galois connection induces a lower adjoint.  -/
GaloisConnection.lowerAdjoint : {α : Type u_1} →
  {β : Type u_4} →
    [inst : Preorder α] → [inst_1 : Preorder β] → {l : α → β} → {u : β → α} → GaloisConnection l u → LowerAdjoint u
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulLeft_inj : ∀ {R : Type u_6} {A : Type u_7} [inst : Semiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] {a b : A}, LinearMap.mulLeft R a = LinearMap.mulLeft R b ↔ a = b
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.leftRel_pi : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → AddGroup (β i)] (s' : (i : ι) → AddSubgroup (β i)),
  QuotientAddGroup.leftRel (AddSubgroup.pi Set.univ s') = piSetoid
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizeUsingInstancesStep : List Lean.MVarId → Lean.Elab.TermElabM (List Lean.MVarId)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n : d → ℤ` is dense.  -/
UnitAddTorus.mFourierSubalgebra_closure_eq_top : ∀ {d : Type u_1} [inst : Fintype d], (UnitAddTorus.mFourierSubalgebra d).topologicalClosure = ⊤
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.Functor.mk.hcongr_8 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (D D' : Type u₂),
          D = D' →
            ∀ (inst_1 : CategoryTheory.Category.{v₂, u₂} D) (inst'_1 : CategoryTheory.Category.{v₂, u₂} D'),
              inst_1 ≍ inst'_1 →
                ∀ (obj : C → D) (obj' : C' → D'),
                  obj ≍ obj' →
                    ∀ (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map' : {X Y : C'} → (X ⟶ Y) → (obj' X ⟶ obj' Y)),
                      map ≍ map' →
                        ∀
                          (map_id :
                            ∀ (X : C),
                              map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
                          (map_id' :
                            ∀ (X : C'),
                              map' (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj' X)),
                          map_id ≍ map_id' →
                            ∀
                              (map_comp :
                                ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
                                  map (CategoryTheory.CategoryStruct.comp f g) =
                                    CategoryTheory.CategoryStruct.comp (map f) (map g))
                              (map_comp' :
                                ∀ {X Y Z : C'} (f : X ⟶ Y) (g : Y ⟶ Z),
                                  map' (CategoryTheory.CategoryStruct.comp f g) =
                                    CategoryTheory.CategoryStruct.comp (map' f) (map' g)),
                              map_comp ≍ map_comp' →
                                { obj := obj, map := map, map_id := map_id, map_comp := map_comp } ≍
                                  { obj := obj', map := map', map_id := map_id', map_comp := map_comp' }
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The type underlying the multiequalizer diagram.  -/
CategoryTheory.Limits.WalkingMulticospan : CategoryTheory.Limits.MulticospanShape → Type (max w w')
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- See also `rpow_neg_eq_inv_rpow` for a version with `x⁻¹ ^ y` in the RHS.  -/
Real.rpow_neg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), x ^ (-y) = (x ^ y)⁻¹
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Result type for `s₁.subseq s₂`
 -/
Lean.Grind.AC.SubseqResult : Type
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.classifier_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Sheaf.classifier J).truth = CategoryTheory.Sheaf.truth J
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.toList_rxcIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] {z : Std.DTreeMap.Internal.Zipper α β} {bound : α},
  { internalState := { iter := z, upper := bound } }.toList =
    List.takeWhile (fun e => (compare e.fst bound).isLE) z.toList
-- Mathlib.NumberTheory.FrobeniusNumber
frobeniusNumber_iff : ∀ {n : ℕ} {s : Set ℕ}, FrobeniusNumber n s ↔ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
-- Mathlib.GroupTheory.Finiteness
/-- A monoid is finitely generated iff there exists a surjective homomorphism from a `FreeMonoid`
on finitely many generators.  -/
Monoid.fg_iff_exists_freeMonoid_hom_surjective : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
topDualPairing_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousConstSMul 𝕜 𝕜]
  (v : E →L[𝕜] 𝕜) (x : E), ((topDualPairing 𝕜 E) v) x = v x
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.antitone_lowerCentralSeries : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M],
  Antitone (LieModule.lowerCentralSeries R L M)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.union_left : ∀ {α : Type u_2} {M : Matroid α} {X S : Set α},
  M.Spanning S → autoParam (X ⊆ M.E) Matroid.Spanning.union_left._auto_1 → M.Spanning (S ∪ X)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.prod_ite_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (s : Finset ι)
  (f : ι → M), (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
-- Lean.Parser.Types
Lean.Parser.instBEqCacheableParserContext : BEq Lean.Parser.CacheableParserContext
-- Mathlib.CategoryTheory.Linear.LinearFunctor
/-- An additive functor `F` is `R`-linear provided `F.map` is an `R`-module morphism.  -/
CategoryTheory.Functor.Linear : (R : Type u_1) →
  [inst : Semiring R] →
    {C : Type u_2} →
      {D : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive C] →
              [inst_4 : CategoryTheory.Preadditive D] →
                [CategoryTheory.Linear R C] → [CategoryTheory.Linear R D] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.ofTypeMonad_μ_app : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m] (X : Type u),
  (CategoryTheory.ofTypeMonad m).μ.app X = TypeCat.ofHom joinM
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.good.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsFunctor_map : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] {X Y : Rep.{u, u, u} k G} (f : X ⟶ Y),
  (groupCohomology.cochainsFunctor k G).map f = groupCohomology.cochainsMap (MonoidHom.id G) f
-- Mathlib.Data.Set.Lattice.Image
/-- The `Set.image2` version of `Set.image_eq_iUnion`  -/
Set.image2_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β),
  Set.image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The identity in the "underlying" category of an enriched category.  -/
CategoryTheory.ForgetEnrichment.homTo_id : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C),
  CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.eId W (CategoryTheory.ForgetEnrichment.to W X)
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] (r : R), Squarefree r = ∀ (x : R), x * x ∣ r → IsUnit x
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.ElimEmptyInductive.elim : Lean.MVarId → Lean.FVarId → Lean.Meta.ElimEmptyInductive.M Bool
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_C_mul_X_pow_eq : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (p.sum fun n a => Polynomial.C a * Polynomial.X ^ n) = p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the compatibility condition on `fst` and `snd` with respect to the structure
isomorphisms  -/
CategoryTheory.Limits.CategoricalPullback.Hom.w : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (self : x.Hom y),
  CategoryTheory.CategoryStruct.comp (F.map self.fst) y.iso.hom =
    CategoryTheory.CategoryStruct.comp x.iso.hom (G.map self.snd)
-- Mathlib.Algebra.Notation.Support
Function.ext_iff_mulSupport : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f g : ι → M},
  f = g ↔ Function.mulSupport f = Function.mulSupport g ∧ ∀ x ∈ Function.mulSupport f, f x = g x
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_iff_forall_mem : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded s ↔ ∀ x_1 ∈ s, Bornology.IsBounded s
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_symm_algebraMap : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜] (r : R),
  (DirectSum.decompose 𝒜).symm ((algebraMap R (DirectSum ι fun i => ↥(𝒜 i))) r) = (algebraMap R A) r
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → Zero ↑(Set.Icc 0 1)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_neg_iff : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.MemLp (-f) p μ ↔ MeasureTheory.MemLp f p μ
-- Mathlib.Analysis.Normed.Ring.Lemmas
RingHom.isometry : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : SeminormedRing 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂)
  [RingHomIsometric σ], Isometry ⇑σ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instNeg : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] → [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → Neg (SchwartzMap E F)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.congr_right : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ t₃ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Mathlib.Algebra.Homology.QuasiIso
isoOfQuasiIsoAt_hom_inv_id : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : QuasiIsoAt f i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) (isoOfQuasiIsoAt f i).inv =
    CategoryTheory.CategoryStruct.id (K.homology i)
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.IsBalanced.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N]
  [inst_2 : CommRing R] [inst_3 : Module R M] [inst_4 : Module R N] {P : RootPairing ι R M N},
  P.IsPerfectCompl (P.rootSpan R) (P.corootSpan R) → P.IsBalanced
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.isometry_pos_mul : ∀ (a : { x // 0 < x }), Isometry fun x => a • x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.commute_of_mem_adjoin_singleton_of_commute : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {a b c : A},
  c ∈ NonUnitalAlgebra.adjoin R {b} → Commute a b → Commute a c
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
fderivWithin_continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {s : Set E}
  {x : E} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  DifferentiableWithinAt 𝕜 f s x →
    (∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x) →
      UniqueDiffWithinAt 𝕜 s x →
        fderivWithin 𝕜 (fun x => (f x) fun x_1 => g x_1 x) s x =
          (ContinuousAlternatingMap.apply 𝕜 F G fun x_1 => g x_1 x) ∘SL fderivWithin 𝕜 f s x +
            ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL fderivWithin 𝕜 (g i) s x
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap_comp'_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y Z : C} {n : M} (f : X ⟶ Y)
  (g : Y ⟶ (CategoryTheory.shiftFunctor C n).obj Z) (a a' : M) (ha' : n + a = a') {Z_1 : A}
  (h : (F.shift a').obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (F.shiftMap (CategoryTheory.CategoryStruct.comp f g) a a' ha') h =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map f)
      (CategoryTheory.CategoryStruct.comp (F.shiftMap g a a' ha') h)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_add_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, (s + t).card ≤ s.card * t.card
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.linear_surjective_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [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] (f : P1 →ᵃ[k] P2),
  Function.Surjective ⇑f.linear ↔ Function.Surjective ⇑f
-- Batteries.CodeAction.Attr
/-- The state of the tactic code actions extension.  -/
Batteries.CodeAction.TacticCodeActions : Type
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.add.match_1.eq_1 : ∀ (motive : Num → Num → Sort u_1) (a : Num) (h_1 : (a : Num) → motive Num.zero a) (h_2 : (b : Num) → motive b Num.zero)
  (h_3 : (a b : PosNum) → motive (Num.pos a) (Num.pos b)),
  (match Num.zero, a with
    | Num.zero, a => h_1 a
    | b, Num.zero => h_2 b
    | Num.pos a, Num.pos b => h_3 a b) =
    h_1 a
-- Mathlib.GroupTheory.Sylow
Sylow.card_eq_card_quotient_normalizer : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  Nat.card (Sylow p G) = Nat.card (G ⧸ Subgroup.normalizer ↑P)
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.rel_of_right₂ : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α m] [inst_4 : Std.Iterators.Finite α₂ m]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ : Std.IterM m β},
  Std.Iterators.Types.Flatten.Rel✝ α β m { internalState := { it₁ := it₁, it₂ := none } }
    { internalState := { it₁ := it₁, it₂ := some it₂ } }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_add : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Add R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (f g : BoundedContinuousFunction α R), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingSum.eq_1 : ∀ {G : Type u_4} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G], [].alternatingSum = 0
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.isOpenMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → IsOpenMap f
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.dotProduct_toMatrix_mulVec`. -/
BilinForm.dotProduct_toMatrix_mulVec : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (x y : n → R₁),
  x ⬝ᵥ ((LinearMap.BilinForm.toMatrix b) B).mulVec y = (B (b.equivFun.symm x)) (b.equivFun.symm y)
-- Mathlib.Algebra.Opposites
AddOpposite.instAdd.eq_1 : ∀ {α : Type u_1} [inst : Add α],
  AddOpposite.instAdd = { add := fun x y => AddOpposite.op (AddOpposite.unop y + AddOpposite.unop x) }
-- Init.Data.Rat.Lemmas
Rat.zero_mkRat : ∀ (n : ℕ), mkRat 0 n = 0
-- Batteries.Recycling.RBTree.Basic
/-- A stream over the iterator.  -/
RBTree.RBMap.Keys.toStream : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap.Keys α β cmp → RBTree.RBMap.Keys.Stream α β
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instAddCommGroup : {𝕜₁ : 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 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : TopologicalSpace F] →
                          [IsTopologicalAddGroup F] → (𝔖 : Set (Set E)) → AddCommGroup (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.homCongr_apply : ∀ (k : Type u_1) {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : Semiring k]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z)
  (f : X ⟶ W),
  (CategoryTheory.Linear.homCongr k f₁ f₂) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁.inv f) f₂.hom
-- Mathlib.Analysis.Normed.Group.Basic
/-- An injective group homomorphism from a `CommGroup` to a
`NormedCommGroup` induces a `NormedCommGroup` structure on the domain.  -/
NormedAddCommGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : NormedAddGroup F] →
            [AddMonoidHomClass 𝓕 E F] → (f : 𝓕) → Function.Injective ⇑f → NormedAddCommGroup E
-- Mathlib.Analysis.Convex.Side
AffineSubspace.not_sOppSide_bot : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x y : P),
  ¬⊥.SOppSide x y
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_iff_lt_pred : ∀ {α : Type u_1} {b : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  Order.IsPredPrelimit b ↔ ∀ (a : α), b < a → b < Order.pred a
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (F.map h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) h_1) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom
            h_1)))
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_dvd_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R), EuclideanDomain.gcd a b ∣ a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.property : Lean.Lsp.CompletionItemKind
-- Init.Data.UInt.Lemmas
UInt8.lt_of_le_of_lt : ∀ {a b c : UInt8}, a ≤ b → b < c → a < c
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.inftyNormedRing : {I : Type u_5} →
  {B : I → Type u_6} → [inst : (i : I) → NormedRing (B i)] → [∀ (i : I), NormOneClass (B i)] → NormedRing ↥(lp B ⊤)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mul_mem_sup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x y : A},
  x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Algebra.Divisibility.Basic
/-- Right divisibility relation. `RightDvd a b` means `a` right-divides `b`,
i.e., `∃ c, b = c * a`.  -/
RightDvd : {α : Type u_1} → [Semigroup α] → α → α → Prop
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'_convex : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w // w.IsComplex }),
  Convex ℝ (NumberField.mixedEmbedding.convexBodyLT' K f w₀)
-- Init.Data.List.Find
List.find?_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a) {p : β → Bool},
  List.find? p (List.pmap f xs H) =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      (List.find?
        (fun x =>
          match x with
          | ⟨a, m⟩ => p (f a ⋯))
        xs.attach)
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
UpperSemicontinuous.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  UpperSemicontinuous f →
    UpperSemicontinuous g →
      (∀ (x : α), ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → UpperSemicontinuous fun z => f z + g z
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on `{ω | X ω = x}`.

It is `μ` restricted to `{ω | X ω = x}` and scaled by the inverse of `μ {ω | X ω = x}`
(to make it a probability measure): `(μ {ω | X ω = x})⁻¹ • μ.restrict {ω | X ω = x}`.  -/
ProbabilityTheory.«term__[|_←_]» : Lean.TrailingParserDescr
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sInf_empty : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α], sInf ∅ = ⊤
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_leadingCoeff : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.leadingCoeff = f.trailingCoeff