mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : S.LeftHomologyData), S.Exact ↔ CategoryTheory.Epi h.f'
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.Monadic.step.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (next : α) → motive (some next)),
  (match none with
    | none => h_1 ()
    | some next => h_2 next) =
    h_1 ()
-- Mathlib.Data.List.Basic
List.getElem_fin_surjective_iff : ∀ {α : Type u} {l : List α}, (Function.Surjective fun n => l[↑n]) ↔ ∀ (x : α), x ∈ l
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ne_of_mem_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.sphere x ε → ε ≠ 0 → y ≠ x
-- Aesop.Tree.Free
_private.Aesop.Tree.Free.0.Aesop.freeGoalRef : Aesop.GoalRef → Aesop.MVarClusterRef → Aesop.GoalRef → BaseIO Unit
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.image : ∀ {R : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] {s : Set M} {f : M →ₗ[R] M'},
  LinearIndepOn R id s → Disjoint (Submodule.span R s) f.ker → LinearIndepOn R id (⇑f '' s)
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finite_finsupp_self_iff : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1}, Module.Finite R (ι →₀ R) ↔ Subsingleton R ∨ Finite ι
-- Mathlib.Analysis.Real.Sqrt
Continuous.sqrt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ}, Continuous f → Continuous fun x => √(f x)
-- Mathlib.Algebra.Group.AddChar
/-- The function maps addition in `A` to multiplication in `M`.

Do not use this directly. Instead use `AddChar.map_add_eq_mul`.  -/
AddChar.map_add_eq_mul' : ∀ {A : Type u_1} [inst : AddMonoid A] {M : Type u_2} [inst_1 : Monoid M] (self : AddChar A M) (a b : A),
  self.toFun (a + b) = self.toFun a * self.toFun b
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsClosedEmbedding.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsClosedEmbedding f), Topology.IsClosedEmbedding (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearComp_zero : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  {E' : Type u_11} {F' : Type u_12} [inst_9 : SeminormedAddCommGroup E'] [inst_10 : SeminormedAddCommGroup F']
  {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [inst_11 : NontriviallyNormedField 𝕜₁'] [inst_12 : NontriviallyNormedField 𝕜₂']
  [inst_13 : NormedSpace 𝕜₁' E'] [inst_14 : NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
  {σ₂₃' : 𝕜₂' →+* 𝕜₃} [inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃']
  [inst_17 : RingHomIsometric σ₂₃] [inst_18 : RingHomIsometric σ₁₃'] [inst_19 : RingHomIsometric σ₂₃']
  {gE : E' →SL[σ₁'] E} {gF : F' →SL[σ₂'] F}, ContinuousLinearMap.bilinearComp 0 gE gF = 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one_def : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons 0 Tactic.ComputeAsymptotics.MultiseriesExpansion.one
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- A finite set of group elements witnessing that `f` is an equidecomposition.  -/
Equidecomp.witness : {X : Type u_1} → {G : Type u_2} → [inst : SMul G X] → Equidecomp X G → Finset G
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.of_X : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0),
  (ChainComplex.of X d sq).X = X
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult : Type
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.comap_singleton_isClosed_of_surjective : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → ∀ (x : PrimeSpectrum S), IsClosed {x} → IsClosed {PrimeSpectrum.comap f x}
-- Mathlib.Data.Quot
Quotient.liftOn₂'_mk : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s : Setoid α} {t : Setoid β} (f : α → β → γ)
  (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s a₁ b₁ → t a₂ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β),
  ⟦a⟧.liftOn₂' ⟦b⟧ f h = f a b
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_setPreimage : ∀ {α : Type u_2} {β : Type u_3} (f : α → β), ⇑(CompleteLatticeHom.setPreimage f) = Set.preimage f
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution G F] (x : C × C),
  (CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting F G).app x =
    CategoryTheory.CategoryStruct.comp (β_ ((F, G).1.obj x.1) ((F, G).2.obj x.2)).hom
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit G F).app (x.2, x.1))
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution G F).map (β_ (x.2, x.1).1 (x.2, x.1).2).hom))
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.mk : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          {A B : HomologicalComplex V c} →
            (f : (i : ι) → A.X i ⟶ B.X i) →
              autoParam
                  (∀ (i j : ι),
                    c.Rel i j →
                      CategoryTheory.CategoryStruct.comp (f i) (B.d i j) =
                        CategoryTheory.CategoryStruct.comp (A.d i j) (f j))
                  HomologicalComplex.Hom.comm'._autoParam →
                A.Hom B
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRicIterIteratorOfUpwardEnumerableOfLeast? : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.ToStream (Std.Ric α) (Std.Iter α)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioo_pred_left_eq_Ioc_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Finset.Ioo (Order.pred a) b = Finset.Ico a b
-- Lean.Elab.Tactic.Grind.Param
/-- Removes all theorems that are not `match`-equations nor local theorems.
 -/
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.Grind.filterThms : Lean.PArray Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.GrindM (Lean.PArray Lean.Meta.Grind.EMatchTheorem)
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A locally Noetherian scheme is quasi-separated.  -/
AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X], QuasiSeparatedSpace ↥X
-- Mathlib.Algebra.MonoidAlgebra.Grading
/-- `AddMonoidAlgebra.gradeBy` describe an internally graded algebra.  -/
AddMonoidAlgebra.gradeBy.isInternal : ∀ {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 →+ ι), DirectSum.IsInternal (AddMonoidAlgebra.gradeBy R ⇑f)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.uniformInducing_toMatrixAux : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalCStarAlgebra A] [inst_3 : PartialOrder A] [inst_4 : StarOrderedRing A],
  IsUniformInducing ⇑CStarMatrix.ofMatrix.symm
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then
`ω ↦ exp (|t| * |X| + v * X)` is integrable.  -/
ProbabilityTheory.integrable_exp_abs_mul_abs_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (|t| * |X ω| + v * X ω)) μ
-- Mathlib.Data.Num.Bitwise
/-- Add an inactive bit at the end of a `NzsNum`. This mimics `PosNum.bit0`.  -/
NzsNum.bit0 : NzsNum → NzsNum
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.iso_hom : ∀ {X : SSet} [inst : X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n),
  (SSet.Nonsingular.iso x hx).hom = SSet.Subcomplex.toOfSimplex x
-- Mathlib.Tactic.Use
/-- `use e₁, e₂, ⋯` instantiates all existential quantifiers in the main goal by using `e₁`, `e₂`, ...
as witnesses, creates goals for all the remaining witnesses, and tries to discharge these goals
automatically.

`use` is similar to `exists` or `existsi`, but unlike `exists` it is equivalent to applying the
tactic `refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩` with any number of placeholders (rather than just one) and
then trying to close goals associated to the placeholders with a configurable discharger (rather
than just `try trivial`).

* `use! e₁, e₂, ⋯` applies constructors everywhere rather than just for goals that correspond to the
  last argument of a constructor. This gives the effect that nested constructors are being flattened
  out, with the supplied values being used along the leaves and nodes of the tree of constructors.
* `use (discharger := tac) e₁, e₂, ...` calls `tac` as a discharger, on all remaining `Prop`-valued
  goals. If this option is omitted, `use` calls `try with_reducible use_discharger` as default
  discharger.
  To turn off the discharger and keep all goals, use `(discharger := skip)`.
  To allow "heavy refls", use `(discharger := try use_discharger)`.
  If `tac` fails on the new goal, `use (discharger := tac)` fails (hint: you might want to use
  `(discharger := try tac)` instead).

Examples:

```lean
example : ∃ x : Nat, x = x := by use 42

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42

example : Nonempty Nat := by use 5

example : Nonempty (PNat ≃ Nat) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

-- With `use!` one can feed in each `42` one at a time:
example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
/-
The second line makes use of the fact that `use!` tries refining with the argument before
applying a constructor. Also note that `use`/`use!` by default uses a tactic
called `use_discharger` to discharge goals, so `use! 42` will close the goal in this example since
`use_discharger` applies `rfl`, which as a consequence solves for the other `Nat` metavariable.
-/
```
 -/
Mathlib.Tactic.«tacticUse!___,,» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₃.X₁` is the cokernel of `v₁₂.τ₁ : L₁.X₁ ⟶ L₂.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₃τ₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.v₂₃.τ₁ ⋯)
-- Init.Data.List.ToArray
List.replace_toArray : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l : List α) (a b : α), l.toArray.replace a b = (l.replace a b).toArray
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.eval.eq_1 : ∀ (lc : Lean.Omega.LinearCombo) (values : Lean.Omega.Coeffs), lc.eval values = lc.const + lc.coeffs.dot values
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_mk0 : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))),
  (ClassGroup.mk K) ((FractionalIdeal.mk0 K) I) = ClassGroup.mk0 I
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A sum over `s.subtype p` equals one over `{x ∈ s | p x}`.  -/
Finset.sum_subtype_eq_sum_filter : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (f : ι → M) {p : ι → Prop}
  [inst_1 : DecidablePred p], ∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s with p x, f x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproductBiproductIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)]
  [inst_3 : CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i],
  (CategoryTheory.Limits.biproductBiproductIso f g).inv =
    CategoryTheory.Limits.biproduct.lift fun i =>
      CategoryTheory.Limits.biproduct.lift fun x => CategoryTheory.Limits.biproduct.π (fun p => g p.fst p.snd) ⟨i, x⟩
-- Mathlib.Probability.Density
/-- Random variables are independent iff their joint density is a product of marginal densities.  -/
MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : MeasurableSpace F] {ν : MeasureTheory.Measure F} {X : Ω → E}
  {Y : Ω → F} [MeasureTheory.IsFiniteMeasure ℙ] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)],
  ProbabilityTheory.IndepFun X Y ℙ ↔
    MeasureTheory.pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z =>
      MeasureTheory.pdf X ℙ μ z.1 * MeasureTheory.pdf Y ℙ ν z.2
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsFibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y]
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))),
  (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).Z = h.Z
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.hasForgetToSemigroup.eq_1 : MonCat.hasForgetToSemigroup =
  {
    forget₂ :=
      { obj := fun M => Semigrp.of ↑M, map := fun {X Y} f => Semigrp.ofHom ↑(MonCat.Hom.hom f),
        map_id := MonCat.hasForgetToSemigroup._proof_1, map_comp := @MonCat.hasForgetToSemigroup._proof_2 },
    forget_comp := MonCat.hasForgetToSemigroup._proof_4 }
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `Polynomial.Gal.galAction` as a permutation representation  -/
Polynomial.Gal.galActionHom : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] →
            [Fact (Polynomial.map (algebraMap F E) p).Splits] → p.Gal →* Equiv.Perm ↑(p.rootSet E)
-- Mathlib.Algebra.Group.Basic
sub_eq_neg_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), a - b = -b + a
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_neg : ∀ {𝕜 : 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'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieAddGroup I' n G] (f : ContMDiffMap I I' N G n), ⇑(-f) = -⇑f
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k k' : α},
  (k == k') = true → k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).get? k' = some k
-- Mathlib.Order.BoundedOrder.Monotone
StrictMono.apply_eq_bot_iff : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : Preorder β] {f : α → β} {a : α},
  StrictMono f → (f a = f ⊥ ↔ a = ⊥)
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- `Functor.toCostructuredArrow` can be expressed in terms of `Cocone.toCostructuredArrow`.  -/
CategoryTheory.Functor.toCostructuredArrowIsoToCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (G : CategoryTheory.Functor J K) →
              (F : CategoryTheory.Functor K C) →
                (X : C) →
                  (f : (Y : J) → F.obj (G.obj Y) ⟶ X) →
                    (h : ∀ {Y Z : J} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) →
                      G.toCostructuredArrow F X f ⋯ ≅
                        { pt := X, ι := { app := f, naturality := ⋯ } }.toCostructuredArrow.comp
                          (CategoryTheory.CostructuredArrow.pre G F { pt := X, ι := { app := f, naturality := ⋯ } }.pt)
-- Mathlib.Computability.Primrec.List
Primrec.nat_sqrt : Primrec Nat.sqrt
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveCoyonedaObj_obj_carrier : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C),
  ↑((CategoryTheory.preadditiveCoyonedaObj X).obj Y) = (X ⟶ Y)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
SSet.Edge.mk.congr_simp : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (edge edge_1 : X.obj (Opposite.op { len := 1 }))
  (e_edge : edge = edge_1)
  (src_eq : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) edge = x₀)
  (tgt_eq : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) edge = x₁),
  SSet.Edge.mk edge src_eq tgt_eq = SSet.Edge.mk edge_1 ⋯ ⋯
-- Mathlib.Topology.MetricSpace.Polish
/-- A distance on an open subset `s` of a metric space, designed to make it complete.  It is given
by `dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|`, where the second term blows up close to
the boundary to ensure that Cauchy sequences for `dist'` remain well inside `s`.  -/
TopologicalSpace.Opens.CompleteCopy.instDist : {α : Type u_1} → [inst : MetricSpace α] → {s : TopologicalSpace.Opens α} → Dist s.CompleteCopy
-- Mathlib.Order.RelClasses
/-- All values are accessible under the well-founded relation.  -/
IsWellFounded.apply : ∀ {α : Type u} (r : α → α → Prop) [IsWellFounded α r] (a : α), Acc r a
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofNat_re : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo], RCLike.re (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_add_le_self : ∀ {p a : ℕ} [hp : Fact (Nat.Prime p)], p < a → padicValNat p a + p ≤ a
-- Qq.Typ
Qq.instReprQuoted : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_empty : ∀ {α : Type u_2} [inst : Monoid α], ThreeGPFree ∅
-- Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A] [inst_3 : CategoryTheory.MonoidalCategory A]
      [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A]
      {FC : A → A → Type u_1} {CC : A → Type w} [inst_6 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)]
      [inst_7 : CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A]
      [(CategoryTheory.forget A).ReflectsIsomorphisms]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [∀ (X : A),
          CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
            (CategoryTheory.MonoidalCategory.tensorLeft X)]
      [∀ (X : A),
          CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
            (CategoryTheory.MonoidalCategory.tensorRight X)]
      [J.HasSheafCompose (CategoryTheory.forget A)], J.W.IsMonoidal
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.instDecidableRelAdjToGraphOfDecidableEq : {α : Type u_1} →
  {V : Type u_2} →
    {A : Matrix V V α} →
      [inst : MulZeroOneClass α] →
        [inst_1 : Nontrivial α] → [DecidableEq α] → (h : A.IsAdjMatrix) → DecidableRel h.toGraph.Adj
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.isMittagLeffler_iff_eventualRange : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)),
  F.IsMittagLeffler ↔ ∀ (j : J), ∃ i f, F.eventualRange j = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
/-- The canonical morphism `(pullback.{u} φ).obj (unit S) ⟶ unit R`
of sheaves of modules corresponding to a continuous map between ringed sites.  -/
SheafOfModules.pullbackObjUnitToUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] →
                        (SheafOfModules.pullback φ).obj (SheafOfModules.unit S) ⟶ SheafOfModules.unit R
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.piCongrRight_symm_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {ι : Type u_9} {M : ι → Type u_10} [inst_1 : (i : ι) → TopologicalSpace (M i)]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R₁ (M i)] {N : ι → Type u_11}
  [inst_4 : (i : ι) → TopologicalSpace (N i)] [inst_5 : (i : ι) → AddCommMonoid (N i)]
  [inst_6 : (i : ι) → Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i) (n : (i : ι) → N i) (i : ι),
  (ContinuousLinearEquiv.piCongrRight f).symm n i = (f i).symm (n i)
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] → [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → FunLike (EsakiaHom α β) α β