mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The isomorphism from `A` to its copy under `f : Copy A B`.  -/
SimpleGraph.Copy.isoToSubgraph : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → (f : A.Copy B) → A ≃g f.toSubgraph.coe
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doIf; doElems`
`doIf` is of the form
```
"if " >> optIdent >> termParser >> " then " >> doSeq
 >> many (group (try (group (" else " >> " if ")) >> optIdent >> termParser >> " then " >> doSeq))
 >> optional (" else " >> doSeq)
```   -/
Lean.Elab.Term.Do.ToCodeBlock.doIfToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Std.Time.Internal.UnitVal
/-- Cast a UnitVal through an equality in the rational numbers.  -/
Std.Time.Internal.UnitVal.cast : {a b : ℚ} → a = b → Std.Time.Internal.UnitVal a → Std.Time.Internal.UnitVal b
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.Tendsto.prod_atBot : ∀ {α : Type u_3} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder γ] {f g : α → γ},
  Filter.Tendsto f Filter.atBot Filter.atBot →
    Filter.Tendsto g Filter.atBot Filter.atBot → Filter.Tendsto (Prod.map f g) Filter.atBot Filter.atBot
-- Std.Sat.AIG.Basic
/-- Create an empty `Cache`, valid with respect to any `Array Decl`.
 -/
Std.Sat.AIG.Cache.empty : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → {decls : Array (Std.Sat.AIG.Decl α)} → Std.Sat.AIG.Cache α decls
-- Mathlib.Analysis.Complex.ReImTopology
Bornology.IsBounded.reProdIm : ∀ {s t : Set ℝ}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s ×ℂ t)
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_filter.instNeBot : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α} [f.NeBot], (a +ᵥ f).NeBot
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddCommMonoid β]
  (T : Set α → β),
  T ∅ = 0 →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ {ι : Type u_8} (S : ι → Set α) (sι : Finset ι),
        (∀ (i : ι), MeasurableSet (S i)) →
          (∀ i ∈ sι, μ (S i) ≠ ⊤) →
            (∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.numPrec : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_mul_Ioi_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b : α),
  Set.Ici a * Set.Ioi b ⊆ Set.Ioi (a * b)
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceOperator_inner : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_4 : CompleteSpace E],
  MeasureTheory.MemLp id 2 μ →
    ∀ (x y : E), inner ℝ ((ProbabilityTheory.covarianceOperator μ) x) y = ∫ (z : E), inner ℝ x z * inner ℝ y z ∂μ
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousOn.norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun x => ‖f x‖) s
-- Mathlib.Data.List.GetD
List.getI_cons_zero : ∀ {α : Type u} (x : α) (xs : List α) [inst : Inhabited α], (x :: xs).getI 0 = x
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.hom_ext_iff : ∀ {X Y : TwoP} {f g : X ⟶ Y}, f = g ↔ f.hom = g.hom
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestMatchAt_of_get : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  p (pos.get h) = true → String.Slice.Pattern.Model.IsLongestMatchAt p pos (pos.next h)
-- Mathlib.Order.SymmDiff
sdiff_symmDiff_eq_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff (a \ b) b = a ⊔ b
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.aeval_X_g_mul_mk_X : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  (Polynomial.aeval P.X) P.g *
      (Ideal.Quotient.mk (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})) Polynomial.X =
    1
-- Std.Time.Format.Modifier
Std.Time.Modifier.m.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.m presentation = Std.Time.Modifier.m presentation_1 → presentation = presentation_1
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `biUnion`).  -/
MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set ι} {s : ι → Set α},
  S.Countable → ⋃ i ∈ S, s i = Set.univ → (μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i))
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instInv : {α : Type u_1} → [Inv α] → Inv (Lex α)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_le_subst_cert.eq_1 : ∀ (x : Lean.Grind.Linarith.Var) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_le_subst_cert x p₁ p₂ p₃ =
    (decide (p₁.coeff x ≥ 0) && p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioi_disjoint_Iio_same : ∀ {α : Type v} [inst : Preorder α] {a : α}, Disjoint (Set.Ioi a) (Set.Iio a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.map_equation : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (x y : R), (W.map f).Equation (f x) (f y) ↔ W.Equation x y
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.of_prod_left : ∀ {α : Type u_1} {I : Type u_2} [inst : CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I},
  IsRelPrime (∏ i ∈ t, s i) x → ∀ i ∈ t, IsRelPrime (s i) x
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Multiset.card_finsuppSum : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} [inst : Zero M] (f : ι →₀ M) (g : ι → M → Multiset α),
  (f.sum g).card = f.sum fun i m => (g i m).card
-- Lean.Structure
Lean.StructureResolutionOrderResult.mk : Array Lean.Name → Array Lean.StructureResolutionOrderConflict → Lean.StructureResolutionOrderResult
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_fromEdgeSet : ∀ {V : Type u} (s : Set (Sym2 V)), (SimpleGraph.fromEdgeSet s).edgeSet = s \ Sym2.diagSet
-- Mathlib.CategoryTheory.Category.GaloisConnection
/-- An adjunction between preorder categories induces a Galois connection.
 -/
CategoryTheory.Adjunction.gc : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] {L : CategoryTheory.Functor X Y}
  {R : CategoryTheory.Functor Y X} (adj : L ⊣ R), GaloisConnection L.obj R.obj
-- Mathlib.Logic.Equiv.Defs
/-- Restatement of `Equiv.right_inv` in terms of `Function.RightInverse`.  -/
Equiv.right_inv' : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.RightInverse ⇑e.symm ⇑e
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetSourceParams.pos : Lean.Widget.GetWidgetSourceParams → Lean.Lsp.Position
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_isIso_leftRightHomologyComparison' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData)
  [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)], S.HasHomology
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqAuthority.beq : Std.Http.URI.Authority → Std.Http.URI.Authority → Bool
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesMap_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  X.opcyclesMap f g f g (CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.mk₂ f g)) n =
    CategoryTheory.CategoryStruct.id (X.opcycles f g n)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsStackFor_generate_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Presieve S), F.IsStackFor (CategoryTheory.Sieve.generate R).arrows ↔ F.IsStackFor R
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- **Alias** of `le_mul_of_le_right`. -/
le_mul_left : ∀ {α : Type u} [inst : Mul α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b c : α}, a ≤ c → a ≤ b * c
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Ici : ∀ (x : ↑unitInterval), MeasureTheory.volume (Set.Ici x) = ENNReal.ofReal (1 - ↑x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.splitter : (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) →
  (w : ℕ) →
    (x : Std.Tactic.BVDecide.BVExpr w) →
      ((w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx)) →
        ((w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val)) →
          ((len w start : ℕ) →
              (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr)) →
            ((w : ℕ) →
                (lhs : Std.Tactic.BVDecide.BVExpr w) →
                  (op : Std.Tactic.BVDecide.BVBinOp) →
                    (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs)) →
              ((w : ℕ) →
                  (op : Std.Tactic.BVDecide.BVUnOp) →
                    (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand)) →
                ((w l r : ℕ) →
                    (lhs : Std.Tactic.BVDecide.BVExpr l) →
                      (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h)) →
                  ((w w_1 n : ℕ) →
                      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
                        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h)) →
                    ((w n : ℕ) →
                        (lhs : Std.Tactic.BVDecide.BVExpr w) →
                          (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs)) →
                      ((w n : ℕ) →
                          (lhs : Std.Tactic.BVDecide.BVExpr w) →
                            (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs)) →
                        ((w n : ℕ) →
                            (lhs : Std.Tactic.BVDecide.BVExpr w) →
                              (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)) →
                          motive w x
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.findLeadingSpacesSize.consumeSpaces.eq_def : ∀ {s : String} (it : s.Pos) (curr min : ℕ),
  String.findLeadingSpacesSize.consumeSpaces✝ it curr min =
    if h : it.IsAtEnd then min
    else
      if (it.get h == ' ' || it.get h == '\t') = true then
        String.findLeadingSpacesSize.consumeSpaces✝ (it.next h) (curr + 1) min
      else
        if (it.get h == '\n') = true then String.findLeadingSpacesSize.findNextLine✝ (it.next h) min
        else String.findLeadingSpacesSize.findNextLine✝ (it.next h) (curr.min min)
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
/-- See equation (68), page 285 of [Jacobson, *Basic Algebra I, 4.12*][jacobson1974].

Given a polynomial `f` with integer coefficients, we can find a constant `c : ℝ` and for each prime
`p > |f₀|`, `nₚ : ℤ` and `gₚ : ℤ[X]` such that

* `p` does not divide `nₚ`
* `deg(gₚ) < p * deg(f)`
* all complex roots `r` of `f` satisfy `|nₚ * e ^ r - p * gₚ(r)| ≤ c ^ p / (p - 1)!`

In the proof of Lindemann-Weierstrass, we will take `f` to be a polynomial whose complex roots
are the algebraic numbers whose exponentials we want to prove to be linearly independent.

Note: Jacobson writes `Nₚ` for our `nₚ` and `M` for our `c` (modulo a constant factor).
 -/
LindemannWeierstrass.exp_polynomial_approx : ∀ (f : Polynomial ℤ),
  Polynomial.eval 0 f ≠ 0 →
    ∃ c,
      ∀ p > (Polynomial.eval 0 f).natAbs,
        Nat.Prime p →
          ∃ n,
            ¬↑p ∣ n ∧
              ∃ gp,
                gp.natDegree ≤ p * f.natDegree - 1 ∧
                  ∀ {r : ℂ},
                    r ∈ f.aroots ℂ → ‖n • Complex.exp r - p • (Polynomial.aeval r) gp‖ ≤ c ^ p / ↑(p - 1).factorial
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.toRatVec_mono : ∀ {ι : Type u_3} (x y : ι → ℕ), toRatVec✝ x ≤ toRatVec✝ y ↔ x ≤ y
-- Mathlib.Order.BooleanAlgebra.Basic
eq_of_sdiff_eq_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ≤ z → y ≤ z → z \ x = z \ y → x = y
-- Mathlib.Analysis.Analytic.Constructions
/-- The Cartesian product of analytic functions is analytic.  -/
AnalyticOnNhd.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : E → G} {s : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 g s → AnalyticOnNhd 𝕜 (fun x => (f x, g x)) s
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_add_of_nonneg : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R} {m n : ℤ}, 0 ≤ m → 0 ≤ n → A ^ (m + n) = A ^ m * A ^ n
-- Init.Data.Vector.Attach
Vector.any_subtype : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → xs.any f = xs.unattach.any g
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ker_eq_ker_aeval_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), P.ker = RingHom.ker (MvPolynomial.aeval P.val)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_of_ord_ring : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.Linarith.Context α)
  (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_ne_one_cert p = true →
    Lean.Grind.Linarith.Var.denote ctx 0 = One.one → Lean.Grind.Linarith.Poly.denote' ctx p ≠ 0
-- Mathlib.Topology.Covering.Basic
IsDiscrete.of_openPartialHomeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) {t : Set E}
  {x : X}, t ⊆ f ⁻¹' {x} → (∀ e ∈ t, ∃ φ, e ∈ φ.source ∧ ↑φ = f) → IsDiscrete t
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sum_sum_apply_embedding : ∀ {n : ℕ} {A : Type u_1} [inst : AddCommMonoid A] (a : Fin n → A) (x : Composition n),
  ∑ i, ∑ j, a ((x.embedding i) j) = ∑ i, a i
-- Mathlib.Data.List.Infix
List.IsInfix.nodup : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₂.Nodup → l₁.Nodup
-- Mathlib.Order.RelIso.Basic
/-- A `RelHomClass` sends related elements to related elements  -/
RelHomClass.map_rel : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {r : outParam (α → α → Prop)}
  {s : outParam (β → β → Prop)} {inst : FunLike F α β} [self : RelHomClass F r s] (f : F) {a b : α},
  r a b → s (f a) (f b)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.copy_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : α → β) (hf : ↑e = f) (g : β → α) (hg : ↑e.symm = g)
  (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t), (e.copy f hf g hg s hs t ht).target = t
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J), ⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h).symm
-- Mathlib.Tactic.CategoryTheory.CancelIso
/-- Version of `IsIso.hom_inv_id_assoc` for internal use of the `cancelIso` simproc. Do not use.  -/
Mathlib.Tactic.CategoryTheory.CancelIso.hom_inv_id_of_eq_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {x y : C} (f : x ⟶ y) [inst_1 : CategoryTheory.IsIso f]
  (g : y ⟶ x),
  CategoryTheory.inv f = g →
    ∀ {z : C} (k : x ⟶ z), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k) = k
-- Mathlib.NumberTheory.Dioph
Dioph.const_dioph : ∀ {α : Type} (n : ℕ), Dioph.DiophFn (Function.const (α → ℕ) n)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.separatingLeft_toLinearMap₂'_iff : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R},
  ((Matrix.toLinearMap₂' R) M).SeparatingLeft ↔ M.SeparatingLeft
-- Mathlib.Algebra.Notation.Prod
Prod.fst_add : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).1 = p.1 + q.1
-- Init.Data.Vector.Zip
Vector.getElem_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n} {i : ℕ} {h : i < n},
  (as.zip bs)[i] = (as[i], bs[i])
-- Lean.Linter.Init
Lean.Linter.getLinterValue : Lean.Option Bool → Lean.Linter.LinterOptions → Bool
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Color `G ⊕g H` with `Fin (n + m)` given a coloring of `G` with `Fin n` and a coloring of `H`
with `Fin m`  -/
SimpleGraph.Coloring.sumFin : {V : Type u_3} →
  {W : Type u_5} →
    {G : SimpleGraph V} →
      {H : SimpleGraph W} → {n m : ℕ} → G.Coloring (Fin n) → H.Coloring (Fin m) → (G ⊕g H).Coloring (Fin (max n m))
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.Ok.zero : ∀ {c : Turing.ToPartrec.Code},
  c.Ok →
    ∀ {v : List ℕ},
      StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) =
        Turing.ToPartrec.Cfg.halt <$> c.eval v
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabLeadingParserMacro : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Algebra.MulAction
OrderDual.instContinuousVAdd_left : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X], ContinuousVAdd Mᵒᵈ X
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.eventually_filterAt_subset_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X) {ε : ℝ}, 0 < ε → ∀ᶠ (t : Set X) in v.filterAt x, t ⊆ Metric.closedBall x ε
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- Let `F` be a functor from sheaf of `R`-module to sheaf of `S`-module, if `F` preserves
colimits and `F.obj (unit R) ≅ unit S`, given generating sections `G : M.GeneratingSections`,
then we obtain a morphism `free G.I ⟶ F.obj M`.  -/
SheafOfModules.GeneratingSections.mapFreeHom : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {C' : Type u₁} →
              [inst_3 : CategoryTheory.Category.{v₁, u₁} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        {M : SheafOfModules R} →
                          (G : M.GeneratingSections) →
                            (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                              [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁,
                                      max (max (u + 1) u') v', max (max (u + 1) u₁) v₁}
                                    F] →
                                (SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) →
                                  (SheafOfModules.free G.I ⟶ F.obj M)
-- Mathlib.Data.Set.Basic
Set.exists_of_ssubset : ∀ {α : Type u} {s t : Set α}, s ⊂ t → ∃ x ∈ t, x ∉ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.leadingCoeffC.eq_1 : ∀ (n i : ℕ),
  Polynomial.Chebyshev.leadingCoeffC✝ n i =
    (∏ j ∈ (Finset.range (n + 1)).erase i, (Polynomial.Chebyshev.node n i - Polynomial.Chebyshev.node n j))⁻¹
-- Mathlib.RingTheory.Valuation.RankOne
/-- A valuative relation has a rank one valuation when it is both nontrivial
and the rank is at most one.  -/
Valuation.RankOne.ofRankLeOneStruct : {R : Type u_3} →
  [inst : Ring R] →
    [inst_1 : ValuativeRel R] →
      [ValuativeRel.IsNontrivial R] → ValuativeRel.RankLeOneStruct R → (ValuativeRel.valuation R).RankOne
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.map_smul : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {f : Ω → Ω'} (c : NNReal)
  (ν : MeasureTheory.FiniteMeasure Ω), (c • ν).map f = c • ν.map f
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.instToString : {α : Type} → [ToString α] → ToString (Std.Tactic.BVDecide.BoolExpr α)
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_iInf₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α]
  [inst_1 : CompleteLattice β] (f : α ≃o β) (x : (i : ι) → κ i → α), f (⨅ i, ⨅ j, x i j) = ⨅ i, ⨅ j, f (x i j)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j)
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom
        (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
          (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯))
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Subarray.Internal.iter_eq : ∀ {α : Type u} {s : Subarray α}, Std.Slice.Internal.iter s = { internalState := { xs := s } }
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projective_iff_hasProjectiveDimensionLT_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C},
  CategoryTheory.Projective X ↔ CategoryTheory.HasProjectiveDimensionLT X 1
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.comp : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S} {υ : Type u_7}
  {T : Type u_8} [inst_1 : CommRing T] [inst_2 : Algebra S T] {b : τ → MvPowerSeries υ T},
  MvPowerSeries.HasSubst a →
    ∀ (hb : MvPowerSeries.HasSubst b), MvPowerSeries.HasSubst fun s => (MvPowerSeries.substAlgHom hb) (a s)
-- Mathlib.Algebra.Free
FreeMagma.instTraversable.eq_1 : FreeMagma.instTraversable = { toFunctor := FreeMagma.instMonad.toFunctor, traverse := @FreeMagma.traverse }