mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Coinductive
/-- Generates unfolding lemmas that relate coinductive predicates to their flat inductive forms.
These lemmas are essential for the constructor generation process, providing the bridge
between the user-facing coinductive predicates and their internal flat representations.

Example:

Given a definition:
```
coinductive infSeq (r : α → α → Prop) : α → Prop where
| step : r a b → infSeq r b → infSeq r a
```

We generate the following unfolding lemma:
```
  infSeq.functor_unfold (α : Type) (r : α → α → Prop) (a✝ : α) : infSeq α r a✝ = infSeq._functor α r (infSeq α r) a✝
```
 -/
_private.Lean.Elab.Coinductive.0.Lean.Elab.Command.generateEqLemmas : Array Lean.InductiveVal → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_fst_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) {X_1 Y : X} (f : X_1 ⟶ Y),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).fst.map f = (J.map f).fst
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- If `G` is a fundamental group for `F`, it is canonically homeomorphic to `Aut F`.  -/
CategoryTheory.PreGaloisCategory.toAutHomeo : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        (G : Type u_1) →
          [inst_2 : Group G] →
            [inst_3 : (X : C) → MulAction G (F.obj X).obj] →
              [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
                [inst_5 : TopologicalSpace G] →
                  [inst_6 : IsTopologicalGroup G] →
                    [inst_7 : CompactSpace G] →
                      [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] → G ≃ₜ CategoryTheory.Aut F
-- Init.Data.Order.Lemmas
Std.lt_of_lt_of_le : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2]
  [Std.LawfulOrderLT α] {a b c : α}, a < b → b ≤ c → a < c
-- Mathlib.Data.List.Basic
List.get_eq_getElem? : ∀ {α : Type u} (l : List α) (i : Fin l.length), l.get i = l[i]?.get ⋯
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cellsOfRowLens.eq_def : ∀ (x : List ℕ),
  YoungDiagram.cellsOfRowLens x =
    match x with
    | [] => ∅
    | w :: ws =>
      {0} ×ˢ Finset.range w ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens ws)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- The quotient by a maximal ideal is a group with zero. This is a `def` rather than `instance`,
since users will have computable inverses in some applications.

See note [reducible non-instances].  -/
Ideal.Quotient.groupWithZero : {R : Type u_3} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → [hI : I.IsMaximal] → GroupWithZero (R ⧸ I)
-- Mathlib.Analysis.Normed.Group.Real
nnnorm_norm' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (x : E), ‖‖x‖‖₊ = ‖x‖₊
-- Init.Data.Nat.Dvd
Nat.dvd_of_mul_dvd_mul_right : ∀ {k m n : ℕ}, 0 < k → m * k ∣ n * k → m ∣ n
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.subtypeₐᵢ_linear : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s], s.subtypeₐᵢ.linear = s.direction.subtype
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- The unit isomorphism induced by `Γ₂N₁`.  -/
CategoryTheory.Idempotents.DoldKan.ε : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.IsIdempotentComplete C] →
        [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C] →
          CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C) ≅
            CategoryTheory.Idempotents.DoldKan.N.comp CategoryTheory.Idempotents.DoldKan.Γ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.head.eq_1 : ∀ (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.head k q =
    Turing.PartrecToTM2.Λ'.move Turing.PartrecToTM2.natEnd k Turing.PartrecToTM2.K'.rev
      (Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.rev (fun x => some Turing.PartrecToTM2.Γ'.cons)
        (Turing.PartrecToTM2.Λ'.read fun s =>
          (if s = some Turing.PartrecToTM2.Γ'.consₗ then id
            else Turing.PartrecToTM2.Λ'.clear (fun x => decide (x = Turing.PartrecToTM2.Γ'.consₗ)) k)
            (Turing.PartrecToTM2.unrev q)))
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instDiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Div β],
  MeasureTheory.SimpleFunc.instDiv = { div := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 / x2) f).seq g }
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Iso.mk_hom_toFun : ∀ {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : α.X), (Pointed.Iso.mk e he).hom.toFun a = e a
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitEpi f},
  x.section_ = y.section_ → x = y
-- Mathlib.LinearAlgebra.Quotient.Basic
LinearMap.range_mkQ_comp : ∀ {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), f.range.mkQ ∘ₛₗ f = 0
-- Mathlib.Data.Set.Prod
Set.eval_image_pi_of_notMem : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [inst : Decidable (s.pi t).Nonempty],
  i ∉ s → Function.eval i '' s.pi t = if (s.pi t).Nonempty then Set.univ else ∅
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.Legacy.mkIterator.eq_1 : ∀ (s : String), String.Legacy.mkIterator s = { s := s, i := 0 }
-- Init.Data.List.Basic
/-- The first list is a prefix of the second.

`IsPrefix l₁ l₂`, written `l₁ <+: l₂`, means that there exists some `t : List α` such that `l₂` has
the form `l₁ ++ t`.

The function `List.isPrefixOf` is a Boolean equivalent.


Conventions for notations in identifiers:

 * The recommended spelling of `<+:` in identifiers is `prefix` (not `isPrefix`). -/
List.«term_<+:_» : Lean.TrailingParserDescr
-- Mathlib.Logic.Basic
Imp.swap : ∀ {a : Sort u_1} {b : Sort u_2} {c : Prop}, (∀ (a : a) (a : b), c) ↔ ∀ (a_1 : b) (a : a), c
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_bijective : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, Function.Bijective SimpleGraph.Walk.reverse
-- Lean.Elab.Deriving.Basic
/-- Constructs an instance of the class `classExpr` by figuring out the correct position to insert `val`
to create a type `className ... val ...` such that there is already an instance for it.
The `declVal` argument is the value to use in place of `val` when creating the new instance.

Heuristics:
- `val` must not use an outParam.
- `val` should use an explicit parameter, or a parameter that has already been given a value.
- If there are multiple explicit parameters, we try each possibility.
- If the class has instance arguments, we require that they be synthesizable while synthesizing this instance.
  While we could allow synthesis failure and abstract such instances,
  we leave such conditional instances to be defined by users.
- If this all fails and `val` is a constant application, we try unfolding it once and try again.

For example, when deriving `MonadReader (ρ : outParam (Type u)) (m : Type u → Type v)`,
we will skip `ρ` and try using `m`.

Note that we try synthesizing instances even if there are still metavariables in the type.
If that succeeds, then one can abstract those metavariables and create a parameterized instance.
The abstraction is not done by this function.

Expects to be run with an empty message log.
 -/
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.mkInst : Lean.Expr → Lean.Name → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.MkInstResult✝
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly convex function `f` and positive weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` are all equal
(and in fact all equal to their center of mass w.r.t. `w`).  -/
StrictConvexOn.map_sum_eq_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i)
-- Mathlib.Order.KrullDimension
Order.height_add_one_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → Order.height a + 1 ≤ Order.height b
-- Std.Data.HashMap.Lemmas
Std.HashMap.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  Std.HashMap.forIn (fun a x d => f a d) init m = forIn m.keysArray init f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  HasFDerivAt (↑NumberField.mixedEmbedding.fundamentalCone.expMap)
    (NumberField.mixedEmbedding.fundamentalCone.fderiv_expMap x) x
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- The continued fraction of a rational number terminates.  -/
GenContFract.terminates_of_rat : ∀ (q : ℚ), (GenContFract.of q).Terminates
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_add_erase : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] (i : ι)
  (f : Π₀ (i : ι), β i), (fun₀ | i => f i) + DFinsupp.erase i f = f
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_finTwoArrow : ∀ {α : Type u} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (MeasureTheory.Measure.pi fun x => μ) (μ.prod μ)
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv_coeff_zero : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
-- Mathlib.Tactic.GCongr.Core
/-- Environment extension for "generalized congruence" (`gcongr`) lemmas.  -/
Mathlib.Tactic.GCongr.gcongrExt : Lean.SimpleScopedEnvExtension Mathlib.Tactic.GCongr.GCongrLemma Mathlib.Tactic.GCongr.GCongrLemmas
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- If `f : ℝⁿ → E` is continuous on a rectangular box `I`, then it is Box integrable on `I`
w.r.t. a locally finite measure `μ` with the same integral.  -/
MeasureTheory.ContinuousOn.hasBoxIntegral : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [CompleteSpace E] {f : (ι → ℝ) → E} (μ : MeasureTheory.Measure (ι → ℝ))
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι},
  ContinuousOn f (BoxIntegral.Box.Icc I) →
    ∀ (l : BoxIntegral.IntegrationParams),
      BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
-- Std.Data.DHashMap.Basic
Std.DHashMap.instInter : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inter (Std.DHashMap α β)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.mk : {α : Type u_4} →
  [inst : TopologicalSpace α] →
    (toCompacts : TopologicalSpace.Compacts α) →
      (interior toCompacts.carrier).Nonempty → TopologicalSpace.PositiveCompacts α
-- Lean.Elab.Tactic.Grind.Main
/-- Add all definitions from the current file.  -/
Lean.Elab.Tactic.elabGrindLocals : Lean.Meta.Grind.Params → Lean.MetaM Lean.Meta.Grind.Params
-- Mathlib.Topology.Algebra.ConstMulAction
isHomeomorph_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G), IsHomeomorph fun x => c +ᵥ x
-- Mathlib.Analysis.Convex.Basic
convex_halfSpace_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w | r < f w}
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
setOfPred_liouville_eq_irrational_inter_iInter_iUnion : {x | Liouville x} = {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by the identity morphism is just the identity functor.  -/
CategoryTheory.Over.mapId_eq : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T),
  CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.Functor.id (CategoryTheory.Over Y)
-- Mathlib.CategoryTheory.Core
/-- The functor `functorToCore (𝟭 G)` is a section of `inclusion G`.  -/
CategoryTheory.Core.inclusionCompFunctorToCoreIso : {G : Type u₂} →
  [inst : CategoryTheory.Groupoid G] →
    (CategoryTheory.Core.inclusion G).comp (CategoryTheory.Core.functorToCore (CategoryTheory.Functor.id G)) ≅
      CategoryTheory.Functor.id (CategoryTheory.Core G)
-- Mathlib.Order.SymmDiff
symmDiff_fst : ∀ {α : Type u_2} {β : Type u_3} [inst : GeneralizedCoheytingAlgebra α] [inst_1 : GeneralizedCoheytingAlgebra β]
  (a b : α × β), (symmDiff a b).1 = symmDiff a.1 b.1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_add : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ ν : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  (μ + ν).transpose B = μ.transpose B + ν.transpose B
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_desc_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc f g) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.stepRet.match_1.eq_3 : ∀ (motive : Turing.ToPartrec.Cont → List ℕ → Sort u_1) (ns : List ℕ) (k : Turing.ToPartrec.Cont) (v : List ℕ)
  (h_1 : (v : List ℕ) → motive Turing.ToPartrec.Cont.halt v)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₁ fs as k) v)
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₂ ns k) v)
  (h_4 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.comp f k) v)
  (h_5 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.fix f k) v),
  (match Turing.ToPartrec.Cont.cons₂ ns k, v with
    | Turing.ToPartrec.Cont.halt, v => h_1 v
    | Turing.ToPartrec.Cont.cons₁ fs as k, v => h_2 fs as k v
    | Turing.ToPartrec.Cont.cons₂ ns k, v => h_3 ns k v
    | Turing.ToPartrec.Cont.comp f k, v => h_4 f k v
    | Turing.ToPartrec.Cont.fix f k, v => h_5 f k v) =
    h_3 ns k v
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β],
  Finset.smul = { smul := Finset.image₂ fun x1 x2 => x1 • x2 }
-- Mathlib.Data.Set.Image
Set.preimage_eq_univ_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' s = Set.univ ↔ Set.range f ⊆ s
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (X_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.hom.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry_eq_get_minEntry? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {he : l.isEmpty = false},
  l.minEntry he = l.minEntry?.get ⋯
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_apply_map_symm_eq : ∀ {α : Type u_1} {β : Type u_2} {x : FreeMonoid β} (e : α ≃ β), (FreeMonoid.map ⇑e) ((FreeMonoid.map ⇑e.symm) x) = x
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- The edges of the disjoint sum of `G` and `H` are in bijection with
the disjoint sum of the edges of `G` and the edges of `H`  -/
SimpleGraph.edgeSetSumEquiv : {V : Type u_3} →
  {W : Type u_5} → {G : SimpleGraph V} → {H : SimpleGraph W} → ↑(G ⊕g H).edgeSet ≃ ↑G.edgeSet ⊕ ↑H.edgeSet
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_inverse_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).left = f.left
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_ediv_iff_of_dvd_of_pos_of_neg : ∀ {a b c d : ℤ}, 0 < b → d < 0 → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ c * b ≤ d * a)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.one_mul : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation F (MonCat.Colimits.Prequotient.one.mul x) x
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- If the submodule `P` has a basis, `x ∈ P` iff it is a linear combination of basis vectors.  -/
Module.Basis.mem_submodule_iff : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {P : Submodule R M} (b : Module.Basis ι R ↥P) {x : M}, x ∈ P ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
-- Std.Http.Data.Headers.Basic
/-- The `Transfer-Encoding` header, representing the list of transfer codings applied to the message body.

Validation rules (RFC 9112 Section 6.1):
- "chunked" may appear at most once.
- If "chunked" is present, it must be the last encoding in the list.

Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1
 -/
Std.Http.Header.TransferEncoding : Type
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextEdit.mk.inj : ∀ {range : Lean.Lsp.Range} {newText : String} {leanExtSnippet? : Option Lean.Lsp.SnippetString}
  {annotationId? : Option String} {range_1 : Lean.Lsp.Range} {newText_1 : String}
  {leanExtSnippet?_1 : Option Lean.Lsp.SnippetString} {annotationId?_1 : Option String},
  { range := range, newText := newText, leanExtSnippet? := leanExtSnippet?, annotationId? := annotationId? } =
      { range := range_1, newText := newText_1, leanExtSnippet? := leanExtSnippet?_1,
        annotationId? := annotationId?_1 } →
    range = range_1 ∧ newText = newText_1 ∧ leanExtSnippet? = leanExtSnippet?_1 ∧ annotationId? = annotationId?_1
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- The topology on `MvPowerSeries` is a right linear topology
when the ring of coefficients has a linear topology.  -/
MvPowerSeries.LinearTopology.instIsLinearTopologyMulOpposite : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  [IsLinearTopology Rᵐᵒᵖ R], IsLinearTopology (MvPowerSeries σ R)ᵐᵒᵖ (MvPowerSeries σ R)
-- Mathlib.Algebra.Order.Field.Power
abs_neg_one_zpow : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (p : ℤ), |(-1) ^ p| = 1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRupCheck.eq_1 : ∀ {n : ℕ} (rupHints : Array ℕ) (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.performRupCheck
      rupHints =
    match
      Array.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint clauses)
        (assignments, [], false, false) rupHints with
    | (assignments, derivedLits, derivedEmpty, encounteredError) =>
      ({ clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }, derivedLits,
        derivedEmpty, encounteredError)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.fixedPoints.eq_1 : ∀ (M : Type u_1) (α : Type u_3) [inst : AddMonoid M] [inst_1 : AddAction M α],
  AddAction.fixedPoints M α = {a | ∀ (m : M), m +ᵥ a = a}
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.nnnorm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α}, Measurable f → Measurable fun a => ‖f a‖₊
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Lean.LibrarySuggestions.SineQuaNon
/-- A global `IO.Ref` containing the "sine qua non" triggers. This is initialized on first use.  -/
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTriggersRef : IO.Ref (Option (Lean.NameMap (List (Lean.Name × Float))))
-- Mathlib.Algebra.Quandle
/-- `Conj` is functorial
 -/
Quandle.Conj.map : {G : Type u_2} →
  {H : Type u_3} → [inst : Group G] → [inst_1 : Group H] → (G →* H) → ShelfHom (Quandle.Conj G) (Quandle.Conj H)
-- Mathlib.Algebra.Category.Ring.Under.Basic
AlgEquiv.toUnder_trans : ∀ {R : CommRingCat} {A B C : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra (↑R) A] [inst_4 : Algebra (↑R) B] [inst_5 : Algebra (↑R) C] (f : A ≃ₐ[↑R] B) (g : B ≃ₐ[↑R] C),
  (f.trans g).toUnder = f.toUnder ≪≫ g.toUnder
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.isIso_toOfSimplex : ∀ {X : SSet} [X.Nonsingular] {n : ℕ}, ∀ x ∈ X.nonDegenerate n, CategoryTheory.IsIso (SSet.Subcomplex.toOfSimplex x)