mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `a ≤ b` from an equality `a = b` coming from the core.  -/
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat : Lean.Expr →
  Lean.Expr →
    ℕ →
      Lean.Meta.Grind.Arith.Linear.LinExpr →
        Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr_mapAccumr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁} {s₂ : σ₂}
  (xs : List.Vector α n) (f₁ : β → σ₁ → σ₁ × γ) (f₂ : α → σ₂ → σ₂ × β),
  List.Vector.mapAccumr f₁ (List.Vector.mapAccumr f₂ xs s₂).2 s₁ =
    have m :=
      List.Vector.mapAccumr
        (fun x s =>
          have r₂ := f₂ x s.2;
          have r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs (s₁, s₂);
    (m.1.1, m.2)
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
/-- If `n + i = m`, this is the morphism `⦋n⦌ ⟶ ⦋m⦌` in the simplex category
which is obtained as the `i`th iteration of `δ 0`: it sends `j : Fin (n + 1)` to
`⟨j.val + i, _⟩`. This may also be described as the order embedding
`Fin.addNatOrderEmb i : Fin (n + 1) ↪o Fin (n + 1 + i)`
followed by the order isomorphism `Fin (n + 1 + i) ≃o Fin (m + 1)`.  -/
SimplexCategory.δ₀Iter : (i : ℕ) → {n m : ℕ} → autoParam (n + i = m) SimplexCategory.δ₀Iter._auto_1 → ({ len := n } ⟶ { len := m })
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in a string `s`. If
there is no match `none` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".find? Char.isWhitespace).map (·.get!) == some ' '`

* `"tea".find? (fun (c : Char) => c == 'X') == none`

* `("coffee tea water".find? "tea").map (·.get!) == some 't'`
 -/
String.find? : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        (s : String) → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → Option s.Pos
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mem_carrier : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R}, x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      m.contains k = false →
        (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isNone = true →
          (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size = (↑m).size
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The orthonormal basis of the tensor product of two orthonormal bases.  -/
OrthonormalBasis.tensorProduct : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] →
                {ι₁ : Type u_6} →
                  {ι₂ : Type u_7} →
                    [inst_5 : Fintype ι₁] →
                      [inst_6 : Fintype ι₂] →
                        OrthonormalBasis ι₁ 𝕜 E →
                          OrthonormalBasis ι₂ 𝕜 F → OrthonormalBasis (ι₁ × ι₂) 𝕜 (TensorProduct 𝕜 E F)
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x`, `1 x = 1`, and `(f ^ n) x = f x ^ n`
is a monoid if `β` is a monoid.  -/
FunLike.monoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Monoid β] → [IsOneApply F α β] → [IsMulApply F α β] → [IsPowApply ℕ F α β] → Monoid F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.keyAtIdx_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF) (h : t₁.Equiv t₂) {i : ℕ} {h' : i < t₁.size}, t₁.keyAtIdx ⋯ i h' = t₂.keyAtIdx ⋯ i ⋯
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalFactorizationRing m k hn p =
    TensorProduct (MvPolynomial (Fin n) R) R (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R))
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
/-- If `f : ℂ → ℂ` is complex-analytic without zero, then `log ‖f‖` is harmonic.
 -/
AnalyticAt.harmonicAt_log_norm : ∀ {f : ℂ → ℂ} {z : ℂ}, AnalyticAt ℂ f z → f z ≠ 0 → InnerProductSpace.HarmonicAt (fun x => Real.log ‖f x‖) z
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mk.congr_simp : ∀ {n : ℕ} (blocks blocks_1 : List ℕ) (e_blocks : blocks = blocks_1) (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i)
  (blocks_sum : blocks.sum = n),
  { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := blocks_sum } =
    { blocks := blocks_1, blocks_pos := ⋯, blocks_sum := ⋯ }
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The index or Haar covering number or ratio of `K` w.r.t. `V`, denoted `(K : V)`:
it is the smallest number of (left) translates of `V` that is necessary to cover `K`.
It is defined to be 0 if no finite number of translates cover `K`.  -/
MeasureTheory.Measure.haar.index : {G : Type u_1} → [Group G] → Set G → Set G → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_dropUntil_lt_length : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w} (h : u ∈ p.support),
  u ≠ v → (p.dropUntil u h).length < p.length
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_le : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (U : TopologicalSpace.Opens G)
  (K : TopologicalSpace.Compacts G), ↑U ⊆ ↑K → μ.innerContent U ≤ μ K
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSheafFor.extend.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows)
  (f f_1 : S.functor ⟶ P), f = f_1 → h.extend f = h.extend f_1
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.trans_domCongr_domCongr : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} {O : Type u_9} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] [inst_5 : AddMonoid O]
  (e : M ≃+ N) (f : N ≃+ O),
  (AddMonoidAlgebra.domCongr R A e).trans (AddMonoidAlgebra.domCongr R A f) = AddMonoidAlgebra.domCongr R A (e.trans f)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f)[k]? = Option.map f t[k]?
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eq_three : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R},
  f.support.card = 3 ↔
    ∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z,
          ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
            f =
              Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.mk.inj : ∀ {α : Type u} {inst : UniformSpace α} {space : Type v} {coe : α → space} {uniformStruct : UniformSpace space}
  {complete : CompleteSpace space} {separation : T0Space space} {isUniformInducing : IsUniformInducing coe}
  {dense : DenseRange coe} {space_1 : Type v} {coe_1 : α → space_1} {uniformStruct_1 : UniformSpace space_1}
  {complete_1 : CompleteSpace space_1} {separation_1 : T0Space space_1} {isUniformInducing_1 : IsUniformInducing coe_1}
  {dense_1 : DenseRange coe_1},
  { space := space, coe := coe, uniformStruct := uniformStruct, complete := complete, separation := separation,
        isUniformInducing := isUniformInducing, dense := dense } =
      { space := space_1, coe := coe_1, uniformStruct := uniformStruct_1, complete := complete_1,
        separation := separation_1, isUniformInducing := isUniformInducing_1, dense := dense_1 } →
    space = space_1 ∧ coe ≍ coe_1 ∧ uniformStruct ≍ uniformStruct_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- If `X` is a zero object, `Y ≅ X ⊞ Y` for any `Y`.  -/
CategoryTheory.Limits.isoZeroBiprod : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → CategoryTheory.Limits.IsZero X → (Y ≅ X ⊞ Y)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCompletionItem : Inhabited Lean.Lsp.CompletionItem
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.LocallyLinear.instDecidable : {α : Type u_1} → {G : SimpleGraph α} → [DecidableEq α] → [Fintype α] → [DecidableRel G.Adj] → Decidable G.LocallyLinear
-- Mathlib.Topology.UniformSpace.Cauchy
UniformSpace.firstCountableTopology : ∀ (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated], FirstCountableTopology α
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- When `R : Cᵒᵖ ⥤ RingCat`, `M : PresheafOfModules R`, and `X : C`, this is the
bijection `((free R).obj (yoneda.obj X) ⟶ M) ≃ M.obj (Opposite.op X)`.  -/
PresheafOfModules.freeYonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M : PresheafOfModules R} →
        {X : C} → ((PresheafOfModules.free R).obj (CategoryTheory.yoneda.obj X) ⟶ M) ≃ ↑(M.obj (Opposite.op X))
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Given the name of a declaration to unfold, return the `SimpEntry` (or entries) that
implement this unfolding, using either the equational theorems, or `SimpEntry.toUnfold`, or both.
 -/
Lean.Meta.mkSimpEntryOfDeclToUnfold : Lean.Name → Lean.MetaM (Array Lean.Meta.SimpEntry)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.base : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → ι → ℕ
-- Mathlib.Tactic.Simps.Basic
/-- Syntax for renaming a projection in `initialize_simps_projections`.  -/
Lean.Parser.Command.simpsRule.rename : Lean.ParserDescr
-- Mathlib.Topology.Order.Monotone
/-- **Alias** of `AntitoneOn.countable_setOfPred_two_preimages`.

---

If a function is antitone on a set in a second countable topological space, then there
are only countably many points that have several preimages.  -/
AntitoneOn.countable_setOf_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α],
  AntitoneOn f s → {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.coe_toOrderEmbedding : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f)
  (h : Function.Injective f), ⇑(LeftOrdContinuous.toOrderEmbedding f hf h) = f
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : αᵒᵈ), OrderDual.ofDual (a - b) = OrderDual.ofDual a - OrderDual.ofDual b
-- Mathlib.Topology.LocallyFinsupp
/-- For T1 spaces, the condition `supportLocallyFiniteWithinDomain'` is equivalent to saying that the
support is codiscrete within `U`.
 -/
supportDiscreteWithin_iff_locallyFiniteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [inst_2 : Zero Y] {f : X → Y},
  Function.support f ⊆ U → (f =ᶠ[Filter.codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a finite affinely independent family has dimension one less than its
cardinality.  -/
AffineIndependent.finrank_vectorSpan_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] [Nonempty ι] {p : ι → P},
  AffineIndependent k p → Module.finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_left_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) f =
      CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) g ↔
    f = g
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The `C^n` groupoid is closed under restriction.  -/
instClosedUnderRestrictionContDiffGroupoid : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  ClosedUnderRestriction (contDiffGroupoid n I)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.meas_iInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω}
  [inst : Fintype ι],
  ProbabilityTheory.Kernel.iIndep m κ μ →
    (∀ (i : ι), MeasurableSet (s i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_inter_support : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s : Set α) (f : α → M),
  (s ∩ Function.support f).indicator f = s.indicator f
-- Std.Data.TreeMap.Basic
Std.TreeMap.Equiv.mk : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeMap α β cmp},
  m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Isomorphism of cones preserves whether or not they are limiting cones.  -/
CategoryTheory.Limits.IsLimit.equivIsoLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cone F} →
            (r ≅ t) → CategoryTheory.Limits.IsLimit r ≃ CategoryTheory.Limits.IsLimit t
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instVAddMemClass : ∀ {R : Type u} {M : Type v} [inst : VAdd R M], VAddMemClass (SubAddAction R M) R M
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.IsLimit.hom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F}
  (hc : CategoryTheory.Limits.IsLimit c) {X : C} {f g : X ⟶ c.pt},
  (∀ (j : (CategoryTheory.Limits.multicospanShapeEnd J).L),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Multifork.ι c j) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Multifork.ι c j)) →
    f = g
-- Mathlib.Order.Interval.Finset.Defs
OrderDual.instLocallyFiniteOrderTop.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α],
  OrderDual.instLocallyFiniteOrderTop =
    { finsetIoi := fun a => Finset.Iio (OrderDual.ofDual a), finsetIci := fun a => Finset.Iic (OrderDual.ofDual a),
      finset_mem_Ici := ⋯, finset_mem_Ioi := ⋯ }
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- An element of `QuadraticAlgebra R a b` has norm equal to `1`
if and only if it is contained in the submonoid of unitary elements.  -/
QuadraticAlgebra.norm_eq_one_iff_mem_unitary : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {z : QuadraticAlgebra R a b},
  QuadraticAlgebra.norm z = 1 ↔ z ∈ unitary (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instInjectiveXIntObjPlusFibrantObjects : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : HomotopicalAlgebra.FibrantObject (CochainComplex.Plus C)) (n : ℤ), CategoryTheory.Injective (K.obj.obj.X n)
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_le_of_mul_inv_le : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, b < 0 → a * b⁻¹ ≤ c → c * b ≤ a
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.equivRange.congr_simp : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)),
  ContinuousLinearMap.equivRange hinj hclo = ContinuousLinearMap.equivRange hinj hclo
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.single.eq_1 : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R] (x : M),
  Convexity.StdSimplex.single x = { weights := fun₀ | x => 1, nonneg := ⋯, total := ⋯ }
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_add_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  μ.compProd (κ + η) = μ.compProd κ + μ.compProd η
-- Std.Data.TreeMap.Basic
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.TreeMap.diff : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.TreeMap α β cmp → Std.TreeMap α β cmp
-- Mathlib.Order.InitialSeg
PrincipalSeg.ofElement_top : ∀ {α : Type u_4} (r : α → α → Prop) (a : α), (PrincipalSeg.ofElement r a).top = a
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], ↑1 = 1
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.JD.eq_1 : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R],
  LieAlgebra.Orthogonal.JD l R = Matrix.fromBlocks 0 1 1 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ), e.leftOp.functor.obj X = Opposite.unop (e.functor.obj (Opposite.unop X))
-- Mathlib.Algebra.Group.TransferInstance
Equiv.mul.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β],
  e.mul = { mul := fun x y => e.invFun (e.toFun x * e.toFun y) }
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.IsWeightedHomogeneous.C_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {m : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ m → ∀ (r : R), MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.C r * φ) m
-- Mathlib.Data.ZMod.Basic
ZMod.cast_neg : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (a : ZMod n), (-a).cast = -a.cast
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_monomial_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) (i : σ) {a : R},
  a ≠ 0 → MvPolynomial.degreeOf i ((MvPolynomial.monomial s) a) = s i
-- Lean.Widget.InteractiveCode
Lean.Widget.SubexprInfo.mk.injEq : ∀ (info : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx) (subexprPos : Lean.SubExpr.Pos)
  (diffStatus? : Option Lean.Widget.DiffTag) (info_1 : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx)
  (subexprPos_1 : Lean.SubExpr.Pos) (diffStatus?_1 : Option Lean.Widget.DiffTag),
  ({ info := info, subexprPos := subexprPos, diffStatus? := diffStatus? } =
      { info := info_1, subexprPos := subexprPos_1, diffStatus? := diffStatus?_1 }) =
    (info = info_1 ∧ subexprPos = subexprPos_1 ∧ diffStatus? = diffStatus?_1)
-- Lean.Environment
/-- Resulting "async branch" environment which should be used in a new task and then to call
`PromiseCheckedResult.commitChecked` to commit results back to the main environment. If it is not
called and the `PromiseCheckedResult` object is dropped, the kernel environment will be left
unchanged.
 -/
Lean.Environment.PromiseCheckedResult.asyncEnv : Lean.Environment.PromiseCheckedResult → Lean.Environment
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {x y : α},
  CauSeq.const abs x ≤ CauSeq.const abs y ↔ x ≤ y
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.liftₐ_apply : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (I : Ideal A) [inst_5 : I.IsTwoSided] (f : A →ₐ[R₁] B)
  (hI : ∀ a ∈ I, f a = 0) (x : A ⧸ I), (Ideal.Quotient.liftₐ I f hI) x = (Ideal.Quotient.lift I (↑f) hI) x
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_div : ∀ {G : Type u_5} [inst : AddGroup G] {x y : WithZero (Multiplicative G)}, x ≠ 0 → y ≠ 0 → (x / y).log = x.log - y.log
-- Mathlib.Analysis.Complex.Basic
Complex.hasSum_iff : ∀ {α : Type u_1} {L : SummationFilter α} (f : α → ℂ) (c : ℂ),
  HasSum f c L ↔ HasSum (fun x => (f x).re) c.re L ∧ HasSum (fun x => (f x).im) c.im L
-- Mathlib.MeasureTheory.Integral.Bochner.Set
measure_le_lintegral_thickenedIndicator : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : PseudoEMetricSpace X] (μ : MeasureTheory.Measure X) {E : Set X},
  MeasurableSet E → ∀ {δ : ℝ} (δ_pos : 0 < δ), μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ
-- Init.Data.List.Count
List.countP_eq_length_filter : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.countP p l = (List.filter p l).length
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofEquivalence_Ω : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (𝒞₁ : CategoryTheory.Subobject.Classifier C) (e : C ≌ D), (𝒞₁.ofEquivalence e).Ω = e.functor.obj 𝒞₁.Ω
-- Mathlib.Algebra.Ring.Basic
inv_neg_one : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R], (-1)⁻¹ = -1
-- Mathlib.NumberTheory.FactorisationProperties
Nat.abundant_twelve : Nat.Abundant 12
-- Mathlib.GroupTheory.Index
AddSubgroup.index_comap_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) {f : G' →+ G},
  Function.Surjective ⇑f → (AddSubgroup.comap f H).index = H.index