mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Basic
pow_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (p : Prop) [inst_1 : Decidable p] (a : α) (b c : β),
  (a ^ if p then b else c) = if p then a ^ b else a ^ c
-- Lean.Level
Lean.Level.brecOn.go : {motive : Lean.Level → Sort u} →
  (t : Lean.Level) → ((t : Lean.Level) → Lean.Level.below t → motive t) → motive t ×' Lean.Level.below t
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.tsupport_mono : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} {k m : ℕ},
  k ≤ m → ↑m ≤ n → HasFTaylorSeriesUpTo n f p → (tsupport fun x => p x m) ⊆ tsupport fun x => p x k
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_filterMapM : ∀ {α β γ δ : Type w} {ps : Std.Do.PostShape} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o] [LawfulMonad o]
  [inst_10 : Std.Do.WPMonad o ps] [inst_11 : Std.IteratorLoop α m n] [inst_12 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_15 : MonadLiftT m n] [inst_16 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← liftM (f b)
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.filterMapM f it) ⦃Q⦄
-- Mathlib.Order.Category.Preord
Preord.Iso.mk_hom : ∀ {α β : Preord} (e : ↑α ≃o ↑β), (Preord.Iso.mk e).hom = Preord.ofHom ↑e
-- Init.Data.SInt.Bitwise
Int64.shiftRight_or : ∀ {a b c : Int64}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0)
      (CategoryTheory.Limits.prod.map f f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) 0)
-- Mathlib.Data.Set.Sigma
Set.uncurry_preimage_sigma_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : (i : ι) → α i → Type u_7} (s : Set ι) (t : (i : ι) → Set (α i))
  (u : (p : (i : ι) × α i) → Set (β p.fst p.snd)),
  Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi fun i => (t i).pi fun j => u ⟨i, j⟩
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.instSubsingletonOfAddArchimedean : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [Archimedean M],
  Subsingleton (FiniteArchimedeanClass M)
-- Mathlib.Geometry.Euclidean.Basic
/-- The distance between two points given with `affineCombination`,
in terms of the pairwise distances between the points in that
combination.  -/
EuclideanGeometry.dist_affineCombination : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ι : Type u_3} {s : Finset ι} {w₁ w₂ : ι → ℝ} (p : ι → P),
  ∑ i ∈ s, w₁ i = 1 →
    ∑ i ∈ s, w₂ i = 1 →
      have a₁ := (Finset.affineCombination ℝ s p) w₁;
      have a₂ := (Finset.affineCombination ℝ s p) w₂;
      dist a₁ a₂ * dist a₁ a₂ =
        (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
-- Mathlib.Algebra.Ring.Divisibility.Basic
map_dvd_iff_dvd_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : Semigroup α] [inst_1 : Semigroup β] {F : Type u_3} [inst_2 : EquivLike F α β]
  [inst_3 : MulEquivClass F α β] (f : F) {a : α} {b : β}, f a ∣ b ↔ a ∣ (↑f).symm b
-- Lean.Meta.WHNF
Lean.Meta.reduceUnaryNatOp : (ℕ → ℕ) → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Group.End
MulAut.one_def : ∀ (M : Type u_2) [inst : Mul M], 1 = MulEquiv.refl M
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.restoreM_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  (x : m (Except ε α)) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp x (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail ⦄ MonadControl.restoreM x ⦃ post;
    epost ⦄
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_1 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_1 ()
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- If `f` is a `C^n` local diffeomorphism of Banach manifolds (`n ≠ 0`),
each differential is a linear equivalence.  -/
IsLocalDiffeomorph.mfderivToContinuousLinearEquiv : {𝕜 : 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] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            IsLocalDiffeomorph I J n f →
                                              n ≠ 0 → (x : M) → TangentSpace I x ≃L[𝕜] TangentSpace J (f x)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_bif' : ∀ {w : ℕ} (d : Bool) (a b c : BitVec w), ((bif d then a else c) == bif d then b else c) = (!d || a == b)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.image_antilipschitz : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {s : Set X}
  {ε K₁ : NNReal} {f : X → Y},
  Metric.IsSeparated (↑ε) s → AntilipschitzWith K₁ f → 0 < K₁ → Metric.IsSeparated (↑(ε / K₁)) (f '' s)
-- Mathlib.Order.Quotient
Quotient.instTotalLe_mathlib : ∀ {α : Type u_1} {s : Setoid α} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.linear_isTheta_left : ∀ (d : ℤ) {z : ℂ}, z ≠ 0 → (fun c => ↑c * z + ↑d) =Θ[Filter.cofinite] fun n => ↑n
-- Mathlib.Order.BooleanAlgebra.Basic
GeneralizedBooleanAlgebra.toOrderBot : {α : Type u} → [inst : GeneralizedBooleanAlgebra α] → OrderBot α
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The right adjoint functor to `L` given by `[ComonadicLeftAdjoint L]`.  -/
CategoryTheory.comonadicRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) → [CategoryTheory.ComonadicLeftAdjoint L] → CategoryTheory.Functor D C
-- Mathlib.GroupTheory.Nilpotent
/-- An additive group is nilpotent if and only if its lower central series eventually
reaches the trivial additive subgroup.  -/
AddSubgroup.nilpotent_iff_lowerCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.IsNilpotent G ↔ ∃ n, ⊤.lowerCentralSeries n = ⊥
-- Init.Data.String.Basic
String.Pos.toReplaceEnd : {s : String} → (p₀ pos : s.Pos) → pos ≤ p₀ → (s.sliceTo p₀).Pos
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.restrict_adj : ∀ {V : Type u} {G : SimpleGraph V} {G' G'' : G.Subgraph} (v w : ↑G'.verts),
  (SimpleGraph.Subgraph.restrict G'').Adj v w ↔ G'.Adj ↑v ↑w ∧ G''.Adj ↑v ↑w
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.or.injEq : ∀ (a a_1 a_2 a_3 : Mathlib.Tactic.ITauto.IProp), (a.or a_1 = a_2.or a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- The space of continuous linear maps equipped with the topology of pointwise convergence,
sometimes also called the *strong operator topology*. We avoid this terminology since so many other
things share similar names, and using "pointwise convergence" in the name is more informative.

This topology is also known as the weak⋆-topology in the case that `σ = RingHom.id 𝕜` and `F = 𝕜`  -/
«term_→SLₚₜ[_]_» : Lean.TrailingParserDescr
-- Lean.Data.Lsp.InitShutdown
/-- If omitted, we default to off.  -/
Lean.Lsp.InitializeParams.trace : Lean.Lsp.InitializeParams → Lean.Lsp.Trace
-- Std.Sat.AIG.RelabelNat
/-- This invariant ensures that we only insert an atom at most once and with a monotonically increasing
index.
 -/
Std.Sat.AIG.RelabelNat.State.Inv1 : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → ℕ → Std.HashMap α ℕ → Prop
-- Init.Internal.Order.Basic
Lean.Order.PProd.snd : {α : Sort u} →
  {β : Sort v} → [Lean.Order.CompleteLattice α] → [Lean.Order.CompleteLattice β] → (α ×' β → Prop) → β → Prop
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquivClass.coe_symm_apply_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Mul α] [inst_1 : Mul β] {F : Type u_11} [inst_2 : EquivLike F α β]
  [inst_3 : MulEquivClass F α β] (e : F) (x : α), (↑e).symm (e x) = x
-- Mathlib.Topology.Irreducible
/-- A preirreducible set `s` is one where there is no non-trivial pair of disjoint opens on `s`.  -/
IsPreirreducible : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, Std.ExtDTreeMap.Const.get? (t.insert k v) k = some v
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instProjectiveOfHasProjectiveDimensionLTOfNatNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  [CategoryTheory.HasProjectiveDimensionLT X 1], CategoryTheory.Projective X
-- Mathlib.Order.Hom.Basic
OrderIso.symm_trans_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ)
  (c : γ), (e₁.trans e₂).symm c = e₁.symm (e₂.symm c)
-- Mathlib.Order.SetAccumulate
Set.disjoint_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α],
  Pairwise (Function.onFun Disjoint s) → ∀ {i j : α}, i < j → Disjoint (Set.accumulate s i) (s j)
-- Mathlib.Data.Nat.Choose.Central
/-- The central binomial coefficient, `Nat.choose (2 * n) n`.
 -/
Nat.centralBinom : ℕ → ℕ
-- Mathlib.Order.CountableDenseLinearOrder
/-- The set of partial isomorphisms defined at `b : β`, together with a proof that any
partial isomorphism can be extended to include `b`. We prove this by symmetry.  -/
Order.PartialIso.definedAtRight : (α : Type u_1) →
  {β : Type u_2} →
    [inst : LinearOrder α] →
      [inst_1 : LinearOrder β] →
        [DenselyOrdered α] → [NoMinOrder α] → [NoMaxOrder α] → [Nonempty α] → β → Order.Cofinal (Order.PartialIso α β)
-- Init.Data.SInt.Basic
/-- Constructs an `Int16` from an `Int`, clamping if the value is too small or too large.  -/
Int16.ofIntClamp : ℤ → Int16
-- Mathlib.Geometry.Manifold.Instances.Icc
Homeomorph.constVSub.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p p_1 : P),
  p = p_1 → Homeomorph.constVSub p = Homeomorph.constVSub p_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.congr_mfderiv : ∀ {𝕜 : 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'} {x : M}
  {f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f' → f' = f₁' → HasMFDerivAt% f x f₁'
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasStrictDerivAt_ofNat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (n : ℕ) [inst_3 : OfNat F n], HasStrictDerivAt (OfNat.ofNat n) 0 x
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsGLB.sub : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G},
  IsGLB s a → IsLUB t b → IsGLB (s - t) (a - b)
-- Init.Data.Dyadic.Basic
Dyadic.toRat_ofIntWithPrec_eq_mul_two_pow : ∀ {n k : ℤ}, (Dyadic.ofIntWithPrec n k).toRat = ↑n * 2 ^ (-k)
-- Mathlib.Algebra.Group.PUnit
PUnit.instAdd_mathlib : Add PUnit.{u_1 + 1}
-- Mathlib.Topology.Order.LeftRight
frequently_lt_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α) [(nhdsWithin a (Set.Iio a)).NeBot],
  ∃ᶠ (x : α) in nhds a, x < a
-- Mathlib.Topology.Order.Rolle
/-- If a function `f` is continuous on an unordered open interval
and tends to the same value at its endpoints,
then it has a local extremum on this unordered open interval.  -/
exists_isLocalExtr_uIoo_of_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
  a ≠ b →
    ContinuousOn f (Set.uIoo a b) →
      Filter.Tendsto f (nhdsWithin a (Set.uIoo a b)) (nhds l) →
        Filter.Tendsto f (nhdsWithin b (Set.uIoo a b)) (nhds l) → ∃ c ∈ Set.uIoo a b, IsLocalExtr f c
-- Init.Data.String.Substring
/-- Returns the ending position of the common prefix, working up from `spos, tpos`.  -/
_private.Init.Data.String.Substring.0.Substring.Raw.commonPrefix.loop : Substring.Raw → Substring.Raw → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Algebra.Quaternion
/-- Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$,
denoted as `ℍ[R,a,b]`.
Implemented as a structure with four fields: `re`, `imI`, `imJ`, and `imK`.  -/
QuaternionAlgebra : (R : Type u_1) → R → R → R → Type u_1
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits FintypeCat.incl
-- Mathlib.NumberTheory.Padics.ProperSpace
/-- The set of p-adic integers `ℤ_[p]` is a compact topological space.  -/
PadicInt.compactSpace : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], CompactSpace ℤ_[p]
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.sSup_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S : Set (IntermediateField F E)), S.Nonempty → (sSup S).toSubfield = sSup (IntermediateField.toSubfield '' S)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.deleteElem_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {I : Set α}, (M.delete {e}).Indep I ↔ M.Indep I ∧ e ∉ I
-- Mathlib.Order.SuccPred.Tree
RootedTree.subtrees.eq_1 : ∀ (t : RootedTree), t.subtrees = {x | IsAtom x.root}
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.card_univ : Ordinal.univ.{u, v}.card = Cardinal.univ.{u, v}
-- Mathlib.GroupTheory.Index
Subgroup.instFiniteIndex_subgroupOf : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) [H.FiniteIndex], (H.subgroupOf K).FiniteIndex
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas.0.RootPairing.termΦ : Lean.ParserDescr
-- Init.Core
Sigma.mk.inj : ∀ {α : Type u} {β : α → Type v} {fst : α} {snd : β fst} {fst_1 : α} {snd_1 : β fst_1},
  ⟨fst, snd⟩ = ⟨fst_1, snd_1⟩ → fst = fst_1 ∧ snd ≍ snd_1
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The `Equiv` underlying an `AddEquiv`.  -/
AddEquiv.toEquiv : {A : Type u_9} → {B : Type u_10} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A ≃ B
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_comp_pseudoEpimorphism : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  (g : EsakiaHom β γ) (f : EsakiaHom α β),
  { toOrderHom := ↑(g.comp f), exists_map_eq_of_map_le' := ⋯ } =
    { toOrderHom := ↑g, exists_map_eq_of_map_le' := ⋯ }.comp { toOrderHom := ↑f, exists_map_eq_of_map_le' := ⋯ }
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_aux : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ) [IsPRadical i p]
  (x : L), ∃ y, i y.2 = x ^ p ^ y.1
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_mapRange_index : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
  [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] [inst_5 : AddCommMonoid γ] {f : (i : ι) → β₁ i → β₂ i}
  {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : (i : ι) → β₂ i → γ},
  (∀ (i : ι), h i 0 = 0) → (DFinsupp.mapRange f hf g).sum h = g.sum fun i b => h i (f i b)
-- Mathlib.Algebra.Group.Basic
multiplicative_of_symm_of_total : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β) [Std.Symm p],
  (∀ {a b : α}, p a b → f a b * f b a = 1) →
    (∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c) →
      ∀ {a b c : α}, p a b → p b c → p a c → f a c = f a b * f b c
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- For every prime `p` dividing the order of a finite additive group `G` there exists an element of
order `p` in `G`. This is the additive version of Cauchy's theorem.  -/
exists_prime_addOrderOf_dvd_card : ∀ {G : Type u_3} [inst : AddGroup G] [inst_1 : Fintype G] (p : ℕ) [Fact (Nat.Prime p)],
  p ∣ Fintype.card G → ∃ x, addOrderOf x = p
-- Mathlib.Order.SuccPred.WithBot
WithBot.succ_strictMono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] [NoMaxOrder α],
  StrictMono WithBot.succ
-- Init.Data.Vector.Monadic
/-- We can express a for loop over a vector which always yields as a fold.  -/
Vector.forIn'_yield_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : (a : α) → a ∈ xs → β → m γ) (g : (a : α) → a ∈ xs → β → γ → β) (init : β),
  (forIn' xs init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    Vector.foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init xs.attach
-- Mathlib.Order.DirSupClosed
/-- The condition `(d ∩ s).Nonempty` in `DirSupInacc` can be replaced with the stronger
`∃ b ∈ d, Ici b ∩ d ⊆ s`.  -/
dirSupInacc_iff_inter_subset : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  DirSupInacc s ↔
    ∀ ⦃d : Set α⦄,
      d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapAddMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : AddZeroClass Z] (f : C(X, Y)),
  LocallyConstant.comapAddMonoidHom f = { toFun := LocallyConstant.comap f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.range_eq_closure_interior : ∀ {𝕜 : 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),
  Set.range ↑I = closure (interior (Set.range ↑I))
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- See also `LinearMap.isPosSemidef_iff_posSemidef_toMatrix` for the semi-definite case.  -/
LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix : ∀ {n : Type u_2} [inst : Fintype n] {R : Type u_5} {M : Type u_6} [inst_1 : CommRing R] [inst_2 : PartialOrder R]
  [inst_3 : StarRing R] [TrivialStar R] [inst_5 : AddCommGroup M] [inst_6 : Module R M] [inst_7 : DecidableEq n]
  (b : Module.Basis n R M) (B : LinearMap.BilinForm R M),
  B.IsSymm → ((LinearMap.BilinMap.toQuadraticMap B).PosDef ↔ ((LinearMap.BilinForm.toMatrix b) B).PosDef)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObj.toMonObj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {R : C} → [self : CategoryTheory.RingObj R] → CategoryTheory.MonObj R
-- Mathlib.Algebra.Group.MinimalAxioms
AddGroup.ofRightAxioms.eq_1 : ∀ {G : Type u} [inst : Add G] [inst_1 : Neg G] [inst_2 : Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c))
  (mul_one : ∀ (a : G), a + 0 = a) (mul_inv_cancel : ∀ (a : G), a + -a = 0),
  AddGroup.ofRightAxioms assoc mul_one mul_inv_cancel =
    { toAdd := inst, add_assoc := assoc, toZero := inst_2, zero_add := ⋯, add_zero := mul_one, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯, toNeg := inst_1, sub := SubNegMonoid.sub', zsmul := zsmulRec,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.filterM.eq_1 : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (p : α → m Bool) (as : Array α) (start stop : ℕ),
  Array.filterM p as start stop =
    Array.foldlM
      (fun acc a => do
        let __do_lift ← p a
        if __do_lift = true then pure (acc.push a) else pure acc)
      #[] as start stop
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.mk_Iio_toType_ord_lt : ∀ {c : Cardinal.{u_1}} (i : c.ord.ToType), Cardinal.mk ↑(Set.Iio i) < c
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat : {α : Type u} → Std.Rcc.Sliceable (Subarray α) ℕ (Subarray α)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.brecOn.eq : ∀ {motive : Int.Internal.Linear.Expr → Sort u} (t : Int.Internal.Linear.Expr)
  (F_1 : (t : Int.Internal.Linear.Expr) → Int.Internal.Linear.Expr.below t → motive t),
  Int.Internal.Linear.Expr.brecOn t F_1 = F_1 t (Int.Internal.Linear.Expr.brecOn.go t F_1).2
-- Init.Data.UInt.Lemmas
UInt64.ofNat_le_iff : ∀ {n : UInt64} {m : ℕ}, m < UInt64.size → (UInt64.ofNat m ≤ n ↔ m ≤ n.toNat)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path.eq_1 : ∀ (x y : Circle), x.path y = ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)).map Circle.path._proof_5).cast ⋯ ⋯