mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.closed_point_mem_iff : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {U : TopologicalSpace.Opens (PrimeSpectrum R)},
  IsLocalRing.closedPoint R ∈ U ↔ U = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.nonDegenerateEquivOfIso_apply_coe : ∀ {X Y : SSet} (e : X ≅ Y) {n : ℕ} (x : ↑(X.nonDegenerate n)),
  ↑((SSet.nonDegenerateEquivOfIso e) x) =
    (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := n }))) ↑x
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.star_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (X_1 : C),
  ((CategoryTheory.Over.star X).obj X_1).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ X_1)))
      CategoryTheory.Limits.prod.fst
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_addEquiv_comp : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_8} [inst_2 : AddZeroClass P]
  (f : G →+ N) (iso : N ≃+ P), ((↑iso).comp f).ker = f.ker
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mk.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} (verts verts_1 : Set V) (e_verts : verts = verts_1) (Adj Adj_1 : V → V → Prop)
  (e_Adj : Adj = Adj_1) (adj_sub : ∀ {v w : V}, Adj v w → G.Adj v w) (edge_vert : ∀ {v w : V}, Adj v w → v ∈ verts)
  (symm : Std.Symm Adj),
  { verts := verts, Adj := Adj, adj_sub := adj_sub, edge_vert := edge_vert, symm := symm } =
    { verts := verts_1, Adj := Adj_1, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- The edge set of `G.deleteIncidenceSet x` is the edge set of `G` set difference the incidence
set of the vertex `x`.  -/
SimpleGraph.edgeSet_deleteIncidenceSet : ∀ {V : Type u_1} (G : SimpleGraph V) (x : V), (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x
-- Mathlib.Algebra.Group.Submonoid.Finsupp
Submonoid.mem_closure_range_iff_of_fintype : ∀ {M : Type u_1} [inst : CommMonoid M] {ι : Type u_2} {f : ι → M} {x : M} [inst_1 : Fintype ι],
  x ∈ Submonoid.closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.equitabilise.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m m_1 : ℕ} (e_m : m = m_1) {a a_1 : ℕ} (e_a : a = a_1)
  {b b_1 : ℕ} (e_b : b = b_1) {P P_1 : Finpartition s},
  P = P_1 → ∀ (h : a * m + b * (m + 1) = s.card), Finpartition.equitabilise h = Finpartition.equitabilise ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  [inst_1 : Inhabited (β a)], (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a `CommMonoid` is a `CommMonoid`.  -/
SubmonoidClass.toCommMonoid : {M : Type u_5} →
  [inst : CommMonoid M] → {A : Type u_4} → [inst_1 : SetLike A M] → [SubmonoidClass A M] → (S : A) → CommMonoid ↥S
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.App.mk.sizeOf_spec : ∀ (coe fn arg : Lean.Expr), sizeOf { coe := coe, fn := fn, arg := arg } = 1 + sizeOf coe + sizeOf fn + sizeOf arg
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.iInf_ker_coroot'_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ⨅ i, LinearMap.ker (P.coroot' i) = (Submodule.span R (Set.range P.coroot')).dualCoannihilator
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.eq_gcd_cert.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (v : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k v p))
  (h_2 : (g : ℤ) → motive (Lean.Grind.CommRing.Poly.num g)),
  (match Lean.Grind.CommRing.Poly.add k v p with
    | Lean.Grind.CommRing.Poly.add k v p => h_1 k v p
    | Lean.Grind.CommRing.Poly.num g => h_2 g) =
    h_1 k v p
-- Mathlib.Topology.LocallyClosed
Topology.IsOpenEmbedding.coborder_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → ∀ (s : Set Y), coborder (f ⁻¹' s) = f ⁻¹' coborder s
-- Mathlib.RepresentationTheory.Maschke
LinearMap.equivariantProjection_condition : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (i : V →ₗ[MonoidAlgebra k G] W)
  [inst_10 : Fintype G],
  IsUnit ↑(Nat.card G) → (∀ (v : V), π (i v) = v) → ∀ (v : V), (LinearMap.equivariantProjection G π) (i v) = v
-- Aesop.Forward.Match
Aesop.ForwardRuleMatch.instToMessageData : Lean.ToMessageData Aesop.ForwardRuleMatch
-- Init.Data.List.MinMaxOn
List.le_apply_maxOn_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []) {b : β}, b ≤ f (List.maxOn f xs h) ↔ ∃ x ∈ xs, b ≤ f x
-- Init.Data.BitVec.Lemmas
Fin.rev.eq_1 : ∀ {n : ℕ} (i : Fin n), i.rev = ⟨n - (↑i + 1), ⋯⟩
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Restrict the domain of a quadratic map  -/
QuadraticMap.restrict : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → QuadraticMap R M N → (V : Submodule R M) → QuadraticMap R (↥V) N
-- Mathlib.Algebra.Ring.Centralizer
Set.neg_mem_centralizer : ∀ {M : Type u_1} {S : Set M} {a : M} [inst : Mul M] [inst_1 : HasDistribNeg M], a ∈ S.centralizer → -a ∈ S.centralizer
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Comp.mk : Mathlib.Ineq → Mathlib.Tactic.Linarith.Linexp → Mathlib.Tactic.Linarith.Comp
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.support_cycleOf_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x : α),
  (f.cycleOf x).support ⊆ f.support
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ι_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {d : CategoryTheory.Limits.Cocone G} (hd : CategoryTheory.Limits.IsColimit d)
  (c : CategoryTheory.Limits.Cocone F) (α : G ⟶ F) (j : J),
  CategoryTheory.CategoryStruct.comp (d.ι.app j) (hd.map c α) = CategoryTheory.CategoryStruct.comp (α.app j) (c.ι.app j)
-- Mathlib.Order.Category.BddDistLat
/-- The type of morphisms in `BddDistLat R`.  -/
BddDistLat.Hom : BddDistLat → BddDistLat → Type u
-- Mathlib.Topology.Homotopy.Path
/-- Suppose `p₀` and `q₀` are paths from `x₀` to `x₁`, `p₁` and `q₁` are paths from `x₁` to `x₂`.
Furthermore, suppose `F : Homotopy p₀ q₀` and `G : Homotopy p₁ q₁`. Then we can define a homotopy
from `p₀.trans p₁` to `q₀.trans q₁`.
 -/
Path.Homotopy.hcomp : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ x₂ : X} →
      {p₀ q₀ : Path x₀ x₁} →
        {p₁ q₁ : Path x₁ x₂} → p₀.Homotopy q₀ → p₁.Homotopy q₁ → (p₀.trans p₁).Homotopy (q₀.trans q₁)
-- Init.Data.Int.Gcd
Int.gcd_add_mul_left_right : ∀ (m n k : ℤ), m.gcd (n + m * k) = m.gcd n
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_top : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α] [inst_3 : OrderTop β]
  {l : α → β} {u : β → α}, GaloisConnection l u → u ⊤ = ⊤
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffAt_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E} {y : H}, ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => (f x).ofLp i) y
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.congr_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {α β : F ⟶ G}, α = β → ∀ (X : C), α.app X = β.app X
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.isSchemeTheoreticallyDominant_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsSchemeTheoreticallyDominant f ↔ AlgebraicGeometry.Scheme.Hom.ker f = ⊥
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : F} (c : F), HasFDerivAt (fun x => x - c) (ContinuousLinearMap.id 𝕜 F) x
-- Mathlib.Topology.Instances.Int
Int.dist_cast_real : ∀ (x y : ℤ), dist ↑x ↑y = dist x y
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_inv_iff : ∀ {α : Type u_3} {m : MeasurableSpace α} {G : Type u_4} [inst : InvolutiveInv G] [inst_1 : MeasurableSpace G]
  [MeasurableInv G] {f : α → G}, (Measurable fun x => (f x)⁻¹) ↔ Measurable f
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- A cone in `HomologicalComplex C c` is limit if the induced cones obtained
by applying `eval C c i : HomologicalComplex C c ⥤ C` for all `i` are limit.  -/
HomologicalComplex.isLimitOfEval : {C : Type u_1} →
  {ι : Type u_2} →
    {J : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_3} J] →
          {c : ComplexShape ι} →
            [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (F : CategoryTheory.Functor J (HomologicalComplex C c)) →
                (s : CategoryTheory.Limits.Cone F) →
                  ((i : ι) → CategoryTheory.Limits.IsLimit ((HomologicalComplex.eval C c i).mapCone s)) →
                    CategoryTheory.Limits.IsLimit s
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The boundary map in the resolution of a topological representation induced
by `TopRep.coind₁Functor`.  -/
TopRep.d : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] → (X : TopRep k G) → (n : ℕ) → X.resolutionX n ⟶ X.resolutionX (n + 1)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mapComp_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.mapComp F G).hom.app X =
    (match X with
      | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of (G.obj (F.obj a)))
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The limit of `F.leftOp` is the unopposite of `colimit F`.  -/
CategoryTheory.Limits.limitLeftOpIsoUnopColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.limit F.leftOp ≅ Opposite.unop (CategoryTheory.Limits.colimit F)
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.instIteratorLoop : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {n : Type x → Type x'} →
        [inst : Monad m] →
          [Monad n] → [inst_2 : Std.Iterator α m β] → Std.IteratorLoop (Std.Iterators.Types.Drop α m β) m n
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.coe_id : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} (f : U ⟶ U), ⇑f = id
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
/-- If `E` is a finite-dimensional space over `ℝ`, then `toEuclidean` is a continuous `ℝ`-linear
equivalence between `E` and the Euclidean space of the same dimension.  -/
toEuclidean : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [T2Space E] →
          [inst_4 : Module ℝ E] →
            [ContinuousSMul ℝ E] → [FiniteDimensional ℝ E] → E ≃L[ℝ] EuclideanSpace ℝ (Fin (Module.finrank ℝ E))
-- Mathlib.Algebra.Group.Equiv.Defs
EmbeddingLike.map_eq_one_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M}, f x = 1 ↔ x = 1
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.precomp_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} (G : Type u_6) [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜₃ G] [inst_15 : RingHomSurjective σ]
  [inst_16 : RingHomIsometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G), (ContinuousLinearMap.precomp G L) f = f ∘SL L
-- Lean.Setup
Lean.instFromJsonImport : Lean.FromJson Lean.Import
-- Std.Tactic.Do.Syntax
/-- Start the stateful proof mode of `Std.Do.SPred`.
This will transform a stateful goal of the form `H ⊢ₛ T` into `⊢ₛ H → T`
upon which `mintro` can be used to re-introduce `H` and give it a name.
It is often more convenient to use `mintro` directly, which will
try `mstart` automatically if necessary.
 -/
Lean.Parser.Tactic.mstart : Lean.ParserDescr
-- Mathlib.Data.List.MinMax
List.foldl_argAux_eq_none : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {l : List α} {o : Option α},
  List.foldl (List.argAux r) o l = none ↔ l = [] ∧ o = none
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.setLike : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  (𝒜 : ιA → σA) →
                    (ℳ : ιM → σM) →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [inst_7 : GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [inst_11 : DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] →
                                          [inst_13 : SetLike.GradedSMul 𝒜 ℳ] → SetLike (HomogeneousSubmodule 𝒜 ℳ) M
-- Std.Data.DHashMap.Raw
/-- Creates a hash map from an array of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.Raw.Const.ofArray : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Array (α × β) → Std.DHashMap.Raw α fun x => β
-- Mathlib.Order.Comparable
AntisymmRel.compRel_congr : ∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) c d → (CompRel (fun x1 x2 => x1 ≤ x2) a c ↔ CompRel (fun x1 x2 => x1 ≤ x2) b d)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.coe_list_prod : ∀ {M : Type u_1} [inst : Monoid M] (s : Submonoid M) (l : List ↥s), ↑l.prod = (List.map Subtype.val l).prod
-- Init.Data.Int.Gcd
Int.gcd_dvd_natAbs_mul : ∀ (m n : ℤ), m.gcd n ∣ m.natAbs * n.natAbs
-- Mathlib.Logic.Function.Basic
Function.not_involutive : Function.Involutive Not
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Composition of continuous semilinear maps as a continuous semibilinear map.  -/
ContinuousLinearMap.compSL : {𝕜 : 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] →
                              (σ₁₂ : 𝕜 →+* 𝕜₂) →
                                (σ₂₃ : 𝕜₂ →+* 𝕜₃) →
                                  {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      [RingHomIsometric σ₂₃] →
                                        [RingHomIsometric σ₁₃] →
                                          [RingHomIsometric σ₁₂] →
                                            (F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.open_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (self : Bundle.Pretrivialization F proj), IsOpen self.target
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
this.  -/
Ideal.span_pow_eq_map_homogeneousSubmodule : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : ι → R) (n : ℕ),
  Ideal.span (Set.range x) ^ n =
    Submodule.map (MvPolynomial.aeval x).toLinearMap (MvPolynomial.homogeneousSubmodule ι R n)
-- Init.Data.String.Basic
/-- Given a string and two valid positions within the string, obtain a slice on the string formed
by the new bounds, or return `none` if the given end is strictly less then the given start.  -/
String.slice? : (s : String) → s.Pos → s.Pos → Option String.Slice
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points not equal to `p`, adding the angles between them at `p` in cyclic order
results in 0.  -/
EuclideanGeometry.oangle_add_cyc3 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p →
    p₂ ≠ p →
      p₃ ≠ p →
        EuclideanGeometry.oangle p₁ p p₂ + EuclideanGeometry.oangle p₂ p p₃ + EuclideanGeometry.oangle p₃ p p₁ = 0
-- Mathlib.Algebra.Group.Prod
Units.embedProduct_injective : ∀ (α : Type u_6) [inst : Monoid α], Function.Injective ⇑(Units.embedProduct α)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_3.eq_2 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (it₂ : Std.IterM m γ)
  (h_1 : Unit → motive none) (h_2 : (it₂ : Std.IterM m γ) → motive (some it₂)),
  (match some it₂ with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_2 it₂
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α →CO β),
  f.comp (ContinuousOpenMap.id α) = f
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuousAt_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {a : α},
  ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.toMethodsRef : Lean.Meta.Grind.Methods → Lean.Meta.Grind.MethodsRef
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.HasAffineProperty : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q)
-- Mathlib.Tactic.Linter.Header
/-- `firstNonImport? stx` assumes that the input `Syntax` is of kind `Lean.Parser.Module.module`.
It returns
* `none`, if `stx` consists only of `import` statements,
* the first non-`import` command in `stx`, otherwise.

The intended use-case is to use the output of `testParseModule` as the input of
`firstNonImport?`.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.firstNonImport? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.isStarNormal_of_mem : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] {x : R}, x ∈ skewAdjoint R → IsStarNormal x
-- Mathlib.Order.Closure
LowerAdjoint.mem_iff : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (s : Set β)
  (x : β), x ∈ l.toFun s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_succ_fst_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) (j : ℕ) (hj : j < k),
  (F.intervalGapsWithin h a b ↑j.succ).1 = ((F.orderEmbOfFin h) ⟨j, hj⟩).2
-- Mathlib.Order.CompactlyGenerated.Basic
/-- A compact element `k` has the property that any `b < k` lies below a "maximal element below
`k`", which is to say `[⊥, k]` is coatomic.  -/
CompleteLattice.Iic_coatomic_of_compact_element : ∀ {α : Type u_2} [inst : CompleteLattice α] {k : α}, IsCompactElement k → IsCoatomic ↑(Set.Iic k)
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y},
  CategoryTheory.HasLiftingProperty i p → CategoryTheory.HasLiftingProperty p.unop i.unop
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.getAnchor.match_1.splitter : (motive : Option UInt64 → Sort u_1) →
  (x : Option UInt64) →
    ((a : UInt64) → motive (some a)) →
      ((x : Option UInt64) → (∀ (a : UInt64), x = some a → False) → motive x) → motive x
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitBackward.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
  (p : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s.hom),
  CategoryTheory.OverPresheafAux.counitBackward F s p =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯)))
      (CategoryTheory.OverPresheafAux.YonedaCollection.snd p.val)
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.mul_compl_self : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  {P : { P // IsLprojection X P }}, ↑P * ↑Pᶜ = 0