mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- If a morphism of short complexes `φ : S₁ ⟶ S₂` is such that `φ.τ₁` is epi, `φ.τ₂` is an iso,
and `φ.τ₃` is mono, then the induced morphism on left homology is an isomorphism.  -/
CategoryTheory.ShortComplex.instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap φ)
-- Mathlib.Analysis.Convex.Strict
/-- The translation of a strictly convex set is also strictly convex.  -/
StrictConvex.vadd : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [ContinuousAdd E] {s : Set E},
  StrictConvex 𝕜 s → ∀ (x : E), StrictConvex 𝕜 (x +ᵥ s)
-- Init.Data.List.Lemmas
List.getLast_eq_getElem : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast h = l[l.length - 1]
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.prod_le_prod' : ∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] {l : List ι}
  {f g : ι → M}, (∀ i ∈ l, f i ≤ g i) → (List.map f l).prod ≤ (List.map g l).prod
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_of_ae_restrict_of_subset : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {p : α → Prop},
  s ⊆ t → (∀ᵐ (x : α) ∂μ.restrict t, p x) → ∀ᵐ (x : α) ∂μ.restrict s, p x
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ClosedComplemented.isCompl_complement : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M} (h : p.ClosedComplemented), IsCompl p h.complement
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.left : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (e : TensorProduct R M N ≃ₗ[R] R), Module.Invertible R M
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_def : ∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S], p.aroots S = (Polynomial.map (algebraMap T S) p).roots
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofEquivalence_χ₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (𝒞₁ : CategoryTheory.Subobject.Classifier C) (e : C ≌ D) (Y : D),
  (𝒞₁.ofEquivalence e).χ₀ Y =
    CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.functor.map (𝒞₁.χ₀ (e.inverse.obj Y)))
-- Mathlib.Order.Category.BddOrd
bddOrd_dual_comp_forget_to_partOrd : BddOrd.dual.comp (CategoryTheory.forget₂ BddOrd PartOrd) = (CategoryTheory.forget₂ BddOrd PartOrd).comp PartOrd.dual
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.op_vadd_finset_subset_add : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α}, a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.erase.sizeOf_spec : ∀ (toErase : Lean.Meta.Origin), sizeOf (Lean.Elab.Tactic.ElabSimpArgResult.erase toErase) = 1 + sizeOf toErase
-- Init.Data.Array.Find
Array.of_findIdx?_eq_some : ∀ {α : Type u_1} {i : ℕ} {xs : Array α} {p : α → Bool},
  Array.findIdx? p xs = some i →
    match xs[i]? with
    | some a => p a = true
    | none => false = true
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.iff_comap_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f ↔ Function.Injective f ∧ MeasurableSpace.comap f inst_1 = inst ∧ MeasurableSet (Set.range f)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_ae_eq_trim_condExp : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) {s : Set Ω},
  MeasurableSet s →
    (fun ω => ((ProbabilityTheory.condExpKernel μ m) ω).real s) =ᵐ[μ.trim hm] μ[s.indicator fun ω => 1 | m]
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.sat_iff : ∀ {assign : ℕ → Bool} {aig : Std.Sat.AIG ℕ} {state : Std.Sat.AIG.toCNF.State✝ aig},
  Std.Sat.AIG.toCNF.State.Sat✝ assign state ↔ Std.Sat.CNF.Sat assign (Std.Sat.AIG.toCNF.State.cnf✝ state)
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {V W : CoalgCat R} {x y : V.Hom W}, x = y ↔ x.toCoalgHom' = y.toCoalgHom'
-- Mathlib.Algebra.Order.Ring.WithTop
/-- `Nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`.  -/
WithBot.instMulZeroOneClass : {α : Type u_1} → [DecidableEq α] → [MulZeroOneClass α] → [Nontrivial α] → MulZeroOneClass (WithBot α)
-- Mathlib.Topology.UniformSpace.Defs
/-- An alternative constructor for `UniformSpace.Core`. This version unfolds various
`Filter`-related definitions.  -/
UniformSpace.Core.mk' : {α : Type u} →
  (U : Filter (α × α)) →
    (∀ r ∈ U, ∀ (x : α), (x, x) ∈ r) →
      (∀ r ∈ U, Prod.swap ⁻¹' r ∈ U) → (∀ r ∈ U, ∃ t ∈ U, SetRel.comp t t ⊆ r) → UniformSpace.Core α
-- Lean.Util.MonadCache
/-- If entry `a := b` is already in the cache, then return `b`.
Otherwise, execute `b ← f ()`, store `a := b` in the cache and return `b`.  -/
Lean.checkCache : {α β : Type} → {m : Type → Type} → [Lean.MonadCache α β m] → [Monad m] → α → (Unit → m β) → m β
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_lineMap_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) (c : ℝ),
  ((signedDist v) ((AffineMap.lineMap p q) c)) q = (1 - c) * ((signedDist v) p) q
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.isStrictMap_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E]
  [ContinuousSMul 𝕜 E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [inst_10 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F] [FiniteDimensional 𝕜 F] (f : E →L[𝕜] F),
  Topology.IsStrictMap ⇑f
-- Mathlib.Order.Category.BddLat
/-- The functor that adds a bottom and a top element to a lattice. This is the free functor.  -/
latToBddLat : CategoryTheory.Functor Lat BddLat
-- Mathlib.Algebra.Order.SuccPred.PartialSups
/-- See `partialSups_add_one` for another decomposition of `partialSups f (i + 1)`.  -/
partialSups_add_one' : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : LinearOrder ι] [inst_2 : Add ι] [inst_3 : One ι]
  [inst_4 : OrderBot ι] [inst_5 : LocallyFiniteOrder ι] [SuccAddOrder ι] (f : ι → α) (i : ι),
  (partialSups f) (i + 1) = f ⊥ ⊔ (partialSups (f ∘ fun k => k + 1)) i
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.lift_unique : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A] (I : Ideal B),
  IsNilpotent I → ∀ (g₁ g₂ : A →ₐ[R] B), (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂ → g₁ = g₂
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.forget_obj`. -/
CommSemiRingCat.forget_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] (X : C), (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
-- Mathlib.Algebra.Group.Irreducible.Defs
/-- An irreducible element is not a unit.  -/
Irreducible.not_isUnit : ∀ {M : Type u_1} [inst : Monoid M] {p : M}, Irreducible p → ¬IsUnit p
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instInhabitedNormCastExtension.default : Lean.Meta.NormCast.NormCastExtension
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_mul : ∀ {i : Lean.Grind.IntInterval}, i.isFinite = true → ∀ (x y : ℤ), i.wrap (x * y) = i.wrap (i.wrap x * i.wrap y)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.comp_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D)
  (a : B), (F.comp G).mapId a = G.map₂Iso (F.mapId a) ≪≫ G.mapId (F.obj a)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_naturality : ∀ {X : SSet} {m n : SimplexCategory} (f : m ⟶ n) (g : SSet.stdSimplex.obj n ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (SSet.yonedaEquiv g) =
    SSet.yonedaEquiv (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map f) g)
-- Mathlib.Order.Filter.Lift
Filter.map_lift'_eq2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β},
  Monotone g → (Filter.map m f).lift' g = f.lift' (g ∘ Set.image m)
-- Mathlib.Order.Preorder.Chain
Flag.coe_ofIsMaxChain : ∀ {α : Type u_1} [inst : LE α] (c : Set α) (hc : IsMaxChain (fun x1 x2 => x1 ≤ x2) c), ↑(Flag.ofIsMaxChain c hc) = c
-- Mathlib.Algebra.Lie.Prod
LieHom.inr_eq_prod : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], LieHom.inr R L₁ L₂ = LieHom.prod 0 LieHom.id
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.eq_1 : ∀ {V : Type u} (G : SimpleGraph V), G.Preconnected = ∀ (u v : V), G.Reachable u v
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.mem_comap : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} {x : L},
  x ∈ LieIdeal.comap f J ↔ f x ∈ J
-- Init.Data.UInt.Bitwise
UInt32.xor_comm : ∀ (a b : UInt32), a ^^^ b = b ^^^ a
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan), CategoryTheory.Bicategory.HasLeftKanLift f g
-- Init.Data.Array.Range
Array.zipIdx_map_snd : ∀ {α : Type u_1} (i : ℕ) (xs : Array α), Array.map Prod.snd (xs.zipIdx i) = Array.range' i xs.size
-- Mathlib.Logic.OpClass
RightCommutative.mk : ∀ {α : Sort u} {β : Sort v} {op : β → α → β},
  (∀ (b : β) (a₁ a₂ : α), op (op b a₁) a₂ = op (op b a₂) a₁) → RightCommutative op
-- Mathlib.Logic.Basic
ite_eq_iff' : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b c : α}, (if P then a else b) = c ↔ (P → a = c) ∧ (¬P → b = c)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.map.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f f_1 : P.Hom P'),
  f = f_1 → Algebra.Extension.H1Cotangent.map f = Algebra.Extension.H1Cotangent.map f_1
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (r : R) (f : N →ₗ[R] P), LinearMap.rTensor M (r • f) = r • LinearMap.rTensor M f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_getElem?_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t[a]?.isSome = true ↔ a ∈ t
-- Mathlib.Order.MinMax
min_le_of_right_le : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, c ≤ a → min b c ≤ a
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` is monotone on the positive axis.  -/
Real.monotoneOn_posLog : MonotoneOn Real.posLog (Set.Ici 0)
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.isClosed : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (x : A), IsClosed ↑(Algebra.elemental R x)
-- Init.Core
/-- `Empty.elim : Empty → C` says that a value of any type can be constructed from
`Empty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
 -/
Empty.elim : {C : Sort u} → Empty → C
-- Mathlib.Analysis.Convex.Mul
ConvexOn.smul_concaveOn' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F}
  [IsOrderedModule 𝕜 E],
  ConvexOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → MonovaryOn f g s → ConvexOn 𝕜 s (f • g)
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_of_mul : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (a b : ℤ) (f : ModularForm Γ a) (g : ModularForm Γ b),
        UpperHalfPlane.qExpansion h
            ⇑(((DirectSum.of (ModularForm Γ) a) f * (DirectSum.of (ModularForm Γ) b) g) (a + b)) =
          UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, we have that `λ ^ 2` divides `S'.c`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.lambda_sq_dvd_c : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  (hζ.toInteger - 1) ^ 2 ∣ FermatLastTheoremForThreeGen.Solution'.c✝ S'
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_smul_nonzero : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R), a ≠ 0 → (a • p).roots = p.roots
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.mk.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {state : Std.Http.Protocol.H1.Reader.State dir} {input : ByteArray.Iterator}
  {messageHead : Std.Http.Protocol.H1.Message.Head dir} {messageCount bodyBytesRead headerBytesRead : ℕ}
  {noMoreInput : Bool} {state_1 : Std.Http.Protocol.H1.Reader.State dir} {input_1 : ByteArray.Iterator}
  {messageHead_1 : Std.Http.Protocol.H1.Message.Head dir} {messageCount_1 bodyBytesRead_1 headerBytesRead_1 : ℕ}
  {noMoreInput_1 : Bool},
  { state := state, input := input, messageHead := messageHead, messageCount := messageCount,
        bodyBytesRead := bodyBytesRead, headerBytesRead := headerBytesRead, noMoreInput := noMoreInput } =
      { state := state_1, input := input_1, messageHead := messageHead_1, messageCount := messageCount_1,
        bodyBytesRead := bodyBytesRead_1, headerBytesRead := headerBytesRead_1, noMoreInput := noMoreInput_1 } →
    state = state_1 ∧
      input = input_1 ∧
        messageHead = messageHead_1 ∧
          messageCount = messageCount_1 ∧
            bodyBytesRead = bodyBytesRead_1 ∧ headerBytesRead = headerBytesRead_1 ∧ noMoreInput = noMoreInput_1
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_uIcc : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  NNRat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π (α.app X))
        ((CategoryTheory.Limits.cokernel.π α).app X) (CategoryTheory.CategoryStruct.id (G.obj X))
        (CategoryTheory.Limits.cokernelComparison α ((CategoryTheory.evaluation C D).obj X)) ⋯)
      (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X)
          (CategoryTheory.Limits.cokernel.π α)).inv
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.union_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₁).Equiv ↑m₂ → (↑(m₁.union m₃)).Equiv ↑(m₂.union m₃)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  (NumberField.mixedEmbedding K) ↑↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a) = ↑a
-- Mathlib.Topology.ContinuousOn
continuousOn_pi : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_5} {X : ι → Type u_6}
  [inst_1 : (i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) → X i} {s : Set α},
  ContinuousOn f s ↔ ∀ (i : ι), ContinuousOn (fun y => f y i) s
-- Init.Data.SInt.Lemmas
instAssociativeInt16HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_fmod_self_right : ∀ (a b c : ℤ), (a * b + c).fmod b = c.fmod b
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.instDecidableMem : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → {x : α} → {s : Aesop.OrderedHashSet α} → Decidable (x ∈ s)
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The condition that the image of the map `e.f` of an embedding of
complex shapes `e : Embedding c c'` is stable by `c'.next`.  -/
ComplexShape.Embedding.IsTruncGE : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → Prop
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.mkUnfoldEq.doRealize : Lean.Name → Lean.Elab.Structural.EqnInfo → Lean.Name → Lean.MetaM Unit
-- Init.Data.List.Basic
List.flatMap_nil : ∀ {α : Type u} {β : Type v} {f : α → List β}, List.flatMap f [] = []
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).minKey? =
        Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.minKey?
-- Lean.Elab.InfoTree.Main
Lean.Elab.instToFormatCustomInfo : Std.ToFormat Lean.Elab.CustomInfo
-- Mathlib.Topology.UniformSpace.Equiv
/-- **Alias** of `UniformEquiv.prodPUnit`.

---

`α × {*}` is uniformly isomorphic to `α`.  -/
UniformEquiv.prodPunit : (α : Type u) → [inst : UniformSpace α] → α × PUnit.{u_4 + 1} ≃ᵤ α
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_whiskerLeft : ∀ {R : Type u} [inst : CommSemiring R] (L : SemimoduleCat R) {M N : SemimoduleCat R} (f : M ⟶ N),
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) =
    LinearMap.lTensor (↑L) (SemimoduleCat.Hom.hom f)
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.mk.sizeOf_spec : ∀ (type : Lean.Lsp.MessageType) (message : String) (actions? : Option (Array Lean.Lsp.MessageActionItem)),
  sizeOf { type := type, message := message, actions? := actions? } = 1 + sizeOf type + sizeOf message + sizeOf actions?
-- Mathlib.Order.RelIso.Basic
RelEmbedding.refl_apply : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), (RelEmbedding.refl r) a = a
-- Init.Coe
/-- `⇑ t` coerces `t` to a function.  -/
coeFunNotation : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α}
  [CompleteSpace α], Multipliable f → ∀ (s : Set β), Multipliable (s.mulIndicator f)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance2.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : α) →
        (x_2 : RBTree.RBNode α) →
          ((a : RBTree.RBNode α) →
              (x : α) →
                (b : RBTree.RBNode α) →
                  (y : α) →
                    (c : RBTree.RBNode α) →
                      (z : α) →
                        (d : RBTree.RBNode α) →
                          motive a x
                            (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d))) →
            ((a : RBTree.RBNode α) →
                (x : α) →
                  (b : RBTree.RBNode α) →
                    (y : α) →
                      (c : RBTree.RBNode α) →
                        (z : α) →
                          (d : RBTree.RBNode α) →
                            (∀ (c : RBTree.RBNode α) (z : α) (d_1 : RBTree.RBNode α),
                                d = RBTree.RBNode.node RBTree.RBColor.red c z d_1 → False) →
                              motive a x
                                (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z
                                  d)) →
              ((a : RBTree.RBNode α) →
                  (x : α) →
                    (b : RBTree.RBNode α) →
                      (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
                          b =
                              RBTree.RBNode.node RBTree.RBColor.red b_1 y
                                (RBTree.RBNode.node RBTree.RBColor.red c z d) →
                            False) →
                        (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
                            b =
                                RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b_1 y c) z
                                  d →
                              False) →
                          motive a x b) →
                motive x x_1 x_2
-- Mathlib.Algebra.Star.StarRingHom
/-- If a (unital or non-unital) star ring morphism has an inverse, it is an isomorphism of
star rings.  -/
StarRingEquiv.ofStarRingHom : {F : Type u_1} →
  {G : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : NonUnitalNonAssocSemiring A] →
          [inst_1 : Star A] →
            [inst_2 : NonUnitalNonAssocSemiring B] →
              [inst_3 : Star B] →
                [inst_4 : FunLike F A B] →
                  [inst_5 : NonUnitalRingHomClass F A B] →
                    [NonUnitalStarRingHomClass F A B] →
                      [inst_7 : FunLike G B A] →
                        (f : F) → (g : G) → (∀ (x : A), g (f x) = x) → (∀ (x : B), f (g x) = x) → A ≃⋆+* B
-- 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.Roi.iter : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.Roi α → Std.Iter α