mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.comp_δ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.comp_δ._auto_1) {Z : C}
      (h_1 : (DerivedCategory.homologyFunctor C n₁).obj T.obj₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n₀).map T.mor₂)
          (CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ T n₀ n₁ h) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Data.Multiset.Find
Multiset.find?_cons : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α) (s : Multiset α)
  (hp : {x | x ∈ a ::ₘ s ∧ p x}.Subsingleton),
  Multiset.find? p (a ::ₘ s) hp = if h : p a then some a else Multiset.find? p s ⋯
-- Mathlib.Analysis.Quaternion
Quaternion.re_coeComplex : ∀ (z : ℂ), (↑z).re = z.re
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseWeekdayNumberText : (Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.hasLaw : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreBrownianReal._auto_1},
  ProbabilityTheory.IsPreBrownianReal X P →
    ∀ (I : Finset NNReal),
      ProbabilityTheory.HasLaw (fun ω => I.restrict fun x => X x ω) (ProbabilityTheory.BrownianReal.projectiveFamily I)
        P
-- Lean.Parser.Basic
Lean.Parser.instBEqLeadingIdentBehavior.beq : Lean.Parser.LeadingIdentBehavior → Lean.Parser.LeadingIdentBehavior → Bool
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.instQuiver : Quiver CategoryTheory.Cat
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.link.congr_simp : ∀ (self : Batteries.UnionFind) (x x_1 : Fin self.size),
  x = x_1 →
    ∀ (y y_1 : Fin self.size) (e_y : y = y_1) (yroot : self.parent ↑y = ↑y), self.link x y yroot = self.link x_1 y_1 ⋯
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The product is homeomorphic to the product of the underlying spaces,
equipped with the product topology.
 -/
TopCat.piIsoPi : {ι : Type v} → (α : ι → TopCat) → ∏ᶜ α ≅ TopCat.of ((i : ι) → ↑(α i))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toArray_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).toArray = Array.filter (fun p => f p.fst p.snd) t.toArray
-- Mathlib.Order.Sublattice
Sublattice.inclusion_apply : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α} (h : L ≤ M) (a : ↥L),
  (Sublattice.inclusion h) a = Set.inclusion h a
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves multiplication  -/
MulHom.map_mul' : ∀ {M : Type u_10} {N : Type u_11} [inst : Mul M] [inst_1 : Mul N] (self : M →ₙ* N) (x y : M),
  self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the reverse direction of `OpenPartialHomeomorph.IsImage.iff_preimage_eq`. -/
OpenPartialHomeomorph.IsImage.of_preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.source ∩ ↑e ⁻¹' t = e.source ∩ s → e.IsImage s t
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_singleton : ∀ {M : Type u_3} [inst : AddCommMonoid M] (a : M), {a}.sum = a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  x = Std.DTreeMap.Internal.Impl.leaf →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
      | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
        h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) ≍
      h_1 ()
-- Init.Core
/-- `Task α` is a primitive for asynchronous computation.
It represents a computation that will resolve to a value of type `α`,
possibly being computed on another thread. This is similar to `Future` in Scala,
`Promise` in Javascript, and `JoinHandle` in Rust.

The tasks have an overridden representation in the runtime.
 -/
Task : Type u → Type u
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [inst_10 : RingHomSurjective τ₁₂]
  [inst_11 : RingHomSurjective τ₂₃] [inst_12 : RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃),
  (g ∘ₛₗ f).range = Submodule.map g f.range
-- Mathlib.Data.Set.Sups
Set.sups_subset_iff : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t u : Set α}, s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for `ComposableArrows C 2`.  -/
CategoryTheory.ComposableArrows.mk₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X₀ X₁ X₂ : C} → (X₀ ⟶ X₁) → (X₁ ⟶ X₂) → CategoryTheory.ComposableArrows C 2
-- Lean.Widget.InteractiveGoal
/-- The target type.  -/
Lean.Widget.InteractiveGoalCore.type : Lean.Widget.InteractiveGoalCore → Lean.Widget.CodeWithInfos
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Adjunction.mapAddMon_counit : ∀ {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 D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [inst_6 : a.IsMonoidal],
  a.mapAddMon.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddMonCompIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddMonNatTrans a.counit)
        CategoryTheory.Functor.mapAddMonIdIso.hom)
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.B₁_sa : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → star B₁ = B₁
-- Std.Time.Duration
Std.Time.Duration.instHAddPlainTime : HAdd Std.Time.PlainTime Std.Time.Duration Std.Time.PlainTime
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.extend_eq_extend : ∀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent ENNReal C),
  ⇑(MeasureTheory.AddContent.extend hC m) = MeasureTheory.extend fun x x_1 => m x
-- Mathlib.Algebra.GCDMonoid.PUnit
PUnit.gcd_eq : ∀ {x y : PUnit.{u_1 + 1}}, gcd x y = PUnit.unit
-- Mathlib.Algebra.Group.End
/-- If `e` is also a permutation, we can write `permCongr`
completely in terms of the group structure.  -/
Equiv.permCongr_eq_mul : ∀ {α : Type u_4} (e p : Equiv.Perm α), (Equiv.permCongr e) p = e * p * e⁻¹
-- Mathlib.Data.Multiset.Interval
Multiset.instLocallyFiniteOrder : {α : Type u_1} → [DecidableEq α] → LocallyFiniteOrder (Multiset α)
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_add : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ₁ φ₂ : ↥p →ₗ[R] F}
  {ψ₁ ψ₂ : ↥q →ₗ[R] F},
  LinearMap.ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = LinearMap.ofIsCompl h φ₁ ψ₁ + LinearMap.ofIsCompl h φ₂ ψ₂
-- Mathlib.Topology.Homotopy.Basic
/-- Currying a homotopy to a continuous function from `I` to `C(X, Y)`.
 -/
ContinuousMap.Homotopy.curry : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → f₀.Homotopy f₁ → C(↑unitInterval, C(X, Y))
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.Pushforward.id_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X),
  (TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X)).obj ℱ = ℱ
-- Mathlib.Algebra.Order.Monoid.TypeTags
Additive.isOrderedAddMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α], IsOrderedAddMonoid (Additive α)
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.getFixedParamsInfo : Array Lean.Elab.PreDefinition → Lean.MetaM Lean.Elab.FixedParams.Info
-- Init.Data.List.Erase
List.eraseP_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, ¬p a = true → List.eraseP p (List.replicate n a) = List.replicate n a
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.one_def : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M), 1 = ⟨1, ⋯⟩
-- Mathlib.Topology.LocallyFinite
locallyFinite_option : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : Option ι → Set X},
  LocallyFinite f ↔ LocallyFinite (f ∘ some)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → M),
  Convexity.iConvexComb s f = Convexity.sConvexComb (Convexity.StdSimplex.map f s)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.associator_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (P Q R : C),
  (CategoryTheory.Limits.prod.associator P Q R).hom =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)
        CategoryTheory.Limits.prod.snd)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_diagonal : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (v : n → 𝕜),
  ‖Matrix.diagonal v‖ = ‖v‖
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
PowerBasis.equivAdjoinSimple_aeval : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L)
  (f : Polynomial K),
  pb.equivAdjoinSimple ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f) =
    (Polynomial.aeval pb.gen) f
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.cases.sizeOf_spec : ∀ (declName : Lean.Name) (eager : Bool),
  sizeOf (Lean.Meta.Grind.Entry.cases declName eager) = 1 + sizeOf declName + sizeOf eager
-- Mathlib.Algebra.Group.Commute.Basic
Commute.zpow_zpow : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → ∀ (m n : ℤ), Commute (a ^ m) (b ^ n)
-- Mathlib.Topology.Algebra.Module.Complement
/-- The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`.  -/
Submodule.projectionL_eq_self_iff : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : M), (p.projectionL q h) x = x ↔ x ∈ p
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.hasStrictDerivAt_exp : ∀ (x : ℝ), HasStrictDerivAt Real.exp (Real.exp x) x
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.postponedSafeRule.sizeOf_spec : ∀ (r : Aesop.PostponedSafeRule), sizeOf (Aesop.UnsafeQueueEntry.postponedSafeRule r) = 1 + sizeOf r
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.dep_iff_superset_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {X : Set α},
  autoParam (X ⊆ M.E) Matroid.dep_iff_superset_isCircuit._auto_1 → (M.Dep X ↔ ∃ C ⊆ X, M.IsCircuit C)
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_sup : ∀ {R : Type u_1} {N : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] (M₁ M₂ : Submodule R N)
  [IsNoetherian R ↥M₁] [IsNoetherian R ↥M₂], IsNoetherian R ↥(M₁ ⊔ M₂)
-- Mathlib.Topology.Algebra.Group.Defs
Continuous.sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G}, Continuous f → Continuous g → Continuous (f - g)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.cofanInr_of_binaryCoproductDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y]
  {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inr
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_rcc : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
        List.filter (fun e => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLE = true))
          t.toList
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} (t t_1 : Std.TreeSet α cmp) (e_t : t = t_1) (h : t.isEmpty = false),
  t.max h = t_1.max ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₆_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.b₆ = W.a₃ ^ 2 + W.a₆
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- If `f` is differentiable at `x`, and `L` is `σ`-semilinear, then `L ∘ f ∘ σ⁻¹` is
differentiable at `σ x`.  -/
DifferentiableAt.comp_semilinear₁ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {σ : 𝕜 →+* 𝕜} (σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ']
  {F' : Type u_1} [inst_5 : NormedAddCommGroup F'] [inst_6 : NormedSpace 𝕜 F'] (L : F →SL[σ] F'),
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (⇑L ∘ f ∘ ⇑σ') (σ x)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.isAddCommutative : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α], IsAddCommutative α
-- Mathlib.Order.Filter.CardinalInter
/-- Every filter is a CardinalInterFilter with c = ℵ₀  -/
Filter.cardinalInterFilter_aleph0 : ∀ {α : Type u} (l : Filter α), CardinalInterFilter l Cardinal.aleph0
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
/-- Measure `μ` has value zero on singletons.  -/
MeasureTheory.NullSingletonClass : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.coe_basisMonomials : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R],
  ⇑(MvPolynomial.basisMonomials σ R) = fun s => (MvPolynomial.monomial s) 1
-- Init.Data.String.Defs
String.Pos.Raw.byteIdx_sub_slice : ∀ {p : String.Pos.Raw} {s : String.Slice}, (p - s).byteIdx = p.byteIdx - s.utf8ByteSize
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_pos : ∀ {p : ℝ}, 0 < ENNReal.ofReal p ↔ 0 < p
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.rTensor_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F),
  LinearIsometryEquiv.rTensor G f = TensorProduct.congrIsometry f (LinearIsometryEquiv.refl 𝕜 G)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.mk.inj : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {hom : u.right ⟶ v.left}
  {comm :
    autoParam
      (CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g = CategoryTheory.CategoryStruct.comp u.hom hom)
      CategoryTheory.Arrow.LeftHomotopy.comm._autoParam}
  {hom_1 : u.right ⟶ v.left}
  {comm_1 :
    autoParam
      (CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g =
        CategoryTheory.CategoryStruct.comp u.hom hom_1)
      CategoryTheory.Arrow.LeftHomotopy.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Lean.Parser.Types
Lean.Parser.ParserState.popSyntax : Lean.Parser.ParserState → Lean.Parser.ParserState
-- Lean.Message
Lean.MessageData.ofFormatWithInfos.inj : ∀ {a a_1 : Lean.FormatWithInfos},
  Lean.MessageData.ofFormatWithInfos a = Lean.MessageData.ofFormatWithInfos a_1 → a = a_1
-- Mathlib.Order.Lattice
/-- The infimum is a lower bound on the first argument  -/
Lattice.inf_le_left : ∀ {α : Type u} [self : Lattice α] (a b : α), Lattice.inf a b ≤ a
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.tsum_eqOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [T2Space α], HasSumUniformlyOn f g s → Set.EqOn (fun x => ∑' (b : ι), f b x) g s
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.Abelian.tfae_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (Z : C),
  [CategoryTheory.Epi f, CategoryTheory.Limits.cokernel.π f = 0,
      { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.Exact].TFAE
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_eq_nil_of_not_periodic_pt : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∉ Function.periodicPts f → Function.periodicOrbit f x = Cycle.nil
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_le_of_inv_le₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → a⁻¹ ≤ b → b⁻¹ ≤ a
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
/-- The extension of a nonzero integral ideal along an injective extension of domains.  -/
ClassGroup.extendedIdeal : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [Module.IsTorsionFree A B] →
            [IsDomain A] → [IsDomain B] → ↥(nonZeroDivisors (Ideal A)) → ↥(nonZeroDivisors (Ideal B))
-- Mathlib.Topology.Filter
ContinuousWithinAt.nhds : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}
  {s : Set X}, ContinuousWithinAt f s x → ContinuousWithinAt (nhds ∘ f) s x
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.equivMapOfInjective.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (f : G →+ N)
  (hf : Function.Injective ⇑f), H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_self : ∀ {a : ℤ}, a ≠ 0 → a / a = 1
-- Mathlib.CategoryTheory.CommSq
/-- Now we consider a square:
```
  A ---f---> X
  |          |
  i          p
  |          |
  v          v
  B ---g---> Y
```

The datum of a lift in a commutative square, i.e. an up-right-diagonal
morphism which makes both triangles commute.  -/
CategoryTheory.CommSq.LiftStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} → {f : A ⟶ X} → {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → CategoryTheory.CommSq f i p g → Type v_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.foldr_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {δ : Type w}
  [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : (a : α) → β a → δ → δ} {init : δ},
          Std.DTreeMap.Internal.Impl.foldr f init t₁ = Std.DTreeMap.Internal.Impl.foldr f init t₂
-- Mathlib.Data.ENNReal.Basic
ENNReal.some_eq_coe : ∀ (a : NNReal), some a = ↑a
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (iter : Φ.Iteration j)
  {k l : J} (h : k ≤ l) (h' : l ≤ j), iter.mapObj iter h ⋯ h' ⋯ = iter.F.map (CategoryTheory.homOfLE h)
-- Mathlib.Order.BooleanAlgebra.Basic
compl_le_self : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], xᶜ ≤ x ↔ x = ⊤
-- Mathlib.CategoryTheory.Sites.Abelian
CategoryTheory.presheafToSheaf_additive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 : CategoryTheory.Abelian D] {J : CategoryTheory.GrothendieckTopology C}
  [inst_3 : CategoryTheory.HasSheafify J D], (CategoryTheory.presheafToSheaf J D).Additive
-- Mathlib.NumberTheory.Chebyshev
/-- Explicit integral bound, we expose a BigO version below since the constants and lower order term
aren't very convenient.  -/
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.integral_one_div_log_sq_le_explicit : ∀ {x : ℝ}, 4 ≤ x → ∫ (t : ℝ) in 2..x, 1 / Real.log t ^ 2 ≤ 4 * x / Real.log x ^ 2 + √x / Real.log 2 ^ 2
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- For a finite set `S` of prime ideals, the partial sum
$\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}$ is bounded above by the number of
elements of `S`.  -/
NumberField.Set.primeIdealZetaSum_le_card_of_finite : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))},
  S.Finite → ∀ {s : ℝ}, 0 ≤ s → NumberField.Set.primeIdealZetaSum S s ≤ ↑S.ncard
-- Mathlib.Order.Category.BddLat
/-- `OrderDual` as a functor.  -/
BddLat.dual : CategoryTheory.Functor BddLat BddLat
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).contains k = (f (t.get? k)).isSome
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_map : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : MeasurableSpace β]
  (g : MeasureTheory.SimpleFunc β ENNReal) {f : α → β} (hf : Measurable f),
  g.lintegral (MeasureTheory.Measure.map f μ) = (g.comp f hf).lintegral μ
-- Lean.Meta.Match.MatcherInfo
/-- Actual fields (not including discr eqns)  -/
Lean.Meta.Match.AltParamInfo.numFields : Lean.Meta.Match.AltParamInfo → ℕ