mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- Turn an element of a type `F` satisfying `CocompactMapClass F α β` into an actual
`CocompactMap`. This is declared as the default coercion from `F` to `CocompactMap α β`.  -/
CocompactMapClass.toCocompactMap : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : FunLike F α β] → [CocompactMapClass F α β] → F → CocompactMap α β
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.ext_iff : ∀ {R : Type u_2} {A : Type u_3} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : Coalgebra R A} {x y : GroupLike R A}, x = y ↔ ↑x = ↑y
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectOutput.below.direct : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive : (a : Std.IterM m β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} {it : Std.IterM m β} {out : β}
  (a : it.IsPlausibleOutput out), Std.IterM.IsPlausibleIndirectOutput.below ⋯
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.prodMk_space : ∀ {𝕜 : 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'] {E'' : Type u_8} [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E'']
  {s : Set M} {x : M} {f : M → E'} {g : M → E''}, MDiffAt[s] f x → MDiffAt[s] g x → (MDiffAt[s] fun x => (f x, g x)) x
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.PulledChunk.mk : Bool → Bool → Std.Http.Chunk → Std.Http.Protocol.H1.PulledChunk
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldr.eq_def : ∀ {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) (x : RBTree.RBNode.Stream α) (x_1 : σ),
  RBTree.RBNode.Stream.foldr f x x_1 =
    match x, x_1 with
    | RBTree.RBNode.Stream.nil, b => b
    | RBTree.RBNode.Stream.cons v r tail, b => f v (RBTree.RBNode.foldr f r (RBTree.RBNode.Stream.foldr f tail b))
-- Mathlib.Logic.Basic
xor_iff_not_iff : ∀ (P Q : Prop), Xor P Q ↔ ¬(P ↔ Q)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.Pattern.Model.find?_eq_some_iff.match_1_2.eq_2 : ∀ {s : String.Slice} (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (startPos endPos : s.Pos)
  (h_1 : (s_1 endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched s_1 endPos))
  (h_2 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos)),
  (match String.Slice.Pattern.SearchStep.rejected startPos endPos with
    | String.Slice.Pattern.SearchStep.matched s_1 endPos => h_1 s_1 endPos
    | String.Slice.Pattern.SearchStep.rejected startPos endPos => h_2 startPos endPos) =
    h_2 startPos endPos
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.polarBilin_prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P),
  (Q₁.prod Q₂).polarBilin =
    LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.isStarProjection_inr_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] {p : A}, IsStarProjection ↑p ↔ IsStarProjection p
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableAtom_of_measurableSingletonClass : ∀ {β : Type u_2} [inst : MeasurableSpace β] [MeasurableSingletonClass β] (x : β), measurableAtom x = {x}
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates colimits of shape `Jᵒᵖ`, then `F : C ⥤ Dᵒᵖ` creates limits
of shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C Dᵒᵖ) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F.leftOp] → CategoryTheory.CreatesLimitsOfShape J F
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_zero : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  WithVal.toVal v 0 = 0
-- Mathlib.Algebra.Notation.Defs
Zero.instNonempty : ∀ {α : Type u} [Zero α], Nonempty α
-- Lean.Expr
Lean.mkNatLitCore : Lean.Expr → Lean.Expr
-- Mathlib.Control.Functor
Functor.Const.ext : ∀ {α : Type u_1} {β : Type u_2} {x y : Functor.Const α β}, x.run = y.run → x = y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {ρ : Type u_1} [inst_1 : ForIn Id ρ α]
  (t t_1 : Std.ExtTreeSet α cmp), t = t_1 → ∀ (l l_1 : ρ), l = l_1 → t.insertMany l = t_1.insertMany l_1
-- Mathlib.Analysis.InnerProductSpace.LinearMap
flip_innerSL_real : ∀ (F : Type u_3) [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F], (innerSL ℝ).flip = innerSL ℝ
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.eventually_mul_le : ∀ {u : ℕ → EReal} {a : EReal}, a < LinearGrowth.linearGrowthInf u → ∀ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : MulOneClass α],
  Set.singletonMonoidHom = { toFun := Set.singletonMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurveAt_comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ a : ℝ},
  a ≠ 0 → (IsMIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a) ↔ IsMIntegralCurveAt γ v t₀)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instVAddCommClassSubtypeMem_2 : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [inst_5 : VAddMemClass S N α] [inst_6 : VAddAssocClass M N α] (s : S)
  [VAddCommClass N M α], VAddCommClass N M ↥s
-- Mathlib.Lean.Elab.InfoTree
/-- Finds the first result of `← f ctx info children` which is `some a`, descending the
tree from the top. Merges and updates contexts as it descends the tree.

`f` is **only** evaluated on nodes when some context is present. An initial context should be
provided via the `ctx?` argument if invoking `findSomeM?` during a larger traversal of the
infotree. A failure to provide `ctx? := some ctx` when `t` is not the outermost `InfoTree` is thus
likely to cause `findSomeM?` to always return `none`.
 -/
Lean.Elab.InfoTree.findSomeM? : {m : Type → Type} →
  [Monad m] →
    {α : Type} →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m (Option α)) →
        Lean.Elab.InfoTree → optParam (Option Lean.Elab.ContextInfo) none → m (Option α)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.isAlgebraic : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R], IsTranscendenceBasis R x → Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A
-- Batteries.Linter.UnnecessarySeqFocus
/-- The information we record for each `<;>` node appearing in the syntax.  -/
Batteries.Linter.UnnecessarySeqFocus.Entry : Type
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_comm : ∀ {α : Type u_3} [inst : DivisionSemiring α] (q : ℚ≥0) (a : α), ↑q * a = a * ↑q
-- Std.Http.Data.Response
Std.Http.instInhabitedResponse : {a : Type} → [Inhabited a] → Inhabited (Std.Http.Response a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∉ m → (f (Std.DHashMap.Const.get? m k)).isNone = true → (Std.DHashMap.Const.alter m k f).size = m.size
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.fixedBy.eq_1 : ∀ {M : Type u_1} (α : Type u_3) [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M),
  AddAction.fixedBy α m = {x | m +ᵥ x = x}
-- Mathlib.Logic.Equiv.Defs
/-- See Note [custom simps projection]  -/
Equiv.Simps.symm_apply : {α : Sort u} → {β : Sort v} → α ≃ β → β → α
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedCustomEliminator.default : Lean.Meta.CustomEliminator
-- Mathlib.Algebra.Group.Units.Defs
Units.commute_inv_coe : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), Commute ↑a⁻¹ ↑a
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] [inst_5 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km : α},
        Std.Internal.List.minKey! l = km ↔
          Std.Internal.List.containsKey km l = true ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare km k).isLE = true
-- Mathlib.Data.Multiset.MapFold
Multiset.map_singleton : ∀ {α : Type u_1} {β : Type v} (f : α → β) (a : α), Multiset.map f {a} = {f a}
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesEpimorphisms.iso_iff`. -/
CategoryTheory.Functor.preservesEpimorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.PreservesEpimorphisms ↔ G.PreservesEpimorphisms
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.costructuredArrowRightwards_final_iff_of_iso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ X₃' : C₃} (e : X₃ ≅ X₃'), (w.costructuredArrowRightwards X₃).Final ↔ (w.costructuredArrowRightwards X₃').Final
-- Mathlib.Data.Set.Basic
/-- See also `nonempty_iff_ne_empty'`.  -/
Set.not_nonempty_iff_eq_empty' : ∀ {α : Type u} {s : Set α}, ¬Nonempty ↑s ↔ s = ∅
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.right_inv : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.GrpObj X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.GrpObj.inv)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one
-- Init.Data.BitVec.Basic
/-- Bitwise or for bitvectors. Usually accessed via the `|||` operator.

SMT-LIB name: `bvor`.

Example:
* `0b1010#4 ||| 0b0110#4 = 0b1110#4`
 -/
BitVec.or : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.Topology.MetricSpace.HolderNorm
memHolder_iff_holderWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {r : NNReal} {f : X → Y},
  MemHolder r f ↔ HolderWith (nnHolderNorm r f) r f
-- Mathlib.SetTheory.Ordinal.Topology
/-- A set of ordinals is closed below an ordinal if it contains all of
its accumulation points below the ordinal.  -/
Ordinal.IsClosedBelow : Set Ordinal.{u_1} → Ordinal.{u_1} → Prop
-- Std.Data.ExtDTreeMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.ExtDTreeMap.modify : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → (β a → β a) → Std.ExtDTreeMap α β cmp
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.EquicontinuousWithinAt.mono : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H H' : Set (X → α)} {S : Set X}
  {x₀ : X}, H.EquicontinuousWithinAt S x₀ → H' ⊆ H → H'.EquicontinuousWithinAt S x₀
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.em.sizeOf_spec : ∀ (classical : Bool) (p : Lean.Name),
  sizeOf (Mathlib.Tactic.ITauto.Proof.em classical p) = 1 + sizeOf classical + sizeOf p
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.utf8Len.match_1.eq_1 : ∀ (motive : List Char → Sort u_1) (h_1 : Unit → motive []) (h_2 : (c : Char) → (cs : List Char) → motive (c :: cs)),
  (match [] with
    | [] => h_1 ()
    | c :: cs => h_2 c cs) =
    h_1 ()
-- Mathlib.Topology.ContinuousMap.Basic
Homeomorph.coe_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ), ↑(f.trans g) = (↑g).comp ↑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.TreeMap.Raw.unitOfList l cmp}, (Std.TreeMap.Raw.unitOfList l cmp).getKey k' h' = k
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.append.injEq : ∀ {α : Type u} (a a_1 : Array (Lean.Widget.TaggedText α)),
  (Lean.Widget.TaggedText.append a = Lean.Widget.TaggedText.append a_1) = (a = a_1)
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- A representative of a finite module in the same universe as the ring.  -/
Module.Finite.repr : (R : Type u) →
  (M : Type u_1) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [Module.Finite R M] → Type u
-- Init.Data.Vector.Lemmas
Vector.getElem_setIfInBounds_self : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α} (hi : i < n), (xs.setIfInBounds i x)[i] = x
-- Mathlib.LinearAlgebra.Prod
LinearMap.inl_eq_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.inl R M M₂ = LinearMap.id.prod 0
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
FGAlgCatSkeleton.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)),
  sizeOf { n := n, I := I } = 1 + sizeOf n + sizeOf I
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_im_le_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ‖RCLike.im z‖ ≤ ‖z‖
-- Mathlib.Data.Nat.Cast.Basic
Pi.natCast_def : ∀ {α : Type u_1} {π : α → Type u_3} [inst : (a : α) → NatCast (π a)] (n : ℕ), ↑n = fun x => ↑n
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearMap_ofAlgHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
  (h₂ : g.comp f = AlgHom.id R A₁), (AlgEquiv.ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap
-- Mathlib.Algebra.Star.Basic
starMulAut_apply : ∀ {R : Type u} [inst : CommSemigroup R] [inst_1 : StarMul R] (a : R), starMulAut a = star a
-- Mathlib.Algebra.Group.Basic
const_div_involutive : ∀ {G : Type u_3} [inst : CommGroup G] (a : G), Function.Involutive fun x => a / x
-- Mathlib.Data.ENNReal.Inv
ENNReal.instDivInvOneMonoid : DivInvOneMonoid ENNReal
-- Init.SimpLemmas
bne.eq_1 : ∀ {α : Type u} [inst : BEq α] (a b : α), (a != b) = !a == b
-- Init.Prelude
/-- `a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`. -/
HSMul.hSMul : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HSMul α β γ] → α → β → γ
-- Mathlib.Algebra.Group.PUnit
PUnit.div_eq : ∀ (x y : PUnit.{u_1 + 1}), x / y = PUnit.unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.abs_discr_rpow_ge_of_isTotallyComplex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NumberField.IsTotallyComplex K],
  ↑(Module.finrank ℚ K) ^ 2 / (4 / Real.pi * ↑(Module.finrank ℚ K).factorial ^ (2 * (↑(Module.finrank ℚ K))⁻¹)) ≤
    ↑|NumberField.discr K| ^ (↑(Module.finrank ℚ K))⁻¹
-- Mathlib.Data.Nat.Squarefree
/-- Assuming that `n` has no factors less than `k`, returns the smallest prime `p` such that
`p^2 ∣ n`.  -/
Nat.minSqFacAux : ℕ → ℕ → Option ℕ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_mul : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → MulZeroClass (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)]
  [inst_4 : ∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r : G i)
  (x : RestrictedProduct (fun i => G i) (fun i => ↑(A i)) Filter.cofinite),
  RestrictedProduct.single A i (r * x i) = RestrictedProduct.single A i r * x
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.toAddSubgroup_eq_top : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : NonUnitalSubring R}, S.toAddSubgroup = ⊤ ↔ S = ⊤
-- Mathlib.Data.QPF.Univariate.Basic
QPF.liftpPreservation_iff_uniform : ∀ {F : Type u → Type u} [q : QPF F], QPF.LiftpPreservation ↔ QPF.IsUniform
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.Splits.of_natDegree_le_one_of_monic`. -/
Polynomial.splits_of_natDegree_le_one_of_monic : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree ≤ 1 → f.Monic → f.Splits
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t.toList.isEmpty = t.isEmpty
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesHasSum.neg : ∀ {f : ℕ → ℂ} {s a : ℂ}, LSeriesHasSum f s a → LSeriesHasSum (-f) s (-a)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {a : α} {b : β a},
  (m.getThenInsertIfNew? a b).1 = (Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The restriction of an infinite place along an embedding.  -/
NumberField.InfinitePlace.comap : {k : Type u_1} →
  [inst : Field k] →
    {K : Type u_2} → [inst_1 : Field K] → NumberField.InfinitePlace K → (k →+* K) → NumberField.InfinitePlace k
-- Batteries.Data.NameSet
Lean.NameSet.instInter_batteries : Inter Lean.NameSet
-- Mathlib.Combinatorics.Quiver.Path
Prefunctor.mapPath_comp : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) {a b : V} (p : Quiver.Path a b) {c : V}
  (q : Quiver.Path b c), F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.mutuallySingular_compProd_left_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [MeasureTheory.SigmaFinite ν]
  [ProbabilityTheory.IsSFiniteKernel κ] [hκ : ∀ (x : α), NeZero (κ x)],
  (μ.compProd κ).MutuallySingular (ν.compProd κ) ↔ μ.MutuallySingular ν
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_lt_top : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y},
  eHolderNorm r f < ⊤ ↔ MemHolder r f
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.eq_1 : ∀ (M : Type u_1) [inst : Mul M], SemigroupIdeal M = SubMulAction M M
-- Mathlib.FieldTheory.Finite.Basic
/-- If `p` is a prime natural number and `x` is an integer number, then there exist natural numbers
`a ≤ p / 2` and `b ≤ p / 2` such that `a ^ 2 + b ^ 2 ≡ x [ZMOD p]`. This is a version of
`ZMod.sq_add_sq` with estimates on `a` and `b`.  -/
Nat.sq_add_sq_zmodEq : ∀ (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ), ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
-- Mathlib.Analysis.Complex.Conformal
/-- A complex function is conformal if and only if the function is holomorphic or antiholomorphic
with a nonvanishing differential.  -/
conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj : ∀ {f : ℂ → ℂ} {z : ℂ},
  ConformalAt f z ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (r : ↑(X.presheaf.obj (Opposite.op ⊤))),
  AlgebraicGeometry.IsAffine ↑(X.basicOpen r)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {fallback : α} {he : Std.DTreeMap.Internal.Impl.contains (t.minKeyD fallback) t = true},
      t.getKey (t.minKeyD fallback) he = t.minKeyD fallback
-- Mathlib.RingTheory.Binomial
Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (r : R) (k : ℕ),
  (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.instNormedAddCommGroup : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      [inst : NormedAddCommGroup V] →
        [inst_1 : NormedAddCommGroup W] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 V] → [inst_4 : NormedSpace 𝕜 W] → NormedAddCommGroup (V →ᴬ[𝕜] W)
-- Lean.Level
Lean.Level.PP.Context.mk.inj : ∀ {mvars : Bool} {lIndex? : Lean.LMVarId → Option ℕ} {mvars_1 : Bool} {lIndex?_1 : Lean.LMVarId → Option ℕ},
  { mvars := mvars, lIndex? := lIndex? } = { mvars := mvars_1, lIndex? := lIndex?_1 } →
    mvars = mvars_1 ∧ lIndex? = lIndex?_1
-- Mathlib.Topology.Homotopy.Contractible
Homeomorph.contractibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ContractibleSpace Y]
  (e : X ≃ₜ Y), ContractibleSpace X
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.sigma_factor : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α}, Summable f → ∀ (b : β), Summable fun c => f ⟨b, c⟩
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerRight.injEq : ∀ {C : Type u} {X₁ X₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom X₂)
  (Y : CategoryTheory.FreeMonoidalCategory C) (f_1 : X₁.Hom X₂), (f.whiskerRight Y = f_1.whiskerRight Y) = (f = f_1)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
eq_zero_of_mul_self_add_mul_self_eq_zero : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R]
  [PosMulMono R] [AddLeftMono R], a * a + b * b = 0 → a = 0