mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- **Alias** of `AddMonoidHom.domRestrict_range`. -/
AddMonoidHom.restrict_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (K : AddSubgroup G) (f : G →+ N),
  (f.domRestrict K).range = AddSubgroup.map f K
-- Mathlib.Data.Int.GCD
pow_eq_one_iff_of_coprime : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {m n : ℕ}, m.Coprime n → (a ^ m = 1 ∧ a ^ n = 1 ↔ a = 1)
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- The *identity principle* for analytic functions, global version: if two functions are
analytic on a connected set `U` and coincide at points which accumulate to a point `z₀ ∈ U`, then
they coincide globally in `U`.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
see `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`.  -/
AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜},
  AnalyticOnNhd 𝕜 f U →
    AnalyticOnNhd 𝕜 g U → IsPreconnected U → z₀ ∈ U → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) → Set.EqOn f g U
-- Mathlib.Topology.Order.NhdsSet
Iio_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  b < c → Set.Iio c ∈ nhdsSet (Set.Ioc a b)
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_eq_image' : ∀ (n : ℕ), Finset.HasAntidiagonal.antidiagonal n = Finset.image (fun i => (n - i, i)) (Finset.range (n + 1))
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match fuel.succ with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_2 fuel
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.uniformity_eq_seminorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι],
  uniformity (ContinuousMultilinearMap 𝕜 E G) = ⨅ r, ⨅ (_ : r > 0), Filter.principal {f | ‖-f.1 + f.2‖ < r}
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.iSup_primaryComponent_eq_top : ∀ {A : Type u_1} {M : Type u_2} [inst : CommRing A] [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  [IsDedekindDomain A], Module.IsTorsion A M → ⨆ P, Ideal.primaryComponent M P.asIdeal = ⊤
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H0IsoOfIsTrivial.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupCohomology.H0IsoOfIsTrivial A = groupCohomology.H0IsoOfIsTrivial A
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceGE : Lean.Meta.Simp.Simproc
-- Init.Data.List.Basic
List.replicateTR.loop.eq_2 : ∀ {α : Type u} (a : α) (a_1 : List α) (n : ℕ), List.replicateTR.loop a n.succ a_1 = List.replicateTR.loop a n (a :: a_1)
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- `uIcc a b` is the set of elements lying between `a` and `b`, with `a` and `b` included.
Note that we define it more generally in a lattice as `Set.Icc (a ⊓ b) (a ⊔ b)`. In a product type,
`uIcc` corresponds to the bounding box of the two elements.  -/
Set.uIcc : {α : Type u_1} → [Lattice α] → α → α → Set α
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- A fundamental sequence is strictly monotonic.  -/
Ordinal.IsFundamentalSeq.strictMono : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → StrictMono f
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.of_carrier : ∀ (X : TopCat), TopCat.of ↑X = X
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
MonoidAlgebra.instIsCocomm : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A], Coalgebra.IsCocomm R (MonoidAlgebra A X)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isSymm_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm ↔ ∀ (x y : M), (B x) y = (B y) x
-- Std.Sat.CNF.Relabel
_private.Std.Sat.CNF.Relabel.0.Std.Sat.CNF.nonempty_or_impossible : ∀ {α : Type u_1} (f : Std.Sat.CNF α), Nonempty α ∨ ∃ n, f = { clauses := Array.replicate n [] }
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.fold_filterMapM : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← f b
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.Iter.filterMapM f it) ⦃Q⦄
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instAddMonoid : {ι : Type u_1} → {M : Type u_3} → [inst : AddMonoid M] → AddMonoid (ι →₀ M)
-- Mathlib.Topology.Order.Basic
exists_Ioc_subset_of_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhds a → ∀ {l : α}, l < a → ∃ l' ∈ Set.Ico l a, Set.Ioc l' a ⊆ s
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Icc_succ_left_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ b → insert a (Set.Icc (Order.succ a) b) = Set.Icc a b
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.coeff_coeff_sumAlgEquiv_apply_apply_apply : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : AddMonoidAlgebra R (S₁ ⊕ S₂ →₀ ℕ))
  (a_1 : S₁ →₀ ℕ) (b : S₂ →₀ ℕ), (((MvPolynomial.sumAlgEquiv R S₁ S₂) a).coeff a_1).coeff b = a.coeff (a_1.sumElim b)
-- Mathlib.Data.Fin.Parity
Fin.even_add_one_iff_odd : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Even (k + 1) ↔ Odd k
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyLED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α → α
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_inverse_map : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N) {X Y : CategoryTheory.SingleObj N}
  (a : N), e.toSingleObjEquiv.inverse.map a = e.symm a
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- `MonoidHom.toAdditiveLeft` as a `MulEquiv`.  -/
MonoidHom.toAdditiveLeftMulEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Monoid M] → [inst_1 : AddCommMonoid N] → (M →* Multiplicative N) ≃* Multiplicative (Additive M →+ N)
-- Mathlib.Order.Lattice
Function.Injective.semilatticeSup.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Max α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : SemilatticeSup β] (f : α → β)
  (hf_inj : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y)
  (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b),
  Function.Injective.semilatticeSup f hf_inj le lt map_sup =
    { toPartialOrder := Function.Injective.partialOrder f hf_inj ⋯ ⋯, sup := fun a b => a ⊔ b, le_sup_left := ⋯,
      le_sup_right := ⋯, sup_le := ⋯ }
-- Mathlib.Combinatorics.Additive.Dissociation
/-- The span of a finset `s` is the finset of elements of the form `∑ a ∈ s, ε a • a`
where `ε ∈ {-1, 0, 1} ^ s`.

This is an analog of the linear span in a vector space, but with the "scalars" restricted to
`0` and `±1`.  -/
Finset.addSpan : {α : Type u_1} → [AddCommGroup α] → [DecidableEq α] → [Fintype α] → Finset α → Finset α
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 f s x → derivWithin (c • f) s x = c x • derivWithin f s x + derivWithin c s x • f x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_union : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  Disjoint s₁ s₂ → ∑ x ∈ s₁ ∪ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.pos : ∀ (p q : ENNReal) [p.HolderConjugate q], 0 < p
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The kernel of `S.normedMk` is `S`.  -/
AddSubgroup.ker_normedMk : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), S.normedMk.ker = S
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_reindex_inv : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)] (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f (ε b))
      (CategoryTheory.Limits.Sigma.reindex ε f).inv =
    CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.fieldAutoParam.injEq : ∀ (fieldName structName fieldName_1 structName_1 : Lean.Name),
  (Lean.Elab.Term.TacticMVarKind.fieldAutoParam fieldName structName =
      Lean.Elab.Term.TacticMVarKind.fieldAutoParam fieldName_1 structName_1) =
    (fieldName = fieldName_1 ∧ structName = structName_1)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcompFunctor_obj : ∀ (C : Type u_1) {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] (A : Type u_5)
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] (F : CategoryTheory.SingleFunctors C D A),
  (CategoryTheory.SingleFunctors.postcompFunctor C A G).obj F = F.postcomp G
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
jacobiSym.even_odd : ∀ {a : ℤ} {b : ℕ},
  a % 2 = 0 → b % 2 = 1 → (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (a / 2) b else jacobiSym (a / 2) b) = jacobiSym a b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.mul_vlt_mul_iff_left`. -/
ValuativeRel.vlt_mul_right_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ z → (x * z <ᵥ y * z ↔ x <ᵥ y)
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typesGrothendieckTopology_eq_canonical : CategoryTheory.typesGrothendieckTopology = CategoryTheory.Sheaf.canonicalTopology (Type u)
-- Std.Sync.CancellationToken
Std.CancellationReason.custom.sizeOf_spec : ∀ (msg : String), sizeOf (Std.CancellationReason.custom msg) = 1 + sizeOf msg
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filterMap.go.eq_def : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a))
  (acc : Std.DHashMap.Internal.AssocList α γ) (a : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.filterMap.go✝ f acc a =
    match a with
    | Std.DHashMap.Internal.AssocList.nil => acc
    | Std.DHashMap.Internal.AssocList.cons k v t =>
      match f k v with
      | none => Std.DHashMap.Internal.AssocList.filterMap.go✝ f acc t
      | some v' => Std.DHashMap.Internal.AssocList.filterMap.go✝ f (Std.DHashMap.Internal.AssocList.cons k v' acc) t
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L],
  ⨆ α, ⨆ (_ : α.IsNonZero), LieAlgebra.IsKilling.corootSubmodule α = H.toLieSubmodule
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddSubgroup.isAddCyclic_of_le : ∀ {G : Type u_2} [inst : AddGroup G] {H H' : AddSubgroup G}, H ≤ H' → ∀ [IsAddCyclic ↥H'], IsAddCyclic ↥H
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V : E → E} {s : Set E}, VectorField.lieBracketWithin 𝕜 V V s = 0
-- Mathlib.Algebra.Quaternion
Quaternion.smul_coe : ∀ {R : Type u_3} [inst : CommRing R] (x y : R), x • ↑y = ↑(x * y)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_range_comap_of_surjective : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → IsClosed (Set.range (PrimeSpectrum.comap f))
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
of `s`, and over all subsets of `s` to which one adds `x`.  -/
Finset.prod_powerset_cons : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : CommMonoid β] (ha : a ∉ s) (f : Finset α → β),
  ∏ t ∈ (Finset.cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.lt_one_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R], v.IsEquiv w → ∀ {x : R}, v x < 1 ↔ w x < 1
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
RootPairing.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] (s : Set ι),
  LinearIndepOn R (⇑P.root) s →
    (∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)) →
      ∀ (f : M →+ ℚ), (∀ i ∈ s, f (P.root i) = 1) → s = IsAddIndecomposable.baseOf (⇑P.root) f
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
/-- If `F` is a monoidal functor out of `Type`, it takes the (n+1)st Cartesian power
of a type to the image of that type, tensored with the image of the nth Cartesian power.  -/
CategoryTheory.MonoidalFunctor.mapPi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (F : CategoryTheory.Functor (Type u_2) C) →
        [F.Monoidal] →
          (n : ℕ) →
            (β : Type u_2) →
              F.obj (Fin (n + 1) → β) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj β) (F.obj (Fin n → β))
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- If `g` has a closable extension `f`, then `g` itself is closable.  -/
LinearPMap.IsClosable.leIsClosable : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f g : E →ₗ.[R] F}, f.IsClosable → g ≤ f → g.IsClosable
-- Mathlib.Order.Defs.Unbundled
IsTrans.mk : ∀ {α : Sort u_1} {r : α → α → Prop}, (∀ (a b c : α), r a b → r b c → r a c) → IsTrans α r
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- `FactorSet α` representation elements of unique factorization domain as multisets.
`Multiset α` produced by `normalizedFactors` are only unique up to associated elements, while the
multisets in `FactorSet α` are unique by equality and restricted to irreducible elements. This
gives us a representation of each element as a unique multisets (or the added ⊤ for 0), which has a
complete lattice structure. Infimum is the greatest common divisor and supremum is the least common
multiple.
 -/
Associates.FactorSet : (α : Type u) → [CommMonoidWithZero α] → Type u
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.neg_left_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy (-a) x y ↔ SemiconjBy a x y
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If an intermediate field of `E / F` is separable over `F`, and `E` is purely inseparable
over it, then it is equal to the separable closure of `F` in `E`.  -/
eq_separableClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [Algebra.IsSeparable F ↥L] [IsPurelyInseparable (↥L) E], L = separableClosure F E
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.GeometricallyReduced.geometrically_isReduced : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.GeometricallyReduced f],
  AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced f
-- Std.Time.Date.Basic
Std.Time.instHAddOffset_3 : HAdd Std.Time.Minute.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Mathlib.Topology.Algebra.Monoid
monoidHomOfMemClosureRangeCoe_apply : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : MulOneClass M₁]
  [inst_3 : MulOneClass M₂] [inst_4 : ContinuousMul M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂]
  [inst_6 : MonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun f x => f x)),
  ⇑(monoidHomOfMemClosureRangeCoe f hf) = f
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Monotone.mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Preorder M₀] [inst_3 : Preorder α]
  {f g : α → M₀} [PosMulMono M₀] [MulPosMono M₀],
  Monotone f → Monotone g → (∀ (x : α), 0 ≤ f x) → (∀ (x : α), 0 ≤ g x) → Monotone (f * g)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_empty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α], Std.DTreeMap.Internal.Impl.empty.Ordered
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The vanishing ideal sheaf of a closed set,
which is the largest ideal sheaf whose support is equal to it.
The reduced induced scheme structure on the closed set is the quotient of this ideal.  -/
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal : {X : AlgebraicGeometry.Scheme} → TopologicalSpace.Closeds ↥X → X.IdealSheafData
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.throwFailed : {α : Type} → Lean.Meta.SizeOfSpecNested.M α
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.unitCompPartialBijective.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (A : C) {B : C} (hB : i.essImage B),
  CategoryTheory.unitCompPartialBijective A hB =
    Trans.trans
      (Trans.trans ((CategoryTheory.Iso.refl A).homCongr hB.getIso.symm)
        (CategoryTheory.unitCompPartialBijectiveAux A hB.witness))
      ((CategoryTheory.Iso.refl (i.obj ((CategoryTheory.reflector i).obj A))).homCongr hB.getIso)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.inhabited : {K : Type u_1} →
  {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → [Inhabited Λ] → Inhabited (Turing.TM2to1.Λ' K Γ Λ σ)
-- Mathlib.Order.CompleteLattice.Basic
iSup_pos : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α} (hp : p), ⨆ (h : p), f h = f hp
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `CostructuredArrow.post` is a special case of `CostructuredArrow.map₂` up to natural
isomorphism.  -/
CategoryTheory.CostructuredArrow.postIsoMap₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (S : C) →
              (F : CategoryTheory.Functor B C) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.CostructuredArrow.post F G S ≅
                    CategoryTheory.CostructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (F.comp G))
                      (CategoryTheory.CategoryStruct.id (G.obj S))
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- Recursion principle for `Multiplicative`, supported by `cases` and `induction`.  -/
Multiplicative.rec : {α : Type u} →
  {motive : Multiplicative α → Sort u_1} →
    ((a : α) → motive (Multiplicative.ofAdd a)) → (a : Multiplicative α) → motive a
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Iio : ∀ {a : ℝ}, MeasureTheory.volume (Set.Iio a) = ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ)
  (acc lhs rhs : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr acc).aig.decls.size
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_pair : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {p₁ p₂ : P}, List.Sbtw R [p₁, p₂] ↔ p₁ ≠ p₂
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- We construct a bijection between morphisms `L(A ⊗ B) ⟶ X` and morphisms `LA ⊗ LB ⟶ X`.
This bijection has two key properties:
* It is natural in `X`: See `bijection_natural`.
* When `X = LA ⨯ LB`, then the backwards direction sends the identity morphism to the product
  comparison morphism: See `bijection_symm_apply_id`.

Together these help show that `L` preserves binary products. This should be considered
*internal implementation* towards `preservesBinaryProductsOfExponentialIdeal`.
 -/
CategoryTheory.bijection : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (i : CategoryTheory.Functor D C) →
          [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
            [inst_3 : CategoryTheory.Reflective i] →
              [inst_4 : CategoryTheory.MonoidalClosed C] →
                [inst_5 : CategoryTheory.CartesianMonoidalCategory D] →
                  [CategoryTheory.ExponentialIdeal i] →
                    [CategoryTheory.BraidedCategory C] →
                      (A B : C) →
                        (X : D) →
                          ((CategoryTheory.reflector i).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B) ⟶ X) ≃
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.reflector i).obj A)
                                ((CategoryTheory.reflector i).obj B) ⟶
                              X)