mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.blsub_lt_ord_lift : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Ordinal.{max u v}},
  Cardinal.lift.{v, u} o.card < c.cof → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.blsub f < c
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.norm_le_of_forall_inner_le : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] {M : CStarMatrix m n A} {C : NNReal},
  (∀ (v : WithCStarModule A (m → A)) (w : WithCStarModule A (n → A)),
      ‖inner A w ((CStarMatrix.toCLM M) v)‖ ≤ ↑C * ‖v‖ * ‖w‖) →
    ‖M‖ ≤ ↑C
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multicofork for `I.toLinearOrder` deduced from a multicofork
for `I : MultispanIndex (.prod ι) C` when `ι` is linearly ordered.  -/
CategoryTheory.Limits.Multicofork.toLinearOrder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      [inst_1 : LinearOrder ι] →
        {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
          CategoryTheory.Limits.Multicofork I → CategoryTheory.Limits.Multicofork I.toLinearOrder
-- Mathlib.Order.SupClosed
ClosureOperator.ofCompletePred.congr_simp : ∀ {α : Type u_1} [inst : CompleteLattice α] (p p_1 : α → Prop) (e_p : p = p_1)
  (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)),
  ClosureOperator.ofCompletePred p hsinf = ClosureOperator.ofCompletePred p_1 ⋯
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.workerExited.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.workerExited = 1
-- Mathlib.RingTheory.PicardGroup
/-- A representative of an element in the Picard group.  -/
CommRing.Pic.AsModule : {R : Type u} → [inst : CommSemiring R] → CommRing.Pic R → Type u
-- Lean.Environment
Lean.instNonemptyEnvironmentHeader : Nonempty Lean.EnvironmentHeader
-- Init.GrindInstances.Ring.SInt
Lean.Grind.ISize.intCast : IntCast ISize
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)) {x : ((i : ι) → Em i) × G},
  CPolynomialAt 𝕜 (fun p => (f p.1) p.2) x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_sdiff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  a • (s \ t) = a • s \ a • t
-- Lean.Parser.Types
Lean.Parser.Token : Type
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.splitter : {n : ℕ} →
  (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1) →
    (x : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
      ((c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c))) →
        (Unit → motive (some none)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.Normed.Module.Basic
/-- A structure encapsulating minimal axioms needed to defined a normed vector space, as found
in textbooks. This is meant to be used to easily define `NormedAddCommGroup E` and `NormedSpace E`
instances from scratch on a type with no preexisting distance or topology.  -/
NormedSpace.Core : (𝕜 : Type u_6) → (E : Type u_7) → [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [Module 𝕜 E] → [Norm E] → Prop
-- Mathlib.RingTheory.Algebraic.Pi
Polynomial.algebraMap_pi_self_eq_eval : ∀ (R : Type u_1) [inst : CommSemiring R], ⇑(algebraMap (Polynomial R) (R → R)) = fun p z => Polynomial.eval z p
-- Init.Data.String.Slice
/-- Returns the last character in `s`. If `s` is empty, returns `(default : Char)`.

Examples:

* `"abc".toSlice.back = 'c'`

* `"".toSlice.back = (default : Char)`
 -/
String.Slice.back : String.Slice → Char
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In a canonically-ordered monoid, if `S'` is contained in `(S.erase d) ∪ {d'}` and
`f d' < f d` for some `d ∈ S`, then the product of `f` over `S'` is strictly less than over `S`.  -/
Finset.prod_lt_prod_of_subset_erase_union_singleton : ∀ {ι : Type u_9} {M : Type u_10} [inst : DecidableEq ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [CanonicallyOrderedMul M] [MulLeftStrictMono M] {S S' : Finset ι} {f : ι → M} {d d' : ι},
  d ∈ S → S' ⊆ S.erase d ∪ {d'} → f d' < f d → ∏ x ∈ S', f x < ∏ x ∈ S, f x
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α),
  Multiset.powersetCard n (Multiset.map f s) = Multiset.map (Multiset.map f) (Multiset.powersetCard n s)
-- Mathlib.Order.Minimal
/-- If two sets are antitonically order isomorphic, their minimals/maximals are too.  -/
OrderIso.setOfPredMinimalIsoSetOfPredMaximal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} →
          {t : Set β} →
            ↑s ≃o (↑t)ᵒᵈ → ↑{x | Minimal (fun x => x ∈ s) x} ≃o ↑{x | Maximal (fun x => x ∈ t) (OrderDual.ofDual x)}
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.exists_index_le_card_of_leftCoset_cover : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ → ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroMinOfIsClosedUnderIsomorphisms_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [P.ContainsZero]
  [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms], (P ⊓ Q).ContainsZero
-- Init.Data.Slice.Array.Lemmas
Subarray.forIn_toList : ∀ {α : Type u} {s : Subarray α} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
  {f : α → γ → m (ForInStep γ)}, forIn (Std.Slice.toList s) init f = forIn s init f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits.0.CategoryTheory.WithTerminal.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithTerminal C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
                motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive X Y f
-- Aesop.Util.EqualUpToIds
Aesop.tacticStatesEqualUpToIds : Option Lean.MetavarContext →
  Lean.MetavarContext →
    Lean.MetavarContext → Array Lean.MVarId → Array Lean.MVarId → optParam Bool false → Lean.MetaM Bool
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Util.0.Int.Internal.Linear.Poly.pp.go : Lean.MessageData → Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM Lean.MessageData
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] (i : ι) (x : M i),
  Pi.mulSingle i x = Function.update 1 i x
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_set_eq_biUnion : ∀ {α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β), s.sup f = ⋃ x ∈ s, f x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_rpow_iff_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → 0 < y → z < 0 → (x ^ z < y ^ z ↔ y < x)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mulAntidiagonal_one : ∀ {A : Type u_1} [inst : CommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedMul A]
  [inst_3 : Finset.HasMulAntidiagonal A], Finset.HasMulAntidiagonal.mulAntidiagonal 1 = {(1, 1)}
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.extendedHom`.

---

The ring homomorphism that extends a fractional ideal of `A` to a fractional ideal of `B` for
an extension of domains `A ⊆ B`.
 -/
FractionalIdeal.extendedHomₐ : {A : Type u_1} →
  {K : Type u_2} →
    (L : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing A] →
          [IsDomain A] →
            [inst_2 : CommRing B] →
              [IsDomain B] →
                [inst_4 : Algebra A B] →
                  [Module.IsTorsionFree A B] →
                    [inst_6 : Field K] →
                      [inst_7 : Field L] →
                        [inst_8 : Algebra A K] →
                          [inst_9 : Algebra B L] →
                            [IsFractionRing A K] →
                              [IsFractionRing B L] →
                                FractionalIdeal (nonZeroDivisors A) K →+* FractionalIdeal (nonZeroDivisors B) L
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id_assoc : ∀ {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.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d (CategoryTheory.CategoryStruct.id c))
      h =
    h
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle between a nonnegative multiple of a vector and that vector is 0.  -/
Orientation.oangle_smul_left_self_of_nonneg : ∀ {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 : ℝ}, 0 ≤ r → o.oangle (r • x) x = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
  {fallback : (a : α) × β a}, Std.Internal.List.getEntryD k fallback (⟨k, v⟩ :: l) = ⟨k, v⟩
-- Mathlib.Combinatorics.Additive.Corner.Roth
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.mk_mem_triangleIndices : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Finset (G × G)} {a b c : G},
  (a, b, c) ∈ Corners.triangleIndices✝ A ↔ (a, b) ∈ A ∧ c = a + b
-- Mathlib.Data.Set.Prod
Set.fst_injOn_graph : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn Prod.fst (Set.graphOn f s)
-- Mathlib.Topology.Connected.PathConnected
/-- If `x₁` is joined to `x₂` and `y₁` is joined to `y₂`, then `(x₁, y₁)` is joined to
`(x₂, y₂)` in the product space.  -/
Joined.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y},
  Joined x₁ x₂ → Joined y₁ y₂ → Joined (x₁, y₁) (x₂, y₂)
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Icc_sdiff_Ico_same`. -/
Set.Icc_diff_Ico_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Icc a b \ Set.Ico a b = {b}
-- Mathlib.Algebra.GroupWithZero.Defs
mul_right_cancel₀ : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [IsRightCancelMulZero M₀] {a b c : M₀},
  b ≠ 0 → a * b = c * b → a = c
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.map_comp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y Z : T}
  [inst_2 : P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g),
  CategoryTheory.MorphismProperty.Over.map Q ⋯ =
    (CategoryTheory.MorphismProperty.Over.map Q hf).comp (CategoryTheory.MorphismProperty.Over.map Q hg)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
MeasureTheory.Integrable.hasSum_intervalIntegral : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E},
  MeasureTheory.Integrable f μ →
    ∀ (y : ℝ), HasSum (fun n => ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.volumeIoiPow_apply_Iio : ∀ (n : ℕ) (x : ↑(Set.Ioi 0)),
  (MeasureTheory.Measure.volumeIoiPow n) (Set.Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
-- Batteries.Control.Nondet.Basic
/-- Squash a monadic nondeterministic value to a nondeterministic value.
 -/
Nondet.squash : {σ : Type} →
  {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → (Unit → m (Nondet m α)) → Nondet m α
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitorImpl_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.leftUnitorImpl.inv.f =
    CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X.src) (CategoryTheory.CategoryStruct.id X.src)
-- Init.Sym.DSimp.DSimprocDSL
/-- Post-processing simproc chain.  -/
Lean.Parser.Command.symDSimpFieldPost : Lean.ParserDescr
-- Mathlib.Order.Disjointed
iUnion_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : PartialOrder ι] [inst_1 : LocallyFiniteOrderBot ι] {f : ι → Set α},
  ⋃ i, disjointed f i = ⋃ i, f i
-- Mathlib.Algebra.Opposites
AddOpposite.instZero : {α : Type u_1} → [Zero α] → Zero αᵃᵒᵖ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `lt_inv_mul_iff_mul_lt`. -/
mul_lt_of_lt_inv_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b < a⁻¹ * c → a * b < c
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchesAt_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {pos : s.Pos}, String.Slice.Pattern.Model.MatchesAt pat (pos.cast hst) ↔ String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.cancel_epi_assoc_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {g h : Y ⟶ Z}
  {W : C} {k l : Z ⟶ W},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) l ↔
    CategoryTheory.CategoryStruct.comp g k = CategoryTheory.CategoryStruct.comp h l
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.mk : {α : Type u} →
  [toCompleteLattice : CompleteLattice α] →
    [toHImp : HImp α] →
      (∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) →
        [toCompl : Compl α] →
          (∀ (a : α), a ⇨ ⊥ = aᶜ) →
            [toSDiff : SDiff α] →
              (∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) →
                [toHNot : HNot α] →
                  (∀ (a : α), ⊤ \ a = ￢a) →
                    (∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)) →
                      CompletelyDistribLattice α
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring : {α : Type u} → [self : NonUnitalNonAssocRing α] → NonUnitalNonAssocSemiring α
-- Aesop.Stats.File
Aesop.StatsFileRecord.mk.sizeOf_spec : ∀ (toStats : Aesop.Stats) («syntax» file : String) (position : Option Lean.Position) (declaration : Option Lean.Name)
  (goalSolved : Bool),
  sizeOf
      { toStats := toStats, «syntax» := «syntax», file := file, position := position, declaration := declaration,
        goalSolved := goalSolved } =
    1 + sizeOf toStats + sizeOf «syntax» + sizeOf file + sizeOf position + sizeOf declaration + sizeOf goalSolved
-- Batteries.Data.AssocList
Batteries.AssocList.length_toList : ∀ {α : Type u_1} {β : Type u_2} (l : Batteries.AssocList α β), l.toList.length = l.length
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counit_surjective : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  Function.Surjective ⇑CoalgebraStruct.counit
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.recoverCode : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Suppose `X Y : SheafedSpace C`, where `C` is a concrete category,
whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits.
Then a morphism `X ⟶ Y` that is a topological open embedding
is an open immersion iff every stalk map is an iso.
 -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C]
  [inst_2 : CategoryTheory.Limits.HasColimits C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X Y : AlgebraicGeometry.SheafedSpace C}
  (f : X ⟶ Y),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base) →
    ∀
      [H :
        ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)],
      AlgebraicGeometry.SheafedSpace.IsOpenImmersion f
-- Mathlib.Data.Finset.Dedup
Finset.toList.eq_1 : ∀ {α : Type u_1} (s : Finset α), s.toList = s.val.toList
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypeCongrHom_apply : ∀ {α : Type u_4} (p : α → Prop) [inst : DecidablePred p] (pair : Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a }),
  (Equiv.Perm.subtypeCongrHom p) pair = pair.1.subtypeCongr pair.2
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.sdiff_of_sup_edge : ∀ {α : Type u_1} {G : SimpleGraph α} {v w : α} {s : Set α}, (G ⊔ SimpleGraph.edge v w).IsClique s → G.IsClique (s \ {v})
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLEGT n).obj j).mor₂ = (t.truncGTπ n).app j
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The `Aut F` action on the fiber of a Galois object is transitive. See
`pretransitive_of_isConnected` for the same result for connected objects.  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive (CategoryTheory.Aut F) (F.obj X).obj
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The first modified cyclotomic polynomial is `X - 1`.  -/
Polynomial.cyclotomic'_one : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.cyclotomic' 1 R = Polynomial.X - 1
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).inverse.obj X).obj.obj X_1 =
    X.obj.obj (Opposite.op (e.functor.obj (Opposite.unop X_1)))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator_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 Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
              (F.obj Z)))))
-- Mathlib.Data.Fintype.Basic
/-- Given that `α × β` is a fintype, `β` is also a fintype.  -/
Fintype.prodRight : {α : Type u_4} → {β : Type u_5} → [DecidableEq β] → [Fintype (α × β)] → [Nonempty α] → Fintype β
-- Mathlib.Algebra.Star.Basic
InvolutiveStar.mk : {R : Type u} → [toStar : Star R] → Function.Involutive star → InvolutiveStar R
-- Mathlib.Data.Set.Function
Set.BijOn.inter : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.BijOn f s₁ t₁ → Set.BijOn f s₂ t₂ → Set.InjOn f (s₁ ∪ s₂) → Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
-- Mathlib.Data.Set.Lattice
Set.biInter_univ : ∀ {α : Type u_1} {β : Type u_2} (u : α → Set β), ⋂ x ∈ Set.univ, u x = ⋂ x, u x
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.rel.injEq : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) (l_1 : ℕ)
  (R_1 : L.Relations l_1) (ts_1 : Fin l_1 → L.Term (α ⊕ Fin n)),
  (FirstOrder.Language.BoundedFormula.rel R ts = FirstOrder.Language.BoundedFormula.rel R_1 ts_1) =
    (l = l_1 ∧ R ≍ R_1 ∧ ts ≍ ts_1)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.isReturnOf : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.FVarId → Bool
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_nat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ},
  ContDiffWithinAt 𝕜 (↑n) f s x ↔ ∃ u ∈ nhdsWithin x (insert x s), ∃ p, HasFTaylorSeriesUpToOn (↑n) f p u
-- Mathlib.Algebra.Jordan.Basic
two_nsmul_lie_lmul_lmul_add_add_eq_zero : ∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] [IsCommJordan A] (a b c : A),
  2 •
      (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * c)⁆ +
          ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * a)⁆ +
        ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * b)⁆) =
    0