mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.Compact
/-- A closed embedding is proper, i.e., inverse images of compact sets are contained in compacts.
Moreover, the preimage of a compact set is compact, see `IsClosedEmbedding.isCompact_preimage`.  -/
Topology.IsClosedEmbedding.tendsto_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- `c.index j` is the index of the block in the composition `c` containing `j`.  -/
Composition.index : {n : ℕ} → (c : Composition n) → Fin n → Fin c.length
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.localInsts : Lean.Elab.Command.FinalizeContext✝ → Lean.LocalInstances
-- Mathlib.ModelTheory.Satisfiability
Cardinal.empty_infinite_Theory_isComplete : FirstOrder.Language.empty.infiniteTheory.IsComplete
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getKey!` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getKey!ₘ : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → [Inhabited α] → α
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_le_neg : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {S T : Submodule R M}, -S ≤ -T ↔ S ≤ T
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.homologyπ S.leftHomologyIso.inv = S.leftHomologyπ
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongr_symm_apply : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a))
  (f : (b : β) → Z b), (h₁.piCongr h₂).symm f = fun a => (h₂ a).symm (f (h₁ a))
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A finite type torsion free module over a PID admits a basis.  -/
Module.basisOfFiniteTypeTorsionFree' : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [IsPrincipalIdealRing R] →
            [IsDomain R] → [Module.Finite R M] → [Module.IsTorsionFree R M] → (n : ℕ) × Module.Basis (Fin n) R M
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a homomorphism `f` from the quotient of a monoid by a congruence relation, `f` equals the
homomorphism on the quotient induced by `f` composed with the natural map from the monoid to
the quotient.  -/
Con.lift_apply_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} (f : c.Quotient →* P),
  c.lift (f.comp c.mk') ⋯ = f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_ofList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → (Std.DHashMap.ofList l).size = l.length
-- Aesop.Search.SearchM
Aesop.instInhabitedNormSimpContext.default : Aesop.NormSimpContext
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.decompLinearIsometryEquiv_symm_apply : ∀ (𝕜 : Type u_1) (R : Type u_2) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : Ring R] [inst_6 : Module R W] [inst_7 : ContinuousConstSMul R W]
  [inst_8 : SMulCommClass 𝕜 R W] (p : W × (V →L[𝕜] W)) (x : V),
  ((ContinuousAffineMap.decompLinearIsometryEquiv 𝕜 R V W).symm p) x = p.2 x + p.1
-- Mathlib.GroupTheory.CoprodI
/-- A reduced word does not contain `1`  -/
Monoid.CoprodI.Word.ne_one : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (self : Monoid.CoprodI.Word M),
  ∀ l ∈ self.toList, l.snd ≠ 1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_iUnion : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {γ : Sort u_3} (s : γ → Set A),
  ProjectiveSpectrum.zeroLocus 𝒜 (⋃ i, s i) = ⋂ i, ProjectiveSpectrum.zeroLocus 𝒜 (s i)
-- Init.Data.BitVec.Lemmas
BitVec.neg_ne_intMin_inj : ∀ {w : ℕ} {x : BitVec w}, -x ≠ BitVec.intMin w ↔ x ≠ BitVec.intMin w
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.mono_lift_of_mono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.CartesianMonoidalCategory.lift f g)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {l : List ((a : α) × β a)}, (↑↑(m.insertMany l)).size ≤ (↑m).size + l.length
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)),
  G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- A category `HasPullbacks` if it has all limits of shape `WalkingCospan`, i.e. if it has a
pullback for every pair of morphisms with the same codomain.  -/
CategoryTheory.Limits.HasPullbacks : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Topology.Filter
Filter.mem_closure : ∀ {α : Type u_2} {s : Set (Filter α)} {l : Filter α}, l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'
-- Mathlib.Analysis.Calculus.DiffContOnCl
IsClosed.diffContOnCl_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  IsClosed s → (DiffContOnCl 𝕜 f s ↔ DifferentiableOn 𝕜 f s)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic' n K` splits.  -/
Polynomial.cyclotomic'_splits : ∀ {K : Type u_1} [inst : Field K] (n : ℕ), (Polynomial.cyclotomic' n K).Splits
-- Mathlib.Data.FP.Basic
FP.ValidFinite : [C : FP.FloatCfg] → ℤ → ℕ → Prop
-- Lean.Meta.Basic
/-- Takes an array `xs` of free variables or metavariables and a term `e` that may contain those variables, and abstracts and binds them as universal quantifiers.

- if `usedOnly = true` then only variables that the expression body depends on will appear.
- if `usedLetOnly = true` same as `usedOnly` except for let-bound variables. (That is, local constants which have been assigned a value.)
- if `generalizeNondepLet = true` then nondependent `ldecl`s become foralls too.
  -/
Lean.Meta.mkForallFVars : Array Lean.Expr →
  Lean.Expr →
    optParam Bool false →
      optParam Bool true → optParam Bool true → optParam Lean.BinderInfo Lean.BinderInfo.implicit → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.monMonoidalStruct_tensorHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.AddMon C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Mathlib.RingTheory.Adjoin.Singleton
Algebra.RingHom.adjoinAlgebraMap_surjective : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C]
  [inst_6 : IsScalarTower A B C] (b : B), Function.Surjective ⇑(Algebra.RingHom.adjoinAlgebraMap b)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_iff_val_eq_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
-- Mathlib.Topology.Category.Compactum
/-- The inclusion of `X` into `Ultrafilter X`.  -/
Compactum.incl : (X : Compactum) → X.A → Ultrafilter X.A
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inr.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], OrderAddMonoidHom.inr α β = { toAddMonoidHom := AddMonoidHom.inr α β, monotone' := ⋯ }
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.ConcreteCategory.forget₂_comp_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {D : Type u_3} [inst_3 : CategoryTheory.Category.{v_2, u_3} D]
  {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)}
  [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : CategoryTheory.HasForget₂ C D] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (x : CategoryTheory.ToType ((CategoryTheory.forget₂ C D).obj X)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C D).map (CategoryTheory.CategoryStruct.comp f g))) x =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C D).map g))
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C D).map f)) x)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.compContinuousLinearMapₗ_apply : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R M'] [inst_6 : TopologicalSpace M'] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : TopologicalSpace N] [inst_10 : ContinuousAdd N] [inst_11 : ContinuousConstSMul R N] (f : M →L[R] M')
  (g : M' [⋀^ι]→L[R] N), (ContinuousAlternatingMap.compContinuousLinearMapₗ f) g = g.compContinuousLinearMap f
-- Mathlib.Order.Heyting.Basic
codisjoint_hnot_hnot_right_iff : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, Codisjoint a (￢￢b) ↔ Codisjoint a b
-- Mathlib.Order.Grade
/-- An `𝕆`-graded order is an order `α` equipped with a strictly monotone function
`grade 𝕆 : α → 𝕆` which preserves order covering (`CovBy`).  -/
GradeOrder : (𝕆 : Type u_5) → (α : Type u_6) → [Preorder 𝕆] → [Preorder α] → Type (max u_5 u_6)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_comp : ∀ {M N T : MonCat} (f : M ⟶ N) (g : N ⟶ T),
  MonCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (MonCat.Hom.hom g).comp (MonCat.Hom.hom f)
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.pow_relIndex_mem : ∀ {G : Type u_6} [inst : Group G] (H : Subgroup G) [H.Normal] {K : Subgroup G} {g : G}, g ∈ K → g ^ H.relIndex K ∈ H
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonModuleHierarchyOptions.toJson : Lean.Lsp.ModuleHierarchyOptions → Lean.Json
-- Mathlib.Logic.Function.Basic
Function.Involutive.comp_self : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → f ∘ f = id
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_zero_of_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E} (y : E), ‖x‖ = 0 → inner 𝕜 x y = 0
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.universallyInjective_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.UniversallyInjective
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X},
  IsNoetherianRing ↑(X.presheaf.stalk x)
-- Mathlib.Tactic.GRewrite.Core
/-- The core of the `grw` implementation. Rewrite in the expression `e` which occurs under the
relation `relName`/`rel?`, using the `GRewriteLemma` stored in `GRewriteM`.
If `e` itself cannot be rewritten, descend into subexpressions of `e` using `@[gcongr]` lemmas.

`rel?` should be an expression with head symbol `relName`,
unless the relation is `→`: `relName` is `_Implies` and `rel?` is `none`.

Returns the new expression and a proof that it is related to `e`, if a rewrite was found.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.grewriteCore : Lean.Name →
  Option Lean.Expr →
    Lean.Expr →
      Bool → Mathlib.Tactic.GRewrite.Config → Mathlib.Tactic.GRewrite.GRewriteM✝ (Option (Lean.Expr × Lean.Expr))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- If `P` is local at the source, local at the target and is stable under post-composition with
open immersions, then `P` can be checked locally around points.  -/
AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  [P.RespectsRight AlgebraicGeometry.IsOpenImmersion],
  P f ↔
    ∀ (x : ↥X),
      ∃ U V,
        ∃ (_ : x ∈ V.carrier) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          P (AlgebraicGeometry.Scheme.Hom.resLE f U V e)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.productiveRel_of_snd : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Productive α₁ m] [inst_4 : Std.Iterators.Productive α₂ m]
  {it₂ it₂' : Std.IterM m β},
  it₂'.finitelyManySkips.Rel it₂.finitelyManySkips →
    Std.Iterators.Types.Append.ProductiveRel α₁ α₂ m β (Std.IterM.Intermediate.appendSnd α₁ it₂')
      (Std.IterM.Intermediate.appendSnd α₁ it₂)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f f_1 : β a → β a),
  f = f_1 →
    ∀ (a_1 a_2 : Std.DHashMap.Internal.AssocList α β),
      a_1 = a_2 → Std.DHashMap.Internal.AssocList.modify a f a_1 = Std.DHashMap.Internal.AssocList.modify a f_1 a_2
-- Lean.ReservedNameAction
/-- Similar to `resolveGlobalConstCore`, but also executes reserved name actions.
 -/
Lean.realizeGlobalConstCore : Lean.Name → Lean.CoreM (List Lean.Name)
-- Mathlib.Tactic.ReduceModChar
/-- Evaluates `e` to an integer using `norm_num` and reduces the result modulo `n`.  -/
Tactic.ReduceModChar.normBareNumeral : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n n' : Q(ℕ)) →
      Q(Mathlib.Meta.NormNum.IsNat «$n» «$n'») →
        (e : Q(«$α»)) → (x : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Topology.Category.TopPair
/-- The projection functor to the first component is left adjoint to the diagonal functor.  -/
TopPair.proj₁AdjDiag : TopPair.proj₁ ⊣ TopPair.diag
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.isEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → Topology.IsEmbedding e
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
AntitoneOn.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, AntitoneOn f s → MonotoneOn (fun x => (f x)⁻¹) s
-- Mathlib.RingTheory.LocalRing.Etale
/-- For finite étale extensions of local rings,
`finrank R S = finrank (ResidueField R) (ResidueField S)`.  -/
IsLocalRing.finrank_eq_finrank_residueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing S] [inst_4 : IsLocalRing R] [inst_5 : Module.Finite R S] [inst_6 : FaithfulSMul R S]
  [Algebra.Etale R S], Module.finrank R S = Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (m₁ m₂ m₃ : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X)
      ((CategoryTheory.shiftFunctor C m₁).map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C m₃).map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X))
        ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).obj X)))
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Flip the order of arguments of a continuous bilinear map.
For a version bundled as `LinearIsometryEquiv`, see
`ContinuousLinearMap.flipL`.  -/
ContinuousLinearMap.flip : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      {E : Type u_4} →
        {F : Type u_6} →
          {G : Type u_8} →
            [inst : SeminormedAddCommGroup E] →
              [inst_1 : SeminormedAddCommGroup F] →
                [inst_2 : SeminormedAddCommGroup G] →
                  [inst_3 : NontriviallyNormedField 𝕜] →
                    [inst_4 : NontriviallyNormedField 𝕜₂] →
                      [inst_5 : NontriviallyNormedField 𝕜₃] →
                        [inst_6 : NormedSpace 𝕜 E] →
                          [inst_7 : NormedSpace 𝕜₂ F] →
                            [inst_8 : NormedSpace 𝕜₃ G] →
                              {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                                {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                  [RingHomIsometric σ₂₃] →
                                    [RingHomIsometric σ₁₃] → (E →SL[σ₁₃] F →SL[σ₂₃] G) → F →SL[σ₂₃] E →SL[σ₁₃] G
-- Mathlib.Logic.Equiv.Prod
/-- Product of two equivalences. If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then `α₁ × β₁ ≃ α₂ × β₂`. This is
`Prod.map` as an equivalence.  -/
Equiv.prodCongr : {α₁ : Type u_9} → {α₂ : Type u_10} → {β₁ : Type u_11} → {β₂ : Type u_12} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
ULift.dist_eq : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β), dist x y = dist x.down y.down
-- Lean.Compiler.LCNF.Basic
/-- An erased value that is irrelevant for computation.
 -/
Lean.Compiler.LCNF.LetValue.erased : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.op_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), h.op.ι = h.π.op
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The sigma type of all `data.I₁ i₁ i₂` for `⟨i₁, i₂⟩ : data.I₀ × data.I₀`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.I₁' : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} → {X : C} → F.PreOneHypercoverDenseData X → Type w
-- Mathlib.Topology.Inseparable
IsOpen.not_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, IsOpen s → x ∈ s → y ∉ s → ¬Inseparable x y
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app._auto_1),
  (CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso C n).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ ∩ t₂).getKeyD k fallback = if k ∈ t₂ then t₁.getKeyD k fallback else fallback
-- Init.Data.Vector.Lemmas
Vector.foldr_congr : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs ys : Vector α n},
  xs = ys → ∀ {f g : α → β → β}, f = g → ∀ {a b : β}, a = b → Vector.foldr f a xs = Vector.foldr g b ys
-- Aesop.Forward.Match.Types
Aesop.CompleteMatch.clusterMatches : Aesop.CompleteMatch → Array Aesop.Match
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instBornology : {A : Type u_3} → {E : Type u_4} → [Bornology E] → Bornology (WithCStarModule A E)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_nonneg : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}, 0 ≤ T_gen✝ p F a
-- Mathlib.Data.ENNReal.Holder
ENNReal.holderConjugate_iff : ∀ {p q : ENNReal}, p.HolderConjugate q ↔ p⁻¹ + q⁻¹ = 1
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.filterRevM.eq_1 : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (p : α → m Bool) (as : Array α) (start stop : ℕ),
  Array.filterRevM p as start stop =
    Array.reverse <$>
      Array.foldrM
        (fun a acc => do
          let __do_lift ← p a
          if __do_lift = true then pure (acc.push a) else pure acc)
        #[] as start stop
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.inhabitedGradedObject : (β : Type w) → (C : Type u) → [Inhabited C] → Inhabited (CategoryTheory.GradedObject β C)
-- Mathlib.Topology.Algebra.Module.Determinant
ContinuousLinearMap.det_pi : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : TopologicalSpace M] [inst_4 : Module R M] [Module.Free R M] [Module.Finite R M] (f : ι → M →L[R] M),
  (ContinuousLinearMap.pi fun i => f i ∘SL ContinuousLinearMap.proj i).det = ∏ i, (f i).det
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P P' Q Q' : Fin 3 → R},
  P ≈ P' → Q ≈ Q' → W'.add P Q ≈ W'.add P' Q'
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.trailingParsers : Lean.Parser.PrattParsingTables → List (Lean.Parser.Parser × ℕ)
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderMonoidHom_strictMono : ∀ {G : Type u_3} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G]
  [inst_3 : LocallyFiniteOrder G], StrictMono ⇑(LocallyFiniteOrder.orderMonoidHom G)
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instMulAction : {M : Type u_1} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction Mᵒᵈ α
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.sSup_def : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (s : Set (MeasureTheory.Filtration ι m))
  (i : ι), ↑(sSup s) i = sSup ((fun f => ↑f i) '' s)
-- Init.Data.List.FinRange
List.mem_finRange : ∀ {n : ℕ} (x : Fin n), x ∈ List.finRange n
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.endsWith_prop_eq_getLast? : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice},
  s.endsWith P = Option.any (fun x => decide (P x)) s.copy.toList.getLast?