mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Free
FreeSemigroup.mul_bind : ∀ {α β : Type u} (f : α → FreeSemigroup β) (x y : FreeSemigroup α), x * y >>= f = (x >>= f) * (y >>= f)
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_mul_goldenConj : Real.goldenRatio * Real.goldenConj = -1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.RightFraction₂.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y X' : C}
  (s : X' ⟶ X) (hs : W s) (f f' : X' ⟶ Y) (X'_1 : C) (s_1 : X'_1 ⟶ X) (hs_1 : W s_1) (f_1 f'_1 : X'_1 ⟶ Y),
  ({ X' := X', s := s, hs := hs, f := f, f' := f' } = { X' := X'_1, s := s_1, hs := hs_1, f := f_1, f' := f'_1 }) =
    (X' = X'_1 ∧ s ≍ s_1 ∧ f ≍ f_1 ∧ f' ≍ f'_1)
-- Mathlib.Data.Nat.Cast.Commute
Commute.natCast_mul_right : ∀ {α : Type u_1} [inst : Semiring α] {a b : α}, Commute a b → ∀ (n : ℕ), Commute a (↑n * b)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_snoc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (x : M) (f : Fin n → M), ∑ i, Fin.snoc f x i = ∑ i, f i + x
-- Mathlib.Data.SetLike.Basic
SetLike.eta : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : ↥p) (hx : ↑x ∈ p), ⟨↑x, hx⟩ = x
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `M` is finite, then `finrank N = rank N` for all `N : Submodule M`. Note that
such an `N` need not be finitely generated.  -/
Submodule.finrank_eq_rank : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] (N : Submodule R M), ↑(Module.finrank R ↥N) = Module.rank R ↥N
-- Init.Data.List.Sublist
List.sublist_append_of_sublist_right : ∀ {α : Type u_1} {l l₂ l₁ : List α}, l.Sublist l₂ → l.Sublist (l₁ ++ l₂)
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Factorized rational functions are analytic wherever the exponent is non-negative.
 -/
Function.FactorizedRational.analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜},
  0 ≤ d x → AnalyticAt 𝕜 (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) x
-- Mathlib.Algebra.Module.Projective
Module.Projective.of_free : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] [Module.Free R P],
  Module.Projective R P
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.commAlgEquiv_single_zero : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (m : M),
  (AddMonoidAlgebra.commAlgEquiv R) (AddMonoidAlgebra.single m 1) =
    AddMonoidAlgebra.single 0 (AddMonoidAlgebra.single m 1)
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatterer_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)}, 𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜
-- Mathlib.Topology.Compactness.Lindelof
/-- Type class for Hereditarily Lindelöf spaces.  -/
HereditarilyLindelofSpace : (X : Type u_2) → [TopologicalSpace X] → Prop
-- Mathlib.Data.Set.Lattice
Set.biUnion_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (t : α → Set β),
  ⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x
-- Lean.Meta.Tactic.TryThis
/-- Delaborate `e` into syntax suitable for use by `refine`.  -/
Lean.Meta.Tactic.TryThis.delabToRefinableSyntax : Lean.Expr → Lean.MetaM Lean.Term
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.reciprocalFactors_even : ∀ {n : ℕ}, n ≠ 0 → Even n → DihedralGroup.reciprocalFactors n = 3 :: DihedralGroup.reciprocalFactors (n / 2)
-- Init.Data.Int.Gcd
Int.lcm_ne_zero : ∀ {m n : ℤ}, m ≠ 0 → n ≠ 0 → m.lcm n ≠ 0
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_toUInt16 : ∀ (n : UInt32), n.toUInt16.toUInt64 = n.toUInt64 % 65536
-- Mathlib.Order.SuccPred.Basic
isMin_of_pred_notMem : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α} [s.OrdConnected] [inst_2 : PredOrder α] {a : ↑s},
  Order.pred ↑a ∉ s → IsMin a
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_mono : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N],
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) Subgroup.prod
    Subgroup.prod
-- Mathlib.Order.Category.PartOrd
PartOrd.uliftFunctor_map : ∀ {X Y : PartOrd} (f : X ⟶ Y),
  PartOrd.uliftFunctor.map f =
    PartOrd.ofHom { toFun := fun x => { down := (CategoryTheory.ConcreteCategory.hom f) x.down }, monotone' := ⋯ }
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.coe_of_h_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ}, v = ↑q → ↑(GenContFract.of q).h = (GenContFract.of v).h
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prevn_startPos : ∀ {n : ℕ} {s : String.Slice}, s.startPos.prevn n = s.startPos
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.optionPelim'.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : (t : Option α) → (t = none → β) → ((val : α) → t = some val → β) → Sort u_2)
  (a : α) (n : some a = none → β) (s : (val : α) → some a = some val → β)
  (h_1 : (a : α) → (n : some a = none → β) → (s : (val : α) → some a = some val → β) → motive (some a) n s)
  (h_2 : (n : none = none → β) → (s : (val : α) → none = some val → β) → motive none n s),
  (match some a, n, s with
    | some a, n, s => h_1 a n s
    | none, n, s => h_2 n s) =
    h_1 a n s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddMonoid : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddMonoid (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddMonoid (DirectLimit G f)
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.scMap_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMap._auto_1),
  (CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi).τ₃ = φ.app ⟨i + 2, ⋯⟩
-- Aesop.Script.SScript
Aesop.Script.SScript.render : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → [Lean.MonadQuotation m] → Aesop.Script.SScript → m (Array Lean.Syntax.Tactic)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'_inv_app : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R),
  (ModuleCat.restrictScalarsId' f hf).inv.app X = (ModuleCat.restrictScalarsId'App f hf X).inv
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.compl_bijective : ∀ {α : Type u_2} [inst : TopologicalSpace α], Function.Bijective TopologicalSpace.Closeds.compl
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalWhiskerLeft.match_1.eq_4 : ∀ (motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u_1) (e : Lean.Expr)
  (a : Mathlib.Tactic.BicategoryLike.Obj) (η : Mathlib.Tactic.BicategoryLike.NormalExpr)
  (h_1 :
    (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) → motive f (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α))
  (h_2 :
    (f : Mathlib.Tactic.BicategoryLike.Atom₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) →
          (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
            (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr) →
              motive (Mathlib.Tactic.BicategoryLike.Mor₁.of f) (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs))
  (h_3 :
    (e : Lean.Expr) →
      (f g : Mathlib.Tactic.BicategoryLike.Mor₁) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g) η)
  (h_4 :
    (e : Lean.Expr) →
      (a : Mathlib.Tactic.BicategoryLike.Obj) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.id e a) η),
  (∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural),
      η = Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α → False) →
    (match Mathlib.Tactic.BicategoryLike.Mor₁.id e a, η with
      | f, Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α => h_1 f e α
      | Mathlib.Tactic.BicategoryLike.Mor₁.of f, Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs =>
        h_2 f e α η ηs
      | Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g, η => h_3 e f g η
      | Mathlib.Tactic.BicategoryLike.Mor₁.id e a, η => h_4 e a η) =
      h_4 e a η
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- The functor in the equivalence of sheaf categories.  -/
CategoryTheory.Equivalence.sheafCongr.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)
-- Lean.Server.Utils
/-- Chains two streams by creating a new stream s.t. writing to it
just writes to `a` but reading from it also duplicates the read output
into `b`, c.f. `a | tee b` on Unix.
NB: if `a` is written to but this stream is never read from,
the output will *not* be duplicated. Use this if you only care
about the data that was actually read.
 -/
Lean.IO.FS.Stream.chainRight : IO.FS.Stream → IO.FS.Stream → optParam Bool false → IO.FS.Stream
-- Lean.Meta.WHNF
Lean.Meta.projectCore? : Lean.Expr → ℕ → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_unique : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : Unique α] (f : α → M), ∑ᶠ (i : α), f i = f default
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  (∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)) →
    (∀ (c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x, y)) →
      (∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)) →
        (∀ (c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x, y)) →
          (∃ C > 0, ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖) → IsBoundedBilinearMap 𝕜 f
-- Mathlib.Algebra.Ring.Shrink
Shrink.instRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [Ring α] → Ring (Shrink.{v, u_1} α)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int64.intCast : IntCast Int64
-- Init.Grind.Order
Lean.Grind.Order.le_of_eq_1 : ∀ {α : Type u_1} [inst : LE α] [Std.IsPreorder α] {a b : α}, a = b → a ≤ b
-- Mathlib.Data.List.Perm.Basic
_private.Mathlib.Data.List.Perm.Basic.0.List.«term_<*>_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is σ-compact
if and only `s` is σ-compact.  -/
Topology.IsInducing.isSigmaCompact_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Topology.IsInducing f → (IsSigmaCompact s ↔ IsSigmaCompact (f '' s))
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.sectL_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (Z : D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Prod.sectL C Z).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Z)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.coe_of : ∀ (R : Type u) [inst : Ring R] (X : Type v) [inst_1 : Ring X] [inst_2 : Module R X], ↑(ModuleCat.of R X) = X
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.braiding_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Prod.braiding C D).functor = CategoryTheory.Prod.swap C D
-- Mathlib.Topology.Algebra.Group.Basic
/-- A version of `Homeomorph.addLeft a (-b)` that is defeq to `a - b`.  -/
Homeomorph.subLeft : {G : Type w} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [IsTopologicalAddGroup G] → G → G ≃ₜ G
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip : ∀ (z : UpperHalfPlane) {N : ℕ}, 0 < N → ∃ n, ModularGroup.T ^ (↑N * n) • z ∈ UpperHalfPlane.verticalStrip (↑N) z.im
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_inj : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  IsPrimitiveRoot ζ k → ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i = j
-- Qq.MetaM
Qq.mkFreshExprMVarQ : {u : Lean.Level} →
  (ty : Q(Sort u)) →
    optParam Lean.MetavarKind Lean.MetavarKind.natural → optParam Lean.Name Lean.Name.anonymous → Lean.MetaM Q(«$ty»)
-- Lean.Util.Trace
Lean.addRawTrace : {m : Type → Type} →
  [Monad m] → [Lean.MonadTrace m] → [Lean.MonadRef m] → [Lean.AddMessageContext m] → Lean.MessageData → m Unit
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instNeg : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddGroup 𝕜] → [inst_1 : LE α] → Neg (IncidenceAlgebra 𝕜 α)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A normed ring is a seminormed ring.  -/
NormedRing.toSeminormedRing : {α : Type u_2} → [β : NormedRing α] → SeminormedRing α
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_ssubset_Iic : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], Finset.Iic a ⊂ Finset.Iic b ↔ a < b
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G),
  CategoryTheory.Limits.HasColimit.isoOfNatIso w =
    (CategoryTheory.Limits.colimit.isColimit F).coconePointsIsoOfNatIso (CategoryTheory.Limits.colimit.isColimit G) w
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instNontrivial : Nontrivial GaussianInt
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_homCategory_id_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : Bᵒᵖ) (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.id f).unop2 = CategoryTheory.CategoryStruct.id f.unop
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- If `s` is a dense set in an additive monoid `M`,
`AddSubsemigroup.closure s = ⊤`, then in order to prove that some predicate `p` holds
for all `x : M` it suffices to verify `p x` for `x ∈ s`, and verify that `p x` and `p y` imply
`p (x + y)`.  -/
AddSubsemigroup.dense_induction : ∀ {M : Type u_1} [inst : Add M] {p : M → Prop} (s : Set M),
  AddSubsemigroup.closure s = ⊤ → (∀ x ∈ s, p x) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (x : M), p x
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_coe : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {i : ι} (x : ↥(ℳ i)),
  (DirectSum.decompose ℳ) ↑x = (DirectSum.of (fun i => ↥(ℳ i)) i) x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [self : E.Small], ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S
-- Mathlib.Algebra.Algebra.Opposite
/-- Swap the `ᵐᵒᵖ` on an algebra isomorphism to the opposite side.  -/
AlgEquiv.opComm : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] Bᵐᵒᵖ) ≃ Aᵐᵒᵖ ≃ₐ[R] B
-- Batteries.Data.Fin.Coding
Fin.decodeOption_encodeOption : ∀ {n : ℕ} (x : Option (Fin n)), Fin.decodeOption (Fin.encodeOption x) = x
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.pow_apply_eq_of_apply_apply_eq_self : ∀ {α : Type u_1} {f : Equiv.Perm α} {x : α}, f (f x) = x → ∀ (n : ℕ), (f ^ n) x = x ∨ (f ^ n) x = f x
-- Std.Http.Data.Status
/-- 412 Precondition Failed
 -/
Std.Http.Status.preconditionFailed : Std.Http.Status
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Probability.Moments.Variance
MeasureTheory.MeasurePreserving.variance_fun_comp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'}
  {ν : MeasureTheory.Measure Ω'} {X : Ω → Ω'},
  MeasureTheory.MeasurePreserving X μ ν →
    ∀ {f : Ω' → ℝ}, AEMeasurable f ν → ProbabilityTheory.variance (fun ω => f (X ω)) μ = ProbabilityTheory.variance f ν
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeletonOfMono_zero : ∀ {X Y : SSet} (i : X ⟶ Y), (SSet.skeletonOfMono i) 0 = SSet.Subcomplex.range i
-- Init.Data.UInt.Lemmas
USize.toNat_ofNat_of_lt' : ∀ {n : ℕ}, n < USize.size → (USize.ofNat n).toNat = n
-- Init.Data.SInt.Lemmas
Int64.toInt_bmod_size : ∀ (a : Int64), a.toInt.bmod Int64.size = a.toInt
-- Mathlib.MeasureTheory.Integral.Marginal
/-- The marginal distribution is independent of the variables in `s`.  -/
MeasureTheory.lmarginal_congr : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] {s : Finset δ} {x y : (i : δ) → X i} (f : ((i : δ) → X i) → ENNReal),
  (∀ i ∉ s, x i = y i) → (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_left_right : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime x (x * z + y)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.objMap_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g h : CategoryTheory.Arrow C} (φ : f ⟶ g) (ψ : g ⟶ h) {Z : C} (h_1 : CategoryTheory.SmallObject.obj I κ h.hom ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ (CategoryTheory.CategoryStruct.comp φ ψ))
      h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ ψ) h_1)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.mul_annihilator : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R), I * Submodule.annihilator I = ⊥
-- Init.Data.Repr
instReprBool : Repr Bool
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If two open cells are equal, so are the underlying cells.  -/
Topology.RelCWComplex.openCell_congr : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  {s t_1 : Topology.RelCWComplex.cell C n},
  Topology.RelCWComplex.openCell n s = Topology.RelCWComplex.openCell n t_1 → s = t_1
-- Mathlib.Analysis.Normed.Affine.AddTorsor
DilationEquiv.smulTorsor_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] {P : Type u_3} [inst_4 : PseudoMetricSpace P] [inst_5 : NormedAddTorsor E P] (c : P)
  {k : 𝕜} (hk : k ≠ 0) (x : P), (DilationEquiv.smulTorsor c hk).symm x = (k⁻¹ • fun x => x -ᵥ c) x
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.toCompletion_ofCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : (↑v).Completion),
  { toCompletion := x }.toCompletion = x
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_add_three : ∀ {a : ByteArray} {i : ℕ} (ha : i + 3 ≤ a.size), a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray
-- Init.Coe
instCoeTOfCoeHTCT : {α : Sort u_1} → {β : Sort u_2} → {a : α} → [CoeHTCT α β] → CoeT α a β
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) → Inhabited (CategoryTheory.Oplax.StrongTrans F F)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_right_mem_nonZeroDivisors_eq_zero_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r x : M₀}, r ∈ nonZeroDivisors M₀ → (x * r = 0 ↔ x = 0)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Conjugate point of the unit disc.  -/
Complex.UnitDisc.instStar : Star Complex.UnitDisc
-- Init.Data.List.MinMaxOn
List.maxOn?_eq_some_maxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.maxOn? f xs = some (List.maxOn f xs h)
-- Mathlib.Combinatorics.Quiver.Basic
/-- An arrow in a quiver can be transported across equalities between the source and target
objects.  -/
Quiver.homOfEq : {V : Type u_1} → [inst : Quiver V] → {X Y X' Y' : V} → (X ⟶ Y) → X = X' → Y = Y' → (X' ⟶ Y')
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_smul_of_mem_nonZeroDivisors : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] {c : R} (B : Matrix m n R),
  c ∈ nonZeroDivisors R → (c • B).rank = B.rank
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.list_prod_apply : ∀ {I : Type u_1} (C : Set (I → Bool)) (x : ↑C) (l : List (LocallyConstant ↑C ℤ)),
  l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.truth_comp_hom`. -/
CategoryTheory.Classifier.truth_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C},
  CategoryTheory.CategoryStruct.comp 𝒞₁.truth (𝒞₁.hom 𝒞₂) = CategoryTheory.CategoryStruct.comp (𝒞₂.χ₀ 𝒞₁.Ω₀) 𝒞₂.truth
-- Aesop.RuleTac.Forward.Basic
Aesop.clearForwardImplDetailHyps : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.nonneg_intCast_of_nonneg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a : ℤ), 0 ≤ a → 0 ≤ ↑a