mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.differentiableAt_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  DifferentiableAt 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (n : ℕ),
  Int.Internal.Linear.cooper_dvd_left_cert p₁ p₂ p₃ d n =
    Int.Internal.Linear.Poly.casesOn p₁ (fun x => false) fun a x x_1 =>
      Int.Internal.Linear.Poly.casesOn p₂ (fun x => false) fun b y x_2 =>
        Int.Internal.Linear.Poly.casesOn p₃ (fun x => false) fun c z x_3 =>
          (Nat.beq x y).and'
            ((Nat.beq x z).and'
              ((decide (a < 0)).and'
                ((decide (b > 0)).and' ((decide (d > 0)).and' (n.beq (a.lcm (a * d / ↑((a * d).gcd c))))))))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : (m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit)
  (h_2 : (m₂ : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit m₂)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
  (m₁_1 : Lean.Grind.CommRing.Mon),
  m₁ = m₁_1 →
    m₂ = Lean.Grind.CommRing.Mon.unit →
      (match m₁, m₂ with
        | m₁, Lean.Grind.CommRing.Mon.unit => h_1 m₁
        | Lean.Grind.CommRing.Mon.unit, m₂ => h_2 m₂
        | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) ≍
        h_1 m₁_1
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.iic_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) (j : J), (c.iic j).F = ⋯.functor.comp c.F
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.mk.injEq : ∀ (tempMark doneMark : Lean.FVarIdHashSet) (newDecls : Array Lean.LocalDecl) (newArgs : Array Lean.Expr)
  (tempMark_1 doneMark_1 : Lean.FVarIdHashSet) (newDecls_1 : Array Lean.LocalDecl) (newArgs_1 : Array Lean.Expr),
  ({ tempMark := tempMark, doneMark := doneMark, newDecls := newDecls, newArgs := newArgs } =
      { tempMark := tempMark_1, doneMark := doneMark_1, newDecls := newDecls_1, newArgs := newArgs_1 }) =
    (tempMark = tempMark_1 ∧ doneMark = doneMark_1 ∧ newDecls = newDecls_1 ∧ newArgs = newArgs_1)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Constructor for `LaxBraidedFunctor C D`.  -/
CategoryTheory.LaxBraidedFunctor.of : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) → [F.LaxBraided] → CategoryTheory.LaxBraidedFunctor C D
-- Mathlib.GroupTheory.Rank
Subgroup.rank_closure_finite_le_nat_card : ∀ {G : Type u_1} [inst : Group G] (s : Set G) [inst_1 : Finite ↑s], Group.rank ↥(Subgroup.closure s) ≤ Nat.card ↑s
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_prod_right : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_3} (s : Finset ι) (f : Polynomial R) (g : ι → Polynomial R) (m : ℕ),
  f.natDegree ≤ m → ∏ i ∈ s, (g i).leadingCoeff ≠ 0 → f.resultant (∏ i ∈ s, g i) m = ∏ i ∈ s, f.resultant (g i) m
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.restrict : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {Γ₀' : Type u_7} [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {w : Valuation R Γ₀'},
  v.IsEquiv w → v.restrict.IsEquiv w.restrict
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → p.dropLast.IsPath
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_zpow_iff_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a < 1 → (1 < a ^ n ↔ n < 0)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.brecOn.go : {V : Type u} →
  {G : SimpleGraph V} →
    {motive : (a a_1 : V) → G.Walk a a_1 → Sort u_1} →
      {a a_1 : V} →
        (t : G.Walk a a_1) →
          ((a a_2 : V) → (t : G.Walk a a_2) → SimpleGraph.Walk.below t → motive a a_2 t) →
            motive a a_1 t ×' SimpleGraph.Walk.below t
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.ne_zero : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R] {i : ι}, LinearIndepOn R v s → i ∈ s → v i ≠ 0
-- Init.SimpLemmas
Lean.true_arrow_congr_left : ∀ (p q : Prop), p = True → Lean.Arrow p q = q
-- Batteries.Data.List.Pairwise
List.pwFilter_nil : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R], List.pwFilter R [] = []
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piRing_symm_apply : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] (S : Type u_4) [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : SMulCommClass R S M] (f : ι → M) (g : ι → R), ((LinearEquiv.piRing R M ι S).symm f) g = ∑ i, g i • f i
-- Lean.Environment
Lean.Kernel.getDiagnostics : Lean.Environment → Lean.Kernel.Diagnostics
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubalgebra.unitization_range : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S),
  (NonUnitalSubalgebra.unitization s).range = Algebra.adjoin R ↑s
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.mk.eq_1 : ∀ (gate : ℕ) (invert : Bool), Std.Sat.AIG.Fanin.mk gate invert = { val := gate * 2 ||| invert.toNat }
-- Lean.Meta.Tactic.Replace
/-- Modify `mvarId` target type left-hand-side using `f`.
Throw an error if target type is not an equality.
 -/
Lean.MVarId.modifyTargetEqLHS : Lean.MVarId → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.MVarId
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_mk : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (hs : IsLowerSet s), ↑{ carrier := s, lower' := hs } = s
-- Mathlib.Topology.Bases
/-- The filter `𝓝 a` is countably generated for all points `a`.  -/
FirstCountableTopology.nhds_generated_countable : ∀ {α : Type u} {t : TopologicalSpace α} [self : FirstCountableTopology α] (a : α), (nhds a).IsCountablyGenerated
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioc_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a c ∪ Set.Ioc b c = Set.Ioc (min a b) c
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux1.eq_1 : ∀ (n : ℕ), n.digitsAux1 = List.replicate n 1
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_zero : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  {i | f i ≠ 0}.Finite → Memℓp f 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_sum : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {p : ℕ} (α : CategoryTheory.Abelian.Ext X Y p) {ι : Type u_1}
  [inst_3 : Fintype ι] {q : ℕ} (β : ι → CategoryTheory.Abelian.Ext Y Z q) {n : ℕ} (h : p + q = n),
  α.comp (∑ i, β i) h = ∑ i, α.comp (β i) h
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_replicateCol : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R] {ι : Type u_11}
  {A : X → n → R}, Continuous A → Continuous fun x => Matrix.replicateCol ι (A x)
-- Mathlib.Analysis.Calculus.Monotone
/-- A Stieltjes function is almost everywhere differentiable, with derivative equal to the
Radon-Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue.  -/
StieltjesFunction.ae_hasDerivAt : ∀ (f : StieltjesFunction ℝ), ∀ᵐ (x : ℝ), HasDerivAt (↑f) (f.measure.rnDeriv MeasureTheory.volume x).toReal x
-- Mathlib.Data.DFinsupp.BigOperators
/-- The `DFinsupp` version of `Finsupp.comp_liftAddHom`  -/
DFinsupp.comp_liftAddHom : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {δ : Type u_1}
  [inst_1 : (i : ι) → AddZeroClass (β i)] [inst_2 : AddCommMonoid γ] [inst_3 : AddCommMonoid δ] (g : γ →+ δ)
  (f : (i : ι) → β i →+ γ), g.comp (DFinsupp.liftAddHom f) = DFinsupp.liftAddHom fun a => g.comp (f a)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.to_map_eq_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {x : R}, M ≤ nonZeroDivisors R → ((algebraMap R S) x = 0 ↔ x = 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk : ∀ {p q : ℕ},
  (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
      (SSet.stdSimplex.obj { len := q })).Finite
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The additive Haar measure is sigma-finite in a second countable group.  -/
MeasureTheory.Measure.sigmaFinite_addHaarMeasure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [SecondCountableTopology G]
  {K₀ : TopologicalSpace.PositiveCompacts G}, MeasureTheory.SigmaFinite (MeasureTheory.Measure.addHaarMeasure K₀)
-- Init.Data.Vector.Lemmas
Vector.flatMap_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m},
  xs.reverse.flatMap f = (xs.flatMap (Vector.reverse ∘ f)).reverse
-- Lean.Meta.Tactic.Grind.Split
/-- Returns `true`, if there are no anchor references restricting the search,
or there is an anchor references `ref` s.t. `ref` matches `c`.
 -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkAnchorRefs : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GrindM Bool
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- If `p` is a closed subspace with finite codimension, then any algebraic complement `q` to `p`
is a topological complement.  -/
Submodule.IsCompl.isTopCompl_of_finiteDimensional_quotient : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {p q : Submodule 𝕜 E}, IsCompl p q → IsClosed ↑p → ∀ [FiniteDimensional 𝕜 (E ⧸ p)], Submodule.IsTopCompl p q
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.IsOpenPosMeasure.open_pos : ∀ {X : Type u_1} {inst : TopologicalSpace X} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  [self : μ.IsOpenPosMeasure] (U : Set X), IsOpen U → U.Nonempty → μ U ≠ 0
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearMap.fixedSubmodule_eq_ker : ∀ {R : Type u_4} [inst : Ring R] {V : Type u_5} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (f : V →ₗ[R] V),
  f.fixedSubmodule = (f - LinearMap.id).ker
-- Mathlib.Data.Set.Image
Set.insert_image_compl_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), insert (f x) (f '' {x}ᶜ) = Set.range f
-- Mathlib.Data.Set.Countable
Set.exists_seq_cover_iff_countable : ∀ {α : Type u} {p : Set α → Prop},
  (∃ s, p s) → ((∃ s, (∀ (n : ℕ), p (s n)) ∧ ⋃ n, s n = Set.univ) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ⋃₀ S = Set.univ)
-- Lean.Meta.DiscrTree.Types
/-- Discrimination trees. It is an index from terms to values of type `α`.
 -/
Lean.Meta.DiscrTree : Type → Type
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.mem_indepSetFinset_iff : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] {n : ℕ}
  {s : Finset α}, s ∈ G.indepSetFinset n ↔ G.IsNIndepSet n s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  t.WF → (k ∈ Std.TreeSet.Raw.filter f t ↔ ∃ (h' : k ∈ t), f (t.get k h') = true)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k : α} {f : β → β}, m.WF → ∀ {hc : k ∈ m.modify k f}, (m.modify k f).getKey k hc = k
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuousConstSMul.instContinuousConstSMul : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X] [UniformContinuousConstSMul M X],
  ContinuousConstSMul M X
-- Mathlib.Algebra.Category.Grp.Colimits
/-- (internal implementation) The colimit cocone of a functor `F`, implemented as a quotient of
`DFinsupp (fun j ↦ F.obj j)`, under the assumption that said quotient is small.
 -/
AddCommGrpCat.Colimits.colimitCocone : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] → [Small.{w, max w u} (AddCommGrpCat.Colimits.Quot F)] → CategoryTheory.Limits.Cocone F
-- Init.System.IO
/-- Reads the entire remaining contents of the file handle as a UTF-8-encoded array of lines.

Newline markers are not included in the lines.

The underlying file is not automatically closed, and subsequent reads from the handle may block
and/or return data.
 -/
IO.FS.Handle.lines : IO.FS.Handle → IO (Array String)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- Constructs a `CommGroupWithZero` structure on a `CommMonoidWithZero`
consisting only of units and 0.  -/
commGroupWithZeroOfIsUnitOrEqZero : {M : Type u_4} → [Nontrivial M] → [hM : CommMonoidWithZero M] → (∀ (a : M), IsUnit a ∨ a = 0) → CommGroupWithZero M
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- If `P` is stable under base change, this is the coverage on `C` where covering presieves
are those where every morphism satisfies `P`.  -/
CategoryTheory.MorphismProperty.coverage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) → [P.IsStableUnderBaseChange] → [P.HasPullbacks] → CategoryTheory.Coverage C
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.coe_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ) (n : ℤ), ↑0 = 0
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Functorially convert a module over `k[G]` into a representation of `G`.  -/
Rep.ofModuleMonoidAlgebra : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → CategoryTheory.Functor (ModuleCat (MonoidAlgebra k G)) (Rep.{w, u, v} k G)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.step_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {array : Array β},
  (array.iterM m).step =
    pure
      (Std.Shrink.deflate
        (if h : 0 < array.size then Std.PlausibleIterStep.yield (array.iterFromIdxM m 1) array[0] ⋯
        else Std.PlausibleIterStep.done ⋯))
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFacAux.match_1.eq_2 : ∀ (motive : ℕ → PosNum → Sort u_1) (fuel : ℕ) (k : PosNum) (h_1 : (x : PosNum) → motive 0 x)
  (h_2 : (fuel : ℕ) → (k : PosNum) → motive fuel.succ k),
  (match fuel.succ, k with
    | 0, x => h_1 x
    | fuel.succ, k => h_2 fuel k) =
    h_2 fuel k
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.mk_zero_pow : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (a : A 0) (n : ℕ),
  GradedMonoid.mk 0 (a ^ n) = GradedMonoid.mk 0 a ^ n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).hom.app X_1).right.right =
    CategoryTheory.CategoryStruct.id X_1.right.right
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- A product of monic polynomials is monic  -/
MonomialOrder.Monic.prod : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R}
  {s : Finset ι}, (∀ i ∈ s, m.Monic (P i)) → m.Monic (∏ i ∈ s, P i)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_of_contains_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.insert k).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.Algebra.Category.ModuleCat.Descent
/-- Extension of scalars by a faithfully flat ring map is comonadic.  -/
comonadicExtendScalars : {A B : Type u} →
  [inst : CommRing A] →
    [inst_1 : CommRing B] →
      {f : A →+* B} → f.FaithfullyFlat → CategoryTheory.ComonadicLeftAdjoint (ModuleCat.extendScalars f)
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthogonalFamily.summable_of_lp : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V → ∀ (f : ↥(lp G 2)), Summable fun i => (V i) (↑f i)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y_1).right.as = PUnit.unit
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.const_boundedAtFilter : ∀ {α : Type u_2} {β : Type u_3} [inst : Norm β] (l : Filter α) (c : β), l.BoundedAtFilter (Function.const α c)
-- Mathlib.Analysis.Convex.Between
Wbtw.left_ne_right_of_ne_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Wbtw R x y z → y ≠ x → x ≠ z
-- Init.Data.UInt.Bitwise
UInt8.xor_neg_one : ∀ {a : UInt8}, a ^^^ -1 = ~~~a
-- Mathlib.LinearAlgebra.Finsupp.Supported
/-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between
`supported M R s` and `s →₀ M`.  -/
Finsupp.supportedEquivFinsupp : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (s : Set α) → ↥(Finsupp.supported M R s) ≃ₗ[R] ↑s →₀ M
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq.sizeOf_spec : ∀ (x : Int.Internal.Linear.Var) (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq x c) = 1 + sizeOf x + sizeOf c
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.dist_integral_le_lintegral_edist : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      dist (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhdsGT_ofNat_neBot : ∀ (n : ℕ) [inst : n.AtLeastTwo], (nhdsWithin (OfNat.ofNat n) (Set.Ioi (OfNat.ofNat n))).NeBot
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_functor_obj_right : ∀ {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 : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).right = X.right
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.Raw.empty.max? = none
-- Mathlib.Topology.Order.Basic
pi_Ioi_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' x' : ι → α} [Nonempty ι], (∀ (i : ι), a' i < x' i) → Set.Ioi a' ∈ nhds x'
-- Mathlib.Algebra.BigOperators.Associated
/-- **Alias** of `Prime.not_dvd_finsetProd`. -/
Prime.not_dvd_finset_prod : ∀ {M₀ : Type u_3} {M : Type u_4} [inst : CommMonoidWithZero M] {S : Finset M₀} {p : M},
  Prime p → ∀ {g : M₀ → M}, (∀ a ∈ S, ¬p ∣ g a) → ¬p ∣ S.prod g
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_of_isIso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  [CategoryTheory.IsIso f] [inst_3 : ∀ (i : ι), K.HasHomology i] [inst_4 : ∀ (i : ι), L.HasHomology i], QuasiIso f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.insertMany t l) k' fallback = v
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : W.FunctorsInverting D)
  (a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)),
  ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).obj G).obj a = G.obj.obj a.as.obj