mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Basic
/-- Extensional dependent tree maps.

A tree map stores an assignment of keys to values. It depends on a comparator function that
defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval
of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one entry
with key either `a` or `b` in a tree map. Looking up either `a` or `b` always yields the same entry,
if any is present. The `get` operations of the _dependent_ tree map additionally require a
`LawfulEqCmp` instance to ensure that `cmp a b = .eq` always implies `a = b`, so that their
respective value types are equal.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.

In contrast to regular dependent tree maps, `Std.ExtDTreeMap` offers several extensionality lemmas
and therefore has more lemmas about equality of tree maps. This doesn't affect the amount of
supported functions though: `Std.ExtDTreeMap` supports all operations from `Std.DTreeMap`.

In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure
that the functions are congruent, i.e. equivalent tree maps as parameters produce equivalent return
values.

These tree maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.DTreeMap.Raw` and
`Std.DTreeMap.Raw.WF` unbundle the invariant from the tree map. When in doubt, prefer
`ExtDTreeMap` over `DTreeMap.Raw`.
 -/
Std.ExtDTreeMap : (α : Type u) → (α → Type v) → autoParam (α → α → Ordering) Std.ExtDTreeMap._auto_1 → Type (max u v)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ici_succ_eq_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : SuccOrder α] [NoMaxOrder α]
  (a : α), Finset.Ici (Order.succ a) = Finset.Ioi a
-- Mathlib.Tactic.DefEqAbuse
/-- Descends through the `MessageData`, visiting all children. If the argument `butFirst` is given
as `some a` (`none` by default), starts with `a`, and combines any values produced by children with
this value.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.descend : {α : Type u_1} → optParam (Option α) none → Lean.MessageData.VisitStep✝ α
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instCoeSortType : CoeSort FiniteAddGrp.{u} (Type u)
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_neg_one : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], RCLike.sqrt (-1) = RCLike.I
-- Mathlib.Order.BooleanAlgebra.Defs
/-- The infimum of `x` and `xᶜ` is at most `⊥`  -/
BooleanAlgebra.inf_compl_le_bot : ∀ {α : Type u} [self : BooleanAlgebra α] (x : α), x ⊓ xᶜ ≤ ⊥
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] →
        [inst_2 : TopologicalSpace β] →
          [inst_3 : Preorder β] →
            (toContinuousOrderHom : α →Co β) →
              (∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom.toFun c = b) →
                EsakiaHom α β
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk : {M : Type u_3} →
  [inst : Mul M] → (carrier : Set M) → (∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier) → Subsemigroup M
-- Mathlib.Order.WellQuasiOrder
/-- A version of **Dickson's lemma**. See `Set.IsPWO.pi` for the finite product of
well-quasi-ordered sets.  -/
Pi.wellQuasiOrderedLE : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] [h : ∀ (i : ι), WellQuasiOrderedLE (α i)]
  [Finite ι], WellQuasiOrderedLE ((i : ι) → α i)
-- Lean.Level
Lean.LevelMap : Type → Type
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.mul_one : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If two morphisms are known to be equal, then their kernels are isomorphic.  -/
CategoryTheory.Limits.kernelIsoOfEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel g] →
              f = g → (CategoryTheory.Limits.kernel f ≅ CategoryTheory.Limits.kernel g)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.integrable_indicator₀ : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.NullMeasurableSet s μ → MeasureTheory.Integrable (s.indicator f) μ
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.instCoeSortType : CoeSort CategoryTheory.Grpd (Type u_1)
-- Mathlib.CategoryTheory.DifferentialObject
/-- The differential `d` satisfies that `d² = 0`.  -/
CategoryTheory.DifferentialObject.d_squared : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (self : CategoryTheory.DifferentialObject S C),
  CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_mulVec : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f : (n → R) →ₗ[R] m → R) (v : n → R), (LinearMap.toMatrix' f).mulVec v = f v
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit_eq_carry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α)
  (input : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig) (lhs rhs : BitVec input.w) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < input.w),
        ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit aig input⟧ =
        BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.DTreeMap.map f t → k ∈ t
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.incl.injEq : ∀ {R : Type u} (x x_1 : R), (Rack.PreEnvelGroup.incl x = Rack.PreEnvelGroup.incl x_1) = (x = x_1)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.carrier_eq_coe : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), s.carrier = ↑s
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.liftCompleteLattice.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : CompleteLattice α]
  (gi : GaloisInsertion l u),
  gi.liftCompleteLattice =
    { toLattice := gi.liftLattice, sSup := fun s => l (sSup (u '' s)), isLUB_sSup := ⋯,
      sInf := fun s => gi.choice (sInf (u '' s)) ⋯, isGLB_sInf := ⋯, toBoundedOrder := gi.liftBoundedOrder }
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An object `Y` is terminal if for every `X` there is a unique morphism `X ⟶ Y`
(as explicit arguments).  -/
CategoryTheory.Limits.IsTerminal.ofUniqueHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} → (h : (X : C) → X ⟶ Y) → (∀ (X : C) (m : X ⟶ Y), m = h X) → CategoryTheory.Limits.IsTerminal Y
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
exist_norm_eq : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ] [c : Nonempty α]
  {f : BoundedContinuousFunction α γ}, f ∈ compactlySupported α γ → ∃ x, ‖f x‖ = ‖f‖
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- The head term of the gcf of `v` is `⌊v⌋`.  -/
GenContFract.of_h_eq_floor : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K},
  (GenContFract.of v).h = ↑⌊v⌋
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)},
  l.Perm l' → (Std.Internal.List.DistinctKeys l ↔ Std.Internal.List.DistinctKeys l')
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.instSMulElemStartsWith : {α : Type u_1} →
  {X : Type u_2} →
    [inst : DecidableEq α] → [MulAction (FreeGroup α) X] → {w : α × Bool} → SMul (↑(FreeGroup.startsWith w)) X
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.isEmpty = true → t.min? = none
-- Init.Data.Nat.Lemmas
Nat.one_mod_two_pow : ∀ {n : ℕ}, 0 < n → 1 % 2 ^ n = 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.go.match_1.congr_eq_2 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.lt),
  x = Ordering.gt →
    (match x with
      | Ordering.eq => h_1 ()
      | Ordering.gt => h_2 ()
      | Ordering.lt => h_3 ()) ≍
      h_2 ()
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeCommRing : ∀ (α : Type u), Cardinal.mk (FreeCommRing α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (toReflexiveRelation : CategoryTheory.ReflexiveRelation p₁ p₂) (s : R ⟶ R)
  (symmetry₁ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam)
  (symmetry₂ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam)
  (c : CategoryTheory.Limits.PullbackCone p₂ p₁) (isLimit : CategoryTheory.Limits.IsLimit c) (t : c.pt ⟶ R)
  (transitivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam)
  (transitivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam)
  (toReflexiveRelation_1 : CategoryTheory.ReflexiveRelation p₁ p₂) (s_1 : R ⟶ R)
  (symmetry₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam)
  (symmetry₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam)
  (c_1 : CategoryTheory.Limits.PullbackCone p₂ p₁) (isLimit_1 : CategoryTheory.Limits.IsLimit c_1) (t_1 : c_1.pt ⟶ R)
  (transitivity₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₁ = CategoryTheory.CategoryStruct.comp c_1.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam)
  (transitivity₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₂ = CategoryTheory.CategoryStruct.comp c_1.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam),
  ({ toReflexiveRelation := toReflexiveRelation, s := s, symmetry₁ := symmetry₁, symmetry₂ := symmetry₂, c := c,
        isLimit := isLimit, t := t, transitivity₁ := transitivity₁, transitivity₂ := transitivity₂ } =
      { toReflexiveRelation := toReflexiveRelation_1, s := s_1, symmetry₁ := symmetry₁_1, symmetry₂ := symmetry₂_1,
        c := c_1, isLimit := isLimit_1, t := t_1, transitivity₁ := transitivity₁_1,
        transitivity₂ := transitivity₂_1 }) =
    (toReflexiveRelation = toReflexiveRelation_1 ∧ s = s_1 ∧ c = c_1 ∧ isLimit ≍ isLimit_1 ∧ t ≍ t_1)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `hasMFDerivWithinAt_iff_hasFDerivWithinAt`. -/
HasFDerivWithinAt.hasMFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E}
  {f' : TangentSpace (modelWithCornersSelf 𝕜 E) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 E') (f x)},
  HasFDerivWithinAt f f' s x → HasMFDerivAt[s] f x f'
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K], ArchimedeanClass.stdPart 0 = 0
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.ControlInfo.mk.injEq : ∀ (breaks continues returnsEarly : Bool) (numRegularExits : ℕ) (noFallthrough : Bool) (reassigns : Lean.NameSet)
  (breaks_1 continues_1 returnsEarly_1 : Bool) (numRegularExits_1 : ℕ) (noFallthrough_1 : Bool)
  (reassigns_1 : Lean.NameSet),
  ({ breaks := breaks, continues := continues, returnsEarly := returnsEarly, numRegularExits := numRegularExits,
        noFallthrough := noFallthrough, reassigns := reassigns } =
      { breaks := breaks_1, continues := continues_1, returnsEarly := returnsEarly_1,
        numRegularExits := numRegularExits_1, noFallthrough := noFallthrough_1, reassigns := reassigns_1 }) =
    (breaks = breaks_1 ∧
      continues = continues_1 ∧
        returnsEarly = returnsEarly_1 ∧
          numRegularExits = numRegularExits_1 ∧ noFallthrough = noFallthrough_1 ∧ reassigns = reassigns_1)
-- Mathlib.Combinatorics.Quiver.Schreier
/-- Equivalence between the original vertex type and the Schreier graph type.  -/
Quiver.SchreierGraph.equiv : (V : Type u_1) → {M : Type u_2} → [inst : SMul M V] → {S : Type u_3} → (ι : S → M) → V ≃ Quiver.SchreierGraph V ι
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
/-- Detecting equality of morphisms factoring through a connected colimit by pulling back along
the inclusions of the colimit.  -/
CategoryTheory.Limits.IsColimit.pullback_hom_ext : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsConnected J] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasPullbacks C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {X Y : C} {f : X ⟶ c.pt} {g h : c.pt ⟶ Y},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (c.ι.app j) f)
          (CategoryTheory.CategoryStruct.comp f g) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (c.ι.app j) f)
          (CategoryTheory.CategoryStruct.comp f h)) →
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h
-- Mathlib.RingTheory.Perfection
Perfection.coeff_map : ∀ {R : Type u_1} [inst : CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {S : Type u₂}
  [inst_2 : CommSemiring S] [inst_3 : CharP S p] (φ : R →+* S) (f : Perfection R p) (n : ℕ),
  (Perfection.coeff S p n) ((Perfection.map p φ) f) = φ ((Perfection.coeff R p n) f)
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.public : Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz then
its derivative at `x₀` has norm bounded by `C`.
Version using `deriv`.  -/
norm_deriv_le_of_lipschitz : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x₀ : 𝕜} {C : NNReal}, LipschitzWith C f → ‖deriv f x₀‖ ≤ ↑C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.continuousAt_tan : ∀ {x : ℝ}, ContinuousAt Real.tan x ↔ Real.cos x ≠ 0
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with a polynomial bound on the remainder

We assume that `f` is `n+1`-times continuously differentiable on the closed set `Icc a b`.
There exists a constant `C` such that for all `x ∈ Icc a b` the difference of `f` and its `n`-th
Taylor polynomial can be estimated by `C * (x - a)^(n+1)`.  -/
exists_taylor_mean_remainder_bound : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {n : ℕ},
  a ≤ b →
    ContDiffOn ℝ (↑n + 1) f (Set.Icc a b) →
      ∃ C, ∀ x ∈ Set.Icc a b, ‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_pure : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f : Filter β} {b : β}, f -ᵥ pure b = Filter.map (fun x => x -ᵥ b) f
-- Mathlib.Algebra.Field.ZMod
/-- `ZMod p` is an integral domain when `p` is prime.  -/
ZMod.instIsDomain : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsDomain (ZMod p)
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R},
  (∀ (n : ℕ), ∃ z, (Ideal.Quotient.mk I) z = (Perfection.coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) →
    (Perfection.teichmuller p I) x = y
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.cacheResult : Lean.Expr → Lean.Meta.Simp.Config → Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Tactic.Sat.FromLRAT
/-- The list of literals as read from the input file  -/
Mathlib.Tactic.Sat.LClause.lits : Mathlib.Tactic.Sat.LClause → Array ℤ
-- Mathlib.Analysis.Convex.Between
wbtw_self_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] (x y : P), Wbtw R x y y
-- Mathlib.Tactic.Order.Graph.Tarjan
Mathlib.Tactic.Order.Graph.TarjanState.mk.inj : ∀ {toDFSState : Mathlib.Tactic.Order.Graph.DFSState} {id lowlink : Std.HashMap ℕ ℕ} {stack : Array ℕ}
  {onStack : Std.HashSet ℕ} {time : ℕ} {toDFSState_1 : Mathlib.Tactic.Order.Graph.DFSState}
  {id_1 lowlink_1 : Std.HashMap ℕ ℕ} {stack_1 : Array ℕ} {onStack_1 : Std.HashSet ℕ} {time_1 : ℕ},
  { toDFSState := toDFSState, id := id, lowlink := lowlink, stack := stack, onStack := onStack, time := time } =
      { toDFSState := toDFSState_1, id := id_1, lowlink := lowlink_1, stack := stack_1, onStack := onStack_1,
        time := time_1 } →
    toDFSState = toDFSState_1 ∧ id = id_1 ∧ lowlink = lowlink_1 ∧ stack = stack_1 ∧ onStack = onStack_1 ∧ time = time_1
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iInter₂_subset_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ) (s : Set α)
  (t : (i : ι) → κ i → Set β), Set.image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, Set.image2 f s (t i j)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.postcomp_comp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M) {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N]
  (f : M →ₗ[A] N) {N' : Type v''} [inst_5 : AddCommGroup N'] [inst_6 : Module A N'] (g : N →ₗ[A] N'),
  solution.postcomp (g ∘ₗ f) = (solution.postcomp f).postcomp g
-- Mathlib.Analysis.Normed.Module.Basic
norm_algebraMap : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  (x : 𝕜), ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct the expression for a structural 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.nil : Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.CategoryTheory.Widesubcategory
/-- The property that the morphism satisfies.  -/
CategoryTheory.InducedWideCategory.Hom.property : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] {F : C → D}
  {P : CategoryTheory.MorphismProperty D} [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.InducedWideCategory D F P}
  (self : X.Hom Y), P self.hom
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Twice the angle between a multiple of a vector and that vector is 0.  -/
Orientation.two_zsmul_oangle_smul_left_self : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ}, 2 • o.oangle (r • x) x = 0
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.mk.injEq : ∀ {X : Type u} [inst : PartialOrder X] (finset : Finset X)
  (nonempty : autoParam finset.Nonempty PartialOrder.NonemptyFiniteChains.nonempty._autoParam)
  (comparable : ∀ (a b : ↥finset), a ≤ b ∨ b ≤ a) (finset_1 : Finset X)
  (nonempty_1 : autoParam finset_1.Nonempty PartialOrder.NonemptyFiniteChains.nonempty._autoParam)
  (comparable_1 : ∀ (a b : ↥finset_1), a ≤ b ∨ b ≤ a),
  ({ finset := finset, nonempty := nonempty, comparable := comparable } =
      { finset := finset_1, nonempty := nonempty_1, comparable := comparable_1 }) =
    (finset = finset_1)
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instHasFiniteLimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteLimits C], CategoryTheory.Limits.HasFiniteLimits (CochainComplex.Plus C)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- Verify that the constructed cocone is indeed a colimit.  -/
CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          [inst_1 : CategoryTheory.IsIso f] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The base `D` is closed.  -/
Topology.RelCWComplex.isClosedBase : ∀ {X : Type u} {inst : TopologicalSpace X} (C : Set X) {D : outParam (Set X)} [self : Topology.RelCWComplex C D],
  IsClosed D
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.rangeRestrict.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  f.rangeRestrict = f.codRestrict f.range ⋯
-- Init.Data.Array.Lemmas
Array.foldlM.loop.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → α → m β) (as : Array α) (stop : ℕ)
  (h : stop ≤ as.size) (i j : ℕ) (b : β),
  Array.foldlM.loop f as stop h i j b =
    if hlt : j < stop then
      match i with
      | 0 => pure b
      | i'.succ =>
        have this := ⋯;
        do
        let __do_lift ← f b as[j]
        Array.foldlM.loop f as stop h i' (j + 1) __do_lift
    else pure b
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.getKey k₁ h₁ = m.getKey k₂ ⋯