mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} (V : C) (str : V ⟶ F.obj V)
  (V_1 : C) (str_1 : V_1 ⟶ F.obj V_1), ({ V := V, str := str } = { V := V_1, str := str_1 }) = (V = V_1 ∧ str ≍ str_1)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.map` as an `AddMonoidHom`.  -/
LocallyConstant.mapAddMonoidHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        [inst_1 : AddZeroClass Y] → [inst_2 : AddZeroClass Z] → (Y →+ Z) → LocallyConstant X Y →+ LocallyConstant X Z
-- Mathlib.LinearAlgebra.Isomorphisms
/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`.  -/
Submodule.quotientQuotientEquivQuotientAux : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (S T : Submodule R M) → S ≤ T → (M ⧸ S) ⧸ Submodule.map S.mkQ T →ₗ[R] M ⧸ T
-- Mathlib.Algebra.Module.Submodule.Invariant
/-- `p` is `f.symm` invariant if and only if `p ≤ p.map f`.  -/
Module.End.mem_invtSubmodule_symm_iff_le_map : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f : M ≃ₗ[R] M}
  {p : Submodule R M}, p ∈ Module.End.invtSubmodule ↑f.symm ↔ p ≤ Submodule.map (↑f) p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isSome_maxKey?_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {f : β → β}, t.WF → (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey?.isSome = !t.isEmpty
-- Mathlib.CategoryTheory.Limits.Fubini
/-- A structure carrying a diagram of cones over the functors `F.obj j`.
 -/
CategoryTheory.Limits.DiagramOfCones : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            CategoryTheory.Functor J (CategoryTheory.Functor K C) → Type (max (max (max (max u_1 u_2) u_3) v_1) v_3)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
map_multiset_sum : ∀ {F : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F) (s : Multiset M), f s.sum = (Multiset.map (⇑f) s).sum
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.groupSMul_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G R] [inst_5 : DistribMulAction G M]
  [inst_6 : IsScalarTower G R M] [inst_7 : SMulCommClass G R M] {v : Module.Basis ι R M} {w : ι → G} (i : ι),
  (v.groupSMul w) i = (w • ⇑v) i
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv : ∀ {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 s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointUniqueUpToIso Q).inv = P.lift r
-- Init.Data.SInt.Lemmas
Int32.toBitVec_div : ∀ {a b : Int32}, (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
-- Init.Data.Ord.Basic
Ordering.not_isGT_eq_isLE : ∀ {o : Ordering}, (!o.isGT) = o.isLE
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f t[k]?).isSome else t.contains k'
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.pos_natCast_of_pos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a : ℕ), 0 < a → 0 < ↑a
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- `fun p => Fintype.card Fq ^ degree p` is an admissible absolute value.
We set `q ^ degree 0 = 0`.  -/
Polynomial.cardPowDegreeIsAdmissible : {Fq : Type u_1} → [inst : Fintype Fq] → [inst_1 : Field Fq] → Polynomial.cardPowDegree.IsAdmissible
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- Composition of additive module object morphisms.  -/
CategoryTheory.AddMod.comp : {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.AddMonObj A] → {M N O : CategoryTheory.AddMod D A} → M.Hom N → N.Hom O → M.Hom O
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_neg_pi_mul_I : Complex.exp (-(↑Real.pi * Complex.I)) = -1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, (s /ₛ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Algebra.BigOperators.Finprod
MulEquiv.map_finprod : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (g : M ≃* N) (f : α → M),
  g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.exists_dvd_radical_self_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, a ≠ 0 → ∃ n, a ∣ UniqueFactorizationMonoid.radical a ^ n
-- Mathlib.Topology.Basic
isOpen_mk : ∀ {X : Type u} {s : Set X} {p : Set X → Prop} {h₁ : p Set.univ} {h₂ : ∀ (s t : Set X), p s → p t → p (s ∩ t)}
  {h₃ : ∀ (s : Set (Set X)), (∀ t ∈ s, p t) → p (⋃₀ s)}, IsOpen s ↔ p s
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.revPositionsFrom.eq_1 : ∀ (s : String) (p : s.Pos),
  s.revPositionsFrom p = Std.Iter.map String.Internal.ofToSliceWithProof (s.toSlice.revPositionsFrom p.toSlice)
-- Init.Data.List.Lemmas
List.partition.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : List α), List.partition p as = List.partition.loop p as ([], [])
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instCompleteSemilatticeSup : (ι : Type u_1) → CompleteSemilatticeSup (PreAbstractSimplicialComplex ι)
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ioo_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x y : (i : ι) → α i) [Nonempty ι],
  (Set.univ.pi fun i => Set.Ioo (x i) (y i)) ⊆ Set.Ioo x y
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Given `AddSubmonoid`s `s`, `t` of `AddMonoid`s `A`, `B` respectively, `s × t` as an
`AddSubmonoid` of `A × B`.  -/
AddSubmonoid.prod : {N : Type u_2} →
  [inst : AddZeroClass N] →
    {M : Type u_5} → [inst_1 : AddZeroClass M] → AddSubmonoid M → AddSubmonoid N → AddSubmonoid (M × N)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.fst_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.AddMon C),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst M N).hom = CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_inv_atBot_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] {l : Filter α}
  {f : α → G}, Filter.Tendsto (fun x => (f x)⁻¹) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop
-- Init.Grind.AC
Lean.Grind.AC.diseq_unsat_cert : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun x => IrreducibleSpace ↥x
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.mk.inj : ∀ {γ : Type} {newEntries : List Lean.KeyedDeclsAttribute.OLeanEntry} {table : Lean.KeyedDeclsAttribute.Table γ}
  {declNames erased : Lean.PHashSet Lean.Name} {newEntries_1 : List Lean.KeyedDeclsAttribute.OLeanEntry}
  {table_1 : Lean.KeyedDeclsAttribute.Table γ} {declNames_1 erased_1 : Lean.PHashSet Lean.Name},
  { newEntries := newEntries, table := table, declNames := declNames, erased := erased } =
      { newEntries := newEntries_1, table := table_1, declNames := declNames_1, erased := erased_1 } →
    newEntries = newEntries_1 ∧ table = table_1 ∧ declNames = declNames_1 ∧ erased = erased_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.Topology.Homeomorph.Defs
/-- Turn an element of a type `F` satisfying `HomeomorphClass F α β` into an actual
`Homeomorph`. This is declared as the default coercion from `F` to `α ≃ₜ β`.  -/
HomeomorphClass.toHomeomorph : {F : Type u_5} →
  {α : Type u_6} →
    {β : Type u_7} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : EquivLike F α β] → [h : HomeomorphClass F α β] → F → α ≃ₜ β
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_add : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (x y : AddMonoidAlgebra R M), AddMonoidAlgebra.map f (x + y) = AddMonoidAlgebra.map f x + AddMonoidAlgebra.map f y
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_smul_of_isRegular : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {r : R},
  IsRegular r → ∀ {f : MvPolynomial σ R}, m.degree (r • f) = m.degree f
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The quotient functor from the category of cofibrant objects to its
homotopy category.  -/
HomotopicalAlgebra.CofibrantObject.toHoCat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject C) (HomotopicalAlgebra.CofibrantObject.HoCat C)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_comap_eq`. -/
Ideal.ramificationIdx_comap_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] (e : S ≃ₐ[R] S₁) (P : Ideal S₁),
  p.ramificationIdx' (Ideal.comap e P) = p.ramificationIdx' P
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.inv_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) = CategoryTheory.Functor.LaxMonoidal.μ F X Y
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.LocallySmall.{w, v, u} C
-- Mathlib.AlgebraicGeometry.Birational.Dominant
AlgebraicGeometry.Scheme.PartialMap.isDominant_toRationalMap_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), f.toRationalMap.IsDominant ↔ AlgebraicGeometry.IsDominant f.hom
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.neg_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : ContinuousNeg M] (x : M), (ContinuousLinearEquiv.neg R) x = -x
-- Batteries.Classes.Order
Std.LawfulLTCmp.eq_compareOfLessAndEq : ∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : LT α] [inst_1 : DecidableEq α] [Std.LawfulEqCmp cmp]
  [Std.LawfulLTCmp cmp] (x y : α) [inst_4 : Decidable (x < y)], cmp x y = compareOfLessAndEq x y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.name : Lean.Lsp.SymbolInformation → String
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A trail doesn't go through an edge that disconnects one of its endpoints from the endpoints of
the trail.  -/
SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v},
  w.IsTrail → ¬(G.deleteEdges {s(x, y)}).Reachable u y → ¬(G.deleteEdges {s(x, y)}).Reachable v y → s(x, y) ∉ w.edges
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq
-- Mathlib.Data.Sym.Sym2
Sym2.fromRelOrderIso_apply : ∀ (α : Type u_1) (r : { r // Std.Symm r }), (Sym2.fromRelOrderIso α) r = Sym2.fromRel ⋯
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_apply : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)
  (x : τ → R) (i : σ), MvPolynomial.comap f x i = (MvPolynomial.aeval x) (f (MvPolynomial.X i))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between two vectors is nonnegative.  -/
InnerProductGeometry.angle_nonneg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  0 ≤ InnerProductGeometry.angle x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = false → Std.Internal.List.getEntry? a (⟨k, v⟩ :: l) = Std.Internal.List.getEntry? a l
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive], Λ.karoubi.F.PreservesZeroMorphisms
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_le_set : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s ≤ᵐ[μ] t ↔ μ (s \ t) = 0
-- Init.Data.Int.Basic
Int.instNegInt : Neg ℤ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow : ∀ {b : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsInt b (Int.negOfNat n) → ∀ (a : ℝ), a ^ b = (a ^ n)⁻¹
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Ric.iter : {α : Type u_1} → [Std.PRange.Least? α] → Std.Ric α → Std.Iter α
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_id : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R), C.map (RingHom.id R) = C
-- Mathlib.CategoryTheory.Action.Basic
/-- An equivalence of categories induces an equivalence of
the categories of `G`-actions within those categories.  -/
CategoryTheory.Equivalence.mapAction : {V : Type u_2} →
  {W : Type u_3} →
    [inst : CategoryTheory.Category.{v_2, u_2} V] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} W] →
        (G : Type u_4) → [inst_2 : Monoid G] → (V ≌ W) → (Action V G ≌ Action W G)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- Given a morphism of simplicial sets `p : Y ⟶ X` and
`A : X.Subcomplex`, this is the induced morphism
`(A.preimage p : SSet) ⟶ (A : SSet)`.  -/
SSet.Subcomplex.fromPreimage : {X Y : SSet} → (A : X.Subcomplex) → (p : Y ⟶ X) → (A.preimage p).toSSet ⟶ A.toSSet
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ici_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderTop α], Finset.Ici ⊤ = {⊤}
-- Mathlib.RingTheory.SimpleModule.Basic
_private.Mathlib.RingTheory.SimpleModule.Basic.0.LinearMap.isSemisimpleModule_of_injective : {R : Type u_2} →
  {S : Type u_3} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {M' : Type u_6} →
          [inst_2 : AddCommGroup M'] →
            [inst_3 : Module R M'] →
              {N' : Type u_7} →
                [inst_4 : AddCommGroup N'] →
                  [inst_5 : Module S N'] →
                    {σ : R →+* S} →
                      (l : M' →ₛₗ[σ] N') →
                        Function.Injective ⇑l → [IsSemisimpleModule S N'] → ProofWanted (IsSemisimpleModule R M')
-- Mathlib.Algebra.Lie.Character
/-- A character of a Lie algebra is a morphism to the scalars.  -/
LieAlgebra.LieCharacter : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type (max v u)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated : ∀ {α : Type u_5} {β : Type u_6} {inst : MeasurableSpace β} [self : MeasurableSpace.CountableOrCountablyGenerated α β],
  Countable α ∨ MeasurableSpace.CountablyGenerated β
-- Mathlib.Algebra.Order.Pi
Pi.existsAddOfLe : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → LE (α i)] [inst_1 : (i : ι) → Add (α i)]
  [∀ (i : ι), ExistsAddOfLE (α i)], ExistsAddOfLE ((i : ι) → α i)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Analyzes a newly recorded atom,
returning a collection of interesting facts about it that should be added to the context.
 -/
Lean.Elab.Tactic.Omega.analyzeAtom : Lean.Expr → Lean.Elab.Tactic.Omega.OmegaM (List Lean.Expr)
-- Mathlib.Data.Set.Card
Set.ncard_ne_zero_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → autoParam s.Finite Set.ncard_ne_zero_of_mem._auto_1 → s.ncard ≠ 0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCoeTCForall : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → CoeTC (α → β) (l.Germ β)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Converse of Thales' theorem in 2D: if three distinct points on a circle
form a right angle, then the chord is a diameter.  -/
EuclideanGeometry.Sphere.isDiameter_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} [Fact (Module.finrank ℝ V = 2)],
  p₁ ∈ s → p₂ ∈ s → p₃ ∈ s → p₁ ≠ p₂ → p₂ ≠ p₃ → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → s.IsDiameter p₁ p₃
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The type of `0`-hypercovers of an object `S : C` in a category equipped with a
coverage `J`. This can be constructed from a covering of `S`.  -/
CategoryTheory.Precoverage.ZeroHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → C → Type (max (max u v) (w + 1))
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).f₂₄ = F.map sq.f₂₄
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_zero : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ), Fin.cons x p 0 = x
-- Init.Data.Array.Lemmas
Array.getElem?_replace_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : ℕ},
  xs[i]? ≠ some a → (xs.replace a b)[i]? = xs[i]?
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) →
          Module R ((AlgebraicGeometry.structureSheafInType R M).obj.obj U)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Submodule.span ℝ ↑(NumberField.Units.unitLattice K) = ⊤
-- Mathlib.Algebra.Ring.Ext
AddCommGroupWithOne.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : AddCommGroupWithOne R⦄, HAdd.hAdd = HAdd.hAdd → One.one = One.one → inst₁ = inst₂
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMul : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Mul R] → [BoundedMul R] → [ContinuousMul R] → Mul (BoundedContinuousFunction α R)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.isSymm_swap : ∀ {R : Type u_1} {n : Type u_2} [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq n] (i j : n),
  (Matrix.swap R i j).IsSymm
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.instMonoidalSkeletonMapSkeleton : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) → [F.Monoidal] → F.mapSkeleton.Monoidal
-- Mathlib.Order.RelIso.Basic
/-- The map `coe_fn : (r ↪r s) → (α → β)` is injective.  -/
RelEmbedding.coe_fn_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective fun f => ⇑f
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
/-- The canonical functor from an additive category into its commutative group objects. This is
always an equivalence, see `commGrpEquivalence`.  -/
CategoryTheory.Preadditive.toCommGrp : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_3 : CategoryTheory.BraidedCategory C] → CategoryTheory.Functor C (CategoryTheory.CommGrp C)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Mono f] {H : CategoryTheory.IsPushout f g h i}, H.IsVanKampen → CategoryTheory.IsPullback f g h i
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.iInf_rat_gt_eq : ∀ (f : StieltjesFunction ℝ) (x : ℝ), ⨅ r, ↑f ↑↑r = ↑f x
-- Mathlib.ModelTheory.Definability
/-- **Alias** of the reverse direction of `Set.termDefinable₁_iff_termDefinable`.

---

`TermDefinable₁` is defined as `TermDefinable` on the `Unit` index type.  -/
Set.TermDefinable.termDefinable₁ : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] (f : M → M),
  (A.TermDefinable L fun v => f (v ())) → Set.TermDefinable₁ L f
-- Mathlib.Topology.DenseEmbedding
Dense.extend_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : ↑s → β}
  [T2Space β] (hs : Dense s), Continuous f → ∀ (x : ↑s), hs.extend f ↑x = f x