mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d._auto_5) {Z : C}
  (h : X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_injective : ∀ {M : Type u_2} [inst : Add M], Function.Injective AddSubsemigroup.unop
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.declNames : Lean.Elab.PartialFixpoint.EqnInfo → Array Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom left map in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            CategoryTheory.MonoidalCategory.curriedTensorPostPost F ⟶
              CategoryTheory.MonoidalCategory.curriedTensorPostPost' F
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- It covers the `forget` for `C` and `D`  -/
CategoryTheory.HasForget₂.forget_comp : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))}
  {inst_2 : CategoryTheory.ConcreteCategory C FC} {D : Type u_3} {inst_3 : CategoryTheory.Category.{v_2, u_3} D}
  {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)}
  {inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))} {inst_5 : CategoryTheory.ConcreteCategory D FD}
  [self : CategoryTheory.HasForget₂ C D],
  CategoryTheory.HasForget₂.forget₂.comp (CategoryTheory.forget D) = CategoryTheory.forget C
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.mkInitialTacticInfo : Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM (Lean.Elab.Tactic.Grind.GrindTacticM Lean.Elab.Info)
-- Init.Prelude
/-- Gadget for marking output parameters in type classes.

For example, the `Membership` class is defined as:
```
class Membership (α : outParam (Type u)) (γ : Type v)
```
This means that whenever a typeclass goal of the form `Membership ?α ?γ` comes
up, Lean will wait to solve it until `?γ` is known, but then it will run
typeclass inference, and take the first solution it finds, for any value of `?α`,
which thereby determines what `?α` should be.

This expresses that in a term like `a ∈ s`, `s` might be a `Set α` or
`List α` or some other type with a membership operation, and in each case
the "member" type `α` is determined by looking at the container type.
 -/
outParam : Sort u → Sort u
-- Init.Data.UInt.Lemmas
UInt16.toNat_zero : UInt16.toNat 0 = 0
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Since `X` is transcendental over `K`, not all coefficients of `φ` can be in `K`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.exists_φ_coeff_not_mem : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → ∃ i, (RatFunc.Luroth.φ✝ E).coeff i ∉ (algebraMap K ↥E).range
-- Init.Data.UInt.Bitwise
UInt16.xor_comm : ∀ (a b : UInt16), a ^^^ b = b ^^^ a
-- Init.Data.List.Control
List.foldlM.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {s : Type u} {α : Type w} (x : s → α → m s) (x_1 : s),
  List.foldlM x x_1 [] = pure x_1
-- Init.Data.Iterators.Basic
/-- Converts a pure iterator (`Iter β`) into a monadic iterator (`IterM Id β`) in the
identity monad `Id`.
 -/
Std.Iter.toIterM : {α β : Type w} → Std.Iter β → Std.IterM Id β
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubmonoid.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] (s : Set α),
  fixingAddSubmonoid M s = { carrier := {ϕ | ∀ (x : ↑s), ϕ +ᵥ ↑x = ↑x}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderiv.fst : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G},
  DifferentiableAt 𝕜 f₂ x → fderiv 𝕜 (fun x => (f₂ x).1) x = ContinuousLinearMap.fst 𝕜 F G ∘SL fderiv 𝕜 f₂ x
-- Mathlib.Data.EReal.Inv
EReal.inv_lt_top : ∀ (x : EReal), x⁻¹ < ⊤
-- Mathlib.Analysis.Complex.Exponential
Real.exp_lt_two_add_div_two_sub : ∀ {x : ℝ}, 0 < x → x < 2 → Real.exp x < (2 + x) / (2 - x)
-- Lean.Util.SafeExponentiation
Lean.exponentiation.threshold : Lean.Option ℕ
-- Init.Grind.Lemmas
Lean.Grind.imp_eq_of_eq_true_left : ∀ {a b : Prop}, a = True → (a → b) = b
-- Mathlib.Order.Heyting.Basic
toDual_sdiff : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a b : α),
  OrderDual.toDual (b \ a) = OrderDual.toDual a ⇨ OrderDual.toDual b
-- Lean.Parser.Command
Lean.Parser.Command.structInstBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.codRestrict.congr_simp : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σS : Type u_2}
  [inst_2 : SetLike σS S] [inst_3 : SubsemiringClass σS S] (f f_1 : R →+* S) (e_f : f = f_1) (s : σS)
  (h : ∀ (x : R), f x ∈ s), f.codRestrict s h = f_1.codRestrict s ⋯
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A ring with finite quotients has only finitely many nonzero prime ideals of bounded norm.  -/
Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] (B : ℕ), {p | Submodule.cardQuot p.asIdeal ≤ B}.Finite
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetWRT ν)` is sigma-finite and for all
measurable sets `t ⊆ sᶜ`, either `ν t = 0` or `μ t = ∞`.  -/
MeasureTheory.Measure.sigmaFiniteSetWRT : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Set α
-- Lean.Parser.Command
/-- Registers a tactic tag, saving its user-facing name and docstring.

Tactic tags can be used by documentation generation tools to classify related tactics.
 -/
Lean.Parser.Command.register_tactic_tag : Lean.Parser.Parser
-- Std.Data.ExtHashSet.Basic
/-- Hash sets.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
and an array of buckets, where each bucket is a linked list of keys. The number of buckets
is always a power of two. The hash set doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
avoid expensive copies.

The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

In contrast to regular hash sets, `Std.ExtHashSet` offers several extensionality lemmas
and therefore has more lemmas about equality of hash maps. This however also makes it lose the
ability to iterate freely over hash sets.

These hash sets contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.HashSet.Raw` and
`Std.HashSet.Raw.WF` unbundle the invariant from the hash set. When in doubt, prefer
`HashSet` or `ExtHashSet` over `HashSet.Raw`.
 -/
Std.ExtHashSet : (α : Type u) → [BEq α] → [Hashable α] → Type u
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_zero_adj : ∀ {u v : Fin 0}, ¬(SimpleGraph.cycleGraph 0).Adj u v
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_lt_top : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ProbabilityTheory.evariance X μ < ⊤
-- Aesop.Tree.ExtractScript
Aesop.ExtractScript.visitRapp : Aesop.Rapp → Aesop.ExtractScriptM Unit
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.map_isStrictlySupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} {D : Type u_4}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Category.{v_2, u_4} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (K : HomologicalComplex C c') (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (e : c.Embedding c') [K.IsStrictlySupported e], ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.containsThenInsertIfNew k v).1 = t.contains k
-- Lean.Meta.Sym.SymM
/-- Adds an issue message to the issue tracker.  -/
Lean.Meta.Sym.reportIssue : Lean.MessageData → Lean.Meta.Sym.SymM Unit
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α}
  {hc : t.minD fallback ∈ t}, t.get (t.minD fallback) hc = t.minD fallback
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.congr_eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) (id : ℕ) (rupHints : Array ℕ),
  step = some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) →
    (match step with
      | none => h_1 ()
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) ≍
      h_2 id rupHints
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.giMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f), Submonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.recvSelector : {α : Type} → Std.CloseableChannel.Unbounded✝ α → Std.Async.Selector (Option α)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.posPart_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : LinearOrder γ] [inst_3 : OrderClosedTopology γ] [inst_4 : Zero γ] (f : α → γ)
  (hf : MeasureTheory.AEStronglyMeasurable f μ),
  (MeasureTheory.AEEqFun.mk f hf).posPart = MeasureTheory.AEEqFun.mk (fun x => max (f x) 0) ⋯
-- Aesop.Forward.State
/-- Inserts a hyp associated with slot `slot` and instantiation `inst`.
The hyp must be a valid assignment for the slot's premise. Returns `true` if
the hyp was not previously associated with `slot` and `inst`.  -/
Aesop.InstMap.insertHyp : Aesop.InstMap → Aesop.SlotIndex → Lean.Expr → Aesop.Hyp → Lean.MetaM (Aesop.InstMap × Bool)
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleDefinition : Lean.Server.GoToKind →
  Lean.Lsp.TextDocumentPositionParams → Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.LeanLocationLink))
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.gradeBy.gradedAlgebra : {M : Type u_1} →
  {ι : Type u_2} →
    {R : Type u_3} →
      [inst : AddMonoid M] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : CommSemiring R] → (f : M →+ ι) → GradedAlgebra (AddMonoidAlgebra.gradeBy R ⇑f)
-- Lean.Elab.DefView
Lean.Elab.DefView.ref : Lean.Elab.DefView → Lean.Syntax
-- Init.Data.UInt.Lemmas
UInt16.toUSize_inj : ∀ {a b : UInt16}, a.toUSize = b.toUSize ↔ a = b
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.isAlgebraic_iff : ∀ {R : Type u_1} {S : Type v} {A : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [IsDomain S]
  [NoZeroDivisors A] {ι : Type u_2} {v : ι → A},
  IsTranscendenceBasis R v → (Algebra.IsAlgebraic S A ↔ ∀ (i : ι), IsAlgebraic S (v i))
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.tendsto_units : ∀ {α : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : α → Γ₀} {γ₀ : Γ₀ˣ},
  Filter.Tendsto f l (nhds ↑γ₀) ↔ ∀ᶠ (x : α) in l, f x = ↑γ₀
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Adjunction.sheafPushforwardContinuous_unit_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K] [inst_4 : G.IsContinuous K J]
  (P : CategoryTheory.Sheaf K E) (X : Dᵒᵖ),
  ((adj.sheafPushforwardContinuous J K).unit.app P).hom.app X = P.obj.map (adj.counit.app (Opposite.unop X)).op
-- Plausible.ArbitraryFueled
/-- Every `ArbitraryFueled` instance gives rise to an `Arbitrary` instance  -/
Plausible.instArbitraryOfArbitraryFueled : {α : Type} → [Plausible.ArbitraryFueled α] → Plausible.Arbitrary α
-- Init.Data.SInt.Bitwise
Int8.or_zero : ∀ {a : Int8}, a ||| 0 = a
-- Lean.Elab.Tactic.Try
/-- Environment extension for user try suggestion generators (supports local scoping)  -/
Lean.Elab.Tactic.Try.trySuggestionExtension : Lean.SimpleScopedEnvExtension Lean.Elab.Tactic.Try.TrySuggestionEntry (Array Lean.Elab.Tactic.Try.TrySuggestionEntry)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A set of points is concyclic if it is cospherical and coplanar. (Most results are stated
directly in terms of `Cospherical` instead of using `Concyclic`.)  -/
EuclideanGeometry.Concyclic : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] → [NormedSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → Set P → Prop
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  K < 1 → S.Nonempty → A.Nonempty → 0 < Finset.expansion✝ K S A
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.rank_eq : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : LinearOrder m]
  [inst_3 : LinearOrder n] [inst_4 : CommRing R] [IsDomain R] {A : Matrix m n R} {l : m → WithTop n},
  A.IsPivotedBy l → A.rank = {i | l i ≠ ⊤}.card
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instFunLikeContMDiffAddMonoidMorphism.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : AddMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : AddMonoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'],
  instFunLikeContMDiffAddMonoidMorphism = { coe := fun a => (↑a.toAddMonoidHom).toFun, coe_injective := ⋯ }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functorialityEquivalence_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cocone.functorialityEquivalence F e).inverse =
    (CategoryTheory.Limits.Cocone.functoriality (F.comp e.functor) e.inverse).comp
      (CategoryTheory.Limits.Cocone.precomposeEquivalence
          (F.associator e.functor e.inverse ≪≫ F.isoWhiskerLeft e.unitIso.symm ≪≫ F.rightUnitor)).functor
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- If `f : ℂ → E` is continuous on the closed annulus `r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`,
and is complex differentiable at all but countably many points of its interior,
then the integrals of `f z / (z - c)` (formally, `(z - c)⁻¹ • f z`)
over the circles `‖z - c‖ = r` and `‖z - c‖ = R` are equal to each other.  -/
Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r R : ℝ},
  0 < r →
    r ≤ R →
      ∀ {f : ℂ → E} {s : Set ℂ},
        s.Countable →
          ContinuousOn f (Metric.closedBall c R \ Metric.ball c r) →
            (∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) →
              ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafificationNatIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (X : CategoryTheory.Sheaf J D),
  ((CategoryTheory.sheafificationNatIso J D).hom.app X).hom = CategoryTheory.toSheafify J X.obj
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.repr_CotangentSpaceMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  {P : Algebra.Generators R S ι} {R' : Type u'} {S' : Type v'} {ι' : Type w'} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : P.Hom P') (i : ι) (j : ι'),
  (P'.cotangentSpaceBasis.repr ((Algebra.Extension.CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j =
    (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))
-- Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
/-- The connection maps in the contravariant long exact sequence of `Ext` are surjective if
the middle term of the short exact sequence is projective.  -/
precomp_extClass_surjective_of_projective_X₂ : ∀ {R : Type u} [inst : Ring R] [inst_1 : Small.{v, u} R] (M : ModuleCat R)
  {S : CategoryTheory.ShortComplex (ModuleCat R)} (h : S.ShortExact) (n : ℕ) [CategoryTheory.Projective S.X₂],
  Function.Surjective ⇑(h.extClass.precomp M ⋯)
-- Mathlib.Data.Set.Finite.Lattice
Finite.Set.finite_sUnion : ∀ {α : Type u} {s : Set (Set α)} [Finite ↑s] [H : ∀ (t : ↑s), Finite ↑↑t], Finite ↑(⋃₀ s)
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toStarModule : ∀ {A : Type u_1} [self : CStarAlgebra A], StarModule ℂ A
-- Mathlib.Geometry.Manifold.Submersion
/-- A choice of chart on the codomain `N` of a submersion `f` at `x`:
w.r.t. this chart and the data `h.domChart` and `h.equiv`,
`f` will look like a projection `(u, v) ↦ u` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.equiv` and `h.domChart`.  -/
Manifold.IsSubmersionAtOfComplement.codChart : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsSubmersionAtOfComplement F I J n f x →
                                                      OpenPartialHomeomorph N G
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.tactic.simp.user.exampleString : Lean.Option String
-- Mathlib.Data.Set.Image
Set.image_compl_eq_range_sdiff_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), f '' sᶜ = Set.range f \ f '' s
-- Mathlib.Data.Set.Image
Set.image_nontrivial : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Function.Injective f → ((f '' s).Nontrivial ↔ s.Nontrivial)
-- Mathlib.Topology.Inseparable
SeparationQuotient.instNonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Nonempty X], Nonempty (SeparationQuotient X)
-- Init.Data.List.ToArray
List.sum.eq_1 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α], List.sum = List.foldr (fun x1 x2 => x1 + x2) 0
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisorsLeft_iff : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] {x : M₀}, x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (y : M₀), x * y = 0 → y = 0
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State.mk.sizeOf_spec : ∀ (visited : Lean.NameSet) (result : Array Lean.LocalDecl),
  sizeOf { visited := visited, result := result } = 1 + sizeOf visited + sizeOf result