mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A]
  [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A]
  [inst_4 : CategoryTheory.Functor.IsDenseSubsite J K G], (G.sheafPushforwardContinuous A J K).IsEquivalence
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- (Implementation detail, see `LinearMap.polyCharpoly`.)

Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear map.
Let `b` be a basis of `L` and `bₘ` a basis of `M`.
Then `LinearMap.polyCharpolyAux φ b bₘ` is the polynomial that evaluates on elements `x` of `L`
to the characteristic polynomial of `φ x` acting on `M`.

This definition does not depend on the choice of `bₘ`
(see `LinearMap.polyCharpolyAux_basisIndep`).  -/
LinearMap.polyCharpolyAux : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {ι : Type u_5} →
        {ιM : Type u_7} →
          [inst : CommRing R] →
            [inst_1 : AddCommGroup L] →
              [inst_2 : Module R L] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    (L →ₗ[R] Module.End R M) →
                      [Fintype ι] →
                        [Fintype ιM] →
                          [DecidableEq ι] →
                            [DecidableEq ιM] → Module.Basis ι R L → Module.Basis ιM R M → Polynomial (MvPolynomial ι R)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_eq_head!_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.minKey! = t.keys.head!
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- Two orthonormal bases with opposite orientations determine opposite "determinant"
top-dimensional forms on `E`.  -/
OrthonormalBasis.det_eq_neg_det_of_opposite_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
  e.toBasis.orientation ≠ f.toBasis.orientation → e.toBasis.det = -f.toBasis.det
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  a ∈ m.insert k ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.small_colimitType_of_hasColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [CategoryTheory.Limits.HasColimit F], Small.{u, max u v} F.ColimitType
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coalgebraEquivOver_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.coalgebraEquivOver X).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun A =>
        CategoryTheory.Comonad.Coalgebra.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.prodComonad X).Coalgebra).obj A).A) ⋯)
      ⋯
-- Lean.Setup
Lean.ModuleArtifacts.olean? : Lean.ModuleArtifacts → Option System.FilePath
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.mem_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ),
  n + 1 = m →
    ∀ (z : CochainComplex.HomComplex.Cochain F G n),
      z ∈ CochainComplex.HomComplex.cocycle F G n ↔ CochainComplex.HomComplex.δ n m z = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_mem_sub_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {s t : Finset α}, 0 ∈ s - t ↔ ¬Disjoint s t
-- Mathlib.Algebra.Group.Hom.End
AddMonoid.End.ofNat_apply : ∀ {M : Type uM} [inst : AddCommMonoid M] (n : ℕ) [inst_1 : n.AtLeastTwo] (m : M), (OfNat.ofNat n) m = n • m
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
MeasureTheory.lintegral_sub_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f g : α → ENNReal),
  Measurable f → ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_id : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  IntervalIntegrable (fun x => x) μ a b
-- Mathlib.Logic.Function.Defs
Function.prod_fst_snd : ∀ {α : Type u_1} {β : Type u_2}, Function.prod Prod.fst Prod.snd = id
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_one_X : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.reflect 1 Polynomial.X = 1
-- Mathlib.Data.Seq.Computation
Computation.results_think_iff : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.think.Results a (n + 1) ↔ s.Results a n
-- Mathlib.NumberTheory.MulChar.Basic
/-- If `n` is positive, then `(χ ^ n) a = (χ a) ^ n`.  -/
MulChar.pow_apply' : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') {n : ℕ},
  n ≠ 0 → ∀ (a : R), (χ ^ n) a = χ a ^ n
-- Init.Internal.Order.Basic
Lean.Order.empty_chain : (α : Sort u_1) → α → Prop
-- Init.Data.SInt.Basic
instReprInt8 : Repr Int8
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {s : Set α},
  MeasurableSet s → m.join s = ∫⁻ (μ : MeasureTheory.Measure α), μ s ∂m
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The relative homology functor of a `HomologyPretheory`.  -/
TopPair.HomologyPretheory.Hₚ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → TopPair.HomologyPretheory C c → ι → CategoryTheory.Functor TopPair C
-- Mathlib.Data.Fin.Fin2
Fin2.fs.sizeOf_spec : ∀ {n : ℕ} (a : Fin2 n), sizeOf a.fs = 1 + sizeOf n + sizeOf a
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.precomp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} (α α_1 : CategoryTheory.Abelian.Ext X Y n),
  α = α_1 → ∀ (Z : C) {a b : ℕ} (h : n + a = b), α.precomp Z h = α_1.precomp Z h
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal_tensorObj_as : ∀ (M : Type u) [inst : Monoid M] (X Y : CategoryTheory.Discrete M),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).as = X.as * Y.as
-- Lean.Meta.Match.AltTelescopes
/-- Extension of `forallAltTelescope` that continues further:

Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs.
Recall that this kind of parameter always occurs after the parameters corresponding to pattern
variables.

The continuation `k` takes four arguments `ys args mask type`.
- `ys` are variables for the hypotheses that have not been eliminated.
- `eqs` are variables for equality hypotheses associated with discriminants annotated with `h : discr`.
- `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
- `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
- `type` is the resulting type for `altType`.

We use the `mask` to build the splitter proof. See `mkSplitterProof`.

This can be used to use the alternative of a match expression in its splitter.
 -/
Lean.Meta.Match.forallAltTelescope : {α : Type} →
  Lean.Expr →
    Lean.Meta.Match.AltParamInfo →
      ℕ → (Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.AddMon C), (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instEpiFunctorπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), CategoryTheory.Epi Φ.π
-- Init.Grind.AC
Lean.Grind.AC.Expr.var.sizeOf_spec : ∀ (x : Lean.Grind.AC.Var), sizeOf (Lean.Grind.AC.Expr.var x) = 1 + sizeOf x
-- Std.Data.TreeSet.Basic
Std.TreeSet.instLawfulSingleton : ∀ {α : Type u} {cmp : α → α → Ordering}, LawfulSingleton α (Std.TreeSet α cmp)
-- Mathlib.Probability.Kernel.RadonNikodym
/-- A set of points in `α × γ` related to the absolute continuity / mutual singularity of
`κ` and `η`. That is,
* `withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a) = 0`,
* `singularPart κ η a (mutuallySingularSetSlice κ η a)ᶜ = 0`.
 -/
ProbabilityTheory.Kernel.mutuallySingularSetSlice : {α : Type u_1} →
  {γ : Type u_2} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α γ → α → Set γ
-- Std.Data.DHashMap.Basic
/-- Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though is not possible
to get anything out of the hash map.
 -/
Std.DHashMap.isEmpty : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → Bool
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.noConfusionType : Sort v✝ → Lean.Meta.Grind.NormalizePattern.PatternArgKind → Lean.Meta.Grind.NormalizePattern.PatternArgKind → Sort v✝
-- Mathlib.Algebra.Module.StablyFree.Basic
_private.Mathlib.Algebra.Module.StablyFree.Basic.0.Module.IsStablyFree.exist_free_prod' : ∀ {R : Type u} {inst : Ring R} {M : Type u_1} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : Module.IsStablyFree R M], ∃ N x x_1, ∃ (_ : Module.Finite R N) (_ : Module.Free R N), Module.Free R (M × N)
-- Mathlib.Data.Set.Card
Set.three_lt_ncard : ∀ {α : Type u_1} {s : Set α},
  autoParam s.Finite Set.three_lt_ncard._auto_1 →
    (3 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).minKey? = some (t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k')
-- Mathlib.Logic.Equiv.Prod
Equiv.uniqueProd_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Unique β] (x : β × α), (Equiv.uniqueProd α β) x = x.2
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleResponse.mk : Array Lean.Lsp.LeanQueriedModule → Lean.Lsp.LeanQueryModuleResponse
-- Mathlib.Order.UpperLower.Closure
ordConnected_iff_upperClosure_inter_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.of_subsingleton : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Subsingleton R],
  Algebra.IsFiniteSplit R S
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (f * g) x
-- Mathlib.Tactic.Attr.Register
/-- A stub attribute for `is_poly`.  -/
Parser.Attr.is_poly : Lean.ParserDescr
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F) (j : J) (x_1 : ↑(F.obj j)),
  RingCat.Colimits.descFunLift F s (RingCat.Colimits.Prequotient.of j x_1) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x_1
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.Monic.one_le_mapMahlerMeasure : ∀ {A : Type u_2} [inst : NormedRing A] {p : Polynomial A} (v : A →+* ℂ) [NormOneClass A],
  Isometry ⇑v → p.Monic → 1 ≤ p.mapMahlerMeasure v
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comap_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] {M N : CategoryTheory.Mod D B} (g : M ⟶ N),
  ((CategoryTheory.Mod.comap f).map g).hom = g.hom
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.isMulCommutative_iSup : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {ι : Type u_3} [Nonempty ι]
  {S : ι → StarSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_lt_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b : α}, a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- Given a linear map `f : M →ₗ[R] A` into an `R`-algebra `A`, which satisfies the condition:
`cond : ∀ m : M, f m * f m = Q(m)`, this is the canonical lift of `f` to a morphism of `R`-algebras
from `CliffordAlgebra Q` to `A`.
 -/
CliffordAlgebra.lift : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) →
            {A : Type u_3} →
              [inst_3 : Semiring A] →
                [inst_4 : Algebra R A] →
                  { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) } ≃ (CliffordAlgebra Q →ₐ[R] A)
-- Init.Data.SInt.Lemmas
Int8.toInt_ofIntClamp : ∀ {x : ℤ}, Int8.minValue.toInt ≤ x → x ≤ Int8.maxValue.toInt → (Int8.ofIntClamp x).toInt = x
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.nonUnitalAlgHom_ext'_iff : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Mul M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] {φ₁ φ₂ : MonoidAlgebra R M →ₙₐ[R] A},
  φ₁ = φ₂ ↔ φ₁.toMulHom.comp (MonoidAlgebra.ofMagma R M) = φ₂.toMulHom.comp (MonoidAlgebra.ofMagma R M)
-- Mathlib.Probability.BorelCantelli
ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} [inst : LinearOrder ι] {i j : ι}
  {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)),
  ProbabilityTheory.iIndepSet s μ →
    i < j → μ[(s j).indicator fun x => 1 | ↑(MeasureTheory.filtrationOfSet hsm) i] =ᵐ[μ] fun x => μ.real (s j)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubgroup_mono : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M},
  Monotone Submodule.toAddSubgroup
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_lt_pow_add : ∀ (n : ℕ) {k : ℕ}, 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
-- Mathlib.MeasureTheory.Group.Prod
/-- Left invariant Borel measures on a measurable group are unique (up to a scalar).  -/
MeasureTheory.measure_eq_div_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant], ν' s ≠ 0 → ν' s ≠ ⊤ → μ' = (μ' s / ν' s) • ν'
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.rightUnitor_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor α).hom.τl = (CategoryTheory.Bicategory.rightUnitor α.l).hom
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A polynomial of weightedTotalDegree `⊥` is weighted homogeneous of degree `⊥`.  -/
MvPolynomial.isWeightedHomogeneous_of_total_degree_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M) {p : MvPolynomial σ R},
  MvPolynomial.weightedTotalDegree w p = ⊥ → MvPolynomial.IsWeightedHomogeneous w p ⊥
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instPathConnectedSpaceTangentSpaceReal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {x : M},
  PathConnectedSpace (TangentSpace I x)
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.isInteger_of_isUnit_den : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {x : K},
  IsUnit ↑(IsFractionRing.den A x) → IsLocalization.IsInteger A x
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- Given a monomorphism `i : X ⟶ Y` of simplicial sets and a nondegenerate `d`-simplex
of `Y` not in the range of `i`, this is the corresponding morphism `Δ[d] ⟶ Y`.  -/
SSet.relativeCellComplexOfMono.Cell.map : {X Y : SSet} → {i : X ⟶ Y} → {d : ℕ} → SSet.relativeCellComplexOfMono.Cell i d → (SSet.stdSimplex.obj { len := d } ⟶ Y)
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.of_subset_cthickening_of_lt : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} {δ : NNReal},
  s ⊆ Metric.cthickening (↑ε) N → ε < δ → Metric.IsCover δ s N
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64.congr_simp : ∀ (a a_1 : USize), a = a_1 → ∀ (h : System.Platform.numBits = 64), a.toBitVec64 h = a_1.toBitVec64 h
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.isoExt_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (hF' : CategoryTheory.Limits.IsImage F'), (hF.isoExt hF').inv = hF'.lift F
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_comp_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.fst.comp (Monoid.Coprod.swap M N) = Monoid.Coprod.snd
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.rightHomologyIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂) {Z : C}
  (h : S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.rightHomologyIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.rightHomologyIso.hom h)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Impl) A preliminary definition to avoid timeouts.  -/
CategoryTheory.Over.ConstructProducts.conesEquivFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (B : C) →
      {J : Type w} →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          CategoryTheory.Functor
            (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F))
            (CategoryTheory.Limits.Cone F)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_1.congr_eq_2 : ∀ (motive : Option Bool → Sort u_1) (val? : Option Bool) (h_1 : (val' : Bool) → motive (some val'))
  (h_2 : (x : Option Bool) → motive x) (x : Option Bool),
  val? = x →
    (∀ (val' : Bool), x = some val' → False) →
      (match val? with
        | some val' => h_1 val'
        | x => h_2 x) ≍
        h_2 x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_coe_ennreal_restrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α NNReal) (s : Set α),
  MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (f.restrict s) =
    (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal f).restrict s
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a conditionally complete lattice
with possibly different definitional equalities.  -/
ConditionallyCompleteLattice.copy : {α : Type u} →
  (c : ConditionallyCompleteLattice α) →
    (le : α → α → Prop) →
      le = LE.le →
        (sup : α → α → α) →
          sup = max →
            (inf : α → α → α) →
              inf = min →
                (sSup : Set α → α) →
                  sSup = SupSet.sSup → (sInf : Set α → α) → sInf = InfSet.sInf → ConditionallyCompleteLattice α
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Turn a `Subsemiring` into a `NonUnitalSubsemiring` by forgetting that it contains `1`.  -/
Subsemiring.toNonUnitalSubsemiring : {R : Type u} → [inst : NonAssocSemiring R] → Subsemiring R → NonUnitalSubsemiring R
-- Mathlib.Topology.Algebra.GroupWithZero
Continuous.inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} [inst_4 : TopologicalSpace α], Continuous f → (∀ (x : α), f x ≠ 0) → Continuous f⁻¹
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_comp_tensorMap : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] [inst_9 : Invertible 2]
  {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄}
  (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄),
  QuadraticMap.comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → (Std.TreeMap.unitOfList l cmp).getKey? k = none
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The metavariable context, which may contain variables appearing in this entry.  -/
Lean.Meta.RefinedDiscrTree.LazyEntry.mctx : Lean.Meta.RefinedDiscrTree.LazyEntry → Lean.MetavarContext
-- Lean.Attributes
Lean.AttributeImpl : Type
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epimorphism is a morphism which is the cokernel of some morphism.  -/
CategoryTheory.NormalEpi.w : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {f : X ⟶ Y} [self : CategoryTheory.NormalEpi f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g f = 0
-- Lean.Declaration
Lean.ConstantInfo.isInductive : Lean.ConstantInfo → Bool
-- Mathlib.Algebra.Ring.AddAut
/-- Left multiplication by a unit of a semiring as an additive automorphism.  -/
AddAut.mulLeft : {R : Type u_1} → [inst : Semiring R] → Rˣ →* Multiplicative (AddAut R)