mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Given two compact sets `K` and `L`, `γ +ᵥ K ∩ L` is nonempty for finitely many `γ`.  -/
ProperlyDiscontinuousVAdd.finite_disjoint_inter_image : ∀ {Γ : Type u_4} {T : Type u_5} {inst : TopologicalSpace T} {inst_1 : VAdd Γ T} [self : ProperlyDiscontinuousVAdd Γ T]
  {K L : Set T}, IsCompact K → IsCompact L → {γ | ((fun x => γ +ᵥ x) '' K ∩ L).Nonempty}.Finite
-- Mathlib.Topology.Connected.Basic
/-- The biUnion of a family of preconnected sets is preconnected if the graph determined by
whether two sets intersect is preconnected.  -/
IsConnected.biUnion_of_reflTransGen : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α},
  t.Nonempty →
    (∀ i ∈ t, IsConnected (s i)) →
      (∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) →
        IsConnected (⋃ n ∈ t, s n)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The action of an object `c : C` on a map `f : d ⟶ d'` in `D`.
If we are to consider the action as a functor `Α : C ⥤ D ⥤ D`,
this is `(Α.obj c).map f`. This is denoted `f ⊵ᵣ c`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft : {C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            {d d' : D} →
              (d ⟶ d') →
                (c : C) →
                  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶
                    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d' c
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a vector and a multiple of a `π / 2` rotation of that vector is
zero.  -/
Orientation.inner_smul_rotation_pi_div_two_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ), inner ℝ x (r • (o.rotation ↑(Real.pi / 2)) x) = 0
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle._auto_1),
  CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃)
      (CochainComplex.homologyδOfTriangle T n₀ n₁ h) =
    CategoryTheory.CategoryStruct.comp
      (DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h)
      ((DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁)
-- Mathlib.Data.Real.Embedding
Archimedean.exists_orderAddMonoidHom_real_injective : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [Archimedean M],
  ∃ f, Function.Injective ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.instNonempty : ∀ {V : Type u} {G : SimpleGraph V} [Nonempty V], Nonempty G.ConnectedComponent
-- Mathlib.Lean.FoldEnvironment
/-- Loop through all constants in modules with module index from `start` to `stop - 1`.  -/
_private.Mathlib.Lean.FoldEnvironment.0.Lean.Meta.foldModules : {α : Type} →
  Lean.NameGenerator →
    Lean.Meta.FoldDeclErrorRef →
      Lean.Environment →
        α →
          (α → Lean.Name → Lean.ConstantInfo → Lean.MetaM α) →
            Lean.Meta.Context → Lean.Core.Context → ℕ → ℕ → EIO Lean.Exception α
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- Auxiliary function used for bounding Eisenstein series, defined as
`z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)`.  -/
EisensteinSeries.r1 : UpperHalfPlane → ℝ
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a b : α), LowerSet.Iic (a ⊓ b) = LowerSet.Iic a ⊓ LowerSet.Iic b
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (j : J),
  ((AlgebraicGeometry.PresheafedSpace.colimitCocone F).ι.app j).c =
    CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp
      (Opposite.op j)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.let : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetDecl pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Init.Data.List.Basic
List.intersperse_cons_cons : ∀ {α : Type u} {x y : α} {zs : List α} {sep : α},
  List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
/-- If `f : X ⟶ S` is geometrically connected and open,
then `f` induces a homeomorphism between the connected components of `X` and `S`.  -/
AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorph : {X S : AlgebraicGeometry.Scheme} →
  (f : X ⟶ S) →
    [AlgebraicGeometry.GeometricallyConnected f] → IsOpenMap ⇑f → ConnectedComponents ↥X ≃ₜ ConnectedComponents ↥S
-- Mathlib.Algebra.CubicDiscriminant
_private.Mathlib.Algebra.CubicDiscriminant.0.Cubic.ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0 → P.toPoly ≠ 0
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_eq_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.mulHeight₁ x = Height.mulHeight ![x, 1]
-- Mathlib.Algebra.Polynomial.CoeffList
/-- The list of coefficients starting from the leading term down to the constant term.  -/
Polynomial.coeffList : {R : Type u_1} → [inst : Semiring R] → Polynomial R → List R
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.instCategory.eq_1 : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A],
  CategoryTheory.Mod.instCategory =
    { Hom := fun M N => M.Hom N, id := CategoryTheory.Mod.id, comp := fun {X Y Z} f g => CategoryTheory.Mod.comp f g,
      id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.mk_Iio_ordinal : ∀ (o : Ordinal.{u}), Cardinal.mk ↑(Set.Iio o) = Cardinal.lift.{u + 1, u} o.card
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `G.copyCount H` is the number of unlabelled copies of `H` in `G`, i.e. the number of subgraphs
of `G` isomorphic to `H`. See `SimpleGraph.labelledCopyCount` for the number of labelled copies.  -/
SimpleGraph.copyCount : {V : Type u_1} → {W : Type u_2} → [Fintype V] → SimpleGraph V → SimpleGraph W → ℕ
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.sub_mem_orthogonal_of_inner_left : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : ClosedSubmodule 𝕜 E} {x y : E}, (∀ (v : ↥K), inner 𝕜 x ↑v = inner 𝕜 y ↑v) → x - y ∈ Kᗮ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_1eq : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_1eq_cert lhs rhs p₁ p₂ = true →
    ↑1 * Lean.Grind.CommRing.Poly.denote ctx p₁ = Lean.Grind.CommRing.Poly.denote ctx p₂ →
      Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.top_apply : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X Y : C} (f : X ⟶ Y), ⊤ f
-- Mathlib.Analysis.Complex.Exponential
Real.exp_approx_end : ∀ (n m : ℕ) (x : ℝ), n + 1 = m → |x| ≤ 1 → |Real.exp x - Real.expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Hom is functorially cocontinuous: coyoneda of a colimit is the limit
over coyoneda of the diagram.  -/
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (F : CategoryTheory.Functor I C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Limits.colimit F)) ≅
              CategoryTheory.Limits.limit (F.op.comp CategoryTheory.coyoneda)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_const : ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (a : Ordinal.{max u v}), (o.bsup fun x x_1 => a) = a
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure : ∀ {Ω' : Type u_2} [inst : MeasurableSpace Ω'] [inst_1 : TopologicalSpace Ω'] [inst_2 : BorelSpace Ω'] {Ω : Type u_3}
  [inst_3 : MeasurableSpace Ω] [inst_4 : TopologicalSpace Ω] [inst_5 : BorelSpace Ω] [NormalSpace Ω'] (f : Ω → Ω'),
  Topology.IsClosedEmbedding f → Topology.IsEmbedding fun μ => μ.map f
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_pi_of_finite : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] [Finite η] (Ss : (i : η) → AddSubgroup (Gs i))
  (n : ℕ),
  (AddSubgroup.pi Set.univ Ss).lowerCentralSeries n = AddSubgroup.pi Set.univ fun i => (Ss i).lowerCentralSeries n
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.mapFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y),
  CategoryTheory.Square.mapFunctor.map τ = CategoryTheory.NatTrans.mapSquare τ
-- Std.Data.Internal.List.Associative
Std.Internal.List.contains_insertList_of_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k l = true →
    Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true
-- Init.Data.List.MinMax
List.le_min?_iff : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderInf α] {xs : List α},
  xs.min? = some a → ∀ {x : α}, x ≤ a ↔ ∀ b ∈ xs, x ≤ b
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.homEquiv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a : CategoryTheory.CatEnrichedOrdinary C},
  CategoryTheory.CatEnrichedOrdinary.homEquiv (CategoryTheory.CategoryStruct.id a) =
    CategoryTheory.CategoryStruct.id a.toBase
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.comp_apply : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P}, φ.CompTriple ψ χ → ∀ (x : M), ψ (φ x) = χ x
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_uIcc_of_antitoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  ContinuousOn f (Set.uIcc a b) → AntitoneOn f (Set.uIcc a b) → f '' Set.uIcc a b = Set.uIcc (f a) (f b)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.mk.inj : ∀ {A : Type u_6} {B : Type u_7} {inst : Mul A} {inst_1 : Mul B} {inst_2 : Star A} {inst_3 : Star B}
  {toMulEquiv : A ≃* B} {map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)}
  {toMulEquiv_1 : A ≃* B} {map_star'_1 : ∀ (a : A), toMulEquiv_1.toFun (star a) = star (toMulEquiv_1.toFun a)},
  { toMulEquiv := toMulEquiv, map_star' := map_star' } = { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 } →
    toMulEquiv = toMulEquiv_1
-- Init.Data.UInt.Lemmas
UInt32.ofNat_uInt8ToNat : ∀ (n : UInt8), UInt32.ofNat n.toNat = n.toUInt32
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_iInter : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
  (p : ι → Set α), omegaLimit f ϕ (⋂ i, p i) ⊆ ⋂ i, omegaLimit f ϕ (p i)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasurableEmbedding.singularPart_map : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
      (MeasureTheory.Measure.map f μ).singularPart (MeasureTheory.Measure.map f ν) =
        MeasureTheory.Measure.map f (μ.singularPart ν)
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.isClosed_topologicalClosure : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M),
  IsClosed ↑s.topologicalClosure
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_cos_eq_of_two_nsmul_eq : ∀ {θ ψ : Real.Angle}, 2 • θ = 2 • ψ → |θ.cos| = |ψ.cos|
-- Lean.Data.Position
Lean.FileMap.mk.inj : ∀ {source : String} {positions : Array String.Pos.Raw} {source_1 : String} {positions_1 : Array String.Pos.Raw},
  { source := source, positions := positions } = { source := source_1, positions := positions_1 } →
    source = source_1 ∧ positions = positions_1
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.neg_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (m : M), (-f) m = -f m
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms],
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₂ → P T.obj₃) →
    P.IsTriangulatedClosed₃
-- Mathlib.Analysis.Normed.Group.Basic
eq_zero_or_norm_pos : ∀ {E : Type u_5} [inst : NormedAddGroup E] (a : E), a = 0 ∨ 0 < ‖a‖
-- Mathlib.Data.Set.Function
Set.EqOn.cancel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f₁ f₂ : α → β} {g : β → γ},
  Set.EqOn (g ∘ f₁) (g ∘ f₂) s → Set.InjOn g t → Set.MapsTo f₁ s t → Set.MapsTo f₂ s t → Set.EqOn f₁ f₂ s
-- Mathlib.Order.Category.PartOrd
PartOrd.hom_ext_iff : ∀ {X Y : PartOrd} {f g : X ⟶ Y}, f = g ↔ PartOrd.Hom.hom f = PartOrd.Hom.hom g
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_min_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) {i : ι}, ⋯.measurableSpace = hτ.measurableSpace ⊓ ↑f i
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.apply : ∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, A.IsSymm → ∀ (i j : n), A j i = A i j
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Auxiliary definition for `isCardinalFiltered`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁ : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] →
        {ι : Type w} →
          (ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) →
            HasCardinalLT ι κ → J → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
DiscreteUniformity.instOfFiniteOfDiscreteTopology : ∀ {Y : Type u_2} [Finite Y] [inst : UniformSpace Y] [DiscreteTopology Y], DiscreteUniformity Y
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A linear isometric equivalence preserves the inner product.  -/
LinearIsometryEquiv.inner_map_map : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x y : E),
  inner 𝕜 (f x) (f y) = inner 𝕜 x y
-- Mathlib.Algebra.MvPolynomial.Basic
/-- Analog of `Polynomial.induction_on`.
If a property holds for any constant polynomial
and is preserved under addition and multiplication by variables
then it holds for all multivariate polynomials.
 -/
MvPolynomial.induction_on : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (p q : MvPolynomial σ R), motive p → motive q → motive (p + q)) →
      (∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) → motive p
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The weight `k` slash action of `GL(2, ℝ)` preserves holomorphic functions.  -/
MDifferentiable.slash : ∀ {f : UpperHalfPlane → ℂ}, MDiff f → ∀ (k : ℤ) (g : GL (Fin 2) ℝ), MDiff (SlashAction.map k g f)
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
IntermediateField.splits_iff_mem : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K}
  {F : IntermediateField K L},
  (Polynomial.map (algebraMap K L) p).Splits → ((Polynomial.map (algebraMap K ↥F) p).Splits ↔ ∀ x ∈ p.rootSet L, x ∈ F)
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Submodule.pointwiseDistribMulAction : {α : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Monoid α] →
              [inst_4 : DistribMulAction α M] → [SMulCommClass α R M] → DistribMulAction α (Submodule R M)
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_succ_equiv_symm_apply : ∀ {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) (a : Function.FromTypes p τ),
  (Function.fromTypes_succ_equiv p τ).symm a = a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomial =
    P 1 ^ 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 3 -
      (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 ^ 2 + W'.a₄ * P 0 * P 2 ^ 4 + W'.a₆ * P 2 ^ 6)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- An equation between morphisms gives an isomorphism between the images.  -/
CategoryTheory.Limits.image.eqToIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f f' : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          [inst_2 : CategoryTheory.Limits.HasImage f'] →
            f = f' → (CategoryTheory.Limits.image f ≅ CategoryTheory.Limits.image f')
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.ComplexConfig.mk.injEq : ∀ (out ctx : Type) (trigger : Option ctx → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx)
  (test : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx → Lean.MVarId → Lean.Elab.Command.CommandElabM out)
  (tell : Lean.Syntax → List Lean.MVarId → ℕ → out → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData))
  (out_1 ctx_1 : Type) (trigger_1 : Option ctx_1 → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx_1)
  (test_1 : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx_1 → Lean.MVarId → Lean.Elab.Command.CommandElabM out_1)
  (tell_1 : Lean.Syntax → List Lean.MVarId → ℕ → out_1 → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)),
  ({ out := out, ctx := ctx, trigger := trigger, test := test, tell := tell } =
      { out := out_1, ctx := ctx_1, trigger := trigger_1, test := test_1, tell := tell_1 }) =
    (out = out_1 ∧ ctx = ctx_1 ∧ trigger ≍ trigger_1 ∧ test ≍ test_1 ∧ tell ≍ tell_1)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Tag.mk : Lean.Name → Mathlib.CrossRef.Database → String → String → Mathlib.CrossRef.Tag
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.instNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)},
  Nonempty (CategoryTheory.Subfunctor F)
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Sigma.isGeneratedBy`. -/
Sigma.deltaGeneratedSpace : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {κ : Type u_1} {Y : κ → Type u_2}
  [inst_1 : (k : κ) → TopologicalSpace (Y k)] [∀ (k : κ), Topology.IsGeneratedBy X (Y k)],
  Topology.IsGeneratedBy X ((k : κ) × Y k)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
lt_of_abs_lt : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, |a| < b → a < b
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingProd.eq_3 : ∀ {G : Type u_4} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G] (g h : G) (t : List G),
  (g :: h :: t).alternatingProd = g * h⁻¹ * t.alternatingProd
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.range_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsInducing f), Set.range (TopologicalSpace.NonemptyCompacts.map f ⋯) = {K | ↑K ⊆ Set.range f}
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.diag_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Functor.diag C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.diag C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_mul_left' : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Finset β)
  (f : β → α) (a : α), Associated (s.gcd fun x => a * f x) (a * s.gcd f)
-- Init.Data.Nat.Simproc
Nat.Simproc.le_add_le : ∀ (a : ℕ) {b c : ℕ}, a ≤ c → (a ≤ b + c) = True
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.hom_ext_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} {f g : x ⟶ y}, f = g ↔ f.fst = g.fst ∧ f.snd = g.snd
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.lift_comp_residue : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : Field S] (f : R →+* S)
  [inst_3 : IsLocalHom f], (IsLocalRing.ResidueField.lift f).comp (IsLocalRing.residue R) = f
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_isOpenMap : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : TopologicalSpace S] [∀ (i : ι), PrespectralSpace (X i)],
  (∀ (i : ι), Continuous (f i)) →
    (∀ (i : ι), IsOpenMap (f i)) →
      ∀ {U : Set S}, (∀ x ∈ U, ∃ i, x ∈ Set.range (f i)) → IsOpen U → IsCompact U → IsCompactOpenCovered f U