mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.InitialSeg
InitialSeg.eq_principalSeg : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s)
  (g : PrincipalSeg r s) (a : α), g.toRelEmbedding a = f a
-- Init.PropLemmas
Bool.dite_else_false_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : p → Bool}, (if h : p then x h else false) = false ↔ ∀ (h : p), x h = false
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_monomial : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], a ≠ 0 → ((Polynomial.monomial n) a).trailingDegree = ↑n
-- Mathlib.Order.Filter.Basic
Filter.eventually_mem_principal : ∀ {α : Type u} (s : Set α), ∀ᶠ (x : α) in Filter.principal s, x ∈ s
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_associator_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Std.Time.Format
/-- Formats a `PlainDateTime` value into an AscTime format string.
 -/
Std.Time.PlainDateTime.toAscTimeString : Std.Time.PlainDateTime → String
-- Mathlib.Geometry.Manifold.IsManifold.Basic
Pregroupoid.mk.congr_simp : ∀ {H : Type u_2} [inst : TopologicalSpace H] (property property_1 : (H → H) → Set H → Prop)
  (e_property : property = property_1)
  (comp :
    ∀ {f g : H → H} {u v : Set H},
      property f u → property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v))
  (id_mem : property id Set.univ)
  (locality :
    ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u)
  (congr : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u),
  { property := property, comp := comp, id_mem := id_mem, locality := locality, congr := congr } =
    { property := property_1, comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_toList_rio : ∀ {n : ℕ}, (*...=n).toList = (*...n + 1).toList
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_eq_singleton : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, (∃ g, ↑H = {g}) ↔ H = ⊥
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
LinearIndependent.sum_smul_of_nondegenerate : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} {M : Type u_4} [inst : Fintype ι] [inst_1 : Finite κ]
  [inst_2 : CommRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v : ι → M},
  LinearIndependent R v → ∀ {A : Matrix κ ι R}, A.Nondegenerate → LinearIndependent R fun i => ∑ j, A i j • v j
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.equivFunOnFinite.congr_simp : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Finite α], Finsupp.equivFunOnFinite = Finsupp.equivFunOnFinite
-- Mathlib.Order.RelIso.Basic
RelIso.symm_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (b : α), f.symm.symm b = f b
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α], uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_mk : ∀ {R : Type u_1} [inst : CommRing R] {toSubsemiring : Subsemiring R}
  (mem_of_isSquare : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) (neg_one_notMem : -1 ∉ toSubsemiring.carrier)
  {x : R},
  x ∈ { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare, neg_one_notMem' := neg_one_notMem } ↔
    x ∈ toSubsemiring
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.image_edgeSet_subset : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G'),
  Sym2.map ⇑f '' G.edgeSet ⊆ G'.edgeSet
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.compCoyonedaIso_hom_app_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X_1 : D)
  (x : F.obj (Opposite.unop X) ⟶ X_1),
  (CategoryTheory.ConcreteCategory.hom ((adj.compCoyonedaIso.hom.app X).app X_1)) x =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X)) (G.map x)
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionTypeName : Lean.Name → Lean.Name
-- Batteries.Data.Array.Merge
/-- Auxiliary definition for `merge`.  -/
Array.merge.go : {α : Type u_1} → (α → α → Bool) → Array α → Array α → Array α → ℕ → ℕ → Array α
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.y_dvd_iff : ∀ {a : ℕ} (a1 : 1 < a) (m n : ℕ), Pell.yn a1 m ∣ Pell.yn a1 n ↔ m ∣ n
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Archimedean equivalence of input is transferred to `HahnSeries.orderTop` equality.  -/
HahnEmbedding.Partial.orderTop_eq_iff : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] (x y : ↥(↑f).domain),
  (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects finite limits, then `F : Cᵒᵖ ⥤ D` reflects finite
colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsFiniteLimits F.rightOp],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k} {h₁ : a ∈ t.insert k v},
  (t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a ⋯
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_ne_nil_iff : ∀ {m n : ℤ}, (m<...=n).toList ≠ [] ↔ m < n
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k k' : α} {f : β k → β k}, (m.modify k f).contains k' = m.contains k'
-- Init.Data.UInt.Lemmas
USize.le_antisymm_iff : ∀ {a b : USize}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Order.ModularLattice
sup_inf_le_assoc_of_le : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x z : α} (y : α), x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.Monadic.step.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((next : α) → motive (some next)) → motive x
-- Mathlib.Tactic.Positivity.Core
/-- `positivity` solves goals of the form `0 ≤ x`, `0 < x` and `x ≠ 0`. The tactic works recursively
according to the syntax of the expression `x`, by attempting to prove subexpressions are
positive/nonnegative/nonzero and combining this into a final proof. This tactic either closes the
goal or fails.

For each subexpression `e`, `positivity` will try to:
* try `@[positivity]`-tagged extensions to recursively prove `e` is positive/nonnegative/nonzero
  based on its subexpressions (see the `positivity` attribute for more details), or
* try the `norm_num` tactic to prove `e` is positive/nonnegative/nonzero, or
* try showing `e : t` is nonnegative because there is a `CanonicallyOrderedAdd t` instance, or
* use a local hypothesis of the form `0 ≤ e`, `0 < e` or `e ≠ 0`.

This tactic is extensible. See the `positivity` attribute documentation for more details.

* `positivity [t₁, …, tₙ]` first executes `have := t₁; …; have := tₙ` in the current goal,
  then runs `positivity`. This is useful when `positivity` needs derived premises such as `0 < y`
  for division/reciprocal, or `0 ≤ x` for real powers.

Examples:
```
example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity

example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity

example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity

example {a b c d : ℝ} (hab : 0 < a * b) (hb : 0 ≤ b) (hcd : c < d) :
    0 < a ^ c + 1 / (d - c) := by
  positivity [sub_pos_of_lt hcd, pos_of_mul_pos_left hab hb]
```
 -/
Mathlib.Tactic.Positivity.positivity : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_succ_assoc : ∀ (i : ℕ) {n m : ℕ} (h : autoParam (n + i = m) SimplexCategory.δ₀Iter_succ._auto_1) {Z : SimplexCategory}
  (h_1 : { len := m + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter (i + 1) ⋯) h_1 =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i h)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) h_1)
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.div_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  AntivaryOn f g₁ s → MonovaryOn f g₂ s → AntivaryOn f (g₁ / g₂) s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
instMulPosStrictMonoIdeal : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], MulPosStrictMono (Ideal A)
-- Init.Data.SInt.Lemmas
Int32.neg_eq_neg_one_mul : ∀ (a : Int32), -a = -1 * a
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_dvd : ∀ {G : Type u} [inst : Monoid G] {n : ℕ}, Monoid.exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- A helper function, providing the lift structure used to construct colimits.  -/
CategoryTheory.MonoOver.liftStructOfHasStrongEpiMonoFactorisation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} →
      [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
        [inst_2 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
          {J : Type u₂} →
            [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) →
                (c : CategoryTheory.Limits.Cocone F) → ⋯.LiftStruct
-- Mathlib.LinearAlgebra.Multilinear.Finsupp
MultilinearMap.freeFinsuppEquiv_def : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : DecidableEq R] [inst_4 : DecidableEq ι'] [inst_5 : (i : ι) → Fintype (κ i)]
  [inst_6 : (i : ι) → DecidableEq (κ i)] (f : ((i : ι) → κ i) × ι' →₀ R),
  MultilinearMap.freeFinsuppEquiv f =
    (LinearEquiv.multilinearMapCongrLeft fun x => finsuppLequivDFinsupp R)
      ((LinearEquiv.multilinearMapCongrRight R (finsuppLequivDFinsupp R)).symm
        (MultilinearMap.freeDFinsuppEquiv ((finsuppLequivDFinsupp R) f)))
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The backwards and forwards edge of `coherentIso` compose to the identity.  -/
SSet.coherentIso.invHomId : SSet.coherentIso.inv.CompStruct SSet.coherentIso.hom (SSet.Edge.id SSet.coherentIso.x₁)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isVonNBounded_image2_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F] {S : Set (ContinuousMultilinearMap 𝕜 E F)},
  Bornology.IsVonNBounded 𝕜 S →
    ∀ {s : Set ((i : ι) → E i)},
      Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 (Set.image2 (fun f x => f x) S s)
-- Mathlib.CategoryTheory.Products.Basic
/-- The Cartesian product of two functors.  -/
CategoryTheory.Functor.prod : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                CategoryTheory.Functor A B → CategoryTheory.Functor C D → CategoryTheory.Functor (A × C) (B × D)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : β → β},
  (Std.DTreeMap.Const.modify t k f).isEmpty = false →
    (Std.DTreeMap.Const.modify t k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!
-- Lean.Message
/-- Returns the error name with which `msg` is tagged, if one exists.

Note that this is distinct from `msg.kind`: the `kind` of a named-error message is not equal to its
name, and there exist message kinds that are not error-name kinds.
 -/
Lean.Message.errorName? : Lean.Message → Option Lean.Name
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Instead of providing all `M →ₗ[R] N ⧸ (I ^ n • ⊤)`, one can just provide
`M →ₗ[R] N ⧸ (I ^ (a n) • ⊤)` for a strictly increasing sequence `a n` to recover all
`M →ₗ[R] N ⧸ (I ^ n • ⊤)`.
 -/
IsAdicComplete.StrictMono.extend : {R : Type u_1} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_5} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {a : ℕ → ℕ} → StrictMono a → ((n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) → (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.WF.alter : ∀ {α : Type u_1} {cut : α → Ordering} {f : Option α → Option α} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  (∀ {x : α} {t' : RBTree.RBNode α} {p : RBTree.RBNode.Path α},
      RBTree.RBNode.zoom cut t = (t', p) →
        f t'.root? = some x →
          RBTree.RBNode.Path.RootOrdered cmp p x ∧ RBTree.RBNode.OnRoot (RBTree.RBNode.cmpEq cmp x) t') →
    RBTree.RBNode.WF cmp t → RBTree.RBNode.WF cmp (RBTree.RBNode.alter cut f t)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a b : α}
  {fallback : β}, cmp a b = Ordering.eq → Std.DTreeMap.Const.getD t a fallback = Std.DTreeMap.Const.getD t b fallback
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instCommRingSubtypeMemAddSubgroup : {R : Type u_1} → [inst : CommRing R] → [inst_1 : StarRing R] → CommRing ↥(selfAdjoint R)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl.eq_1 : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f),
  MvPolynomial.killCompl hf =
    MvPolynomial.aeval fun i => if h : i ∈ Set.range f then MvPolynomial.X ((Equiv.ofInjective f hf).symm ⟨i, h⟩) else 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Ric α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_splits_of_isPrimitiveRoot : ∀ {K : Type u} [inst : Field K] {n : ℕ} {ζ : K},
  IsPrimitiveRoot ζ n → ∀ {α a : K}, α ^ n = a → (Polynomial.X ^ n - Polynomial.C a).Splits
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.map_eq_mapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → δ a),
  Std.DHashMap.Internal.Raw₀.map f m = m.mapₘ f
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_div : ∀ {a b : UInt64}, (a / b).toBitVec = a.toBitVec / b.toBitVec
-- Init.Data.Fin.Lemmas
Fin.reverseInduction_castSucc : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive (Fin.last n)}
  {succ : (i : Fin n) → motive i.succ → motive i.castSucc} (i : Fin n),
  Fin.reverseInduction zero succ i.castSucc = succ i (Fin.reverseInduction zero succ i.succ)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.union : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s =ᶠ[l] t → s' =ᶠ[l] t' → s ∪ s' =ᶠ[l] t ∪ t'
-- Mathlib.Algebra.Lie.Extension
LieHom.range_eq_ker_iff : ∀ {R : Type u_1} {N : 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 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M),
  i.range = LieIdeal.toLieSubalgebra R L p.ker ↔ Function.Exact ⇑i ⇑p
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_def : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam = ⨆ p, G.edist p.1 p.2
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mk_eq_top : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (carrier : AddSubmonoid M) (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier),
  { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊤ ↔ carrier = ⊤
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.opLinearEquiv_toAddEquiv : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (MulOpposite.opLinearEquiv R).toAddEquiv = MulOpposite.opAddEquiv
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.instDecidableEqGraphRel.decEq : {a : ℕ} → (x x_1 : FirstOrder.Language.graphRel a) → Decidable (x = x_1)
-- Mathlib.GroupTheory.Coset.Card
/-- **Lagrange's Theorem**: The order of an additive
subgroup divides the order of its ambient additive group. 

[Wikidata Q505798](https://www.wikidata.org/wiki/Q505798) -/
AddSubgroup.card_addSubgroup_dvd_card : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Nat.card ↥s ∣ Nat.card α
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : CategoryTheory.Functor C Dᵒᵖ) (X_1 : C),
  ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.pack.fun_cases_unfolding : ∀ (spec : Float.Model.Format) (motive : Float.Model.UnpackedFloat → BitVec spec.numBits → Prop),
  motive Float.Model.UnpackedFloat.notANumber (Float.Model.UnpackedFloat.packedNaN spec) →
    (∀ (s : Float.Model.UnpackedFloat.Sign),
        motive (Float.Model.UnpackedFloat.infinity s) (Float.Model.UnpackedFloat.packedInfinity spec s)) →
      (∀ (s : Float.Model.UnpackedFloat.Sign),
          motive (Float.Model.UnpackedFloat.zero s) (Float.Model.UnpackedFloat.packedZero spec s)) →
        (∀ (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ) (mantissa_pos : 0 < m),
            have biasedExponent := (e + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat;
            2 ^ spec.exponentBits ≤ biasedExponent + 1 →
              motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)
                (Float.Model.UnpackedFloat.packedInfinity spec s)) →
          (∀ (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ) (mantissa_pos : 0 < m),
              have actualMantissaBits := m.log2;
              have biasedExponent := (e + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat;
              ¬2 ^ spec.exponentBits ≤ biasedExponent + 1 →
                actualMantissaBits + 1 = spec.mantissaBits →
                  motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)
                    (Float.Model.UnpackedFloat.packComponents spec s (BitVec.ofNat spec.exponentBits biasedExponent)
                      (BitVec.ofNat spec.mantissaBitsWithoutImplicit m))) →
            (∀ (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ) (mantissa_pos : 0 < m),
                have actualMantissaBits := m.log2;
                have biasedExponent := (e + ↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit).toNat;
                ¬2 ^ spec.exponentBits ≤ biasedExponent + 1 →
                  ¬actualMantissaBits + 1 = spec.mantissaBits →
                    motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)
                      (Float.Model.UnpackedFloat.packComponents spec s (0#spec.exponentBits)
                        (BitVec.ofNat spec.mantissaBitsWithoutImplicit m))) →
              ∀ (x : Float.Model.UnpackedFloat), motive x (Float.Model.UnpackedFloat.pack spec x)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l l_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_3 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l_2 = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r), h with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_2@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r), h_3 =>
      h_2 size k v l l_2 size_2 k_2 v_2 l_3 r h h_3) =
    h_2 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ h