mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mdifferentiable_mulInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G]
  [inst_7 : LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G), MDiff fun g => ⟨g, mulInvariantVectorField v g⟩
-- Mathlib.Algebra.NeZero
two_ne_zero' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], 2 ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
CategoryTheory.yonedaRingObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : C) [inst_3 : CategoryTheory.RingObj R] (X : Cᵒᵖ),
  (CategoryTheory.yonedaRingObj R).obj X = RingCat.of (Opposite.unop X ⟶ R)
-- Mathlib.FieldTheory.Fixed
AlgEquiv.card_le : ∀ {F : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : FiniteDimensional F K], Fintype.card Gal(K/F) ≤ Module.finrank F K
-- Std.Time.Date.Unit.Day
Std.Time.Day.instLTOffset : LT Std.Time.Day.Offset
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.of_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Injective ⇑f → ∀ [Algebra.IsAlgebraic R B], Algebra.IsAlgebraic R A
-- Mathlib.Data.List.Cycle
Cycle.Chain.eq_nil_of_well_founded : ∀ {α : Type u_1} {r : α → α → Prop} {s : Cycle α} [IsWellFounded α r], Cycle.Chain r s → s = Cycle.nil
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.mk : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                {P : RootPairing ι R M N} →
                                  {Q : RootPairing ι₂ R M₂ N₂} →
                                    (weightMap : M →ₗ[R] M₂) →
                                      (coweightMap : N₂ →ₗ[R] N) →
                                        (indexEquiv : ι ≃ ι₂) →
                                          weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap →
                                            ⇑weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv →
                                              ⇑coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv.symm → P.Hom Q
-- Lean.DocString.Extension
Lean.ElabInline.custom.inj : ∀ {val val_1 : Dynamic}, Lean.ElabInline.custom val = Lean.ElabInline.custom val_1 → val = val_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.id_snd_coe : ∀ (Δ : SimplexCategoryᵒᵖ),
  ↑(CategoryTheory.SimplicialObject.Splitting.IndexSet.id Δ).snd = CategoryTheory.CategoryStruct.id (Opposite.unop Δ)
-- Lean.Parser.Command
/-- (module system) The `meta` modifier can be applied to a `def` in order to make it available for
compile-time execution, e.g. as part of a macro or tactic. Specifically, attributes such as
`@[macro]` require the annotated declaration to be `meta`, and recursively a `meta` definition may
only refer to other `meta` definitions unless the reference is irrelevant for compilation purposes.
However, imported definitions not originally marked `meta`, such as most parts of the standard
library, can be retroactively be marked so during importing to allow their use in `meta`
definitions. If the metaprogramming use is local to the current module, such as through
`local macro`, this can be done by `meta import`; if the metaprogram is available to other modules
as well, `public meta import` is required.

Conversely, `meta def` makes the definition unavailable for run-time use, e.g. as part of a
`lean_exe` executable generated by Lake. Thus `def`s that are not marked `meta` (nor
`noncomputable`) may not refer to `meta def`s either in compilation-relevant ways. There is no way
to remove the `meta` modifier retroactively. For any potential mixed use of a definition, it should
be defined without `meta` and then imported with the correct modifier as needed. In particular,
the same module can be `import`ed and `meta import`ed at once in order to make such regular `def`s
available in both `meta` and non-`meta` `def`s.
 -/
Lean.Parser.Command.meta : Lean.Parser.Parser
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_subtypePerm : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) {p : α → Prop} [inst_2 : DecidablePred p]
  (h₁ : ∀ (x : α), p (f x) ↔ p x), (∀ (x : α), f x ≠ x → p x) → Equiv.Perm.sign (f.subtypePerm h₁) = Equiv.Perm.sign f
-- Mathlib.Order.GaloisConnection.Defs
/-- Lift the top along a Galois connection  -/
GaloisConnection.liftOrderTop : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [OrderTop α] → [inst_2 : PartialOrder β] → {u : α → β} → {l : β → α} → GaloisConnection l u → OrderTop β
-- Mathlib.Tactic.Ring.Compare
/-- In a commutative semiring, given `Ring.ExSum` objects `va`, `vb` which differ by a positive
(additive) constant, construct a proof of `$a < $b`, where `a` (resp. `b`) is the expression in the
semiring to which `va` (resp. `vb`) evaluates.  -/
Mathlib.Tactic.Ring.evalLT : {v : Lean.Level} →
  {α : Q(Type v)} →
    (ics : Q(CommSemiring «$α»)) →
      (x : Q(PartialOrder «$α»)) →
        Q(IsStrictOrderedRing «$α») →
          {a b : Q(«$α»)} →
            Mathlib.Tactic.Ring.ExSum q(«$ics») a →
              Mathlib.Tactic.Ring.ExSum q(«$ics») b → Lean.MetaM (Except Mathlib.Tactic.Ring.ExceptType Q(«$a» < «$b»))
-- Init.Core
DoResultPRBC.pure.inj : ∀ {α β σ : Type u} {a : α} {a_1 : σ} {a_2 : α} {a_3 : σ},
  DoResultPRBC.pure a a_1 = DoResultPRBC.pure a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_rcc' : ∀ {m n k : ℤ}, Array.map (fun x => k + x) (m...=n).toArray = ((k + m)...=k + n).toArray
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a set of points is a Galois insertion between sets of points of a projective space
and subspaces of the projective space.  -/
Projectivization.Subspace.gi : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → GaloisInsertion Projectivization.Subspace.span SetLike.coe
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_shiftLeft_or_shiftLeft : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n
-- Init.Data.String.Modify
_private.Init.Data.String.Modify.0.String.mapAux.eq_def : ∀ (f : Char → Char) (s : String) (p : s.Pos),
  String.mapAux f s p = if h : p = s.endPos then s else String.mapAux f (p.modify f h) (p.pastModify f h)
-- Mathlib.Topology.ContinuousOn
continuous_of_continuousOn_iUnion_of_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_5}
  {s : ι → Set α}, (∀ (i : ι), ContinuousOn f (s i)) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → Continuous f
-- Mathlib.Order.Bounds.Basic
isLUB_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → IsLUB (Set.Ioc a b) b
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.max : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ →
    MeasureTheory.IsStoppingTime f π → MeasureTheory.IsStoppingTime f fun ω => max (τ ω) (π ω)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.insertAtCollisionNode : {α : Type u_1} →
  {β : Type u_2} → [BEq α] → Lean.PersistentHashMap.CollisionNode α β → α → β → Lean.PersistentHashMap.CollisionNode α β
-- Mathlib.Order.Grade
Flag.instGradeBoundedOrderSubtypeMem : {𝕆 : Type u_1} →
  {α : Type u_3} →
    [inst : PartialOrder α] → [inst_1 : Preorder 𝕆] → [GradeBoundedOrder 𝕆 α] → (s : Flag α) → GradeBoundedOrder 𝕆 ↥s
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.eval_eq : ∀ {assign : ℕ → Bool} {aig : Std.Sat.AIG ℕ} {state : Std.Sat.AIG.toCNF.State✝ aig},
  Std.Sat.AIG.toCNF.State.eval✝ assign state = Std.Sat.CNF.eval assign (Std.Sat.AIG.toCNF.State.cnf✝ state)
-- Mathlib.Tactic.NormNum.ModEq
/-- `norm_num` extension for `Int.ModEq`.  -/
Mathlib.Meta.NormNum.evalIntModEq : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.subset_closure_sdiff_iff_closure_eq`. -/
Matroid.subset_closure_diff_iff_closure_eq : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α},
  Y ⊆ X →
    autoParam (Y ⊆ M.E) Matroid.subset_closure_sdiff_iff_closure_eq._auto_1 →
      (Y ⊆ M.closure (X \ Y) ↔ M.closure (X \ Y) = M.closure X)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_of_subsingleton : ∀ {α : Type u_1} [inst : AddGroup α] [Subsingleton α], IsAddCyclic α
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_annihilator : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.IsTorsionBySet R M ↑(Module.annihilator R M)
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingCongr_trans : ∀ {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ ≃ α₂)
  (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃),
  (e₁.trans e₂).embeddingCongr (e₁'.trans e₂') = (e₁.embeddingCongr e₁').trans (e₂.embeddingCongr e₂')
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app._auto_1)
  {Z : Cᵒᵖ} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app
        (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X))))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).inv.app (Opposite.unop X)).op h)
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomain_pow : ∀ {α : Type u_4} {β : Type u_5} (e : Equiv.Perm α) {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (n : ℕ),
  (e ^ n).extendDomain f = e.extendDomain f ^ n
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- Any uncountable standard Borel space is Borel isomorphic to the Cantor space `ℕ → Bool`.  -/
PolishSpace.measurableEquivNatBoolOfNotCountable : {α : Type u_4} → [inst : MeasurableSpace α] → [StandardBorelSpace α] → ¬Countable α → α ≃ᵐ (ℕ → Bool)
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.not_imp`. -/
not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.modify.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α × RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α)
  (x : α) (b : RBTree.RBNode α) (path : RBTree.RBNode.Path α)
  (h_1 : (snd : RBTree.RBNode.Path α) → motive (RBTree.RBNode.nil, snd))
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (x : α) → (b : RBTree.RBNode α) → (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a x b, path)),
  (match (RBTree.RBNode.node c a x b, path) with
    | (RBTree.RBNode.nil, snd) => h_1 snd
    | (RBTree.RBNode.node c a x b, path) => h_2 c a x b path) =
    h_2 c a x b path
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_right_injective_of_inv : ∀ {l : Type u_1} {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] [inst_3 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
  A * B = 1 → Function.Injective fun x => B * x
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms an array of mappings into a tree map.  -/
Std.DTreeMap.Internal.Impl.Const.ofList : {α : Type u} → {β : Type v} → [Ord α] → List (α × β) → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Topology.ClopenBox
TopologicalSpace.Clopens.finite_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y]
  [CompactSpace X] [Finite (TopologicalSpace.Clopens X)] [Finite (TopologicalSpace.Clopens Y)],
  Finite (TopologicalSpace.Clopens (X × Y))
-- Mathlib.GroupTheory.Complement
/-- A right transversal is finite iff the subgroup has finite index.  -/
AddSubgroup.IsComplement.finite_right_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G},
  AddSubgroup.IsComplement (↑H) T → (Finite ↑T ↔ H.FiniteIndex)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced : ∀ {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] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpis]
  [F.ReflectsEffectiveEpis] [F.Full] [F.Faithful] [F.EffectivelyEnough] [inst_7 : CategoryTheory.Preregular D] (X : C)
  (S : CategoryTheory.Sieve X),
  (∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π) ↔ S ∈ (F.inducedTopology (CategoryTheory.regularTopology D)) X
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The vertical identity 2-square.  -/
CategoryTheory.TwoSquare.vId : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        (T : CategoryTheory.Functor C₁ C₂) →
          CategoryTheory.TwoSquare T (CategoryTheory.Functor.id C₁) (CategoryTheory.Functor.id C₂) T
-- Lean.Data.Lsp.Diagnostics
/-- Diagnostics representing a "goals accomplished" silent message.
Corresponds to `MessageData.tagged `goalsAccomplished ..`.
 -/
Lean.Lsp.LeanDiagnosticTag.goalsAccomplished : Lean.Lsp.LeanDiagnosticTag
-- Mathlib.RingTheory.Extension.Basic
/-- The cotangent is isomorphic to `S ⊗[P] I`.  -/
Algebra.Extension.cotangentEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → TensorProduct P.Ring S ↥P.ker ≃ₗ[S] P.Cotangent
-- Mathlib.Topology.Algebra.Monoid
Submonoid.isClosed_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M] (s : Submonoid M),
  IsClosed ↑s.topologicalClosure
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.instInhabited : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Inhabited (M ≃ₗ⁅R,L⁆ M)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.apply_symm_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S) (x : S),
  e (e.symm x) = x
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.mk.injEq : ∀ (mvarId : Lean.MVarId) (xs eqs eqsNew : List Lean.FVarId) (mvarId_1 : Lean.MVarId)
  (xs_1 eqs_1 eqsNew_1 : List Lean.FVarId),
  ({ mvarId := mvarId, xs := xs, eqs := eqs, eqsNew := eqsNew } =
      { mvarId := mvarId_1, xs := xs_1, eqs := eqs_1, eqsNew := eqsNew_1 }) =
    (mvarId = mvarId_1 ∧ xs = xs_1 ∧ eqs = eqs_1 ∧ eqsNew = eqsNew_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_mul_le_mul_right' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulRightReflectLE α] {a b c : α}, b * a ≤ c * a → b ≤ c
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary coproducts.  -/
CategoryTheory.Limits.preservesBinaryCoproduct_of_preservesBinaryBiproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : C} [CategoryTheory.Limits.PreservesBinaryBiproduct X Y F],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) F
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf.eq_1 : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X) (F : Set X),
  Dynamics.coverEntropyInf T F = ⨆ U ∈ uniformity X, Dynamics.coverEntropyInfEntourage T F U
-- Batteries.Control.Lemmas
StateT.run_throwThe : ∀ {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [inst : Monad m] [inst_1 : MonadExceptOf ε m] (e : ε)
  (s : σ),
  (throwThe ε e).run s = do
    let a ← throwThe ε e
    pure (a, s)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_inj_of_neg_pi_lt_of_le_pi : ∀ {x y : ℂ}, -Real.pi < x.im → x.im ≤ Real.pi → -Real.pi < y.im → y.im ≤ Real.pi → Complex.exp x = Complex.exp y → x = y
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Constant one function has product `1`  -/
hasProd_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  HasProd (fun x => 1) 1 L
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.next.eq_1 : ∀ (x : String.Pos.Raw) (s : String) (b stopPos : String.Pos.Raw),
  { str := s, startPos := b, stopPos := stopPos }.next x =
    if x.offsetBy b = stopPos then x else { byteIdx := (String.Pos.Raw.next s (x.offsetBy b)).byteIdx - b.byteIdx }
-- Mathlib.Algebra.Order.Group.PosPart
le_oneLePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), a ≤ a⁺ᵐ
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsStable.locally : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {p : (ι → Ω → E) → Prop} [inst_1 : OrderBot ι]
  [inst_2 : Zero E] [inst_3 : TopologicalSpace ι] [inst_4 : OrderTopology ι],
  ProbabilityTheory.IsStable 𝓕 p → ProbabilityTheory.IsStable 𝓕 fun Y => ProbabilityTheory.Locally p 𝓕 Y P
-- Init.Data.String.Basic
String.Slice.Pos.offset_le_offset_endExclusive : ∀ {s : String.Slice} {pos : s.Pos}, pos.offset ≤ s.endExclusive.offset
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_injective : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α], Function.Injective NNRat.cast
-- Mathlib.Algebra.Polynomial.Div
Polynomial.dvd_iff_isRoot : ∀ {R : Type u} {a : R} [inst : CommRing R] {p : Polynomial R}, Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_eq_zero : ∀ {α : Type u} {s : Stream'.Seq α} {h : s.Terminates}, s.length h = 0 ↔ s = Stream'.Seq.nil
-- Init.Data.SInt.Bitwise
Int64.toISize_not : ∀ (a : Int64), (~~~a).toISize = ~~~a.toISize
-- Init.Data.SInt.Basic
instMaxInt16 : Max Int16
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.getEntryLT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option ((a : α) × β a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_erase_eq_iff_not_compare_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (t.erase k).minKey he = t.minKey ⋯ ↔ ¬cmp k (t.minKey ⋯) = Ordering.eq
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `add_semigroup` across an `Equiv`  -/
Equiv.addSemigroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddSemigroup β] → AddSemigroup α
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_replicate_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {b : β},
  xs.mapFinIdx f = Array.replicate xs.size b ↔ ∀ (i : ℕ) (h : i < xs.size), f i xs[i] h = b
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra)
  [inst_2 : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))],
  (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).pt =
    F.obj (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A)))
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induce_spanningCoe : ∀ {V : Type u_1} {s : Set V} {G : SimpleGraph ↑s}, SimpleGraph.induce s G.spanningCoe = G
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.comp_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom₃ = CategoryTheory.CategoryStruct.comp f.hom₃ g.hom₃
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.id_hom' : ∀ {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] (M : CategoryTheory.Mod D A),
  (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.RepresentationTheory.Homological.Resolution
Fin.succAboveOrderEmb.eq_1 : ∀ {n : ℕ} (p : Fin (n + 1)), p.succAboveOrderEmb = OrderEmbedding.ofStrictMono p.succAbove ⋯
-- Mathlib.Order.Interval.Finset.Nat
Nat.decreasing_induction_of_infinite : ∀ {P : ℕ → Prop}, (∀ (n : ℕ), P (n + 1) → P n) → {x | P x}.Infinite → ∀ (n : ℕ), P n
-- Mathlib.Data.Set.Basic
Set.sup_eq_union : ∀ {α : Type u}, (fun x1 x2 => x1 ⊔ x2) = fun x1 x2 => x1 ∪ x2
-- Lean.Server.ServerTask
Lean.Server.instInhabitedServerTask.default : {α : Type u} → [Inhabited α] → Lean.Server.ServerTask α
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Restricts an affine isometry to an affine isometry equivalence between a nonempty affine
subspace `E` and its image.

This is an isometry version of `AffineSubspace.equivMap`, having a stronger premise and a stronger
conclusion.
 -/
AffineSubspace.isometryEquivMap : {𝕜 : Type u_1} →
  {V₁' : Type u_4} →
    {V₂ : Type u_5} →
      {P₁' : Type u_9} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V₁'] →
              [inst_2 : NormedSpace 𝕜 V₁'] →
                [inst_3 : MetricSpace P₁'] →
                  [inst_4 : NormedAddTorsor V₁' P₁'] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            (φ : P₁' →ᵃⁱ[𝕜] P₂) →
                              (E : AffineSubspace 𝕜 P₁') →
                                [inst_9 : Nonempty ↥E] → ↥E ≃ᵃⁱ[𝕜] ↥(AffineSubspace.map φ.toAffineMap E)
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_mem_addCommutatorSet : ∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ : G), ⁅g₁, g₂⁆ ∈ addCommutatorSet G