mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkCongr_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y : ↑X} (e : Inseparable x y), (F.stalkCongr e).hom = F.stalkSpecializes ⋯
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_filterWithPostcondition : ∀ {α β δ : 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] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps] [inst_9 : Std.IteratorLoop α m n]
  [inst_10 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o]
  [inst_13 : MonadLiftT m n] [inst_14 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {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 __do_lift ← liftM (f b).run
          if __do_lift.down = true then g d b else pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.filterWithPostcondition f it) ⦃Q⦄
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.coeComonad : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → Coe (CategoryTheory.Comonad C) (CategoryTheory.Functor C C)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo.mk : Lean.Name → Option Lean.Name → ℕ → Bool → Lean.Meta.ElimAltInfo
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.id : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (self : CategoryTheory.Limits.DiagramOfCones F) (j : J),
  (self.map (CategoryTheory.CategoryStruct.id j)).hom =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (self.obj j)).pt
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Finset β}
  {f g : β → α}, s₁ = s₂ → (∀ a ∈ s₂, f a = g a) → s₁.lcm f = s₂.lcm g
-- Lean.Meta.Tactic.Grind.Types
/-- Cache for `Unit`-like types. It maps the type to its element.
We say a type is `Unit`-like if it is a subsingleton and is inhabited.
 -/
Lean.Meta.Grind.UnitLike.State : Type
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.NatTrans.CommShift₂.commShift_app : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} {G₁ G₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} {τ : G₁ ⟶ G₂}
  {h : CategoryTheory.CommShift₂Setup D M} {inst_7 : G₁.CommShift₂ h} {inst_8 : G₂.CommShift₂ h}
  [self : CategoryTheory.NatTrans.CommShift₂ τ h] (X₁ : C₁), CategoryTheory.NatTrans.CommShift (τ.app X₁) M
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_eq_getLastD_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α},
  t.maxD fallback = t.toList.getLastD fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α}, (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Data.Multiset.FinsetOps
Multiset.inter_le_ndinter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∩ t ≤ s.ndinter t
-- Mathlib.FieldTheory.KummerExtension
Algebra.adjoin_root_eq_top_of_isSplittingField : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ {a : K},
      Irreducible (Polynomial.X ^ n - Polynomial.C a) →
        ∀ {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L]
          [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L},
          α ^ n = (algebraMap K L) a → K[α] = ⊤
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.fold_eq_match_step : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : γ → β → γ} {init : γ}
  {it : Std.IterM m β},
  Std.IterM.fold f init it = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, property⟩ => Std.IterM.fold f (f init out) it'
      | ⟨Std.IterStep.skip it', property⟩ => Std.IterM.fold f init it'
      | ⟨Std.IterStep.done, property⟩ => pure init
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
/-- The matrix with variable `X (i,j)` at location `(i,j)`.  -/
Matrix.mvPolynomialX : (m : Type u_1) → (n : Type u_2) → (R : Type u_3) → [inst : CommSemiring R] → Matrix m n (MvPolynomial (m × n) R)
-- Mathlib.Data.Finset.Max
Finset.min'_subset : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t), t.min' ⋯ ≤ s.min' H
-- Std.Do.SPred.Laws
Std.Do.SPred.and_curry : ∀ {σs : List (Type u)} {P Q : Std.Do.SVal.StateTuple σs → Prop},
  ((Std.Do.SVal.curry fun t => { down := P t }) ∧ Std.Do.SVal.curry fun t => { down := Q t }) ⊣⊢ₛ
    Std.Do.SVal.curry fun t => { down := P t ∧ Q t }
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_toList : ∀ {M : Type u_3} [inst : CommMonoid M] (s : Multiset M), s.toList.prod = s.prod
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
AddOpposite.instIsUniformAddGroup : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α], IsUniformAddGroup αᵃᵒᵖ
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.exists_non_zero_rep : ∀ {M : Type u_1} [inst : MonoidWithZero M] {a : Associates M}, a ≠ 0 → ∃ a0, a0 ≠ 0 ∧ Associates.mk a0 = a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeSet.Raw.ofList l cmp).get? k' = some k
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function of a meromorphic function.

If `f : 𝕜 → E` is meromorphic and `a : WithTop E` is any value, this is a logarithmically weighted
measure of the number of times the function `f` takes a given value `a` within the disk `∣z∣ ≤ r`,
taking multiplicities into account.  In the special case where `a = ⊤`, it counts the poles of `f`.
 -/
ValueDistribution.logCounting : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [ProperSpace 𝕜] → {E : Type u_2} → [inst_2 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → WithTop E → ℝ → ℝ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume : ∀ (T : ℝ) [hT : Fact (0 < T)],
  MeasureTheory.AddQuotientMeasureEqMeasurePreimage MeasureTheory.volume MeasureTheory.volume
-- Std.Data.HashSet.Raw
/-- The number of elements present in the set  -/
Std.HashSet.Raw.size : {α : Type u} → Std.HashSet.Raw α → ℕ
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Functor.essImage.counit_isIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {j : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Coreflective j] {A : D},
  j.essImage A → CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction j).counit.app A)
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If a non-unital subring of a non-unital topological ring is commutative, then so is its
topological closure.

See note [reducible non-instances]  -/
NonUnitalSubring.nonUnitalCommRingTopologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalRing R] →
      [inst_2 : IsSemitopologicalRing R] →
        [T2Space R] → (s : NonUnitalSubring R) → (∀ (x y : ↥s), x * y = y * x) → NonUnitalCommRing ↥s.topologicalClosure
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bodyInterest.injEq : ∀ {β : Type} (x x_1 : Bool),
  (Std.Http.Server.Connection.Recv.bodyInterest✝ x = Std.Http.Server.Connection.Recv.bodyInterest✝ x_1) = (x = x_1)
-- Lean.Message
Lean.MessageData.instCoeArrayExpr : Coe (Array Lean.Expr) Lean.MessageData
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousDiv.continuous_div' : ∀ {G : Type u_4} {inst : TopologicalSpace G} {inst_1 : Div G} [self : ContinuousDiv G], Continuous fun p => p.1 / p.2
-- Lean.Data.Trie
/-- Looks up a value at the given key `s`.   -/
Lean.Data.Trie.find? : {α : Type} → Lean.Data.Trie α → String → Option α
-- Mathlib.Topology.GDelta.Basic
/-- The image of a nowhere dense set through an inducing map is nowhere dense.  -/
Topology.IsInducing.isNowhereDense_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → ∀ {s : Set X}, IsNowhereDense s → IsNowhereDense (f '' s)
-- Init.Data.Array.Erase
Array.erase_comm : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a b : α) {xs : Array α}, (xs.erase a).erase b = (xs.erase b).erase a
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The tensor product bifunctor `C ⥤ C ⥤ C` of a monoidal category.  -/
CategoryTheory.MonoidalCategory.curriedTensor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The function `x^n * exp(-x)` tends to `0` at `+∞`, for any natural number `n`.  -/
Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero : ∀ (n : ℕ), Filter.Tendsto (fun x => x ^ n * Real.exp (-x)) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Given three graded objects `X₁`, `X₂`, `X₃` in `GradedObject I C`, this is the
assumption that for all `i₁₂ : I` and `i₃ : I`, the tensor product functor `- ⊗ X₃ i₃`
commutes with the coproduct of the objects `X₁ i₁ ⊗ X₂ i₂` such that `i₁ + i₂ = i₁₂`.  -/
CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor : {I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] →
          CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → Prop
-- Init.Data.String.Basic
String.Pos.Raw.prev_lt_of_pos : ∀ (s : String) (i : String.Pos.Raw), i ≠ 0 → (String.Pos.Raw.prev s i).byteIdx < i.byteIdx
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.rTensorOne_tmul_one : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (m : ↥M), M.rTensorOne (m ⊗ₜ[R] 1) = m
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.take.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (a : α) (as : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match n.succ, a :: as with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_3 n a as
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} {h' : k ∈ Std.DTreeMap.filterMap f t},
  (Std.DTreeMap.filterMap f t).getKey k h' = t.getKey k ⋯
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- If `S` is the empty scheme, the pro-étale site over `S` is a point.  -/
AlgebraicGeometry.Scheme.ProEt.equivOfIsEmpty : (S : AlgebraicGeometry.Scheme) → [IsEmpty ↥S] → S.ProEt ≌ CategoryTheory.Discrete PUnit.{u_1 + 1}
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.imageProdLex : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set (Lex (α × β))},
  s.IsPWO → ((fun x => (ofLex x).1) '' s).IsPWO
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.LawfulEqCmp cmp]
  [inst : Std.TransCmp cmp] {k : α}, k ∈ t.keys ↔ k ∈ t
-- Mathlib.Topology.UniformSpace.Defs
uniformity_lift_le_comp : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : SetRel α α → Filter β},
  Monotone f → ((uniformity α).lift fun s => f (SetRel.comp s s)) ≤ (uniformity α).lift f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α},
  t.getKey? k = some k' ↔ ∃ (h : k ∈ t), t.getKey k h = k'
-- Init.Data.Fin.Fold
Fin.foldr.loop.congr_simp : ∀ {α : Sort u_1} (n : ℕ) (f f_1 : Fin n → α → α),
  f = f_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ n) (a_1 a_2 : α),
      a_1 = a_2 → Fin.foldr.loop n f i a a_1 = Fin.foldr.loop n f_1 i_1 ⋯ a_2
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DHashMap.Raw.Const.get! (m₁ ∪ m₂) k = Std.DHashMap.Raw.Const.get! m₁ k
-- Mathlib.Algebra.Category.GrpWithZero
/-- The category of groups with zero.  -/
GrpWithZero : Type (u_1 + 1)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.matrix_jacobson_bot : ∀ {R : Type u_1} [inst : Ring R] {n : Type u_2} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  TwoSidedIdeal.matrix n ⊥.jacobson = ⊥.jacobson
-- Mathlib.Algebra.Regular.SMul
/-- A unit is `M`-regular.  -/
IsUnit.isSMulRegular : ∀ {R : Type u_1} (M : Type u_3) {a : R} [inst : Monoid R] [inst_1 : MulAction R M], IsUnit a → IsSMulRegular M a
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_not_invert : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {gate : ℕ}
  {inv : Bool} {hgate : gate < aig.decls.size},
  ⟦assign, { aig := aig, ref := { gate := gate, invert := !inv, hgate := hgate } }⟧ =
    !⟦assign, { aig := aig, ref := { gate := gate, invert := inv, hgate := hgate } }⟧
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp.inj : ∀ {R : Type u_1} {inst : Semiring R} {toFinsupp toFinsupp_1 : AddMonoidAlgebra R ℕ},
  { toFinsupp := toFinsupp } = { toFinsupp := toFinsupp_1 } → toFinsupp = toFinsupp_1
-- Mathlib.Analysis.Normed.Module.Basic
RealNormedSpace.cobounded_neBot : ∀ (E : Type u_3) [inst : NormedAddCommGroup E] [Nontrivial E] [NormedSpace ℝ E], (Bornology.cobounded E).NeBot
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.rightHomotopy_congruence : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V],
  CategoryTheory.Congruence (CategoryTheory.Arrow.rightHomotopic V)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The weak universal property of a divided power algebra for morphisms to divided power rings  -/
DividedPowerAlgebra.lift : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_4} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] →
                {I : Ideal A} →
                  DividedPowers I → (g : M →ₗ[R] A) → (∀ (m : M), g m ∈ I) → DividedPowerAlgebra R M →ₐ[R] A
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.node3R : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  l.Sized → m.Sized → r.Sized → (l.node3R x m y r).Sized
-- Init.Data.BitVec.Lemmas
BitVec.toFin_ushiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, (x >>> n).toFin = x.toFin / Fin.ofNat (2 ^ w) (2 ^ n)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.instIsRightAdjointObjOppositeFunctorInternalHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (X : Cᵒᵖ), (CategoryTheory.MonoidalClosed.internalHom.obj X).IsRightAdjoint
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_inv_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)ᵒᵖ),
  (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.inv.app X = (Opposite.unop X).rightOpLeftOpIso.inv.op
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The map `n ↦ Nat.digitsAppend b L` is bijection between the set of natural integers `< b ^ l`
to the set of lists of natural integers of length `l` with coefficients `< b` to .
 -/
Nat.bijOn_digitsAppend : ∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), Set.BijOn (b.digitsAppend l) {n | n < b ^ l} {L | L.length = l ∧ ∀ x ∈ L, x < b}
-- Mathlib.Data.Finset.Preimage
Finset.preimage_map : ∀ {α : Type u} {β : Type v} (f : α ↪ β) (s : Finset α), (Finset.map f s).preimage ⇑f ⋯ = s
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make an object of `P.Arrow Q X` from a morphism `f : A ⟶ B` and a proof of `P f`.  -/
CategoryTheory.MorphismProperty.Arrow.mk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q W : CategoryTheory.MorphismProperty T} → {A B : T} → (f : A ⟶ B) → P f → P.Arrow Q W
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.equivMulOpposite.eq_1 : ∀ {M : Type u_2} [inst : Monoid M],
  MulActionHom.End.equivMulOpposite =
    { toFun := fun f => MulOpposite.op (f 1),
      invFun := fun m => { toFun := fun x => x * MulOpposite.unop m, map_smul' := ⋯ }, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.mu_bdd : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {x y : R}
  (hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)) (n : ℕ),
  ↑(mu✝ μ hn n) / ↑n ∈ Set.Icc 0 1
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!_eq_balance! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size →
        Std.DTreeMap.Internal.Impl.balanceL! k v l r = Std.DTreeMap.Internal.Impl.balance! k v l r
-- Aesop.Script.Step
Aesop.Script.LazyStep.build : {α : Type} → Lean.MVarId → Aesop.Script.LazyStep.BuildInput α → Lean.MetaM (Aesop.Script.LazyStep × α)
-- Mathlib.Data.Multiset.UnionInter
Multiset.coe_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : List α), ↑s ∩ ↑t = ↑(s.bagInter t)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lof_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι) (b : M i), ((DirectSum.lof R ι M i) b) i = b
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.ofHom_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1)
  (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0),
  CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCocone.desc φ α β hαβ) =
    CochainComplex.mappingCocone.descCochain φ α (↑β) CochainComplex.mappingCocone.ofHom_desc._proof_2
-- Init.Data.Vector.Perm
Vector.Perm.symm : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs.Perm ys → ys.Perm xs
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.symm : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {x y : M}, AddConGen.Rel r x y → AddConGen.Rel r y x
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_of_mem_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {a : α}, s ∈ nhds a → s ∈ nhdsWithin a t
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ℕ), ↑(n • a) = n • ↑a
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_sq : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), (UpperHalfPlane.σ g) ((UpperHalfPlane.σ g) z) = z
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_eq_top : ∀ {M : Type u_2} [inst : Add M] {S : AddSubsemigroup Mᵃᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_next : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, (p.next h).prev ⋯ = p
-- Mathlib.Algebra.Group.Subgroup.Pointwise
neg_coe_set : ∀ {G : Type u_2} {S : Type u_4} [inst : InvolutiveNeg G] [inst_1 : SetLike S G] [NegMemClass S G] {H : S}, -↑H = ↑H
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.zero_lt_posForm_iff : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] {x y : ↥(Submodule.span S (Set.range ⇑P.root))},
  0 < (B.posForm x) y ↔ ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y
-- Init.Data.Nat.Basic
Nat.lt_or_gt_of_ne : ∀ {a b : ℕ}, a ≠ b → a < b ∨ a > b
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.isLongestMatchAt : ∀ {pat s : String.Slice} (hpat : pat.isEmpty = false) {pos : String.Pos.Raw}
  (h :
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat.copy.toByteArray s.copy.toByteArray
      pat.utf8ByteSize pos.byteIdx)
  (h' : String.Pos.Raw.IsValidForSlice s (pos.unoffsetBy pat.rawEndPos)),
  String.Slice.Pattern.Model.IsLongestMatchAt pat (s.pos (pos.unoffsetBy pat.rawEndPos) h') (s.pos pos ⋯)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).contains k = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α}
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) = true},
  Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k h' =
    match w :
      List.findSomeRev?
        (fun x =>
          match x with
          | (a, b) => if compare a k = Ordering.eq then some b else none)
        l with
    | some v => v
    | none => Std.DTreeMap.Internal.Impl.Const.get t k ⋯
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Complex.arctan_tan : ∀ {z : ℂ}, z ≠ ↑Real.pi / 2 → -(Real.pi / 2) < z.re → z.re ≤ Real.pi / 2 → (Complex.tan z).arctan = z