mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instCanonicallyOrderedMul : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] [inst_3 : Mul β]
  [inst_4 : LE β] [CanonicallyOrderedMul β], CanonicallyOrderedMul (α × β)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `Iso.inv`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.isoInv : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.IsoLift → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- Functoriality of the weighted limits with fixed weight `W : J ⥤ Type w`
with respect to the functor in `J ⥤ C`.  -/
CategoryTheory.Functor.weightedLimObjMap : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (W : CategoryTheory.Functor J (Type w)) →
          {F₁ F₂ : CategoryTheory.Functor J C} →
            [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F₁] →
              [inst_3 : CategoryTheory.Limits.HasWeightedLimit W F₂] →
                (F₁ ⟶ F₂) → (W.weightedLimObjObj F₁ ⟶ W.weightedLimObjObj F₂)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_im : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : Zero R], a.im.imI = a.imI
-- Mathlib.RingTheory.TensorProduct.Free
LinearMap.toMatrix_baseChange : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} {ι₂ : Type u_5} (A : Type u_6) [inst : Fintype ι]
  [inst_1 : Finite ι₂] [inst_2 : DecidableEq ι] [inst_3 : CommSemiring R] [inst_4 : CommSemiring A]
  [inst_5 : Algebra R A] [inst_6 : AddCommMonoid M₁] [inst_7 : Module R M₁] [inst_8 : AddCommMonoid M₂]
  [inst_9 : Module R M₂] (f : M₁ →ₗ[R] M₂) (b₁ : Module.Basis ι R M₁) (b₂ : Module.Basis ι₂ R M₂),
  (LinearMap.toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂))
      (LinearMap.baseChange A f) =
    ((LinearMap.toMatrix b₁ b₂) f).map ⇑(algebraMap R A)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.IsCyclicallyReduced.eq_1 : ∀ {α : Type u} (L : List (α × Bool)),
  FreeAddGroup.IsCyclicallyReduced L =
    (FreeAddGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2)
-- Mathlib.Topology.Algebra.Ring.Basic
instContinuousAddMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [ContinuousAdd R],
  ContinuousAdd Rᵐᵒᵖ
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Smooth.formallySmooth : ∀ {R : Type u_4} {inst : CommRing R} {A : Type u} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.Smooth R A], Algebra.FormallySmooth R A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_some_getD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.contains a = true → t.get? a = some (t.getD a fallback)
-- Init.Data.String.Lemmas.Splits
String.splits_endPos : ∀ (s : String), s.endPos.Splits s ""
-- Mathlib.Topology.Order.IntermediateValue
Set.OrdConnected.isPreconnected : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {s : Set α}, s.OrdConnected → IsPreconnected s
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.braiding_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C), (X.braiding Y).inv.f = (X.snd.β Y.fst).inv
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.algebraMap_apply : ∀ {n : Type u_2} {R : Type u_3} {A : Type u_5} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] {r : R} {i j : n},
  (algebraMap R (CStarMatrix n n A)) r i j = if i = j then (algebraMap R A) r else 0
-- Mathlib.Algebra.Module.ULift
ULift.mulActionWithZero : {R : Type u} →
  {M : Type v} →
    [inst : MonoidWithZero R] → [inst_1 : Zero M] → [MulActionWithZero R M] → MulActionWithZero (ULift.{u_1, u} R) M
-- Mathlib.Topology.Separation.Basic
/-- For point `x` in a discrete subset `s` of a topological space, there is a set `U`
such that
1. `U` is a punctured neighborhood of `x` (i.e. `U ∪ {x}` is a neighbourhood of `x`),
2. `U` is disjoint from `s`.
 -/
disjoint_nhdsWithin_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsDiscrete s → ∀ {x : X}, x ∈ s → ∃ U ∈ nhdsWithin x {x}ᶜ, Disjoint U s
-- Mathlib.Topology.Algebra.Group.Basic
instDiscreteTopologySubtypeMemSubgroupHSMulOfContinuousConstSMul : ∀ {G : Type w} {H : Type x} [inst : Group G] [inst_1 : Group H] [inst_2 : TopologicalSpace G]
  [inst_3 : MulDistribMulAction H G] [ContinuousConstSMul H G] {𝒢 : Subgroup G} (h : H) [DiscreteTopology ↥𝒢],
  DiscreteTopology ↥(h • 𝒢)
-- Init.Data.SInt.Lemmas
Int8.toInt_toInt16 : ∀ (x : Int8), x.toInt16.toInt = x.toInt
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapLeftRightHom_comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] {Q : Type u_6} [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : Module S P] [inst_12 : IsScalarTower R S P] [inst_13 : Module S Q]
  [inst_14 : IsScalarTower R S Q] {α : M →ₗ[R] P} (j : IsBaseChange S α) (β : N →ₗ[R] Q) (f : M →ₗ[R] N) (m : M),
  ((j.linearMapLeftRightHom β) f) (α m) = β (f m)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName : Type
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.reprW_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁))
  [inst_1 : F.IsRepresentable] (X : Cᵒᵖ) (f : Opposite.unop X ⟶ F.reprX),
  (CategoryTheory.ConcreteCategory.hom (F.reprW.hom.app X)) f =
    (CategoryTheory.ConcreteCategory.hom (F.map f.op)) F.reprx
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Like `LinearMap.isSymmetric_adjoint_mul_self` but domain and range can be different  -/
LinearMap.isSymmetric_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F),
  (LinearMap.adjoint T ∘ₗ T).IsSymmetric
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.toIntCast : {R : Type u} → [self : AddCommGroupWithOne R] → IntCast R
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot.eq_1 : ∀ (n a : ℕ), n.floorRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ (k / n)
-- Batteries.Data.AssocList
Batteries.AssocList.nil.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β], sizeOf Batteries.AssocList.nil = 1
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Ioo : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.image (Fin.cast h) (Finset.Ioo i j) = Finset.Ioo (Fin.cast h i) (Fin.cast h j)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.WeierstrassCurve.Projective.nonsingular_neg_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 ≠ 0 → W.Nonsingular ![P 0 / P 2, W.toAffine.negY (P 0 / P 2) (P 1 / P 2), 1]
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_orthogonalGroup_iff' : ∀ (n : Type u) [inst : DecidableEq n] [inst_1 : Fintype n] (R : Type v) [inst_2 : CommRing R] {A : Matrix n n R},
  A ∈ Matrix.orthogonalGroup n R ↔ A.transpose * A = 1
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The stalk of `Spec R` at `x` is isomorphic to the stalk of `R^~` at `x`.  -/
AlgebraicGeometry.StructureSheaf.commRingCatStalkEquivModuleStalk : (R : Type u) →
  [inst : CommRing R] →
    (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
      ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R R).presheaf x) ≃ₗ[R]
        ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)
-- Mathlib.Topology.Connected.TotallyDisconnected
instTotallyDisconnectedSpaceSigma : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), TotallyDisconnectedSpace (X i)], TotallyDisconnectedSpace ((i : ι) × X i)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) [inst_1 : SizeOf C] (of : C),
  sizeOf { of := of } = 1 + sizeOf of
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.integrable_bilin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [inst_4 : NormedAddCommGroup F₁] [inst_5 : NormedSpace 𝕜 F₁]
  [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.LocallyIntegrableOn φ (↑Ω) μ →
    ∀ (f : TestFunction Ω F₁ n), MeasureTheory.Integrable (fun x => (B (f x)) (φ x)) μ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.zsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s : Finset α},
  s.Nonempty → ∀ {n : ℤ}, (n • s).Nonempty
-- Mathlib.Combinatorics.Tiling.Tile
/-- Coercion from a `PlacedTile` to a set of points. Use the coercion rather than using `coeSet`
directly.  -/
DiscreteTiling.PlacedTile.coeSet : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → {ps : DiscreteTiling.Protoset G X ιₚ} → DiscreteTiling.PlacedTile ps → Set X
-- Init.Data.Vector.Lemmas
Vector.getElem_map : ∀ {α : Type u_1} {β : Type u_2} {n i : ℕ} (f : α → β) {xs : Vector α n} (hi : i < n), (Vector.map f xs)[i] = f xs[i]
-- Lean.Meta.Basic
/-- Number of times each declaration has been unfolded  -/
Lean.Meta.Diagnostics.unfoldCounter : Lean.Meta.Diagnostics → Lean.PHashMap Lean.Name ℕ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonChangeAnnotationSupport : Lean.ToJson Lean.Lsp.ChangeAnnotationSupport
-- Mathlib.NumberTheory.BernoulliPolynomials
/-- Another version of `Polynomial.sum_bernoulli`.  -/
Polynomial.bernoulli_eq_sub_sum : ∀ (n : ℕ),
  (n + 1) • Polynomial.bernoulli n =
    (n + 1) • Polynomial.X ^ n - ∑ k ∈ Finset.range n, (n + 1).choose k • Polynomial.bernoulli k
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β}
  {it₂ : Std.IterM m γ},
  it₂.IsPlausibleStep Std.IterStep.done →
    (Std.IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (Std.IterStep.skip (Std.IterM.flatMapAfterM f it₁ none))
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Ioc : ∀ (x y : NNReal), NNReal.toReal '' Set.Ioc x y = Set.Ioc ↑x ↑y
-- Mathlib.Data.Finsupp.Sigma
/-- `split` returns zero at indices different from where `embSigma` embeds.  -/
Finsupp.split_embSigma_of_ne : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k k' : κ} (f : ι k →₀ M),
  k' ≠ k → f.embSigma.split k' = 0
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.mk.injEq : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (toLinearMap : M →ₗ[R] N)
  (map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆) (toLinearMap_1 : M →ₗ[R] N)
  (map_lie'_1 : ∀ {x : L} {m : M}, toLinearMap_1.toFun ⁅x, m⁆ = ⁅x, toLinearMap_1.toFun m⁆),
  ({ toLinearMap := toLinearMap, map_lie' := map_lie' } = { toLinearMap := toLinearMap_1, map_lie' := map_lie'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.isAdicComplete_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG),
  IsAdicComplete (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R))
    (AdicCompletion (IsLocalRing.maximalIdeal R) R)
-- Mathlib.Probability.Martingale.OptionalSampling
MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [inst_8 : Nonempty ι],
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [MeasureTheory.SigmaFinite (μ.trim ⋯)]
      (i : ι), MeasureTheory.stoppedValue f τ =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f n | hτ.measurableSpace]
-- Mathlib.Topology.LocallyConstant.Basic
/-- The set of clopen subsets of a topological space is equivalent to the locally constant maps to
a two-element set
 -/
LocallyConstant.equivClopens : (X : Type u_1) →
  [inst : TopologicalSpace X] →
    [(s : Set X) → (x : X) → Decidable (x ∈ s)] → LocallyConstant X (Fin 2) ≃ TopologicalSpace.Clopens X
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h' : (P out).Property { down := false })
  (h_1 : (h' : (P out).Property { down := true }) → motive ⟨{ down := true }, h'⟩)
  (h_2 : (h' : (P out).Property { down := false }) → motive ⟨{ down := false }, h'⟩),
  (match ⟨{ down := false }, h'⟩ with
    | ⟨{ down := true }, h'⟩ => h_1 h'
    | ⟨{ down := false }, h'⟩ => h_2 h') =
    h_2 h'
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullbackWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {V : F → F} {s : Set E}, VectorField.pullbackWithin 𝕜 f V s = fun x => (fderivWithin 𝕜 f s x).inverse (V (f x))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.ext : ∀ {α : Type u_1} {m₁ m₂ : MeasurableSpace α}, (∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s) → m₁ = m₂
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.δ₁_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (z : ↥(groupCohomology.cocycles₁ X.X₃)) (y : G → ↑X.X₂),
  ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z →
    ∀ (x : G × G → ↑X.X₁)
      (hx : ⇑(Rep.Hom.hom X.f) ∘ x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ X.X₂)) y),
      (CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hX 1 2 ⋯))
          ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π X.X₃)) z) =
        (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π X.X₁)) ⟨x, ⋯⟩
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_iInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X),
  (∀ (i : ι), StableUnderSpecialization (S i)) → StableUnderSpecialization (⋂ i, S i)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.invRotate_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.invRotate.obj₃ = T.obj₂
-- Lean.Data.Lsp.Internal
/-- Result entry of a module query.  -/
Lean.Lsp.LeanIdentifier : Type
-- Mathlib.Logic.Encodable.Basic
/-- Representative of an equivalence class. This is a computable version of `Quot.out` for a setoid
on an encodable type.  -/
Quotient.rep : {α : Type u_1} → {s : Setoid α} → [DecidableRel fun x1 x2 => x1 ≈ x2] → [Encodable α] → Quotient s → α
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.mk.inj : ∀ {f fType : Lean.Expr} {args mvars : Array Lean.Expr} {bInfos : Array Lean.BinderInfo} {forceRegularApp : Bool}
  {f_1 fType_1 : Lean.Expr} {args_1 mvars_1 : Array Lean.Expr} {bInfos_1 : Array Lean.BinderInfo}
  {forceRegularApp_1 : Bool},
  { f := f, fType := fType, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := forceRegularApp } =
      { f := f_1, fType := fType_1, args := args_1, mvars := mvars_1, bInfos := bInfos_1,
        forceRegularApp := forceRegularApp_1 } →
    f = f_1 ∧
      fType = fType_1 ∧ args = args_1 ∧ mvars = mvars_1 ∧ bInfos = bInfos_1 ∧ forceRegularApp = forceRegularApp_1
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_neg : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  (f : N →ₗ[R] P), LinearMap.lTensor M (-f) = -LinearMap.lTensor M f
-- Mathlib.Topology.JacobsonSpace
Topology.IsClosedEmbedding.preimage_closedPoints : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → f ⁻¹' closedPoints Y = closedPoints X
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.mapWithPostcondition_eq_toIter_mapWithPostcondition_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  {f : β → Std.Iterators.PostconditionT m γ},
  Std.Iter.mapWithPostcondition f it = Std.IterM.mapWithPostcondition f it.toIterM
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.spanningCoe_induce_support : ∀ {V : Type u_1} (G : SimpleGraph V), (SimpleGraph.induce G.support G).spanningCoe = G
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_div : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Div α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋃ i, ⋃ j, s i j) / t = ⋃ i, ⋃ j, s i j / t
-- Init.Sym.DSimp.DSimprocDSL
/-- Parenthesized dsimproc expression.  -/
Lean.Parser.Sym.DSimp.dsimprocParen : Lean.ParserDescr
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ico_succ_right_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico a (Order.succ b) = Set.Icc a b
-- Mathlib.Algebra.Group.Conj
isAddConj_iff_addConjugatesOf_eq : ∀ {α : Type u} [inst : AddMonoid α] {a b : α}, IsAddConj a b ↔ addConjugatesOf a = addConjugatesOf b
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Addition in the colimit is independent of the chosen "maximum" in the filtered
category. In particular, this lemma allows us to "unfold" the definition of the addition of
`x` and `y`, using a custom object `k` and morphisms `f : x.1 ⟶ k` and `g : y.1 ⟶ k`.  -/
AddMonCat.FilteredColimits.colimit_add_mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  AddMonCat.FilteredColimits.M.mk F x + AddMonCat.FilteredColimits.M.mk F y =
    AddMonCat.FilteredColimits.M.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.ne_zero_iff_weightedOrder_finite : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R},
  f ≠ 0 ↔ ↑(MvPowerSeries.weightedOrder w f).toNat = MvPowerSeries.weightedOrder w f
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.kerFun.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x x_1 : X),
  x = x_1 → RKHS.kerFun H x = RKHS.kerFun H x_1
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.norm_compContinuousMultilinearMap_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G),
  ‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.diffExtension.unsafe_impl_5 : Lean.Environment →
  Lean.Environment →
    Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState →
      Lean.CoreM (Option Lean.MessageData)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.whiskeringRight_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : D ⥤ᵣ E} (η : F ⟶ G) (H : C ⥤ᵣ D),
  ((CategoryTheory.RightExactFunctor.whiskeringRight C D E).map η).app H =
    CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
-- Init.Data.UInt.Lemmas
System.Platform.two_pow_numBits_nonneg : 0 ≤ 2 ^ System.Platform.numBits
-- Mathlib.Algebra.Star.StarRingHom
/-- The inverse of a star ring isomorphism is a star ring isomorphism.  -/
StarRingEquiv.symm : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → (A ≃⋆+* B) → B ≃⋆+* A
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.mk.sizeOf_spec : ∀ (fromDeclName toDeclName thmName : Lean.Name),
  sizeOf { fromDeclName := fromDeclName, toDeclName := toDeclName, thmName := thmName } =
    1 + sizeOf fromDeclName + sizeOf toDeclName + sizeOf thmName
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H2π_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥(groupCohomology.cocycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) x = 0 ↔ ⇑x ∈ groupCohomology.coboundaries₂ A
-- Mathlib.Algebra.Lie.Abelian
/-- `maxTrivSubmodule` is functorial.  -/
LieModule.maxTrivHom : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [inst_6 : LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] →
                            [inst_10 : LieModule R L N] →
                              (M →ₗ⁅R,L⁆ N) →
                                ↥(LieModule.maxTrivSubmodule R L M) →ₗ⁅R,L⁆ ↥(LieModule.maxTrivSubmodule R L N)
-- Mathlib.Data.LawfulXor.Basic
LawfulXor.xor_comm : ∀ {α : Type u_1} {inst : XorOp α} {inst_1 : Zero α} [self : LawfulXor α] (a b : α), a ^^^ b = b ^^^ a