mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- The degree `[D : K]` of the decomposition field `D` over `K` equals the number of prime ideals
of `B` lying over `p`.
 -/
IsDecompositionField.rank_right : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [FiniteDimensional K L] [inst_8 : MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal]
  (D : Type u_5) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D] [IsGalois K L]
  [inst_20 : Algebra K D] [IsScalarTower K D L], p ≠ ⊥ → Module.finrank K D = (p.primesOver B).ncard
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceSucc : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.mul_def : ∀ {α : Type u_1} {r : α → α → Prop} (f g : r ↪r r), f * g = g.trans f
-- Init.Data.SInt.Bitwise
ISize.or_not_self : ∀ {a : ISize}, a ||| ~~~a = -1
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.iff_isConstructible_of_isOpenCover : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X}
  [PrespectralSpace X] [QuasiSeparatedSpace X],
  TopologicalSpace.IsOpenCover U →
    (∀ (i : ι), IsCompact ↑(U i)) →
      (Topology.IsLocallyConstructible s ↔ ∀ (i : ι), Topology.IsConstructible (s ∩ ↑(U i)))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.map_mem : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (N : M.Submodule) {X Y : Cᵒᵖ} (f : X ⟶ Y) {x : ↑(M.obj X)},
  x ∈ N.obj X → (CategoryTheory.ConcreteCategory.hom (M.map f)) x ∈ N.obj Y
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The trivial pre-`1`-hypercover of `S` with a single component `S`.  -/
CategoryTheory.PreOneHypercover.trivial : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (S : C) → CategoryTheory.PreOneHypercover S
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.deleteMin : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {s' s : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.WF le s →
    Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s') → Batteries.PairingHeapImp.Heap.WF le s'
-- Mathlib.Order.CompleteLattice.Basic
iInf_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {g : β → α} {f : ι → β},
  ⨅ b ∈ Set.range f, g b = ⨅ i, g (f i)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (x : M) (y : ↥S), AddLocalization.mk x y = x -ₒ y
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsSubordinate.infPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)}
  [inst : Fintype ι], π.IsSubordinate r → ∀ (π' : BoxIntegral.Prepartition I), (π.infPrepartition π').IsSubordinate r
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂)[k]? = m₁[k]?
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedRing : Inhabited Lean.Meta.Grind.Arith.CommRing.Ring
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.below : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv1 a a_1 → Prop} →
        {a : ℕ} → {a_1 : Std.HashMap α ℕ} → Std.Sat.AIG.RelabelNat.State.Inv1 a a_1 → Prop
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.DiscrInfo.mk : Option Lean.Name → Lean.Meta.Match.DiscrInfo
-- Mathlib.Computability.Ackermann
ack_lt_iff_right : ∀ {m n₁ n₂ : ℕ}, ack m n₁ < ack m n₂ ↔ n₁ < n₂
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.epsilon_zero_le_of_omega0_opow_le`. -/
Ordinal.epsilon0_le_of_omega0_opow_le : ∀ {o : Ordinal.{u}}, Ordinal.omega0 ^ o ≤ o → Ordinal.epsilon 0 ≤ o
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsIntCastApply.intCast_apply`. -/
intCast_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : IntCast F} {inst_2 : SMul ℤ α}
  [self : IsIntCastApply F α] (n : ℤ) (x : α), ↑n x = n • x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_idem : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), I.radical.radical = I.radical
-- Mathlib.CategoryTheory.EpiMono
/-- When `g` is a monomorphism, `f ≫ g` is monic iff `f` is.  -/
CategoryTheory.mono_comp_iff_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f) ↔ CategoryTheory.Mono g
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The iteration on a limit element identifies to the colimit of the
value on smaller elements.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.isColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {Φ : CategoryTheory.SmallObject.SuccStruct C} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] →
                [inst_5 : WellFoundedLT J] →
                  {j : J} →
                    (iter : Φ.Iteration j) →
                      (i : J) →
                        Order.IsSuccLimit i →
                          (hij : i ≤ j) →
                            CategoryTheory.Limits.IsColimit (CategoryTheory.SmallObject.coconeOfLE iter.F hij)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.ConnectedComponent.coe_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.toSubgraph.coe = C.toSimpleGraph
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffAt.prodMk : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {x : M} {n : WithTop ℕ∞} {f : M → M'} {g : M → N'},
  ContMDiffAt I I' n f x → ContMDiffAt I J' n g x → ContMDiffAt I (I'.prod J') n (fun x => (f x, g x)) x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸},
  Differentiable 𝕜 a → Differentiable 𝕜 b → Differentiable 𝕜 (a * b)
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed.emptyWff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : Type u_2}, Lean.PrefixTreeNode.WellFormed cmp Lean.PrefixTreeNode.empty
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.tsum_eq_zero_add : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {f : ℕ → G}, Summable f → ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
-- Mathlib.Algebra.Group.Submonoid.Support
/-- **Alias** of `AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem`. -/
AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem₂ : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsPointed → ∀ {x : G}, x ∈ M → -x ∈ M → x = 0
-- Mathlib.NumberTheory.FactorisationProperties
Nat.not_weird_zero : ¬Nat.Weird 0
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.knowsType : Lean.Option Bool
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_counit_tmul_eq : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, CoalgebraStruct.counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a
-- Std.Http.Data.URI.Basic
/-- Sets the host as a domain name, returning `none` if the name contains invalid characters.
The domain name will be automatically lowercased.
Only ASCII alphanumeric characters, hyphens, and dots are allowed.
Each label cannot start or end with `-` and is limited to 63 characters.
Internationalized domain names must be converted to punycode before use.
 -/
Std.Http.URI.Builder.setHost? : Std.Http.URI.Builder → String → Option Std.Http.URI.Builder
-- Mathlib.Topology.MetricSpace.Lipschitz
lipschitzWith_iff_dist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time.  -/
LinearMap : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_16) →
            (M₂ : Type u_17) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → Type (max u_16 u_17)
-- Mathlib.Analysis.Convex.PathConnected
Path.segment_apply : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a b : E) (t : ↑unitInterval), (Path.segment a b) t = (AffineMap.lineMap a b) ↑t
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (m.insertMany l).contains k = (m.contains k || l.contains k)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_one : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), ↑1 = 1
-- Mathlib.CategoryTheory.Yoneda
/-- If `Y` is isomorphic to `X`, representations of `F` by `X` are equivalent
to representations of `F` by `Y`.  -/
CategoryTheory.Functor.RepresentableBy.equivOfIsoObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → {X Y : C} → (Y ≅ X) → F.RepresentableBy X ≃ F.RepresentableBy Y
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.write_mk' : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (b : Γ) (L R : Turing.ListBlank Γ),
  Turing.Tape.write b (Turing.Tape.mk' L R) = Turing.Tape.mk' L (Turing.ListBlank.cons b R.tail)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
DirectedOn.csInf_le : ∀ {α : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → BddBelow s → a ∈ s → sInf s ≤ a
-- Mathlib.Data.List.Sigma
List.sizeOf_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] [inst_1 : SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)),
  sizeOf (List.kerase x xs) ≤ sizeOf xs
-- Mathlib.Order.FixedPoints
/-- **Kleene's fixed point Theorem**: The least fixed point in a complete lattice is
the supremum of iterating a function on bottom arbitrary often.  -/
fixedPoints.lfp_eq_sSup_iterate : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α),
  OmegaCompletePartialOrder.ωScottContinuous ⇑f → OrderHom.lfp f = ⨆ n, (⇑f)^[n] ⊥
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The units of the monoid of non-zero divisors of `M₀` are equivalent to the units of `M₀`.  -/
unitsNonZeroDivisorsEquiv : {M₀ : Type u_1} → [inst : MonoidWithZero M₀] → (↥(nonZeroDivisors M₀))ˣ ≃* M₀ˣ
-- Mathlib.Algebra.Algebra.Epi
Algebra.IsEpi.mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective ⇑(TensorProduct.lift (LinearMap.mul R A)) → Algebra.IsEpi R A
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- A linear functional `φ` can be expressed as a linear combination of linear functionals `f₁,…,fₙ`
if and only if `φ` is continuous with respect to the topology induced by `f₁,…,fₙ`. See
`LinearMap.mem_span_iff_continuous` for a result about arbitrary collections of linear functionals.
 -/
LinearMap.mem_span_iff_continuous_of_finite : ∀ {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [Finite ι] [inst : Field 𝕜] [t𝕜 : TopologicalSpace 𝕜]
  [IsTopologicalRing 𝕜] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [T0Space 𝕜] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜),
  φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous ⇑φ
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_union_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), insert a s ∪ t = s ∪ insert a t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDefinitionParams : Lean.FromJson Lean.Lsp.DefinitionParams
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk'.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃ N) (h : ∀ (x y : M), f (x * y) = f x * f y),
  MulEquiv.mk' f h = { toEquiv := f, map_mul' := h }
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.flip_bijective_iff₁ : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁],
  Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
        (CategoryTheory.CategoryStruct.id Y))
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.newUri : Lean.Lsp.RenameFile → Lean.Lsp.DocumentUri
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} [inst_4 : Inhabited β] {f : Option β → Option β}, m.WF → (m.alter k f)[k]! = (f m[k]?).get!
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm is submultiplicative.  -/
SeminormedRing.norm_mul_le : ∀ {α : Type u_5} [self : SeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_whiskerRight : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} (D : Type u_4) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {F G : CategoryTheory.Functor A B} (η : F ⟶ G)
  (H : CategoryTheory.Functor B C),
  CategoryTheory.Join.mapWhiskerRight (CategoryTheory.Functor.whiskerRight η H) (CategoryTheory.Functor.id D) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft D F H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapWhiskerRight η (CategoryTheory.Functor.id D))
          (CategoryTheory.Join.mapPair H (CategoryTheory.Functor.id D)))
        (CategoryTheory.Join.mapCompLeft D G H).inv)
-- Mathlib.Algebra.Jordan.Basic
_private.Mathlib.Algebra.Jordan.Basic.0.termR : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.continuousWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F}, HasGradientWithinAt f f' s x → ContinuousWithinAt f s x
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_right_assoc : ∀ {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] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (α : G ≅ H) (K : CategoryTheory.Functor D E) {Z : CategoryTheory.Functor B E} (h : F.comp (H.comp K) ≅ Z),
  F.isoWhiskerLeft (CategoryTheory.Functor.isoWhiskerRight α K) ≪≫ h =
    (F.associator G K).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K ≪≫ h
-- Mathlib.Probability.Kernel.Posterior
/-- Posterior of the kernel `κ` with respect to the measure `μ`.  -/
ProbabilityTheory.«term_†_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- Reinterpret `Additive α →+ β` as `α →* Multiplicative β`.  -/
AddMonoidHom.toMultiplicativeRight : {α : Type u_3} →
  {β : Type u_4} → [inst : MulOneClass α] → [inst_1 : AddZeroClass β] → (Additive α →+ β) ≃ (α →* Multiplicative β)
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion_inj_left : ∀ {α : Type u_2} {s₁ s₂ t : Finset α} (h₁ : Disjoint s₁ t) (h₂ : Disjoint s₂ t),
  s₁.disjUnion t h₁ = s₂.disjUnion t h₂ ↔ s₁ = s₂
-- Mathlib.Algebra.Algebra.Unitization
Unitization.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {x y : Unitization R A}, x = y ↔ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 = y.toProd.2
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.addGroupSeminorm.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M},
  QuotientAddGroup.addGroupSeminorm =
    { toFun := fun x => Metric.infDist 0 {m | ↑m = x}, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyBefore.inj : ∀ {s : String.Slice} {pos pos_1 : s.Pos},
  String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos =
      String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos_1 →
    pos = pos_1
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.mk_π : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C)
  (ι : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ pt)
  (hι :
    ∀ ⦃i j : J⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map f.op).app i) (ι i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (ι j))
  (j : J), CategoryTheory.Limits.Multicofork.π (CategoryTheory.Limits.Cowedge.mk pt ι hι) j = ι j
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- The `cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems have a resulting type
that is a big-or of the form `OrOver n (cooper_*_split ...)`. The predicate `(cooper_*_split ...)` has type `Nat → Prop`.
The `cutsat` procedure performs case splitting on `(cooper_*_split ... (n-1))` down to `(cooper_*_split ... 1)`.
If it derives `False` from each case, it uses `orOver_resolve` and `orOver_one` to deduce the final case,
which has type `(cooper_*_split ... 0)`.
 -/
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.PreservesBiproductsOfShape.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  (∀ {f : J → C}, CategoryTheory.Limits.PreservesBiproduct f F) → CategoryTheory.Limits.PreservesBiproductsOfShape J F
-- Mathlib.Analysis.Seminorm
/-- A version of `Seminorm.bound_of_shell` expressed using pointwise scalar multiplication of
seminorms.  -/
Seminorm.bound_of_shell_smul : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p q : Seminorm 𝕜 E) {ε : ℝ} {C : NNReal},
  0 < ε →
    ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ (C • p) x) → ∀ {x : E}, p x ≠ 0 → q x ≤ (C • p) x
-- Init.Data.Ord.Basic
instReprOrdering.repr : Ordering → ℕ → Std.Format
-- Init.Data.List.Basic
List.zipWith.eq_def : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (x : List α) (x_1 : List β),
  List.zipWith f x x_1 =
    match x, x_1 with
    | x :: xs, y :: ys => f x y :: List.zipWith f xs ys
    | x, x_2 => []
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quotient_map_out_comp_out : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomotopyCategory V c} (f : C ⟶ D) (g : D ⟶ E),
  (HomotopyCategory.quotient V c).map (CategoryTheory.CategoryStruct.comp (Quot.out f) (Quot.out g)) =
    CategoryTheory.CategoryStruct.comp f g
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.map_mul : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : NonUnitalNonAssocSemiring R] [inst_4 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) {x y : HahnSeries Γ R}, (x * y).map f = x.map f * y.map f
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
lebesgue_number_lemma_of_metric_sUnion : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {s : Set α} {c : Set (Set α)},
  IsCompact s → (∀ t ∈ c, IsOpen t) → s ⊆ ⋃₀ c → ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, Metric.ball x δ ⊆ t
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_mul : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Mul (γ a b)]
  (x y : (a : α) → (b : β a) → γ a b), Sigma.uncurry (x * y) = Sigma.uncurry x * Sigma.uncurry y
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the bot along a Galois coinsertion  -/
GaloisCoinsertion.liftOrderBot : {α : Type u} →
  {β : Type v} →
    {u : α → β} →
      {l : β → α} → [inst : PartialOrder β] → [inst_1 : Preorder α] → [OrderBot α] → GaloisCoinsertion l u → OrderBot β
-- Lean.Util.Path
/-- A `.olean' search path.  -/
Lean.SearchPath : Type
-- Std.Data.HashMap.Basic
/-- Folds the given function over the mappings in the hash map in some order.  -/
Std.HashMap.fold : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → {γ : Type w} → (γ → α → β → γ) → γ → Std.HashMap α β → γ
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_left_injective : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {r : R},
  r ≠ 0 → Function.Injective fun s => (MvPolynomial.monomial s) r
-- Init.Data.UInt.Lemmas
USize.toNat_mod_uInt64Size : ∀ (n : USize), n.toNat % UInt64.size = n.toNat
-- Mathlib.Algebra.Ring.Defs
two_mul : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.one_le_lift_iff : ∀ {a : Cardinal.{u}}, 1 ≤ Cardinal.lift.{v, u} a ↔ 1 ≤ a