mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
/-- The tensor `(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)` defining when a connection
`∇` on a Riemannian bundle `(M, V)` is compatible with the metric `g`.  -/
CovariantDerivative.derivMetricTensor : {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] →
                  {F : Type u_4} →
                    [inst_5 : NormedAddCommGroup F] →
                      [inst_6 : NormedSpace ℝ F] →
                        {V : M → Type u_5} →
                          [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] →
                            [inst_8 : (x : M) → NormedAddCommGroup (V x)] →
                              [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] →
                                [inst_10 : FiberBundle F V] →
                                  CovariantDerivative I F V →
                                    [inst_11 : VectorBundle ℝ F V] →
                                      [IsContMDiffRiemannianBundle I 1 F V] →
                                        [ContMDiffVectorBundle 1 F V I] →
                                          [FiniteDimensional ℝ F] →
                                            (x : M) → V x →L[ℝ] V x →L[ℝ] TangentSpace I x →L[ℝ] ℝ
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_le_of_isTriangulatedClosed₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {Q : CategoryTheory.ObjectProperty C} [Q.IsTriangulatedClosed₂]
  [Q.IsClosedUnderIsomorphisms], P ≤ Q → ∀ (n : ℕ), P.extensionProductIter n ≤ Q
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMonoid : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Monoid Y] → Monoid (LocallyConstant X Y)
-- Mathlib.Topology.UniformSpace.Equicontinuity
EquicontinuousAt.equicontinuousWithinAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X},
  EquicontinuousAt F x₀ → ∀ (S : Set X), EquicontinuousWithinAt F S x₀
-- Mathlib.Algebra.MonoidAlgebra.Lift
AddMonoidAlgebra.liftNC_single : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : NonUnitalNonAssocSemiring R] (f : k →+ R)
  (g : Multiplicative G → R) (a : G) (b : k),
  (AddMonoidAlgebra.liftNC f g) (AddMonoidAlgebra.single a b) = f b * g (Multiplicative.ofAdd a)
-- Init.Prelude
/-- Is this syntax a node kind `k` wrapping an `atom _ val`?  -/
Lean.Syntax.matchesLit : Lean.Syntax → Lean.SyntaxNodeKind → String → Bool
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- Intermediate result for `CliffordAlgebraComplex.equiv`: `ℂ` can be converted to
`CliffordAlgebraComplex.Q` above can be converted to.  -/
CliffordAlgebraComplex.ofComplex : ℂ →ₐ[ℝ] CliffordAlgebra CliffordAlgebraComplex.Q
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Monotone.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [inst_2 : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [inst_4 : LinearOrder α] [OrderTopology α]
  [SecondCountableTopology α] [inst : LinearOrder β] [OrderClosedTopology β] {f : β → α}, Monotone f → Measurable f
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- The product over the complement of a finset tends to `1` when the finset grows to cover the
whole space. This does not need a multipliability assumption, as otherwise all such products are
one.  -/
tendsto_tprod_compl_atTop_one : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] (f : α → G),
  Filter.Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) Filter.atTop (nhds 1)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.insert : ∀ {𝕜 : 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 : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → ContMDiffWithinAt I I' n f (insert x s) x
-- Init.Data.Array.Attach
Array.size_unattach : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }}, xs.unattach.size = xs.size
-- Mathlib.Algebra.Quandle
/-- The map `x ↦ x ◃ x` is a bijection.  (This has applications for the
regular isotopy version of the Reidemeister I move for knot diagrams.)
 -/
Rack.selfApplyEquiv : (R : Type u_2) → [Rack R] → R ≃ R
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
DifferentiableAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {x : E},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun x => Complex.exp (f x)) x
-- Mathlib.Algebra.Group.EvenFunction
/-- An odd function vanishes at zero.  -/
Function.Odd.map_zero : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommGroup β] [IsAddTorsionFree β] {f : α → β} [inst_2 : NegZeroClass α],
  Function.Odd f → f 0 = 0
-- Mathlib.Algebra.Quandle
Rack.invAct_act_eq : ∀ {R : Type u_1} [inst : Rack R] (x y : R), Rack.invAct x (Shelf.act x y) = y
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coe_ofRingCon : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {c : RingCon R}, ↑{ ringCon := c } = {x | c x 0}
-- Mathlib.RingTheory.Coalgebra.Quotient
/-- A submodule is a coideal iff the counit vanishes on it and its comultiplication image lies
in `I ⊗ C + C ⊗ I`, the textbook form of the coideal condition.  -/
Submodule.isCoideal_iff_comul_mem : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C),
  I.IsCoideal ↔
    (∀ x ∈ I, CoalgebraStruct.counit x = 0) ∧
      ∀ x ∈ I, CoalgebraStruct.comul x ∈ (LinearMap.lTensor C I.subtype).range ⊔ (LinearMap.rTensor C I.subtype).range
-- Mathlib.Algebra.Regular.Basic
/-- An element admitting a left inverse is left-regular.  -/
isLeftRegular_of_mul_eq_one : ∀ {R : Type u_1} [inst : Monoid R] {a b : R}, b * a = 1 → IsLeftRegular a
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.le_linearEquiv_of_sSup_eq_top : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [IsSemisimpleModule R M],
  sSup s = ⊤ → ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.multisetProd_map : ∀ {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Multiset α},
  (∀ x ∈ s, f x ≡ g x [ZMOD n]) → (Multiset.map f s).prod ≡ (Multiset.map g s).prod [ZMOD n]
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A terminal object in a preorder `C` is top element for `C`.  -/
CategoryTheory.Limits.IsTerminal.orderTop : {C : Type u} → [inst : Preorder C] → {X : C} → CategoryTheory.Limits.IsTerminal X → OrderTop C
-- Mathlib.Order.Preorder.Finite
Finite.exists_le_minimal : ∀ {α : Type u_2} [inst : Preorder α] [Finite α] {p : α → Prop} {a : α}, p a → ∃ b ≤ a, Minimal p b
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_5),
  (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).X₂ = X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ`, we have that `ζ ^ j - 1` and `ζ ^ i - 1` are
associated for all `i` and `j` coprime with `n`.  -/
IsPrimitiveRoot.associated_pow_sub_one_pow_of_coprime : ∀ {n i j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → i.Coprime n → j.Coprime n → Associated (ζ ^ j - 1) (ζ ^ i - 1)
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.mem_minimalPrimes_iff : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] {I J : Ideal R}, I ∈ J.minimalPrimes ↔ I.IsPrime ∧ J ≤ I
-- Init.Data.UInt.Bitwise
UInt16.and_eq_neg_one_iff : ∀ {a b : UInt16}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Modifies the delaborator so that it annotates the resulting term using `annotateTermInfo`.
 -/
Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo : Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k a : α} {h' : (m.erase k).contains a = true},
  (m.erase k).getKey a h' = m.getKey a ⋯
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeLam : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Algebra.Order.Module.Defs
neg_of_smul_neg_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosReflectLT α β], a • b < 0 → 0 ≤ b → a < 0
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.exists_lift_of_isLocalizedModule : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup N']
  [inst_6 : Module R N'] (S : Submonoid R) (f : N →ₗ[R] N') [IsLocalizedModule S f] [h : Module.FinitePresentation R M]
  (g : M →ₗ[R] N'), ∃ h s, f ∘ₗ h = s • g
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey : BEq Lean.Elab.Tactic.Grind.DSimpCacheKey
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The condition that a cochain complex `K` is (cohomologically) `≥ n`.  -/
CochainComplex.IsGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CochainComplex C ℤ → ℤ → Prop
-- Mathlib.LinearAlgebra.Prod
LinearMap.prod_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (i : M), (f.prod g) i = Function.prod (⇑f) (⇑g) i
-- Mathlib.Data.Fin.Tuple.Basic
Fin.exists_fin_zero_pi : ∀ {α : Fin 0 → Sort u_1} {P : ((i : Fin 0) → α i) → Prop}, (∃ x, P x) ↔ P finZeroElim
-- Mathlib.Data.Real.Sign
Real.sign_eq_zero_iff : ∀ {r : ℝ}, r.sign = 0 ↔ r = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Naturality of the `prodComparison` morphism in a natural transformation.  -/
CategoryTheory.Limits.prodComparison_natural_of_natTrans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  {F : CategoryTheory.Functor C D} {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {H : CategoryTheory.Functor C D}
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (H.obj A) (H.obj B)] (α : F ⟶ H),
  CategoryTheory.CategoryStruct.comp (α.app (A ⨯ B)) (CategoryTheory.Limits.prodComparison H A B) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
      (CategoryTheory.Limits.prod.map (α.app A) (α.app B))
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- `H¹(L_{S/R})` is independent of the presentation chosen.  -/
Algebra.Generators.equivH1Cotangent : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type w} → (P : Algebra.Generators R S ι) → P.toExtension.H1Cotangent ≃ₗ[S] Algebra.H1Cotangent R S
-- Mathlib.Dynamics.OmegaLimit
/-- An element `y` is in the ω-limit set of `s` w.r.t. `f` if the forward images of `s`
frequently (w.r.t. `f`) intersect arbitrary neighbourhoods of `y`.  -/
mem_omegaLimit_iff_frequently₂ : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  (y : β), y ∈ omegaLimit f ϕ s ↔ ∀ n ∈ nhds y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_zero : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (U : SetRel X X), Dynamics.coverMincard T F U 0 = 1
-- Init.Data.String.Basic
String.get_startPos : ∀ {b : String} (h : b.startPos ≠ b.endPos), b.startPos.get h = b.toList.head ⋯
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.mvqpfCofix : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → MvQPF (MvQPF.Cofix F)
-- Mathlib.Order.UpperLower.Closure
LowerSet.erase_sup_Iic : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {a : α},
  a ∈ s → (∀ b ∈ s, a ≤ b → b = a) → s.erase a ⊔ LowerSet.Iic a = s
-- Mathlib.Order.Minimal
Minimal.and_right : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Minimal P x → Q x → Minimal (fun x => P x ∧ Q x) x
-- Mathlib.Order.Hom.WithTopBot
WithTop.coeOrderHom_apply : ∀ {α : Type u_4} [inst : Preorder α], ⇑WithTop.coeOrderHom = WithTop.some
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.ordered_of_ordered_cons : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {z : Std.DTreeMap.Internal.Zipper α β}, (Std.DTreeMap.Internal.Zipper.cons k v t z).Ordered → z.Ordered
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_one_right_eq_nil : ∀ {m : ℕ}, (m<...1).toArray = #[]
-- Mathlib.Algebra.CubicDiscriminant
/-- The roots of a cubic polynomial.  -/
Cubic.roots : {R : Type u_1} → [inst : CommRing R] → [IsDomain R] → Cubic R → Multiset R
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.comp_hom_c_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (α : X ⟶ Y)
  (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ),
  (CategoryTheory.CategoryStruct.comp α β).hom.c.app U =
    CategoryTheory.CategoryStruct.comp (β.hom.c.app U)
      (α.hom.c.app (Opposite.op ((TopologicalSpace.Opens.map β.hom.base).obj (Opposite.unop U))))
-- Init.Data.UInt.Lemmas
USize.toUInt16_mod_of_dvd : ∀ (a b : USize), b.toNat ∣ 65536 → (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Mathlib.Analysis.Convex.Cone.Basic
/-- A proper cone is a pointed cone `C` that is closed. Proper cones have the nice property that
they are equal to their double dual, see `ProperCone.dual_dual`.
This makes them useful for defining cone programs and proving duality theorems.  -/
ProperCone : (R : Type u_2) →
  (E : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [IsOrderedRing R] → [inst_3 : AddCommMonoid E] → [TopologicalSpace E] → [Module R E] → Type u_3
-- Mathlib.Algebra.Star.Pointwise
Set.compl_star : ∀ {α : Type u_1} {s : Set α} [inst : Star α], star sᶜ = (star s)ᶜ
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.eq_of_mem_smul_span_of_index_eq_index : ∀ {ι : Type u_1} (n : ℕ) [NeZero n] [inst : Finite ι] {x y : ι → ℝ},
  x ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) →
    y ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) →
      BoxIntegral.unitPartition.index n x = BoxIntegral.unitPartition.index n y → x = y
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsert.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.containsThenInsert k v t hl = Std.DTreeMap.Internal.Impl.containsThenInsert k v_1 t hl
-- Mathlib.Data.Complex.Basic
Complex.mul_im : ∀ (z w : ℂ), (z * w).im = z.re * w.im + z.im * w.re
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (entries : Array (α × β))
  (indexes : Std.HashMap α (Array ℕ))
  (validity :
    ∀ (k : α) (p : k ∈ indexes),
      let idx := indexes.get k p;
      idx.size > 0 ∧ ∀ i ∈ idx, i < entries.size)
  (entries_1 : Array (α × β)) (indexes_1 : Std.HashMap α (Array ℕ))
  (validity_1 :
    ∀ (k : α) (p : k ∈ indexes_1),
      let idx := indexes_1.get k p;
      idx.size > 0 ∧ ∀ i ∈ idx, i < entries_1.size),
  ({ entries := entries, indexes := indexes, validity := validity } =
      { entries := entries_1, indexes := indexes_1, validity := validity_1 }) =
    (entries = entries_1 ∧ indexes = indexes_1)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R], Int.fract 0 = 0
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.matchesAll : Aesop.RuleSetNameFilter → Bool
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsInertiaField.mk : ∀ {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 B] {P : Ideal B} {E : Type u_6} [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] [toIsGaloisGroup : IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L],
  IsInertiaField K L P E
-- Init.Core
Equivalence.mk : ∀ {α : Sort u} {r : α → α → Prop},
  (∀ (x : α), r x x) → (∀ {x y : α}, r x y → r y x) → (∀ {x y z : α}, r x y → r y z → r x z) → Equivalence r
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k → a ∈ t
-- Mathlib.Topology.Algebra.Module.UniformConvergence
/-- Let `E` be a topological vector space over a normed field `𝕜`, let `α` be any type.
Let `H` be a submodule of `α →ᵤ E` such that the range of each `f ∈ H` is von Neumann bounded.
Then `H` is a topological vector space over `𝕜`,
i.e., the pointwise scalar multiplication is continuous in both variables.

For convenience we require that `H` is a vector space over `𝕜`
with a topology induced by `UniformFun.ofFun ∘ φ`, where `φ : H →ₗ[𝕜] (α → E)`.  -/
UniformFun.continuousSMul_induced_of_range_bounded : ∀ (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup H] [inst_2 : Module 𝕜 H] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E]
  [inst_5 : TopologicalSpace H] [inst_6 : UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E]
  [inst_9 : FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom),
  Topology.IsInducing (⇑UniformFun.ofFun ∘ ⇑φ) →
    (∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) → ContinuousSMul 𝕜 H
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.instInhabitedWalkingParallelPair : Inhabited CategoryTheory.Limits.WalkingParallelPair
-- Lean.Meta.Basic
/-- Pretty-print the given expression.  -/
Lean.Meta.ppExprWithInfos : Lean.Expr → Lean.MetaM Lean.FormatWithInfos
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_eq_zero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ.restrict s = 0 ↔ μ s = 0
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquivKer_apply : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H) (a : α) (g : ↑(⇑f ⁻¹' {f a})),
  ↑((f.fiberEquivKer a) g) = a⁻¹ * ↑g
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- Given `W : MorphismProperty C` and `Z : C`, this is the index type
parametrising the data of a morphism `f : X ⟶ Y` satisfying `W`
and a morphism `X ⟶ Z`.  -/
CategoryTheory.OrthogonalReflection.D₁ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → C → Type (max u v)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A `Subgroup` is isomorphic to its image under an injective function. If you have an isomorphism,
use `MulEquiv.submonoidMap` for better definitional equalities.  -/
Submonoid.equivMapOfInjective : {N : Type u_2} →
  [inst : MulOneClass N] →
    {M : Type u_5} →
      [inst_1 : MulOneClass M] → (S : Submonoid M) → (f : M →* N) → Function.Injective ⇑f → ↥S ≃* ↥(Submonoid.map f S)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.disjoint_genWeightSpaceOf : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] {x : L} {φ₁ φ₂ : R},
  φ₁ ≠ φ₂ → Disjoint (LieModule.genWeightSpaceOf M φ₁ x) (LieModule.genWeightSpaceOf M φ₂ x)
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.proj_comp_transitionMap : ∀ (S : LightProfinite) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (S.proj (n + 1)) (S.diagram.map (Opposite.op (CategoryTheory.homOfLE ⋯))) =
    S.proj n
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.elabNotDefEq : Array Lean.Expr → Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Grind.EMatchTheoremConstraint
-- Std.Http.Data.Body.Full
_private.Std.Http.Data.Body.Full.0.Std.Http.Body.Full.mk : Std.Mutex (Option ByteArray) → Std.Http.Body.Full
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- If a set is `ℝ`-convex for some normed space structure, then it is `ℝ`-convex for the
normed space structure coming from an `IsRCLikeNormedField 𝕜`. Useful when constructing model
spaces to avoid diamond issues when populating the field `convex_range'`.  -/
Convex.convex_isRCLikeNormedField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] [h : IsRCLikeNormedField 𝕜] {s : Set E}, Convex ℝ s → Convex ℝ s
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The second hexagon identity.  -/
CategoryTheory.BraidedCategory.hexagon_reverse : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y))