mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instFunLike.eq_1 : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.instFunLike = { coe := fun f => (↑f.toAddMonoidHom).toFun, coe_injective := ⋯ }
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.revAll_prop_eq : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String}, s.revAll P = s.toList.all fun x => decide (P x)
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_var_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Bool
-- Mathlib.Algebra.Group.Ext
AddLeftCancelMonoid.toAddMonoid_injective : ∀ {M : Type u}, Function.Injective (@AddLeftCancelMonoid.toAddMonoid M)
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
eval₂_minpolyDiv_self : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_1}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [IsDomain T] [inst_6 : DecidableEq T] (x : S) (σ₁ σ₂ : S →ₐ[R] T),
  Polynomial.eval₂ (↑σ₁) (σ₂ x) (minpolyDiv R x) =
    if σ₁ x = σ₂ x then σ₁ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iff_le_comap : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.comap ϕ.toAddMonoidHom H
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a),
  t.eTruncLTLTIsoLT a b hab = t.eTruncLTLTIsoLT a b hab
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.id.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithInitial.star.id = PUnit.unit
-- Init.Coe
/-- `Coe α β` is the typeclass for coercions from `α` to `β`. It can be transitively
chained with other `Coe` instances, and coercion is automatically used when
`x` has type `α` but it is used in a context where `β` is expected.
You can use the `↑x` operator to explicitly trigger coercion.
 -/
Coe : semiOutParam (Sort u) → Sort v → Sort (max (max 1 u) v)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The canonical cone over `diagram P` with point `P`.  -/
ProfiniteAddGrp.cone : (P : ProfiniteAddGrp.{u}) → CategoryTheory.Limits.Cone P.diagram
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.uniformity_def : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M],
  uniformity (TrivSqZeroExt R M) =
    Filter.comap (fun p => (p.1.fst, p.2.fst)) (uniformity R) ⊓
      Filter.comap (fun p => (p.1.snd, p.2.snd)) (uniformity M)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.lintegral : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ]
  {f : α × β → StieltjesFunction ℝ},
  ProbabilityTheory.IsCondKernelCDF f κ ν →
    ∀ (a : α) (x : ℝ), ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (Set.univ ×ˢ Set.Iic x)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatIso_inv : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] [inst_5 : LF'.IsLeftDerivedFunctor α' W] (τ : F' ≅ F),
  (LF'.leftDerivedNatIso LF α' α W τ).inv = LF.leftDerivedNatTrans LF' α α' W τ.inv
-- Lean.Meta.Sym.Canon
/-- Canonicalize an instance by trying to resynthesize it without caching.
Recall that we have special support for `Decidable` and propositional instances.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInst' : Lean.Expr → optParam Bool true → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).max?.isSome = true
-- Mathlib.Data.Bool.Basic
Bool.ofNat_le_ofNat : ∀ {n m : ℕ}, n ≤ m → Bool.ofNat n ≤ Bool.ofNat m
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.Cache.get?.match_1.splitter : {w : ℕ} →
  (expr : Std.Tactic.BVDecide.BVExpr w) →
    (motive : Option (Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → Sort u_1) →
      (x : Option (Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w)) →
        ((refs : Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → x = some refs → motive (some refs)) →
          (x = none → motive none) → motive x
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.lt_pow_nthRoot_add_one : ∀ {n : ℕ}, n ≠ 0 → ∀ (a : ℕ), a < (n.nthRoot a + 1) ^ n
-- Mathlib.Algebra.Lie.Weights.Killing
/-- In a Lie algebra with non-degenerate Killing form, a Lie ideal decomposes as its intersection
with the Cartan subalgebra plus a sum of root spaces corresponding to some subset of roots.  -/
LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (I : LieIdeal K L),
  LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ α, ⨆ (_ : LieAlgebra.rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), LieAlgebra.rootSpace H ⇑↑α
-- Mathlib.Analysis.Normed.Operator.Mul
/-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically
equivalent to `M`.  -/
ContinuousLinearMap.toSpanSingletonLIE : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E ≃ₗᵢ[𝕜] 𝕜 →L[𝕜] E
-- Mathlib.FieldTheory.Perfect
powMulEquiv_pow : ∀ (M : Type u_1) (p : ℕ) [inst : CommMonoid M] [inst_1 : PerfectRing M p] (n : ℕ),
  powMulEquiv M (p ^ n) = powMulEquiv M p ^ n
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.checkLetArrowRHS : Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.functor_map : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] {f g : α → C} (t : f ⟶ g),
  (CategoryTheory.Limits.Sigma.functor α).map t = CategoryTheory.Limits.Sigma.map t
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Converting a `Stained` to a `String`:
* a `Name` is represented by the corresponding string;
* `goal` is represented by `⊢`;
* `wildcard` is represented by `*`.
 -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instToStringStained : ToString Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Algebra.Category.Ring.Limits
CommSemiRingCat.limitCommSemiring : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommSemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] →
        CommSemiring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommSemiRingCat))).pt
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_eq_setToL1' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : NormedRing 𝕜] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : IsBoundedSMul 𝕜 E]
  [inst_8 : IsBoundedSMul 𝕜 F] [inst_9 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (f : ↥(MeasureTheory.Lp E 1 μ)),
  (MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1' 𝕜 hT h_smul) f
-- Mathlib.Order.CompleteLattice.Basic
biInf_ge_eq_inf : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : PartialOrder ι] (f : ι → α) (i : ι),
  ⨅ j, ⨅ (_ : j ≥ i), f j = f i ⊓ ⨅ j, ⨅ (_ : j > i), f j
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_mul_le : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a.tdiv b * b ≤ a + ↑(if 0 ≤ a then 0 else b.natAbs - 1)
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instLocallyDirectedIsOpenImmersionCover : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰) →
          [inst_2 : Small.{u, u_1} 𝒰.I₀] →
            [inst_3 : Quiver.IsThin 𝒰.I₀] → AlgebraicGeometry.Scheme.Cover.LocallyDirected d.cover
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.ClusterState.matchPremise?.updateSubst : Lean.FVarId → Array Lean.MVarId → Aesop.PremiseIndex → Aesop.Substitution → Aesop.BaseM Aesop.Substitution
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_mul_cancel_left : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x y : M₀), IsUnit x → Ring.inverse x * (x * y) = y
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofan.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C),
  CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f =
    CategoryTheory.Limits.Cofan.mk { I := (i : 𝒜) × (f i).I, obj := fun p => (f p.fst).obj p.snd } fun i =>
      { f := fun x => ⟨i, x⟩, φ := fun x => CategoryTheory.CategoryStruct.id ((f i).obj x) }
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unit_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.inverse.map (e.functor.map f)) =
    CategoryTheory.CategoryStruct.comp f (e.unit.app Y)
-- Mathlib.Data.WSeq.Defs
Stream'.WSeq.nil.eq_1 : ∀ {α : Type u}, Stream'.WSeq.nil = Stream'.Seq.nil
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mul_eq_zero_iff : ∀ {f g : UpperHalfPlane → ℂ}, MDiff f → MDiff g → (f * g = 0 ↔ f = 0 ∨ g = 0)
-- Batteries.Recycling.RBTree.Basic
/-- The predicate asserting that the result of `alterP` is safe to construct.  -/
RBTree.RBSet.AlterWF : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → (Option α → Option α) → Prop
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instReprFanin : Repr Std.Sat.AIG.Fanin
-- Mathlib.RingTheory.Binomial
instBinomialRingOfModuleNNRat : {R : Type u_1} → [inst : AddCommMonoid R] → [Module ℚ≥0 R] → [inst_2 : Pow R ℕ] → BinomialRing R
-- Batteries.Classes.Order
Std.instLawfulOrdBool : Std.LawfulOrd Bool
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} →
              (φK : h₁.K ⟶ h₂.K) →
                (φH : h₁.H ⟶ h₂.H) →
                  autoParam (CategoryTheory.CategoryStruct.comp φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂)
                      CategoryTheory.ShortComplex.LeftHomologyMapData.commi._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp h₁.f' φK = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f')
                        CategoryTheory.ShortComplex.LeftHomologyMapData.commf'._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp h₁.π φH = CategoryTheory.CategoryStruct.comp φK h₂.π)
                          CategoryTheory.ShortComplex.LeftHomologyMapData.commπ._autoParam →
                        CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂
-- Init.Data.Nat.Lemmas
Nat.div_le_iff_le_mul_of_dvd : ∀ {b a c : ℕ}, b ≠ 0 → b ∣ a → (a / b ≤ c ↔ a ≤ c * b)
-- Mathlib.Algebra.Group.Defs
MulOne.toOne : {M : Type u_2} → [self : MulOne M] → One M
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.noncomputable.sizeOf_spec : sizeOf Lean.Elab.ComputeKind.noncomputable = 1
-- Init.Grind.ToInt
/-- The upper bound of the interval, if finite.  -/
Lean.Grind.IntInterval.hi? : Lean.Grind.IntInterval → Option ℤ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_eq_single : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f : α →₀ M} (a : α)
  {g : α → M → N}, (∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1) → (f a = 0 → g a 0 = 1) → f.prod g = g a (f a)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot : Type → Type
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.setTag.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {cidx : ℕ}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_9} {fvarId_1 : Lean.FVarId}
  {cidx_1 : ℕ} {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_9},
  Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h = Lean.Compiler.LCNF.CodeDecl.setTag fvarId_1 cidx_1 h_1 →
    fvarId = fvarId_1 ∧ cidx = cidx_1
-- Mathlib.Algebra.Group.Ext
AddCommMonoid.toAddMonoid_injective : ∀ {M : Type u}, Function.Injective (@AddCommMonoid.toAddMonoid M)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.  -/
MeasurableEquiv.piCongrLeft : {δ : Type u_4} →
  {δ' : Type u_5} →
    (π : δ' → Type u_6) →
      [inst : (x : δ') → MeasurableSpace (π x)] → (f : δ ≃ δ') → ((b : δ) → π (f b)) ≃ᵐ ((a : δ') → π a)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofNat_le_toENat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n ≤ Cardinal.toENat c ↔ OfNat.ofNat n ≤ c
-- Mathlib.Algebra.GroupWithZero.Invertible
div_mul_cancel_of_invertible : ∀ {α : Type u} [inst : GroupWithZero α] (a b : α) [Invertible b], a / b * b = a
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.strictAnti_sumCoeffsExp : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), StrictAnti fun p => ∑ i, a i * b i ^ p
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux_self : ∀ {α : Type u_1} (r : α → α → Bool),
  (∀ (a : α), r a a = true) → ∀ (xs : Array α) (i : ℕ) (h : i ≤ xs.size), xs.isEqvAux xs ⋯ r i h = true
-- Init.Data.SInt.Lemmas
ISize.neg_mul_not_eq_add_mul : ∀ {a b : ISize}, -(a * ~~~b) = a + a * b
-- Mathlib.CategoryTheory.Functor.Functorial
CategoryTheory.map_functorial_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y), CategoryTheory.map F.obj f = F.map f
-- Lean.Server.References
Lean.Server.References.DocumentRefInfo.mk.sizeOf_spec : ∀ (location : Lean.Lsp.Location) (module : Lean.Name) (parentInfo? : Option Lean.Server.References.ParentDecl),
  sizeOf { location := location, module := module, parentInfo? := parentInfo? } =
    1 + sizeOf location + sizeOf module + sizeOf parentInfo?
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.inhabited.eq_1 : ∀ {α : Type u}, WithOne.inhabited = { default := 1 }
-- Mathlib.Computability.Language
/-- An equivalence between the "proxy type" `Symbol.proxyType` and `Symbol`. The proxy type is a reducible definition that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` (and whatever other inductive types appear within the inductive type), and the intended use is to define typeclass instances uses pre-existing instances on these. (Generated by the `proxy_equiv%` elaborator.) -/
Symbol.proxyTypeEquiv : (T : Type u_4) → (N : Type u_5) → T ⊕ N ≃ Symbol T N
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- **Alias** of `NumberField.Units.finrank_modTorsion`. -/
NumberField.Units.rank_modTorsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℤ (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K)) = NumberField.Units.rank K
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.whiskerLeft η Γ).as.app a =
    CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_fiber : ∀ {α : Type u_1} {ι : Type u_4} (f : ι → α) (s : Set α), s.PairwiseDisjoint fun a => f ⁻¹' {a}
-- Mathlib.Algebra.GCDMonoid.Basic
Associated.gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a₁ a₂ b₁ b₂ : α},
  Associated a₁ a₂ → Associated b₁ b₂ → Associated (gcd a₁ b₁) (gcd a₂ b₂)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraAlgEquivDirectSum_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : (m : A) → Decidable (m ≠ 0)],
  ⇑addMonoidAlgebraAlgEquivDirectSum = AddMonoidAlgebra.toDirectSum
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtNormed.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (n : ι),
  InnerProductSpace.gramSchmidtNormed 𝕜 f n =
    (↑‖InnerProductSpace.gramSchmidt 𝕜 f n‖)⁻¹ • InnerProductSpace.gramSchmidt 𝕜 f n
-- Aesop.Tree.Data
/-- At each point during the search, every node of the tree (goal, rapp or mvar
cluster) is in one of these states:

- `proven`: the node is proven.
- `unprovable`: the node is unprovable, i.e. it will never be proven regardless
  of any future expansions that might be performed.
- `unknown`: neither of the above.

Every node starts in the `unknown` state and may later become either `proven` or
`unprovable`. After this, the state does not change any more.
 -/
Aesop.NodeState : Type
-- Mathlib.Analysis.Complex.Exponential
Real.expNear.eq_1 : ∀ (n : ℕ) (x r : ℝ), Real.expNear n x r = ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial + x ^ n / ↑n.factorial * r
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape)
  [inst_1 : Unique J.L] [inst_2 : Unique J.R] {X Y : C} (f g : X ⟶ Y)
  (c : CategoryTheory.Limits.Multifork (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g)),
  ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).functor.obj c).ι = c.ι default
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.wideSubcategoryInclusion.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.WideSubcategory P} {f : X ⟶ Y},
  (CategoryTheory.wideSubcategoryInclusion P).map f = f.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.app
    (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) =
  CategoryTheory.Iso.refl (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero)
-- Mathlib.Data.List.Nodup
List.Nodup.union : ∀ {α : Type u} {l₂ : List α} [inst : BEq α] [LawfulBEq α] (l₁ : List α), l₂.Nodup → (l₁ ∪ l₂).Nodup
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.updateUsedVarsOf : Lean.FVarId → Lean.Elab.Term.MutualClosure.FixPoint.M Unit
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans'_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source)
  (a : α), ↑(e.trans' e' h) a = (↑e' ∘ ↑e) a
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.top_prod : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid N),
  ⊤.prod s = AddSubmonoid.comap (AddMonoidHom.snd M N) s
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type I₂(m).

The corresponding Coxeter-Dynkin diagram is:
```
     m + 2
    o --- o
```
 -/
CoxeterMatrix.I : ℕ → CoxeterMatrix (Fin 2)
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.mem_L1_inner : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f g : ↥(MeasureTheory.Lp E 2 μ)),
  MeasureTheory.AEEqFun.mk (fun x => inner 𝕜 (↑↑f x) (↑↑g x)) ⋯ ∈ MeasureTheory.Lp 𝕜 1 μ
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_inf_distrib_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι) (f : ι → α) (a : α),
  s.sup f ⊓ a = s.sup fun i => f i ⊓ a
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_add_const_Ico : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => x + a) '' Set.Ico b c = Set.Ico (b + a) (c + a)
-- Mathlib.Algebra.Order.Star.Basic
star_nonpos_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, star x ≤ 0 ↔ x ≤ 0
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.of_commsq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S),
  CategoryTheory.CategoryStruct.comp (p.map φ) (CategoryTheory.eqToHom hb) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ha) f →
    p.IsHomLift f φ
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `closure_sdiff_intrinsicInterior`. -/
closure_diff_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [inst_5 : MetricSpace P]
  [inst_6 : NormedAddTorsor V P] (s : Set P), closure s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(0 | b)` vanishes when `b > 1`.  -/
jacobiSym.zero_left : ∀ {b : ℕ}, 1 < b → jacobiSym 0 b = 0
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_add : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x y : R), WithVal.toVal v (x + y) = WithVal.toVal v x + WithVal.toVal v y