mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
instIsEquivalenceFGModuleCatUlift : ∀ (R : Type u) [inst : Ring R], (FGModuleCat.ulift R).IsEquivalence
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendHom.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X : C} (f : s.pt ⟶ X),
  s.extendHom f = { hom := f, w := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instEpiπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] (b : β),
  CategoryTheory.Epi (CategoryTheory.Limits.Sigma.π f b)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.leftPadAscii : ℕ → Char → String → String
-- Std.Data.HashSet.Basic
/-- Two hash sets are equivalent in the sense of `Equiv` iff all their values are equal.
 -/
Std.HashSet.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Algebra.Equiv
AlgHom.ulift_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S →ₐ[R] T) (x : ULift.{u_4, u_2} S),
  (AlgHom.ulift.{u_4, u_6, u_5, u_1, u_2, u_3} f) x = { down := f x.down }
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_symmDiff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
  a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_mem_matrix : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {S : Set α} {M : Matrix m n α} {r : l → m}
  {c : o → n}, M ∈ S.matrix → M.submatrix r c ∈ S.matrix
-- Qq.Match
Qq.Impl.mkNAryFunctionType : ℕ → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.eq_1 : ∀ (M : Type u_1) [inst : CommMonoid M], Algebra.GrothendieckGroup M = Localization ⊤
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.subset_coe_one : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : One M], 1 ⊆ ↑1
-- Mathlib.Topology.ContinuousOn
ContinuousOn.finSnoc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → (j : Fin n) → X j.castSucc} {g : α → X (Fin.last n)}
  {s : Set α}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun a => Fin.snoc (f a) (g a)) s
-- Mathlib.Data.Finset.Preimage
/-- Given an equivalence `e : α ≃ β` and `s : Finset β`, restrict `e` to an equivalence
from `e ⁻¹' s` to `s`.  -/
Equiv.restrictPreimageFinset : {α : Type u} → {β : Type v} → (e : α ≃ β) → (s : Finset β) → ↥(s.preimage ⇑e ⋯) ≃ ↥s
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_nonneg : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 ≤ a → 0 ≤ ConditionallyCompleteLinearOrderedField.inducedMap α β a
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.add_eq_sup : ∀ {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] (N N' : LieSubmodule R L M), N + N' = N ⊔ N'
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instNonUnitalNonAssocRing : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocRing A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalNonAssocSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] → [IsScalarTower R B B] → NonUnitalNonAssocRing (TensorProduct R A B)
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- The morphism  `K ⟶ L.extend e` given by a morphism `K.restriction e ⟶ L`
which satisfy `e.HasLift φ`.  -/
ComplexShape.Embedding.liftExtend : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  {K : HomologicalComplex C c'} →
                    {L : HomologicalComplex C c} →
                      [inst_3 : e.IsRelIff] → (φ : K.restriction e ⟶ L) → e.HasLift φ → (K ⟶ L.extend e)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiable_section_of_subsingleton : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x}
  [Subsingleton F], MDiff (T% s)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_4} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R) (f : α → ENNReal), ∫⁻ (a : α), f a ∂c • μ = c • ∫⁻ (a : α), f a ∂μ
-- Mathlib.Topology.Closure
Filter.HasBasis.lift'_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X},
  l.HasBasis p s → (l.lift' interior).HasBasis p fun i => interior (s i)
-- Lean.Meta.Tactic.Backtrack
/-- Attempts to solve the `goals`, by recursively calling `next` on each
subgoal that appears with a callback to reenter backtracking search.

Further flow control options are available via the `Config` argument.

Returns a list of subgoals which were "suspended" via the `suspend` or
`discharge` hooks in `Config`. In the default configuration, `backtrack`
will either return an empty list or fail.
 -/
Lean.Meta.Tactic.Backtrack.backtrack : optParam Lean.Meta.Tactic.Backtrack.BacktrackConfig { } →
  optParam Lean.Name Lean.Name.anonymous →
    (Lean.MVarId → Lean.MetaM (Lean.Meta.Iterator (List Lean.MVarId))) →
      List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.LinearAlgebra.Orientation
Orientation.map_symm : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  (ι : Type u_4) (e : M ≃ₗ[R] N), (Orientation.map ι e).symm = Orientation.map ι e.symm
-- Mathlib.Data.List.Duplicate
List.Duplicate.duplicate_cons : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l → ∀ (y : α), List.Duplicate x (y :: l)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_fst_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  [ProbabilityTheory.IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ),
  κ.densityProcess κ.fst n a x Set.univ = if (κ.fst a) (MeasurableSpace.countablePartitionSet n x) = 0 then 0 else 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_insert!_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).toList.Perm
        (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) t.toList)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).minKey? = t.minKey?
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_mem : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ (o : Ordinal.{u}), Ordinal.enumOrd s o ∈ s
-- Mathlib.Control.Fold
Monoid.Foldr : Type u → Type u
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.typeInfos : Lean.Elab.Deriving.Context → Array Lean.InductiveVal
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.List.next?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- A `BasedNatTrans` between two `BasedFunctor`s is a natural transformation `α` between the
underlying functors, such that for all `a : 𝒳`, `α.app a` lifts `𝟙 S` whenever `𝒳.p.obj a = S`.  -/
CategoryTheory.BasedNatTrans : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        CategoryTheory.BasedFunctor 𝒳 𝒴 → CategoryTheory.BasedFunctor 𝒳 𝒴 → Type (max u₂ v₃)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The functor `C ⥤ D` that is reconstructed for a morphism
between the `2`-truncated nerves.  -/
CategoryTheory.nerve.functorOfNerveMap : {C D : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.SmallCategory D] →
      (CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶
          CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D)) →
        CategoryTheory.Functor C D
-- Mathlib.Data.Num.Lemmas
PosNum.lt_to_nat : ∀ {m n : PosNum}, ↑m < ↑n ↔ m < n
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.curry_apply_succ : ∀ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → p i) → τ) (a : p 0),
  Function.FromTypes.curry f a = Function.FromTypes.curry (f ∘ Fin.cons a)
-- Batteries.Data.Char.AsciiCasing
/-- Bool-valued comparison of two `Char`s for *ASCII*-case insensitive equality.

```
#eval beqCaseInsensitiveAsciiOnly 'a' 'A' -- true
#eval beqCaseInsensitiveAsciiOnly 'a' 'a' -- true
#eval beqCaseInsensitiveAsciiOnly '$' '$' -- true
#eval beqCaseInsensitiveAsciiOnly 'a' 'b' -- false
#eval beqCaseInsensitiveAsciiOnly 'γ' 'Γ' -- false
#eval beqCaseInsensitiveAsciiOnly 'ä' 'Ä' -- false
```
 -/
Char.beqCaseInsensitiveAsciiOnly : Char → Char → Bool
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.vadd_mem_of_mem_closure_of_mem : ∀ {G : Type u_2} [inst : AddGroup G] {X : Type u_5} [inst_1 : AddAction G X] {s : Set G} {t : Set X},
  (∀ g ∈ s, -g ∈ s) →
    (∀ g ∈ s, ∀ x ∈ t, g +ᵥ x ∈ t) → ∀ {g : G}, g ∈ AddSubgroup.closure s → ∀ {x : X}, x ∈ t → g +ᵥ x ∈ t
-- Mathlib.Topology.ClusterPt
ClusterPt.top : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, ClusterPt x ⊤
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_neg_mem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ) {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.convexBodySum K B → -x ∈ NumberField.mixedEmbedding.convexBodySum K B
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.of.eq_1 : ∀ (M : Type u) [inst : AddGroup M], AddGrpCat.of M = { carrier := M, str := inst }
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- the step where the cell is added  -/
HomotopicalAlgebra.RelativeCellComplex.Cells.j : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} → {f : X ⟶ Y} → {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} → c.Cells → J
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.of_linearEquiv_type : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup S] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R S],
  IsIsotypicOfType R M S → ∀ (e : S ≃ₗ[R] N), IsIsotypicOfType R M N
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.Parser : Type
-- Mathlib.Topology.LocallyClosed
IsLocallyClosed.inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X},
  IsLocallyClosed s → IsLocallyClosed t → IsLocallyClosed (s ∩ t)
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.chebyshev_T_eq_dickson_one_one : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2] (n : ℕ),
  Polynomial.Chebyshev.T R ↑n = Polynomial.C ⅟2 * (Polynomial.dickson 1 1 n).comp (2 * Polynomial.X)
-- Mathlib.Data.Num.ZNum
ZNum.add_zero : ∀ (n : ZNum), n + 0 = n
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
FundamentalGroupoidFunctor.instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)}
  (H : f.Homotopy g), CategoryTheory.IsIso (FundamentalGroupoidFunctor.homotopicMapsNatIso H)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom_inv_id_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.hom) (CategoryTheory.Arrow.Hom.left e.inv) =
    CategoryTheory.CategoryStruct.id f.left
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.TaggedPrepartition.embedBox.congr_simp : ∀ {ι : Type u_1} (I J : BoxIntegral.Box ι) (h : I ≤ J),
  BoxIntegral.TaggedPrepartition.embedBox I J h = BoxIntegral.TaggedPrepartition.embedBox I J h
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A local diffeomorphism has open range.  -/
IsLocalDiffeomorph.isOpen_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f → IsOpen (Set.range f)
-- Mathlib.Algebra.Module.Basic
/-- If `E` is a vector space over a division ring `R` and has a monoid action by `α`, then that
action commutes by scalar multiplication of inverses of integers in `R`  -/
inv_intCast_smul_comm : ∀ {α : Type u_5} {E : Type u_6} (R : Type u_7) [inst : AddCommGroup E] [inst_1 : DivisionRing R] [inst_2 : Module R E]
  [inst_3 : DistribSMul α E] (n : ℤ) (s : α) (x : E), (↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocSemiring.mk : {α : Type u} →
  [toAddCommMonoid : AddCommMonoid α] →
    [toMul : Mul α] →
      (∀ (a b c : α), a * (b + c) = a * b + a * c) →
        (∀ (a b c : α), (a + b) * c = a * c + b * c) →
          (∀ (a : α), 0 * a = 0) → (∀ (a : α), a * 0 = 0) → NonUnitalNonAssocSemiring α
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A submodule has dimension `1` if and only if there is a
single non-zero vector in the submodule such that the submodule is contained in
its span.  -/
rank_submodule_eq_one_iff : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  (s : Submodule K V) [Module.Free K ↥s], Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (Z Z_1 : C),
  Z = Z_1 → CategoryTheory.ProjectiveResolution Z = CategoryTheory.ProjectiveResolution Z_1
-- Mathlib.LinearAlgebra.Complex.Module
le_iff_realPart_imaginaryPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a b : A},
  a ≤ b ↔ realPart a ≤ realPart b ∧ imaginaryPart a = imaginaryPart b
-- Mathlib.Data.Matrix.Basic
Matrix.sum_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddCommMonoid α] (i : m) (j : n) (s : Finset β)
  (g : β → Matrix m n α), (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j
-- Mathlib.Data.Set.Basic
Set.eq_empty_of_forall_notMem : ∀ {α : Type u} {s : Set α}, (∀ (x : α), x ∉ s) → s = ∅
-- Mathlib.Combinatorics.Graph.Maps
Graph.edgeSet_map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β), (Graph.map f G).edgeSet = G.edgeSet
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.postcomp_pi : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace β] [inst_1 : PseudoEMetricSpace γ]
  [inst_2 : Fintype α] {g : β → γ}, Isometry g → Isometry fun f => g ∘ f
-- Mathlib.CategoryTheory.Monad.Basic
/-- Construct a monad isomorphism from a natural isomorphism of functors where the forward
direction is a monad morphism.  -/
CategoryTheory.MonadIso.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {M N : CategoryTheory.Monad C} →
      (f : M.toFunctor ≅ N.toFunctor) →
        autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X)
            CategoryTheory.MonadIso.mk._auto_1 →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) =
                  CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X))
              CategoryTheory.MonadIso.mk._auto_3 →
            (M ≅ N)
-- Init.Data.UInt.Lemmas
USize.zero_add : ∀ (a : USize), 0 + a = a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variable to equation constraint used to eliminate it. `solved` variables should not occur in
`dvdCnstrs`, `lowers`, or `uppers`.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.elimEqs : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
-- Mathlib.Order.SymmDiff
bihimp_eq_bot : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b = ⊥ ↔ IsCompl a b
-- Mathlib.Algebra.Homology.Single
CochainComplex.single₀.congr_simp : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], CochainComplex.single₀ V = CochainComplex.single₀ V
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) (g : β → α)
  [inst_1 : UniformSpace α], HasProdUniformly f g = HasProd (⇑UniformFun.ofFun ∘ f) (UniformFun.ofFun g)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.cancel_left_of_respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [hP : P.RespectsIso]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f], P (CategoryTheory.CategoryStruct.comp f g) ↔ P g
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.Quasicategory₂.mk : ∀ {X : SSet.Truncated 2},
  (∀ {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
      (e₀₁ : SSet.Truncated.Edge x₀ x₁) (e₁₂ : SSet.Truncated.Edge x₁ x₂),
      Nonempty ((e₀₂ : SSet.Truncated.Edge x₀ x₂) × e₀₁.CompStruct e₁₂ e₀₂)) →
    (∀ {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
        {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₂₃ : SSet.Truncated.Edge x₂ x₃}
        {e₀₂ : SSet.Truncated.Edge x₀ x₂} {e₁₃ : SSet.Truncated.Edge x₁ x₃} {e₀₃ : SSet.Truncated.Edge x₀ x₃}
        (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃),
        Nonempty (e₀₂.CompStruct e₂₃ e₀₃)) →
      (∀ {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
          {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₂₃ : SSet.Truncated.Edge x₂ x₃}
          {e₀₂ : SSet.Truncated.Edge x₀ x₂} {e₁₃ : SSet.Truncated.Edge x₁ x₃} {e₀₃ : SSet.Truncated.Edge x₀ x₃}
          (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃),
          Nonempty (e₀₁.CompStruct e₁₃ e₀₃)) →
        X.Quasicategory₂
-- Init.Data.Ord.Basic
Ordering.isLT_swap : ∀ {o : Ordering}, o.swap.isLT = o.isGT
-- Init.Data.SInt.Bitwise
Int64.toISize_or : ∀ (a b : Int64), (a ||| b).toISize = a.toISize ||| b.toISize
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_mul_le_left : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f g : A), ProjectiveSpectrum.basicOpen 𝒜 (f * g) ≤ ProjectiveSpectrum.basicOpen 𝒜 f
-- Mathlib.CategoryTheory.Subobject.FactorThru
/-- `P.factorThru f h` provides a factorisation of `f : X ⟶ Y` through some `P : Subobject Y`,
given the evidence `h : P.Factors f` that such a factorisation exists.  -/
CategoryTheory.Subobject.factorThru : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (P : CategoryTheory.Subobject Y) → (f : X ⟶ Y) → P.Factors f → (X ⟶ CategoryTheory.Subobject.underlying.obj P)
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomapDomain f hf` is the linear map
sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing
`l` with `f`.

This is the linear version of `Finsupp.comapDomain`.  -/
Finsupp.lcomapDomain : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → {β : Type u_9} → (f : α → β) → Function.Injective f → (β →₀ M) →ₗ[R] α →₀ M
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- The second projection.  -/
CategoryTheory.PreZeroHypercover.Relation.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → {E : CategoryTheory.PreZeroHypercover S} → {i j : E.I₀} → (self : E.Relation i j) → self.obj ⟶ E.X j
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
ContinuousLinearEquiv.compactConvergenceCLMCongr_apply : ∀ {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H] [inst_4 : NormedField 𝕜]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : Module 𝕜 G] [inst_8 : Module 𝕜 H] [inst_9 : TopologicalSpace E]
  [inst_10 : TopologicalSpace F] [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace H]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : IsTopologicalAddGroup H] [inst_15 : ContinuousConstSMul 𝕜 G]
  [inst_16 : ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (φ : CompactConvergenceCLM (RingHom.id 𝕜) E H)
  (f : F), ((e₁.compactConvergenceCLMCongr e₂) φ) f = e₂ (φ (e₁.symm f))