mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_cons_apply : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {acc : List γ} (f : (a : α) → β a → γ),
  Std.DHashMap.Raw.Internal.foldRev (fun acc k v => f k v :: acc) acc l =
    List.map (fun p => f p.fst p.snd) (Std.DHashMap.Internal.toListModel l.buckets) ++ acc
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.insertIfNew a b = t_1.insertIfNew a b_1
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.parallelComp_comp_parallelComp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {κ : ProbabilityTheory.Kernel X Y} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7}
  {mX' : MeasurableSpace X'} {mY' : MeasurableSpace Y'} {mZ' : MeasurableSpace Z'} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel Y Z} [ProbabilityTheory.IsSFiniteKernel η] {κ' : ProbabilityTheory.Kernel X' Y'}
  [ProbabilityTheory.IsSFiniteKernel κ'] {η' : ProbabilityTheory.Kernel Y' Z'} [ProbabilityTheory.IsSFiniteKernel η'],
  (η.parallelComp η').comp (κ.parallelComp κ') = (η.comp κ).parallelComp (η'.comp κ')
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.ker_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  p.mkQ.ker = p
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- If `a ≤ b`, then `x^b = O(x^a)` as `x → 0`, `x ≥ 0`, unless `b = 0` and `a ≠ 0`.  -/
Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp : ∀ {a b : ℝ}, a ≤ b → (b = 0 → a = 0) → (fun x => x ^ b) =O[nhdsWithin 0 (Set.Ici 0)] fun x => x ^ a
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.Bounded.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → WithBot α → WithTop α → Sort u_2) (a b : α)
  (h_1 : (a b : α) → motive Ordnode.nil (some a) (some b))
  (h_2 : (x : WithBot α) → (x_1 : WithTop α) → motive Ordnode.nil x x_1)
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) → (r : Ordnode α) → (o₁ : WithBot α) → (o₂ : WithTop α) → motive (Ordnode.node size l x r) o₁ o₂),
  (match Ordnode.nil, some a, some b with
    | Ordnode.nil, some a, some b => h_1 a b
    | Ordnode.nil, x, x_1 => h_2 x x_1
    | Ordnode.node size l x r, o₁, o₂ => h_3 size l x r o₁ o₂) =
    h_1 a b
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opFunctor_additive : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive V], (HomologicalComplex.opFunctor V c).Additive
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_ne_top_of_nonneg : ∀ {x : ENNReal} {y : ℝ}, 0 ≤ y → x ≠ ⊤ → x ^ y ≠ ⊤
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.mk : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] → [inst_1 : MulAction G X] → (ιₚ → DiscreteTiling.Prototile G X) → DiscreteTiling.Protoset G X ιₚ
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_left_of_gcd_eq_one : ∀ {n m k : ℕ}, n.gcd m = 1 → (n * k).gcd m = k.gcd m
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.getMiss : String → Array Lean.FuzzyMatching.Score✝ → ℕ → ℕ → Lean.FuzzyMatching.Score✝
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.coe_mulVecLin : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] (M : Matrix m n R),
  ⇑M.mulVecLin = M.mulVec
-- Aesop.Search.Queue.Class
Aesop.Queue.init : {Q : Type} → [self : Aesop.Queue Q] → BaseIO Q
-- Lean.Meta.Tactic.Grind.Core
/-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class,
and have the same type.
 -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.closeGoalWithValuesEq : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.Multiset.Filter
Multiset.filter_singleton : ∀ {α : Type u_1} {a : α} (p : α → Prop) [inst : DecidablePred p], Multiset.filter p {a} = if p a then {a} else ∅
-- Mathlib.Algebra.GroupWithZero.Basic
instIsDedekindFiniteMonoidOfIsLeftCancelMulZero : ∀ {M₀ : Type u_3} [inst : MonoidWithZero M₀] [IsLeftCancelMulZero M₀], IsDedekindFiniteMonoid M₀
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.refl : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β), m.Equiv m
-- Mathlib.Order.Antichain
isAntichain_union : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α},
  IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.exists_affine_subbasis : ∀ {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] {t : Set P}, affineSpan k t = ⊤ → ∃ s ⊆ t, ∃ b, ⇑b = Subtype.val
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.mapHomologicalComplexObjIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_2, u_3} D] [inst_6 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_7 : H.Additive]
  [inst_8 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj K).X i)
        (((H.mapHomologicalComplex c).obj K).X i)]
  [inst_9 : ((H.mapHomologicalComplex c).obj K).HasPathObject]
  [inst_10 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)
        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)]
  [inst_11 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift
        (CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op))
        (-CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op)))]
  [inst_12 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.op.mapHomologicalComplex c.symm).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op)
          (-CategoryTheory.CategoryStruct.id K.op)))]
  [inst_13 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  HomologicalComplex.pathObject.mapHomologicalComplexObjIso K H hc =
    HomologicalComplex.pathObject.mapHomologicalComplexObjIso K H hc
-- Mathlib.RepresentationTheory.Coinvariants
Representation.coinvariantsFinsuppLEquiv_symm_apply : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (α : Type u_9) (a : α →₀ ρ.Coinvariants),
  (ρ.coinvariantsFinsuppLEquiv α).symm a = (ρ.finsuppToCoinvariants α) a
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_shiftRight : ∀ (a b : UInt8), (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 8)
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor_inv_app : ∀ (C : Type u₁) (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : D),
  (CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor C D).inv.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.left (Opposite.op X)))
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- A quadratic map is said to be **nondegenerate** if its radical is 0,
and the radical of its associated polar form has rank ≤ 1.
(The second condition is automatic if 2 is invertible in `R`, but not in general.)

See [elman-karpenko-merkurjev-2008], Chapter II, §7.
 -/
QuadraticMap.Nondegenerate : {R : Type u_1} →
  {M : Type u_2} →
    {P : Type u_4} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup P] →
          [inst_2 : CommRing R] → [inst_3 : Module R M] → [inst_4 : Module R P] → {Q : QuadraticMap R M P} → Prop
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_zero : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β], LinearMap.mapMatrix 0 = 0
-- Init.Data.Float.Float
/-- 64-bit floating-point numbers.

`Float` corresponds to the IEEE 754 *binary64* format (`double` in C or `f64` in Rust).
Floating-point numbers are a finite representation of a subset of the real numbers, extended with
extra “sentinel” values that represent undefined and infinite results as well as separate positive
and negative zeroes. Arithmetic on floating-point numbers approximates the corresponding operations
on the real numbers by rounding the results to numbers that are representable, propagating error and
infinite values.

Floating-point numbers include [subnormal numbers](https://en.wikipedia.org/wiki/Subnormal_number).
Their special values are:
 * `NaN`, which denotes a class of “not a number” values that result from operations such as
   dividing zero by zero, and
 * `Inf` and `-Inf`, which represent positive and infinities that result from dividing non-zero
   values by zero.

Like other low-level types, `Float` is special-cased by the Lean compiler to correspond to the C
`double` type. From the point of view of Lean's logic, `Float` is equivalent to `Float.Model` (via
the functions `Float.toModel` and `Float.ofModel`), which is itself a subtype of `UInt64`. Some of
the operations on `Float` are defined in terms of their `Float.Model` counterparts, while others
are opaque to Lean's kernel.
 -/
Float : Type
-- Lean.Meta.Sym.Canon
/-- `canonInstDec` variant for normalizing `if-then-else` expressions.  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInstDecCore : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balanceR! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        (Std.DTreeMap.Internal.Impl.balanceR! k v l r).size = l.size + 1 + r.size
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.whiskerLeft_curry'_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.Closed X] [inst_3 : CategoryTheory.Closed Y] (f : Y ⟶ Z) {Z_1 : C} (h : X ⟹ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟹ Y) (CategoryTheory.MonoidalClosed.curry' f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp X Y Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟹ Y)).hom
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom X).map f) h)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.id.eq_1 : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.RationalMap.id X = (AlgebraicGeometry.Scheme.PartialMap.id X).toRationalMap
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.trW_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated], P.op.trW = P.trW.op
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.mk_bounded_subset : ∀ {α : Type u_1},
  (Cardinal.mk α).IsStrongPrelimit →
    ∀ {r : α → α → Prop} [inst : IsWellOrder α r],
      (Cardinal.mk α).ord = Ordinal.type r → Cardinal.mk { s // Set.Bounded r s } = Cardinal.mk α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for signed t-division of `BitVec`s.  -/
BitVec.reduceSDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- If `I ≤ p` and `p` is prime, the height of `p` is bounded by the height of `p ⧸ I R` plus
the span rank of `I`.  -/
Ideal.height_le_height_add_spanFinrank_of_le : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {I p : Ideal R} [p.IsPrime],
  I ≤ p → p.height ≤ (Ideal.map (Ideal.Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_succ_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xn a1 (n + 2) + Pell.xn a1 n = 2 * a * Pell.xn a1 (n + 1)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.get_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {epost : EPred} (post : σ → σ → Pred), ⦃ fun s => post s s ⦄ MonadStateOf.get ⦃ post; epost ⦄
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.isDeclToUnfold : Lean.Meta.Simp.Context → Lean.Name → Bool
-- Mathlib.Order.Hom.Basic
OrderHom.mk : {α : Type u_6} →
  {β : Type u_7} → [inst : Preorder α] → [inst_1 : Preorder β] → (toFun : α → β) → Monotone toFun → α →o β
-- Mathlib.Analysis.Calculus.FDeriv.Pow
HasStrictFDerivAt.pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E},
  HasStrictFDerivAt f f' x →
    ∀ (n : ℕ), HasStrictFDerivAt (f ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
-- Mathlib.LinearAlgebra.Complex.Module
ker_imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  imaginaryPart.ker = selfAdjoint.submodule ℝ A
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_mul_single : ∀ {m : Type u_9} {n : Type u_10} {R : Type u_11} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : NonUnitalNonAssocSemiring R] [inst_4 : Fintype m] (x : Matrix m n R) (i : n) (j : m) (a : R),
  (x * Matrix.single i j a).trace = MulOpposite.op a • x j i
-- Mathlib.Topology.Algebra.UniformRing
/-- The completion extension as a ring morphism.  -/
UniformSpace.Completion.extensionHom : {α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] →
      [inst_2 : IsTopologicalRing α] →
        [inst_3 : IsUniformAddGroup α] →
          {β : Type u} →
            [inst_4 : UniformSpace β] →
              [inst_5 : Ring β] →
                [IsUniformAddGroup β] →
                  [IsTopologicalRing β] →
                    (f : α →+* β) → Continuous ⇑f → [CompleteSpace β] → [T0Space β] → UniformSpace.Completion α →+* β
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Every point is covered by chosen balls, before `p.lastStep`.  -/
Besicovitch.TauPackage.mem_iUnionUpTo_lastStep : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α) (x : β),
  p.c x ∈ p.iUnionUpTo p.lastStep
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : AddMonoidAlgebra R M}, x.coeff = y.coeff ↔ x = y
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TermElabM.toIO : {α : Type} →
  Lean.Elab.TermElabM α →
    Lean.Core.Context →
      Lean.Core.State →
        Lean.Meta.Context →
          Lean.Meta.State →
            Lean.Elab.Term.Context →
              Lean.Elab.Term.State → IO (α × Lean.Core.State × Lean.Meta.State × Lean.Elab.Term.State)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.ltIdeal_le_leIdeal : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : Γ₀ˣ), v.ltIdeal γ ≤ v.leIdeal ↑γ
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_abs_abs`. -/
Asymptotics.IsBigOWith.abs_abs : ∀ {α : Type u_1} {c : ℝ} {l : Filter α} {u v : α → ℝ},
  Asymptotics.IsBigOWith c l u v → Asymptotics.IsBigOWith c l (fun x => |u x|) fun x => |v x|
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.girth_bot : ∀ {α : Type u_1}, ⊥.girth = 0
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
    CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.initial.to X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_right_inv : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ f₂' : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom)
  (iso : f₂ ≅ f₂'), (sq₁₂.ι_iso_of_iso_right sq₁₂' iso).inv = sq₁₂'.mapArrowRight sq₁₂ iso.inv
-- Lean.Elab.Tactic.FalseOrByContra
Lean.MVarId.elabFalseOrByContra : Lean.Elab.Tactic.Tactic
-- Mathlib.NumberTheory.PellMatiyasevic
_private.Mathlib.NumberTheory.PellMatiyasevic.0.Pell.d.congr_simp : ∀ {a a_1 : ℕ} (e_a : a = a_1) (_a1 : 1 < a), Pell.d✝ _a1 = Pell.d✝ ⋯
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.mk.sizeOf_spec : ∀ {M : Type u_8} {N : Type u_9} {φ : M → N} {X : Type u_10} [inst : VAdd M X] {Y : Type u_11} [inst_1 : VAdd N Y]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] [inst_4 : SizeOf X] [inst_5 : SizeOf Y] (toFun : X → Y)
  (map_vadd' : ∀ (m : M) (x : X), toFun (m +ᵥ x) = φ m +ᵥ toFun x),
  sizeOf { toFun := toFun, map_vadd' := map_vadd' } = 1
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux.h2 : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Surjective ⇑g →
      ∀ {k : ℕ} (x : AdicCompletion.AdicCauchySequence I N),
        (∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤) → ∀ (n : ℕ), ∃ d y, d ∈ I ^ (k + n) • ⊤ ∧ f y = ↑x (k + n) - d
-- Mathlib.CategoryTheory.EssentiallySmall
/-- An arbitrarily chosen small model for an essentially small category.
 -/
CategoryTheory.SmallModel : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EssentiallySmall.{w, v, u} C] → Type w
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseP_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (y : β) (h_1 : (y : β) → motive (some y)) (h_2 : Unit → motive none),
  (match some y with
    | some y => h_1 y
    | none => h_2 ()) =
    h_1 y
-- Mathlib.Data.Seq.Basic
/-- Convert a `Seq1` to a sequence.  -/
Stream'.Seq1.toSeq : {α : Type u} → Stream'.Seq1 α → Stream'.Seq α
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.isLocalizedModule_mapExtendScalars : ∀ {R : Type u_4} {M : Type u_5} {N : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) {M' : Type u_1} [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] {N' : Type u_2} [inst_8 : AddCommGroup N']
  [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (Rₛ : Type u_3) [inst_11 : CommRing Rₛ]
  [inst_12 : Algebra R Rₛ] [inst_13 : Module Rₛ M'] [inst_14 : Module Rₛ N'] [inst_15 : IsScalarTower R Rₛ M']
  [inst_16 : IsScalarTower R Rₛ N'] [inst_17 : IsLocalization S Rₛ] [Module.FinitePresentation R M],
  IsLocalizedModule S (IsLocalizedModule.mapExtendScalars S f g Rₛ)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNonUnitalNonAssocSemiring : {k : Type u_1} →
  {G : Type u_2} →
    [Mul G] →
      [inst : NonUnitalNonAssocSemiring k] → [DistribSMul G k] → NonUnitalNonAssocSemiring (SkewMonoidAlgebra k G)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Definable₂.mk_out : ∀ {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₂ f] {x y : PSet.{u}},
  ZFSet.mk (ZFSet.Definable₂.out f x y) = f (ZFSet.mk x) (ZFSet.mk y)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instLE : {ι : Type u_1} → {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → [(i : ι) → LE (α i)] → LE (Π₀ (i : ι), α i)
-- Batteries.Lean.Meta.SavedState
/-- Returns the mvars that are declared but unassigned in `preState`, and
assigned in `postState`. Delayed-assigned mvars are considered assigned.
 -/
Lean.Meta.getAssignedExprMVars : Lean.Meta.SavedState → Lean.Meta.SavedState → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Topology.Constructions.SumProd
frontier_univ_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set Y),
  frontier (Set.univ ×ˢ s) = Set.univ ×ˢ frontier s
-- Init.Data.List.Find
List.idxOf_lt_length_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, List.idxOf a l < l.length ↔ a ∈ l
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.coe_quotientEquivOrthogonal_symm : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  ⇑K.quotientEquivOrthogonal.symm = ⇑(K.quotientEquivOfIsCompl Kᗮ ⋯).symm
-- Mathlib.RingTheory.Filtration
/-- **Artin-Rees lemma**  -/
Ideal.exists_pow_inf_eq_pow_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [IsNoetherianRing R] [Module.Finite R M] (N : Submodule R M),
  ∃ k, ∀ n ≥ k, I ^ n • ⊤ ⊓ N = I ^ (n - k) • (I ^ k • ⊤ ⊓ N)
-- Mathlib.Geometry.Manifold.Notation
/-- `tangentMap% f` elaborates to `tangentMap I J f`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termTangentMap%__» : Lean.ParserDescr
-- Mathlib.Data.Fintype.Sets
List.Subtype.fintype : {α : Type u_1} → [DecidableEq α] → (l : List α) → Fintype { x // x ∈ l }
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_iInter₂_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VAdd α β] (s : Set α)
  (t : (i : ι) → κ i → Set β), s +ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s +ᵥ t i j
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.box.inj : ∀ {ty : Lean.IR.IRType} {x : Lean.IR.VarId} {ty_1 : Lean.IR.IRType} {x_1 : Lean.IR.VarId},
  Lean.IR.Expr.box ty x = Lean.IR.Expr.box ty_1 x_1 → ty = ty_1 ∧ x = x_1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs : List ((a : α) × β a)) (fallback : α),
  Std.Internal.List.minKeyD xs fallback = (Std.Internal.List.minKey? xs).getD fallback
-- Mathlib.Lean.GoalsLocation
/-- The hypothesis specified by the `GoalsLocation`.  -/
Lean.SubExpr.GoalsLocation.fvarId? : Lean.SubExpr.GoalsLocation → Option Lean.FVarId
-- Mathlib.Order.Atoms
CompleteAtomicBooleanAlgebra.instIsAtomistic : ∀ {α : Type u_4} [inst : CompleteAtomicBooleanAlgebra α], IsAtomistic α
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)]
  [inst_2 : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α}, Irreducible p → p.count 0 = 0