mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimit₂ : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t)
  (x₁ x₂ : t.pt),
  ∃ j x₁' x₂',
    (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x₁' = x₁ ∧
      (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x₂' = x₂
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_unitIso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapNatIso i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K K' : AddSubgroup N},
  K ≤ K' → AddSubgroup.comap f K ≤ AddSubgroup.comap f K'
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.mk.inj : ∀ {symbols : Array Lean.HeadIndex} {symbolSet : Std.HashSet Lean.HeadIndex} {bvarsFound : Std.HashSet ℕ}
  {symbols_1 : Array Lean.HeadIndex} {symbolSet_1 : Std.HashSet Lean.HeadIndex} {bvarsFound_1 : Std.HashSet ℕ},
  { symbols := symbols, symbolSet := symbolSet, bvarsFound := bvarsFound } =
      { symbols := symbols_1, symbolSet := symbolSet_1, bvarsFound := bvarsFound_1 } →
    symbols = symbols_1 ∧ symbolSet = symbolSet_1 ∧ bvarsFound = bvarsFound_1
-- Mathlib.Computability.EpsilonNFA
/-- `M.eval x` computes all possible paths through `M` with input `x` starting at an element of
`M.start`.  -/
εNFA.eval : {α : Type u} → {σ : Type v} → εNFA α σ → List α → Set σ
-- Std.Time.Internal.UnitVal
/-- Multiplies the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio.
 -/
Std.Time.Internal.UnitVal.mul : {a : ℚ} → Std.Time.Internal.UnitVal a → (factor : ℤ) → Std.Time.Internal.UnitVal (a / ↑factor)
-- Mathlib.Data.Fin.Rev
Fin.rev_ne_iff : ∀ {n : ℕ} {i j : Fin n}, i.rev ≠ j ↔ i ≠ j.rev
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.instIsFaithfulSubtypeMemLieSubalgebra : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsFaithful R L M] {L' : LieSubalgebra R L}, LieModule.IsFaithful R (↥L') M
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_iInter_apply : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : CompleteLattice M] [inst_1 : Zero M] [Nonempty ι],
  ⊥ = 0 → ∀ (s : ι → Set α) (f : α → M) (x : α), (⋂ i, s i).indicator f x = ⨅ i, (s i).indicator f x
-- Mathlib.Algebra.Order.Pi
Function.const_le_one_of_le_one : ∀ {α : Type u_2} (β : Type u_3) [inst : One α] [inst_1 : Preorder α] {a : α}, a ≤ 1 → Function.const β a ≤ 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.post_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} (F : CategoryTheory.Functor T D) {X_1 Y : CategoryTheory.Over X} (f : X_1 ⟶ Y),
  (CategoryTheory.Over.post F).map f = CategoryTheory.Over.homMk (F.map (CategoryTheory.Over.Hom.left f)) ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.instCoeTypeForall_1 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.RingTheory.Radical.Basic
/-- If `a` divides `b`, then the radical of `a` divides the radical of `b`. The theorem requires
that `b ≠ 0`, since `radical 0 = 1` but `a ∣ 0` holds for every `a`.  -/
UniqueFactorizationMonoid.radical_dvd_radical : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, a ∣ b → b ≠ 0 → UniqueFactorizationMonoid.radical a ∣ UniqueFactorizationMonoid.radical b
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instInhabitedOrdinal : Inhabited Std.Time.Week.Aligned.Ordinal
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_iff_integrableOn_Ioo_of_le : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  a ≤ b →
    autoParam (‖f a‖ₑ ≠ ⊤) intervalIntegrable_iff_integrableOn_Ioo_of_le._auto_1 →
      autoParam (‖f b‖ₑ ≠ ⊤) intervalIntegrable_iff_integrableOn_Ioo_of_le._auto_3 →
        (IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_im_le_pi : ∀ (x : ℂ), (Complex.log x).im ≤ Real.pi
-- Mathlib.Algebra.CharP.Defs
CharP.char_is_prime_of_two_le : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [NoZeroDivisors R] (p : ℕ) [CharP R p], 2 ≤ p → Nat.Prime p
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_antilipschitzWith_ofLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], AntilipschitzWith (2 ^ (1 / p).toReal) WithLp.ofLp
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.instPreservesSheafification : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  {E : Type u_4} [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  (F : CategoryTheory.Functor D E)
  [∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)]
  [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms],
  J.PreservesSheafification F
-- Mathlib.Algebra.Group.Action.Sum
Sum.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul N α]
  [inst_3 : SMul N β] [inst_4 : SMul M N] [IsScalarTower M N α] [IsScalarTower M N β], IsScalarTower M N (α ⊕ β)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.add.injEq : ∀ {R : Type u_1} {X : Type u_2} (a a_1 a_2 a_3 : FreeAlgebra.Pre R X), (a.add a_1 = a_2.add a_3) = (a = a_2 ∧ a_1 = a_3)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.maxKey? = some t.maxKey!
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Array.mapSepElemsMAux : {m : Type → Type} →
  [Monad m] → Array Lean.Syntax → (Lean.Syntax → m Lean.Syntax) → ℕ → Array Lean.Syntax → m (Array Lean.Syntax)
-- Mathlib.Analysis.Complex.CauchyIntegral
DifferentiableOn.deriv : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {s : Set ℂ} {f : ℂ → E},
  DifferentiableOn ℂ f s → IsOpen s → DifferentiableOn ℂ (deriv f) s
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_eq_zero : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [cd : InnerProductSpace.Core 𝕜 F] {x : F}, inner 𝕜 x x = 0 ↔ x = 0
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instMembership : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Membership α (Std.Sat.AIG α)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Cardinal.preAleph (OfNat.ofNat n) = OfNat.ofNat n
-- Init.Data.UInt.Lemmas
UInt32.mod_zero : ∀ {a : UInt32}, a % 0 = a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m} [Countable ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.RootFormIn.eq_1 : ∀ {ι : 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] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : P.IsValuedIn S] [inst_11 : Fintype ι],
  P.RootFormIn S = ∑ i, LinearMap.smulRight (P.coroot'In S i) (P.coroot'In S i)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasStrictFDerivAt_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F] (x : E), HasStrictFDerivAt 1 0 x
-- Mathlib.FieldTheory.Differential.Basic
Differential.instDifferentialAlgebraSubtypeMemIntermediateField : ∀ {F : Type u_2} [inst : Field F] [inst_1 : Differential F] [inst_2 : CharZero F] {K : Type u_3} [inst_3 : Field K]
  [inst_4 : Algebra F K] (B : IntermediateField F K) [inst_5 : FiniteDimensional F ↥B], DifferentialAlgebra F ↥B
-- Mathlib.Probability.Independence.Kernel.Indep
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.iIndepSet_congr`. -/
ProbabilityTheory.Kernel.iIndepSet.congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.iIndepSet s κ μ → ProbabilityTheory.Kernel.iIndepSet s η μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqSymbolKind.beq : Lean.Lsp.SymbolKind → Lean.Lsp.SymbolKind → Bool
-- Lean.Meta.Tactic.TryThis
/-- Add a suggestion for `rw [h₁, ← h₂] at loc`.

Parameters:
* `ref`: the span of the widget diagnostic
* `rules`: a list of arguments to `rw`, with the second component `true` if the rewrite is reversed
* `type?`: the goal after the suggested rewrite, `.none` if the rewrite closes the goal, or `.undef`
  if the resulting goal is unknown
* `loc?`: the hypothesis at which the rewrite is performed, or `none` if the goal is targeted
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `checkState?`: if passed, the tactic state in which the generated tactic will be validated,
  inserting `expose_names` if necessary
 -/
Lean.Meta.Tactic.TryThis.addRewriteSuggestion : Lean.Syntax →
  List (Lean.Expr × Bool) →
    optParam (Lean.LOption Lean.Expr) Lean.LOption.undef →
      optParam (Option Lean.Expr) none →
        optParam (Option Lean.Syntax) none →
          optParam (Option Lean.Elab.Tactic.SavedState) none → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- Ring homomorphism between `A[b]` and `A⟮↑b⟯`.  -/
IntermediateField.RingHom.adjoinAlgebraMapOfAlgebra : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : Field A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : Field C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → ↥A[b] →+* ↥A⟮(algebraMap B C) b⟯
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.hasSmallLocalizedHom_of_isos : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {X Y X' Y' : C}
  (e : X ≅ X') (e' : Y ≅ Y') [CategoryTheory.Localization.HasSmallLocalizedHom W X Y],
  CategoryTheory.Localization.HasSmallLocalizedHom W X' Y'
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.SLOnGLPos_smul_apply : ∀ (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane),
  (s • g) • z = (Matrix.SpecialLinearGroup.toGLPos ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) s) * g) • z
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The inverse of a ContinuousMulEquiv.  -/
ContinuousMulEquiv.symm : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] → [inst_2 : Mul M] → [inst_3 : Mul N] → M ≃ₜ* N → N ≃ₜ* M
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.addActionHom_embedding.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} (ι : Type u_5)
  (hf : Function.Injective ⇑f),
  Function.Injective.addActionHom_embedding ι hf =
    { toFun := fun x => { toFun := f.toFun ∘ x.toFun, inj' := ⋯ }, map_vadd' := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n a n' : ℤ) (hn' : n + a = n')
  (γ : CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'),
  (CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv n a n' hn').symm γ = γ.leftUnshift n hn'
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Terminal.left_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Coalgebra F} (h : CategoryTheory.Limits.IsTerminal A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv h) A.str =
    CategoryTheory.CategoryStruct.id (F.obj A.V)
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1` and `+` is an additive commutative group with one, if it admits an
injective map that preserves `0`, `1` and `+` to an additive commutative group with one.
See note [reducible non-instances].  -/
Function.Injective.addCommGroupWithOne : {R : Type u_1} →
  {S : Type u_3} →
    [inst : Zero S] →
      [inst_1 : One S] →
        [inst_2 : Add S] →
          [inst_3 : SMul ℕ S] →
            [inst_4 : Neg S] →
              [inst_5 : Sub S] →
                [inst_6 : SMul ℤ S] →
                  [inst_7 : NatCast S] →
                    [inst_8 : IntCast S] →
                      [inst_9 : AddCommGroupWithOne R] →
                        (f : S → R) →
                          Function.Injective f →
                            f 0 = 0 →
                              f 1 = 1 →
                                (∀ (x y : S), f (x + y) = f x + f y) →
                                  (∀ (x : S), f (-x) = -f x) →
                                    (∀ (x y : S), f (x - y) = f x - f y) →
                                      (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                        (∀ (n : ℤ) (x : S), f (n • x) = n • f x) →
                                          (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → AddCommGroupWithOne S
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseRightKanExtension_iff_of_iso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} (e₁ : L ≅ L') (e₂ : F ≅ F'),
  L.HasPointwiseRightKanExtension F ↔ L'.HasPointwiseRightKanExtension F'
-- Mathlib.Algebra.Module.Submodule.Defs
/-- Reinterpret a `Submodule` as an `AddSubmonoid`.  -/
Submodule.toAddSubmonoid : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → AddSubmonoid M
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.coe_copy : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B] (f : A →⋆* B)
  (f' : A → B) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.target : Lean.Meta.FunIndParamKind
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.norm_complexMGF_le_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  ‖ProbabilityTheory.complexMGF X μ z‖ ≤ ProbabilityTheory.mgf X μ z.re
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalClear : Lean.Elab.Tactic.Tactic
-- Std.Http.Data.Extensions
/-- Checks whether the extensions contain a value of type `α`.
 -/
Std.Http.Extensions.contains : Std.Http.Extensions → (α : Type) → [TypeName α] → Bool
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
measurableEmbedding_prod_mk_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass α]
  (x : α), MeasurableEmbedding fun y => (y, x)
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_le_iff_covBy : ∀ {R : Type u_1} [inst : CommRing R] {p : Ideal R} {n : ℕ} [p.IsPrime] [IsNoetherianRing R],
  p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n
-- Batteries.Recycling.RBTree.Alter
/-- The `modify` function preserves the balance invariants.  -/
RBTree.RBNode.Balanced.modify : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cut : α → Ordering} {f : α → α} {t : RBTree.RBNode α},
  t.Balanced c n → ∃ c n, (RBTree.RBNode.modify cut f t).Balanced c n
-- Mathlib.Data.Nat.ModEq
Nat.sub_modulus_modEq_iff : ∀ {n a b : ℕ}, n ≤ a → (a - n ≡ b [MOD n] ↔ a ≡ b [MOD n])
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The shape of the multicoequalizer of all pairs of morphisms `g₁ g₂ : Y ⟶ step W Z` with
a `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.  -/
CategoryTheory.OrthogonalReflection.D₂.multispanShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [CategoryTheory.Limits.HasPushouts C] → CategoryTheory.Limits.MultispanShape
-- Mathlib.Algebra.Group.TransferInstance
/-- An equivalence `e : α ≃ β` gives an additive equivalence `α ≃+ β` where
the additive structure on `α` is the one obtained by transporting an additive structure
on `β` back along `e`.  -/
Equiv.addEquiv : {α : Type u_2} →
  {β : Type u_3} →
    (e : α ≃ β) →
      [inst : Add β] →
        have x := e.add;
        α ≃+ β
-- Mathlib.RingTheory.WittVector.MulP
WittVector.mulN_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (n : ℕ) (x : WittVector p R) (k : ℕ),
  (x * ↑n).coeff k = (MvPolynomial.aeval x.coeff) (WittVector.wittMulN p n k)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.zero_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {a : α}, 0 a = 0
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.id_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Adjunction.id.unit = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id C)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_natCast_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoDiv hp a (↑m * p + b) = ↑m + toIcoDiv hp a b
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_of_le._auto_1 →
    (∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a) → Filter.liminf u f ≤ a
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Iter.Equiv.symm : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] {ita : Std.Iter β}
  {itb : Std.Iter β}, ita.Equiv itb → itb.Equiv ita
-- Init.Tactics
/-- `show_term e` elaborates `e`, then prints the generated term.
 -/
Lean.Parser.Tactic.showTermElab : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.isSubwalk_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support),
  (p.takeUntil w h).IsSubwalk p
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef.mk.inj : ∀ {α : Type} {ref ref_1 : IO.Ref (Lean.Meta.LazyDiscrTree α)}, { ref := ref } = { ref := ref_1 } → ref = ref_1
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.false.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.IProp.false = 1
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.insertMany : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.TreeSet.Raw α cmp}, t.WF → (t.insertMany l).WF
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Reinterpret a `Subsemiring` as a `Submonoid`.  -/
Subsemiring.toSubmonoid : {R : Type u} → [inst : NonAssocSemiring R] → Subsemiring R → Submonoid R
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.of_subsingleton : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G} [Subsingleton G], UniqueMul A B a0 b0
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.right_unit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C) {Z : C}
  (h : self.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map (self.η.app X)) (CategoryTheory.CategoryStruct.comp (self.μ.app X) h) = h
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁.val_eq_coe : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₁ A)),
  ↑f = ⇑f
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The coercion from the restricted product of monoids `A i` to the (normal) product
is a monoid homomorphism.  -/
RestrictedProduct.coeMonoidHom : {ι : Type u_1} →
  {R : ι → Type u_2} →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Monoid (R i)] →
              [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] →
                RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕 →* (i : ι) → R i
-- Lean.Data.PersistentArray
Lean.PersistentArray.forInAux : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] → [inh : Inhabited β] → (α → β → m (ForInStep β)) → Lean.PersistentArrayNode α → β → m (ForInStep β)
-- Lean.DocString.Markdown
/-- Registers a builtin inline Markdown renderer.  -/
Lean.Doc.addBuiltinInlineMdRenderer : Lean.Name → Lean.Doc.InlineMdRenderer → IO Unit