mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.pow_finrank_eq_natCard : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_3) [inst_1 : AddCommGroup k] [Finite k] [inst_3 : Module (ZMod p) k],
  p ^ Module.finrank (ZMod p) k = Nat.card k
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.flatMapM.eq_1 : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : Std.Iterator α Id β]
  [inst_3 : Std.Iterator α₂ m γ] (f : β → m (Std.IterM m γ)) (it : Std.Iter β),
  Std.Iter.flatMapM f it = Std.Iter.flatMapAfterM f it none
-- Mathlib.Tactic.GRewrite.Elab
/-- Mostly analogous to `elabRewrite`.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.elabGRewrite : Lean.MVarId →
  Lean.Expr →
    Lean.Syntax →
      Bool → Bool → Mathlib.Tactic.GRewrite.Config → Lean.Elab.Tactic.TacticM Mathlib.Tactic.GRewrite.GRewriteResult
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_map₂ : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{u_1, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ]
  (pkg'' : AbstractCompletion.{vγ, uγ} γ) (f : α → β → γ), UniformContinuous₂ (pkg.map₂ pkg' pkg'' f)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_add : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f g : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral (f + g) = MeasureTheory.L1.integral f + MeasureTheory.L1.integral g
-- Mathlib.Analysis.Analytic.Uniqueness
/-- The *identity principle* for analytic functions: If two analytic functions coincide in a whole
neighborhood of a point `z₀`, then they coincide globally along a connected set.
For a one-dimensional version assuming only that the functions coincide at some points
arbitrarily close to `z₀`, see `AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq`.  -/
AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {U : Set E},
  AnalyticOnNhd 𝕜 f U → AnalyticOnNhd 𝕜 g U → IsPreconnected U → ∀ {z₀ : E}, z₀ ∈ U → f =ᶠ[nhds z₀] g → Set.EqOn f g U
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_univ : ∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Algebra.adjoin R Set.univ = ⊤
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix : Bool → Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Init.Data.Option.Lemmas
Option.pelim_join : ∀ {α : Type u_1} {β : Sort u_2} {o : Option (Option α)} {b : β} {f : (a : α) → a ∈ o.join → β},
  o.join.pelim b f = o.pelim b fun o' ho' => o'.pelim b fun a ha => f a ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.isColimitOfPreserves₂.congr_simp : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ hc₁_1 : CategoryTheory.Limits.IsColimit c₁),
  hc₁ = hc₁_1 →
    ∀ {c₂ : CategoryTheory.Limits.Cocone K₂} (hc₂ hc₂_1 : CategoryTheory.Limits.IsColimit c₂),
      hc₂ = hc₂_1 →
        CategoryTheory.Limits.isColimitOfPreserves₂ G hc₁ hc₂ =
          CategoryTheory.Limits.isColimitOfPreserves₂ G hc₁_1 hc₂_1
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The universal morphism out of the coproduct of a set of subobjects,
after using `[WellPowered C]` to reindex by a small type.
 -/
CategoryTheory.Subobject.smallCoproductDesc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [inst_3 : CategoryTheory.Limits.HasCoproducts C] →
          {A : C} →
            (s : Set (CategoryTheory.Subobject A)) →
              (∐ fun j =>
                  CategoryTheory.Subobject.underlying.obj ((equivShrink (CategoryTheory.Subobject A)).symm ↑j)) ⟶
                A
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁),
  (LinearMap.toMatrixAlgEquiv v₁) (f ∘ₗ g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc : ∀ {R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso S).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_eq_empty : ∀ {α : Type u_1} {s t : Set α}, Subtype.val ⁻¹' t = ∅ ↔ s ∩ t = ∅
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `deriv_finsetProd`. -/
deriv_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) → deriv (∏ i ∈ u, f i) x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • deriv (f i) x
-- Mathlib.Order.RelClasses
instIsWellFoundedInvImage : ∀ {α : Type u} {β : Type v} (r : α → α → Prop) [IsWellFounded α r] (f : β → α), IsWellFounded β (InvImage r f)
-- Init.Data.Iterators.Consumers.Total
Std.Iter.Total.mk.inj : ∀ {α β : Type w} {it it_1 : Std.Iter β}, { it := it } = { it := it_1 } → it = it_1
-- Mathlib.Probability.Kernel.Posterior
/-- The posterior is unique up to a `κ ∘ₘ μ`-null set.  -/
ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] (η : ProbabilityTheory.Kernel 𝓧 Ω)
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.bind ⇑κ).compProd η = (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.swap Ω 𝓧) →
    ⇑η =ᵐ[μ.bind ⇑κ] ⇑(ProbabilityTheory.posterior κ μ)
-- Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Matrix.det_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [Nontrivial R] [inst_2 : CommRing S] [inst_3 : LinearOrder S]
  [IsStrictOrderedRing S] {n : Type u_3} [inst_5 : Fintype n] [inst_6 : DecidableEq n] {A : Matrix n n R}
  {abv : AbsoluteValue R S} {x : S},
  (∀ (i j : n), abv (A i j) ≤ x) → abv A.det ≤ (Fintype.card n).factorial • x ^ Fintype.card n
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : SizeOf R] [inst_4 : SizeOf M] (N : ℕ → Submodule R M) (mono : ∀ (i : ℕ), N (i + 1) ≤ N i)
  (smul_le : ∀ (i : ℕ), I • N i ≤ N (i + 1)), sizeOf { N := N, mono := mono, smul_le := smul_le } = 1
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
LinearMap.linearEquivOfInjective_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : FiniteDimensional K V] [inst_6 : FiniteDimensional K V₂]
  {f : V →ₗ[K] V₂} (hf : Function.Injective ⇑f) (hdim : Module.finrank K V = Module.finrank K V₂) (x : V),
  (f.linearEquivOfInjective hf hdim) x = f x
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Auxiliary lemma for `toModuleMonoidAlgebra`.  -/
Rep.to_Module_monoidAlgebra_map_aux : ∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Monoid G] (V : Type u_3) (W : Type u_4)
  [inst_2 : AddCommGroup V] [inst_3 : AddCommGroup W] [inst_4 : Module k V] [inst_5 : Module k W] (ρ : G →* V →ₗ[k] V)
  (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W),
  (∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) →
    ∀ (r : MonoidAlgebra k G) (x : V),
      f ((((MonoidAlgebra.lift k (V →ₗ[k] V) G) ρ) r) x) = (((MonoidAlgebra.lift k (W →ₗ[k] W) G) σ) r) (f x)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskeringLeft_μ_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u_1) [inst_2 : CategoryTheory.Category.{v_1, u_1} E] [inst_3 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (X Y : CategoryTheory.Functor D E) (X_1 : C),
  (CategoryTheory.Functor.LaxMonoidal.μ ((CategoryTheory.Functor.whiskeringLeft C D E).obj F) X Y).app X_1 =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (X.obj (F.obj X_1)) (Y.obj (F.obj X_1)))
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.leftUnitor_hom_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R} (r : R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) (r ⊗ₜ[R] m) = r • m
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toField : {α : Type u_5} → ConditionallyCompleteLinearOrderedField α → Field α
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.mkProjAndCheck : Lean.Name → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxoHasSize : {n : ℕ} → Std.Rxo.HasSize (BitVec n)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.w' : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma R L} (self : CategoryTheory.CommaMorphism Y X),
  CategoryTheory.CategoryStruct.comp Y.hom (L.map self.right) =
    CategoryTheory.CategoryStruct.comp (R.map self.left) X.hom
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), IsCompact ↑s
-- Mathlib.Topology.Algebra.Group.Pointwise
AddAction.isClosedMap_quotient : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup α]
  [inst_3 : AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] [CompactSpace α], IsClosedMap Quotient.mk'
-- Mathlib.Logic.Equiv.Fin.Rotate
/-- Rotate `Fin n` one step to the right.  -/
finRotate : (n : ℕ) → Equiv.Perm (Fin n)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_apply : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ),
  HahnSeries.addOppositeEquiv x = AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }
-- Batteries.Recycling.RBTree.Basic
/-- We are ready to deliver element `v` with right child `r`,
and where `tail` represents all the subtrees we have yet to destructure.  -/
RBTree.RBNode.Stream.cons : {α : Type u_1} → α → RBTree.RBNode α → RBTree.RBNode.Stream α → RBTree.RBNode.Stream α
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.val.injEq : ∀ (a a_1 : Lean.Expr), (Lean.Meta.Match.Example.val a = Lean.Meta.Match.Example.val a_1) = (a = a_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.preimage_β_inv : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (S.unionProd T).preimage (β_ X Y).inv = T.unionProd S
-- Mathlib.Algebra.Group.Basic
one_eq_inv : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, 1 = a⁻¹ ↔ a = 1
-- Mathlib.Analysis.Normed.Group.Ultra
/-- In a group with an ultrametric norm, open balls around 1 of positive radius are open subgroups.
 -/
IsUltrametricDist.ball_openSubgroup : (S : Type u_1) → [inst : SeminormedGroup S] → [IsUltrametricDist S] → {r : ℝ} → 0 < r → OpenSubgroup S
-- Mathlib.Topology.AlexandrovDiscrete
isClopen_iInter₂ : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsClopen (f i j)) → IsClopen (⋂ i, ⋂ j, f i j)
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_prod_le : ∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (s : Set A) (t : Set B),
  Algebra.adjoin R (s ×ˢ t) ≤ (Algebra.adjoin R s).prod (Algebra.adjoin R t)
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- The order reversing bijection that sends a subgroup of `G` to its dual subgroup in `G →* Mˣ`
where `G` is a finite commutative group and `M` is a commutative monoid with enough `n`th roots of
unity, where `n` is the exponent of `G`.
 -/
CommGroup.subgroupOrderIsoSubgroupMonoidHom : (G : Type u_1) →
  (M : Type u_2) →
    [inst : CommGroup G] →
      [Finite G] →
        [inst_2 : CommMonoid M] →
          [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] → Subgroup G ≃o (Subgroup (G →* Mˣ))ᵒᵈ
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piEquivPiSubtypeProd_symm_apply : ∀ {ι : Type u_7} (p : ι → Prop) (Y : ι → Type u_8) [inst : (i : ι) → TopologicalSpace (Y i)] [inst_1 : DecidablePred p]
  (f : ((i : { x // p x }) → Y ↑i) × ((i : { x // ¬p x }) → Y ↑i)) (x : ι),
  (Homeomorph.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- A linear map **has finite range** if its range is finitely generated.  -/
LinearMap.HasFiniteRange : {K : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_4} →
      [inst : Semiring K] →
        [inst_1 : AddCommMonoid V] →
          [inst_2 : Module K V] → [inst_3 : AddCommMonoid V₂] → [inst_4 : Module K V₂] → (V →ₗ[K] V₂) → Prop
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
_private.Mathlib.MeasureTheory.Function.SimpleFuncDense.0.MeasureTheory.SimpleFunc.nearestPtInd.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (N : ℕ) → motive N.succ),
  (match 0 with
    | 0 => h_1 ()
    | N.succ => h_2 N) =
    h_1 ()
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.denote_zip : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α}
  (input : aig.BinaryRefVec len) (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func]
  [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α func] (idx : ℕ) (hidx : idx < len),
  ⟦assign,
      { aig := (Std.Sat.AIG.RefVec.zip aig input func).aig,
        ref := (Std.Sat.AIG.RefVec.zip aig input func).vec.get idx hidx }⟧ =
    ⟦assign, func aig { lhs := input.lhs.get idx hidx, rhs := input.rhs.get idx hidx }⟧
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom : ∀ (R : CommRingCat),
  (AlgebraicGeometry.StructureSheaf.globalSectionsIso ↑R).hom =
    CommRingCat.ofHom (algebraMap (↑R) ((AlgebraicGeometry.structureSheafInType ↑R ↑R).obj.obj (Opposite.op ⊤)))
-- Mathlib.Tactic.FBinop
FBinopElab.SRec.mk.injEq : ∀ (name : Lean.Name) (args : Array Lean.Expr) (name_1 : Lean.Name) (args_1 : Array Lean.Expr),
  ({ name := name, args := args } = { name := name_1, args := args_1 }) = (name = name_1 ∧ args = args_1)
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open lower half-plane is an open set in the complex plane.  -/
Complex.isOpen_im_lt : ∀ (x : ℝ), IsOpen {z | z.im < x}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)} {k k' fallback : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKeyD k' fallback = k
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_sUnion : ∀ {α : Type u_2} [inst : Bornology α] {S : Set (Set α)},
  S.Finite → (Bornology.IsBounded (⋃₀ S) ↔ ∀ s ∈ S, Bornology.IsBounded s)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.instHasOfPostcompPropertySchemeIsAffineHomIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsAffineHom @AlgebraicGeometry.IsSeparated
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_comp_lmapDomain : ∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] {α' : Type u_7} {M' : Type u_8} [inst_1 : AddCommMonoid M']
  [inst_2 : Module R M'] {v' : α' → M'} (f : α → α'),
  Finsupp.linearCombination R v' ∘ₗ Finsupp.lmapDomain R R f = Finsupp.linearCombination R (v' ∘ f)
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.groupEquivQuotientProdSubgroup.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α},
  Subgroup.groupEquivQuotientProdSubgroup =
    Trans.trans
      (Trans.trans
        (Trans.trans (Equiv.sigmaFiberEquiv QuotientGroup.mk).symm
          (Equiv.sigmaCongrRight fun L => ⋯.mpr (id (⋯.mpr (Equiv.refl { x // Quotient.mk'' x = L })))))
        (Equiv.sigmaCongrRight fun x => Subgroup.leftCosetEquivSubgroup (Quotient.out x)))
      (Equiv.sigmaEquivProd (α ⧸ s) ↥s)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.Cauchy.coeff.congr_simp : ∀ {K : Type u_2} [inst : Field K] {ℱ ℱ_1 : Filter (LaurentSeries K)} (e_ℱ : ℱ = ℱ_1) (hℱ : Cauchy ℱ) (a a_1 : ℤ),
  a = a_1 → LaurentSeries.Cauchy.coeff hℱ a = LaurentSeries.Cauchy.coeff ⋯ a_1
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The Euler characteristic of a graded object as a sum over all indices.
The sign at each index is determined by the `ComplexShape.EulerCharSigns` instance.
Defaults to 0 if the support of the ranks of the objects of `X` is infinite.  -/
GradedObject.eulerChar : {R : Type u_1} →
  [inst : Ring R] →
    {ι : Type u_2} → (c : ComplexShape ι) → [c.EulerCharSigns] → CategoryTheory.GradedObject ι (ModuleCat R) → ℤ
-- Mathlib.Order.CompleteLattice.Basic
biInf_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ},
  ⨅ x ∈ s ×ˢ t, f x.1 x.2 = ⨅ a ∈ s, ⨅ b ∈ t, f a b
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.instHashable : Hashable Aesop.IndexMatchLocation
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_sbtw_right : ∀ {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] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Wbtw R w x z → Sbtw R x y z → Sbtw R w y z
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_l_hom : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.l_hom X⟧ = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.Array.mergeSort.eq_1 : ∀ {α : Type u_1} (xs : Array α) (le : α → α → Bool), xs.mergeSort le = (Std.Rii.Sliceable.mkSlice xs *...*).mergeSort le
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_sub : ∀ {R : Type u} (M : Type v) [inst : Sub R] [inst_1 : SubNegZeroMonoid M] (r₁ r₂ : R),
  TrivSqZeroExt.inl (r₁ - r₂) = TrivSqZeroExt.inl r₁ - TrivSqZeroExt.inl r₂
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.Total.toList.congr_simp : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] (it it_1 : Std.Iter.Total β),
  it = it_1 → it.toList = it_1.toList
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} →
      {p₁ p₂ : R ⟶ X} →
        CategoryTheory.JointlyMono₂ p₁ p₂ →
          (s : R ⟶ R) →
            autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂)
                CategoryTheory.SymmetricRelation.symmetry₁._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁)
                  CategoryTheory.SymmetricRelation.symmetry₂._autoParam →
                CategoryTheory.SymmetricRelation p₁ p₂
-- Mathlib.Algebra.Order.Sub.Defs
tsub_add_eq_tsub_tsub_swap : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] (a b c : α),
  a - (b + c) = a - c - b
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.toFun_eq_coe : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β), f.toFun = ⇑f
-- Mathlib.Algebra.Quaternion
/-- Quaternion conjugate as an `AlgEquiv` to the opposite ring.  -/
QuaternionAlgebra.starAe : {R : Type u_3} →
  {c₁ c₂ c₃ : R} → [inst : CommRing R] → QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] (QuaternionAlgebra R c₁ c₂ c₃)ᵐᵒᵖ
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.tendsto_partialSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x →
    ∀ᶠ (y : E) in nhds 0, Filter.Tendsto (fun n => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'Factor.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.convexBodyLT'Factor K =
    2 ^ (NumberField.InfinitePlace.nrRealPlaces K + 2) * NNReal.pi ^ (NumberField.InfinitePlace.nrComplexPlaces K - 1)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  {X Y : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).base = f.base
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectR_swapRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ), κ.swapLeft.sectR = κ.sectL
-- Init.Data.BitVec.Lemmas
BitVec.or_eq_zero_iff : ∀ {w : ℕ} {x y : BitVec w}, x ||| y = 0#w ↔ x = 0#w ∧ y = 0#w
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.erase.eq_1 : ∀ {α : Type u} [inst : BEq α] (as : Array α) (a : α),
  as.erase a =
    match as.finIdxOf? a with
    | none => as
    | some i => as.eraseIdx ↑i ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.neg_pi_div_two_le_arcsin : ∀ (x : ℝ), -(Real.pi / 2) ≤ Real.arcsin x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P = Q → W'.add P Q = W'.dblXYZ P