mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.tensorObj_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ F₂ : CategoryTheory.Functor J C) {j j' : J} (f : j ⟶ j'),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂).map f =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (F₁.map f) (F₂.map f)
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.localization_away : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [IsLocalization.Away r S], Algebra.IsStandardSmoothOfRelativeDimension 0 R S
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.prod_map_comap_prod' : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {M' : Type u_5} {N' : Type u_6} [inst_2 : Add M']
  [inst_3 : Add N'] (f : M →ₙ+ N) (g : M' →ₙ+ N') (S : AddSubsemigroup N) (S' : AddSubsemigroup N'),
  AddSubsemigroup.comap (f.prodMap g) (S.prod S') = (AddSubsemigroup.comap f S).prod (AddSubsemigroup.comap g S')
-- Lean.Server.FileSource
/-- Yields the file source of `item` by attempting to obtain `mod : Name` from `item.data?`. \
Panics if `item.data?` is not present or does not contain a `mod` field and the first element of a
`data?` array cannot be parsed to `Name`.
Used when `completionItem/resolve` requests pass the watchdog to decide which file worker to forward
the request to.
Since this function can panic and clients typically send `completionItem/resolve` requests for every
selected completion item, all completion items returned by the server in `textDocument/completion`
requests must have a `data?` field that has a `mod` field.
 -/
Lean.Lsp.CompletionItem.getFileSource! : Lean.Lsp.CompletionItem → Lean.Lsp.DocumentUri
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.mk.eq_1 : ∀ {α : Type u_1} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop),
  PresentedAddMonoid.mk rels = { toFun := Quotient.mk (addConGen rels).toSetoid, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.continuous_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous TopologicalSpace.NonemptyCompacts.toCompacts
-- Lean.Parser.Term
Lean.Parser.Term.suffices.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_toUInt16 : ∀ (n : UInt64), n.toUInt16.toUInt8 = n.toUInt8
-- Mathlib.GroupTheory.Torsion
/-- The `p`- and `q`-primary components are disjoint for `p ≠ q`.  -/
AddCommMonoid.primaryComponent.disjoint : ∀ {G : Type u_1} [inst : AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')],
  p ≠ p' → Disjoint (AddCommMonoid.primaryComponent G p) (AddCommMonoid.primaryComponent G p')
-- Mathlib.RingTheory.Smooth.Kaehler
sectionOfRetractionKerToTensorAux_prop : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))),
  l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id →
    ∀ (x y : P),
      (algebraMap P S) x = (algebraMap P S) y →
        x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x)) = y - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) y))
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.eq_1 : ∀ {Ω : Type u_1} {β : Type u_6} {γ : Type u_7} {_mΩ : MeasurableSpace Ω} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepFun f g μ =
    ProbabilityTheory.Kernel.IndepFun f g (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.unop_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → Mᵐᵒᵖ),
  MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
OneHom.withBotMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N] (f : OneHom M N), ⇑f.withBotMap = WithBot.map ⇑f
-- Init.Data.List.Lemmas
List.all_flatten : ∀ {α : Type u_1} {f : α → Bool} {l : List (List α)}, l.flatten.all f = l.all fun x => x.all f
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- For any multiplicative function `f` and any `n > 0`,
we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n`  -/
ArithmeticFunction.IsMultiplicative.multiplicative_factorization : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (f : ArithmeticFunction R),
  f.IsMultiplicative → ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.forIn'.loop.match_3.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (x : 0 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFiltered_op_iff_isCofiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.IsFiltered Cᵒᵖ ↔ CategoryTheory.IsCofiltered C
-- Mathlib.Geometry.Manifold.Riemannian.Basic
IsRiemannianManifold.out : ∀ {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 : PseudoEMetricSpace M}
  {inst_5 : ChartedSpace H M} {inst_6 : Bundle.RiemannianBundle fun x => TangentSpace I x}
  [self : IsRiemannianManifold I M] (x y : M), edist x y = Manifold.riemannianEDist I x y
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} [inst : DecidableEq o] {α : Type u_14} [inst_1 : AddMonoid α]
  [inst_2 : StarAddMonoid α] (M : o → Matrix m n α),
  (Matrix.blockDiagonal M).conjTranspose = Matrix.blockDiagonal fun k => (M k).conjTranspose
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.inter! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {m₁ m₂ : Std.DTreeMap.Internal.Impl α β},
  m₁.WF → (m₁.inter! m₂).WF
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean : Hashable Lean.Grind.Linarith.Poly
-- Batteries.Tactic.PrintOpaques
/-- Collect the results for a given constant.  -/
Batteries.Tactic.CollectOpaques.collect : Lean.Name → Batteries.Tactic.CollectOpaques.M Unit
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.commutant_commutant : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : VonNeumannAlgebra H), S.commutant.commutant = S
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_dvd_finrank_left : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A], Module.finrank K A ∣ Module.finrank F A
-- Init.Data.Vector.Zip
Vector.extract_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {n : ℕ} {as : Vector α n} {bs : Vector α_1 n}
  {i j : ℕ}, (Vector.zipWith f as bs).extract i j = Vector.zipWith f (as.extract i j) (bs.extract i j)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_eq_of_inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} [inst_1 : CategoryTheory.IsIso f]
  {g : X ⟶ Y}, CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X → CategoryTheory.inv f = g
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.kernelFork.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z),
  I.kernelFork = CategoryTheory.Limits.KernelFork.ofι (I.ι.f 0) ⋯
-- Lean.Util.OccursCheck
_private.Lean.Util.OccursCheck.0.Lean.occursCheck.visitMVar : {m : Type → Type} →
  [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → Lean.MVarId → ExceptT Unit (StateT Lean.ExprSet m) Unit
-- Mathlib.Order.KrullDimension
Order.height_nat : ∀ (n : ℕ), Order.height n = ↑n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.addMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (self : CategoryTheory.AddMon C) → CategoryTheory.AddMonObj self.X
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_eq_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {m m' : M} {s s' : ℕ+},
  DivisibleHull.mk m s = DivisibleHull.mk m' s' ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'
-- Mathlib.Algebra.Divisibility.Basic
Dvd.elim : ∀ {α : Type u_1} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → P
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.OplaxTrans F G)
  (θ : CategoryTheory.Lax.OplaxTrans G H) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.vCompApp θ c))
      (η.vCompNaturality θ (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.vCompApp θ c)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (η.vCompNaturality θ g))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (η.vCompApp θ b) (H.map g)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.vCompNaturality θ f) (H.map g))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (η.vCompApp θ a) (H.map f) (H.map g)).hom
              (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapComp f g))))))
-- Mathlib.Order.Minimal
Maximal.mono : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Maximal P x → Q ≤ P → Q x → Maximal Q x
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.ext : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G}, η₁.toNatTrans = η₂.toNatTrans → η₁ = η₂
-- Init.Data.Vector.Lemmas
Vector.toArray_swapAt! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α},
  ((xs.swapAt! i x).1, (xs.swapAt! i x).2.toArray) = ((xs.toArray.swapAt! i x).1, (xs.toArray.swapAt! i x).2)
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocCommSemiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocCommSemiring R⦄,
  HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mem_localTrivAt_baseSet : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B),
  b ∈ (Z.localTrivAt b).baseSet
-- Mathlib.Order.Interval.Basic
Interval.canLift : ∀ {α : Type u_1} [inst : LE α], CanLift (Interval α) (NonemptyInterval α) Interval.coe fun r => r ≠ ⊥
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.ext_iff : ∀ {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.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.HasShift C ℤ} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_6 : CategoryTheory.Pretriangulated C}
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {x y : X.Hom Y}, x = y ↔ x.hom = y.hom
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
/-- This lemma allows the computation of the connecting homomorphism
`D.δ` when `D : SnakeInput C` and `C` is a concrete category.  -/
CategoryTheory.ShortComplex.SnakeInput.δ_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Abelian C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  (D : CategoryTheory.ShortComplex.SnakeInput C) (x₃ : CategoryTheory.ToType D.L₀.X₃)
  (x₂ : CategoryTheory.ToType D.L₁.X₂) (x₁ : CategoryTheory.ToType D.L₂.X₁),
  (CategoryTheory.ConcreteCategory.hom D.L₁.g) x₂ = (CategoryTheory.ConcreteCategory.hom D.v₀₁.τ₃) x₃ →
    (CategoryTheory.ConcreteCategory.hom D.L₂.f) x₁ = (CategoryTheory.ConcreteCategory.hom D.v₁₂.τ₂) x₂ →
      (CategoryTheory.ConcreteCategory.hom D.δ) x₃ = (CategoryTheory.ConcreteCategory.hom D.v₂₃.τ₁) x₁
-- Init.Data.UInt.Lemmas
UInt8.ofNatClamp_finVal : ∀ (n : Fin UInt8.size), UInt8.ofNatClamp ↑n = UInt8.ofFin n
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.functorPullback_functorPushforward_overForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (S : CategoryTheory.Sieve Y),
  CategoryTheory.Sieve.functorPullback (CategoryTheory.Over.forget X)
      (CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.forget X) S) =
    S
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_inj : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ici a = Set.Ici b ↔ a = b
-- Mathlib.RingTheory.RingHom.Locally
RingHom.locally_iff_finite : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instDecidableEqOfTransCmpOfLawfulEqCmpOfLawfulBEq : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] →
          [inst : (k : α) → BEq (β k)] → [∀ (k : α), LawfulBEq (β k)] → DecidableEq (Std.ExtDTreeMap α β cmp)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_congr_right_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (n : ℕ) {s t : Set 𝕜},
  IsOpen s → IsOpen t → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n f t) (s ∩ t)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i).base)
-- Mathlib.Analysis.InnerProductSpace.PiL2
LinearEquiv.isometryOfInner.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f f_1 : E ≃ₗ[𝕜] E')
  (e_f : f = f_1) (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y), f.isometryOfInner h = f_1.isometryOfInner ⋯
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.leadCoeff.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (a : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly)
  (h_1 :
    (a : ℤ) →
      (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add a v p))
  (h_2 : (x : Int.Internal.Linear.Poly) → motive x),
  (match Int.Internal.Linear.Poly.add a v p with
    | Int.Internal.Linear.Poly.add a v p => h_1 a v p
    | x => h_2 x) =
    h_1 a v p
-- Mathlib.Analysis.Calculus.Deriv.Basic
norm_derivWithin_eq_norm_fderivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, ‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖
-- Lean.MetavarContext
/-- When creating binders for abstracted metavariables, we use the following `BinderInfo`.  -/
Lean.MetavarContext.MkBinding.Context.binderInfoForMVars : Lean.MetavarContext.MkBinding.Context → Lean.BinderInfo
-- Init.Grind.Ring.Basic
/-- One is the right identity for multiplication.  -/
Lean.Grind.Semiring.mul_one : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α), a * 1 = a
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.IsContained.lineGraph : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'},
  G.IsContained G' → G.lineGraph.IsContained G'.lineGraph
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.prod_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {η : Type u_5} {ε : Type u_6} (e : PartialEquiv α β)
  (f : PartialEquiv β γ) (e' : PartialEquiv δ η) (f' : PartialEquiv η ε),
  (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
-- Mathlib.Algebra.Lie.Free
_private.Mathlib.Algebra.Lie.Free.0.«termLib.lift» : Lean.ParserDescr
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.adhoc.inj : ∀ {backend backend_1 : Lean.Name},
  Lean.ExternEntry.adhoc backend = Lean.ExternEntry.adhoc backend_1 → backend = backend_1
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- `MvPowerSeries` on a `T0Space` form a `T0Space`  -/
MvPowerSeries.WithPiTopology.instT0Space : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [T0Space R], T0Space (MvPowerSeries σ R)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.null_mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ ⦃t : Set α⦄, ν t = 0 → μ t = 0
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_uInt8ToBitVec : ∀ (x : UInt8), Int8.ofBitVec x.toBitVec = x.toInt8
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- Two submonoids are equal if they have the same elements.  -/
Submonoid.ext : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductively defined smallest multiplicative congruence relation containing a given binary
relation.  -/
ConGen.Rel : {M : Type u_1} → [Mul M] → (M → M → Prop) → M → M → Prop
-- Mathlib.CategoryTheory.Opposites
/-- Given a natural transformation `α : F.rightOp ⟶ G.rightOp`, for `F G : Cᵒᵖ ⥤ D`,
taking `unop` of each component gives a natural transformation `G ⟶ F`.
 -/
CategoryTheory.NatTrans.removeRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor Cᵒᵖ D} → (F.rightOp ⟶ G.rightOp) → (G ⟶ F)
-- Mathlib.RingTheory.OreLocalization.OreSet
/-- Cancellability in monoids with zeros can act as a replacement for the `ore_right_cancel`
condition of an ore set.  -/
OreLocalization.oreSetOfIsCancelMulZero : {R : Type u_1} →
  [inst : MonoidWithZero R] →
    [IsCancelMulZero R] →
      {S : Submonoid R} →
        (oreNum : R → ↥S → R) →
          (oreDenom : R → ↥S → ↥S) →
            (∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s) → OreLocalization.OreSet S
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.mk.injEq : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} (atlas : Set (PartialEquiv M H))
  (chartAt : M → PartialEquiv M H) (mem_chart_source : ∀ (x : M), x ∈ (chartAt x).source)
  (chart_mem_atlas : ∀ (x : M), chartAt x ∈ atlas)
  (open_source : ∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source)
  (continuousOn_toFun :
    ∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source)
  (atlas_1 : Set (PartialEquiv M H)) (chartAt_1 : M → PartialEquiv M H)
  (mem_chart_source_1 : ∀ (x : M), x ∈ (chartAt_1 x).source) (chart_mem_atlas_1 : ∀ (x : M), chartAt_1 x ∈ atlas_1)
  (open_source_1 : ∀ (e e' : PartialEquiv M H), e ∈ atlas_1 → e' ∈ atlas_1 → IsOpen (e.symm.trans e').source)
  (continuousOn_toFun_1 :
    ∀ (e e' : PartialEquiv M H),
      e ∈ atlas_1 → e' ∈ atlas_1 → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source),
  ({ atlas := atlas, chartAt := chartAt, mem_chart_source := mem_chart_source, chart_mem_atlas := chart_mem_atlas,
        open_source := open_source, continuousOn_toFun := continuousOn_toFun } =
      { atlas := atlas_1, chartAt := chartAt_1, mem_chart_source := mem_chart_source_1,
        chart_mem_atlas := chart_mem_atlas_1, open_source := open_source_1,
        continuousOn_toFun := continuousOn_toFun_1 }) =
    (atlas = atlas_1 ∧ chartAt = chartAt_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardOver.eq_1 : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C),
  SheafOfModules.pushforwardOver x =
    { hom := { app := fun U => R.obj.map CategoryTheory.Limits.prod.snd.op, naturality := ⋯ } }
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.smul_mat_empty : ∀ {α : Type u} [inst : NonUnitalNonAssocSemiring α] {m' : Type u_1} (x : α) (A : Fin 0 → m' → α), x • A = ![]
-- Mathlib.Order.WithBot
WithTop.untopA.eq_1 : ∀ {α : Type u_1} [inst : Nonempty α], WithTop.untopA = WithTop.untopD (Classical.arbitrary α)
-- Mathlib.Analysis.CStarAlgebra.Basic
edist_star_star : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x y : E),
  edist (star x) (star y) = edist x y
-- Init.Data.Fin.Fold
Fin.foldrM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] {n k : ℕ} (w : n = k) (f : Fin n → α → m α),
  Fin.foldrM n f = Fin.foldrM k fun i => f (Fin.cast ⋯ i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (assign : α → Bool) (lhsExpr rhsExpr : BitVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lhsExpr.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rhsExpr.getLsbD idx) →
      ⟦assign, { aig := aig, ref := cin }⟧ = BitVec.carry curr lhsExpr rhsExpr false →
        ∀ (idx : ℕ) (hidx1 : idx < w),
          curr ≤ idx →
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig,
                  ref :=
                    (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).vec.get idx
                      hidx1 }⟧ =
              (⟦assign, { aig := aig, ref := lhs.get idx hidx1 }⟧ ^^
                (⟦assign, { aig := aig, ref := rhs.get idx hidx1 }⟧ ^^ BitVec.carry idx lhsExpr rhsExpr false))
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_eq_empty : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] {f g : α →₀ N},
  f.neLocus g = ∅ ↔ f = g
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.finrank_eq_one : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] [Module.Free R M], Module.finrank R M = 1
-- Aesop.Tracing
Aesop.nodeUnknownEmoji : String
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_hom : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V), (X.isoOfEq e).hom = X.homOfLE ⋯