mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_const : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  m ≤ m₀ → ∀ (c : ℝ), ProbabilityTheory.condVar m (fun x => c) μ = 0
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Define a morphism between left lifts by cancelling the whiskered identities.  -/
CategoryTheory.Bicategory.LeftLift.whiskerIdCancel : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (s :
              CategoryTheory.Bicategory.LeftLift f
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) →
            {t : CategoryTheory.Bicategory.LeftLift f g} →
              (s ⟶ t.whisker (CategoryTheory.CategoryStruct.id c)) → (s.ofIdComp ⟶ t)
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing : optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- **Alias** of `UniformFun.isClosed_setOfPred_continuous`.

---

The set of continuous functions is closed in the uniform convergence topology.
This is a simple wrapper over `TendstoUniformly.continuous`.  -/
UniformFun.isClosed_setOf_continuous : ∀ (α : Type u_1) {β : Type u_2} [inst : UniformSpace β] [inst_1 : TopologicalSpace α],
  IsClosed {f | Continuous (UniformFun.toFun f)}
-- Lean.Data.KVMap
Lean.DataValue.ofNat.inj : ∀ {v v_1 : ℕ}, Lean.DataValue.ofNat v = Lean.DataValue.ofNat v_1 → v = v_1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as
a filter basis, for any basis `𝓑` of `𝓤 β` (in the case `𝓑 = (𝓤 β).as_basis` this is true by
definition).  -/
UniformFun.hasBasis_uniformity_of_basis : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set (β × β)},
  (uniformity β).HasBasis p s → (uniformity (UniformFun α β)).HasBasis p (UniformFun.gen α β ∘ s)
-- Aesop.Tree.RunMetaM
Aesop.Goal.runMetaMInParentState : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Goal → m (α × Lean.Meta.SavedState)
-- Mathlib.FieldTheory.Perfect
frobenius.eq_1 : ∀ (R : Type u_3) [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p],
  frobenius R p = { toMonoidHom := powMonoidHom p, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.ext : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {f g : AddConstMap G H a b},
  (∀ (x : G), f x = g x) → f = g
-- Mathlib.RingTheory.MvPolynomial.Localization
/-- The canonical algebra isomorphism from `MvPolynomial Unit R` quotiented by
`C r * X () - 1` to the localization of `R` away from `r`.  -/
IsLocalization.Away.mvPolynomialQuotientEquiv : {R : Type u_2} →
  [inst : CommRing R] →
    (S : Type u_3) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            [IsLocalization.Away r S] →
              (MvPolynomial Unit R ⧸ Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1}) ≃ₐ[R] S
-- Lean.Meta.Tactic.Symm
/-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
add a hypothesis `h_symm : b ~ a`.  -/
Lean.MVarId.symmSaturate : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Group.Indicator
Set.indicator_neg : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] (s : Set α) (f : α → G),
  (s.indicator fun a => -f a) = fun a => -s.indicator f a
-- Init.Data.List.Monadic
List.zipWithM.loop.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x : List α)
  (x_1 : List β) (x_2 : Array γ),
  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
    List.zipWithM.loop f x x_1 x_2 = pure x_2.toList
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.inv : ∀ {x : ℝ*} {r : ℝ}, ¬x.Infinitesimal → x.IsSt r → x⁻¹.IsSt r⁻¹
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_inj : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I I' : Ideal R} {J J' : Ideal S},
  I.prod J = I'.prod J' ↔ I = I' ∧ J = J'
-- Mathlib.Algebra.Group.Action.Defs
/-- Given a tower of additive actions `M → α → β`, if we use `SMul.comp` to pull back both of
`M`'s actions by a map `g : N → M`, then we obtain a new tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables.  -/
VAdd.comp.vaddAssocClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] [inst_2 : VAdd α β]
  [VAddAssocClass M α β] (g : N → M), VAddAssocClass N α β
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.Q.liftOn₂.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] {β : Sort u_1} (q₁ q₂ : Lean.Grind.IntModule.OfNatModule.Q α)
  (f : α × α → α × α → β)
  (h :
    ∀ {a₁ b₁ a₂ b₂ : α × α},
      Lean.Grind.IntModule.OfNatModule.r α a₁ a₂ → Lean.Grind.IntModule.OfNatModule.r α b₁ b₂ → f a₁ b₁ = f a₂ b₂),
  q₁.liftOn₂ q₂ f h = Quot.lift (fun a₁ => Quot.lift (f a₁) ⋯ q₂) ⋯ q₁
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The double dual of a dually finitely generated cone is the cone itself.  -/
PointedCone.DualFG.dual_dual_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N},
  PointedCone.DualFG p C → PointedCone.dual p ↑(PointedCone.dual p.flip ↑C) = C
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An `AddSubsemigroup` of an `AddCommSemigroup` is an `AddCommSemigroup`.  -/
AddMemClass.toAddCommSemigroup : {M : Type u_5} →
  [inst : AddCommSemigroup M] →
    {A : Type u_4} → [inst_1 : SetLike A M] → [AddMemClass A M] → (S : A) → AddCommSemigroup ↥S
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_anti_set_of_le_one' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} [MulLeftMono N],
  (∀ (x : ι), f x ≤ 1) → Antitone fun s => ∏ x ∈ s, f x
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Let `M` be an `R`-module, and `f` an `R`-linear endomorphism of `M`.
For `k : ℕ∞`, we define `UnifEigenvalues f k` to be the type of all
`μ : R` that satisfy `f.HasUnifEigenvalue μ k`.

For `k = 1` this is the type of all eigenvalues of `f`.  -/
Module.End.UnifEigenvalues : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → ℕ∞ → Type v
-- Mathlib.Topology.Constructions.SumProd
/-- If `f` and `g` are embeddings whose ranges are separated, `Sum.elim f g` is an embedding.  -/
Topology.IsEmbedding.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsEmbedding f →
    Topology.IsEmbedding g →
      Disjoint (closure (Set.range f)) (Set.range g) →
        Disjoint (Set.range f) (closure (Set.range g)) → Topology.IsEmbedding (Sum.elim f g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α}, a ∈ (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl → a ∈ t
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The sheaf condition in terms of an equalizer diagram is equivalent
to the reformulation in terms of the presheaf preserving the limit of the diagram
consisting of the `U i` and `U i ⊓ U j`.
 -/
TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections
-- Mathlib.Order.ModularLattice
IsWeakLowerModularLattice.mk : ∀ {α : Type u_2} [inst : Lattice α], (∀ {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a) → IsWeakLowerModularLattice α
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.one_kronecker_one : ∀ {α : Type u_3} {m : Type u_10} {n : Type u_11} [inst : MulZeroOneClass α] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n], Matrix.kroneckerMap (fun x1 x2 => x1 * x2) 1 1 = 1
-- Mathlib.Order.Minimal
OrderEmbedding.minimal_apply_mem_inter_range_iff : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {f : α ↪o β} {t : Set β},
  Minimal (fun x => x ∈ t ∩ Set.range ⇑f) (f x) ↔ Minimal (fun x => f x ∈ t) x
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of `AddMonoid`s
commutes.  -/
AddCon.lift_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
  (H : c ≤ AddCon.ker f) (x : M), (c.lift f H) (c.mk' x) = f x
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_tsub_assoc : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → c ≤ b → a - (b - c) = a - b + c
-- Mathlib.CategoryTheory.Quotient.Linear
CategoryTheory.Quotient.Linear.smul_eq : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (r : HomRel C)
  [inst_4 : CategoryTheory.Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂))
  (a : R) {X Y : C} (f : X ⟶ Y),
  a • (CategoryTheory.Quotient.functor r).map f = (CategoryTheory.Quotient.functor r).map (a • f)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.whiskeringLeftFunctor'_obj : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F : CategoryTheory.Functor D E),
  (CategoryTheory.Localization.whiskeringLeftFunctor' L W E).obj F = L.comp F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.congr_left : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ t₃ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.sum.map_mul : ∀ {α : Type u} [inst : AddGroup α] {x y : FreeGroup α}, (x * y).sum = x.sum + y.sum
-- Mathlib.Topology.Compactness.Compact
/-- If `V : ι → Set X` is a decreasing family of closed compact sets then any neighborhood of
`⋂ i, V i` contains some `V i`. We assume each `V i` is compact *and* closed because `X` is
not assumed to be Hausdorff. See `exists_subset_nhds_of_compact` for version assuming this.  -/
exists_subset_nhds_of_isCompact' : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] [Nonempty ι] {V : ι → Set X},
  Directed (fun x1 x2 => x1 ⊇ x2) V →
    (∀ (i : ι), IsCompact (V i)) →
      (∀ (i : ι), IsClosed (V i)) → ∀ {U : Set X}, (∀ x ∈ ⋂ i, V i, U ∈ nhds x) → ∃ i, V i ⊆ U
-- Lean.ProjFns
Lean.AuxParentProjectionInfo.mk.inj : ∀ {numParams : ℕ} {fromClass : Bool} {numParams_1 : ℕ} {fromClass_1 : Bool},
  { numParams := numParams, fromClass := fromClass } = { numParams := numParams_1, fromClass := fromClass_1 } →
    numParams = numParams_1 ∧ fromClass = fromClass_1
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAt.const_smul` -/
HasFDerivAt.fun_const_smul : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasFDerivAt f f' x → ∀ (c : R), HasFDerivAt (fun i => c • f i) (c • f') x
-- Mathlib.Data.Finset.Sum
Finset.inr_mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {b : β}, Sum.inr b ∈ s.disjSum t ↔ b ∈ t
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a countable family of extended metric spaces,
one may put an extended distance on their product `Π i, E i`.

It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`.  -/
PiCountable.edist : {ι : Type u_2} → [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → EDist (F i)] → EDist ((i : ι) → F i)
-- Batteries.Lean.LawfulMonad
instLawfulMonadMetaM_batteries : LawfulMonad Lean.MetaM
-- Init.Data.String.Modify
String.Pos.set_eq_append : ∀ {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos},
  p.set c hp = (s.sliceTo p).copy ++ String.singleton c ++ (s.sliceFrom (p.next hp)).copy
-- Init.Data.Ord.Basic
Ordering.isLT_eq : Ordering.eq.isLT = false
-- Mathlib.Topology.Inseparable
SeparationQuotient.range_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Set.range SeparationQuotient.mk = Set.univ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ofList_nil : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.DTreeMap.Raw.ofList [] cmp = ∅
-- Lean.Syntax
Lean.Syntax.instBEqRange.beq : Lean.Syntax.Range → Lean.Syntax.Range → Bool
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- The measures that we order lexicographically can be comparing basic measures,
or numbering the functions  -/
Lean.Elab.WF.GuessLex.MutualMeasure : Type
-- Mathlib.Order.SuccPred.LinearLocallyFinite
injective_toZ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι}, Function.Injective (toZ i0)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD.eq_1 : ∀ {α : Type u} (d : α) (x : WithOne α), WithOne.unoneD d x = WithOne.recOneCoe d id x
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Ioo : ∀ {n : ℕ} (i j : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Ioo i j) = Finset.Ioo j.rev i.rev
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHomClass.toOrderMonoidHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : FunLike F α β] [inst_5 : OrderHomClass F α β] [inst_6 : MonoidHomClass F α β]
  (f : F), ↑f = { toMonoidHom := ↑f, monotone' := ⋯ }
-- Mathlib.RingTheory.Etale.Field
/-- This is a weaker version of `of_isSeparable` that additionally assumes `EssFiniteType K L`.
Use that instead.

This is Iversen Corollary II.5.3.
 -/
Algebra.FormallyEtale.of_isSeparable_aux : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L]
  [Algebra.EssFiniteType K L], Algebra.FormallyEtale K L
-- Mathlib.Algebra.Group.Submonoid.Basic
AddMonoidHom.eq_of_eqOn_denseM : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {s : Set M},
  AddSubmonoid.closure s = ⊤ → ∀ {f g : M →+ N}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Init.Data.Fin.Lemmas
Fin.val_sub : ∀ {n : ℕ} (a b : Fin n), ↑(a - b) = (n - ↑b + ↑a) % n
-- Lean.Compiler.IR.Basic
Lean.IR.instReprParam : Repr Lean.IR.Param
-- Mathlib.Data.PNat.Prime
PNat.Coprime.mul_right : ∀ {k m n : ℕ+}, k.Coprime m → k.Coprime n → k.Coprime (m * n)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.LawfulBackwardPattern.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat],
  (∀ {s : String.Slice} (h : s.isEmpty = false),
      String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? pat s h =
        String.Slice.Pattern.BackwardPattern.skipSuffix? pat s) →
    (∀ (s : String.Slice),
        String.Slice.Pattern.BackwardPattern.endsWith pat s =
          (String.Slice.Pattern.BackwardPattern.skipSuffix? pat s).isSome) →
      String.Slice.Pattern.LawfulBackwardPattern pat
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_two_lt_d9 : Real.log 2 < 0.6931471808
-- Mathlib.Topology.Algebra.Monoid
exists_nhds_zero_half : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [ContinuousAdd M] {s : Set M},
  s ∈ nhds 0 → ∃ V ∈ nhds 0, ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s t : Set E}, AbsConvex 𝕜 s → AbsConvex 𝕜 t → AbsConvex 𝕜 (s ∩ t)
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_neg_natCast : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] (d : ℕ), selfZPow x B (-↑d) = IsLocalization.mk' B 1 (Submonoid.pow x d)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.right =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_eq_zero_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : ↥(lp E p)},
  ‖f‖ = 0 ↔ f = 0
-- Init.Data.BitVec.Lemmas
BitVec.append_assoc' : ∀ {w₁ w₂ w₃ : ℕ} {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ (x₂ ++ x₃) = BitVec.cast ⋯ (x₁ ++ x₂ ++ x₃)
-- Mathlib.ModelTheory.Definability
/-- A k-ary `TermDefinable` function composed with k `TermDefinable` others is `TermDefinable`.  -/
Set.TermDefinable.comp : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
  {f : (α → M) → M} {g : α → (β → M) → M},
  A.TermDefinable L f → (∀ (i : α), A.TermDefinable L (g i)) → A.TermDefinable L fun b => f fun x => g x b
-- Mathlib.Algebra.Quandle
/-- A quick way to convert a `PreEnvelGroupRel'` to a `PreEnvelGroupRel`.
 -/
Rack.PreEnvelGroupRel'.rel : ∀ {R : Type u} [inst : Rack R] {a b : Rack.PreEnvelGroup R} (a_1 : Rack.PreEnvelGroupRel' R a b),
  Rack.PreEnvelGroupRel R a b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_eq_of_getEntry?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getEntry? a l = some ⟨k, v⟩ →
    ∀ {h' : Std.Internal.List.containsKey a l = true}, Std.Internal.List.getEntry a l h' = ⟨k, v⟩
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.obj_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n = X.obj (Opposite.op { len := n })
-- Mathlib.Data.Multiset.Defs
Multiset.decidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Multiset α)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- `tensorRightHomEquiv` commutes with tensoring on the left  -/
CategoryTheory.tensorRightHomEquiv_tensor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z Z' : C} [inst_2 : CategoryTheory.ExactPairing Y Y']
  (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y') (g : X' ⟶ Z'),
  (CategoryTheory.tensorRightHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj X' X) Y Y'
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Z' Z)).symm
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
        (CategoryTheory.MonoidalCategoryStruct.associator Z' Z Y').inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' X Y).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g ((CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm f))
-- Mathlib.Data.ENat.Lattice
ENat.sInf_eq_zero : ∀ {s : Set ℕ∞}, sInf s = 0 ↔ 0 ∈ s
-- Init.Data.List.BasicAux
List.get.eq_def : ∀ {α : Type u} (x : List α) (x_1 : Fin x.length),
  x.get x_1 =
    match x, x_1 with
    | a :: tail, ⟨0, isLt⟩ => a
    | head :: as, ⟨i.succ, h⟩ => as.get ⟨i, ⋯⟩
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.contains k = true → (cmp t.minKey! k).isLE = true
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.Kernel.condKernel.congr_simp : ∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ κ_1 : ProbabilityTheory.Kernel α (β × Ω)) (e_κ : κ = κ_1)
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ], κ.condKernel = κ_1.condKernel
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Rel.in₂₁ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₂ c) (Sum3.in₁ b)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An induction principle for `MulArchimedeanClass`.  -/
MulArchimedeanClass.ind : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  {motive : MulArchimedeanClass M → Prop},
  (∀ (a : M), motive (MulArchimedeanClass.mk a)) → ∀ (x : MulArchimedeanClass M), motive x
-- Aesop.Tree.Data
Aesop.NodeState.isUnprovable : Aesop.NodeState → Bool
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toListRev_ensureTermination_eq_toListRev : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toListRev = it.toListRev
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo.mk.sizeOf_spec : ∀ (range : Lean.Lsp.Range) (kind : Lean.Lsp.LeanFileProgressKind),
  sizeOf { range := range, kind := kind } = 1 + sizeOf range + sizeOf kind
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial_apply : ∀ (p : NNReal) (h : p ≤ 1) (n : ℕ) (i : Fin (n + 1)),
  (PMF.binomial p h n) i = ↑p ^ ↑i * (1 - ↑p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)
-- Mathlib.Topology.Filter
Filter.isTopologicalBasis_Iic_principal : ∀ {α : Type u_2}, TopologicalSpace.IsTopologicalBasis (Set.range (Set.Iic ∘ Filter.principal))
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.intCast_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℤ), (↑n).toProd.1 = ↑n
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_comp_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m p : ℤ) {Z : C}
  (h_1 : CochainComplex.ConnectData.X K L p ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.d n m) (CategoryTheory.CategoryStruct.comp (h.d m p) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Lean.Environment
Lean.instMonadEnvOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.MonadEnv m] → Lean.MonadEnv n
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.llift_symm_apply : ∀ (M : Type u_2) (R : Type u_5) (S : Type u_8) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (X : Type u_9) [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] (f : (X →₀ R) →ₗ[R] M)
  (x : X), (Finsupp.llift M R S X).symm f x = f fun₀ | x => 1