mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.CoreM
Lean.Core.Context.quotContext : Lean.Core.Context → Lean.Name
-- Mathlib.Order.Basic
LE.le.ge_iff_eq : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → (b ≤ a ↔ a = b)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- We say a finite root pairing is anisotropic if there are no roots / coroots which have length
zero w.r.t. the root / coroot forms.

Examples include crystallographic pairings in characteristic zero
`RootPairing.instIsAnisotropicOfIsCrystallographic` and pairings over ordered scalars.
`RootPairing.instIsAnisotropicOfLinearOrderedCommRing`.  -/
RootPairing.IsAnisotropic : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Fintype ι] →
          [inst : AddCommGroup M] →
            [inst_1 : AddCommGroup N] →
              [inst_2 : CommRing R] → [inst_3 : Module R M] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.isMittagLeffler_of_exists_finite_range : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J],
  (∀ (j : J), ∃ i f, (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))).Finite) → F.IsMittagLeffler
-- Mathlib.Algebra.Module.PID
/-- A finitely generated `p ^ ∞`-torsion module over a PID is isomorphic to a direct sum of some
`R ⧸ R ∙ (p ^ e i)` for some `e i`.  -/
Module.torsion_by_prime_power_decomposition : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] {p : R},
  Irreducible p →
    Module.IsTorsion' M ↥(Submonoid.powers p) →
      ∀ [h' : Module.Finite R M], ∃ d k, Nonempty (M ≃ₗ[R] DirectSum (Fin d) fun i => R ⧸ R ∙ p ^ k i)
-- Mathlib.Topology.Irreducible
/-- A nonempty open subset of a preirreducible subspace is dense in the subspace.  -/
subset_closure_inter_of_isPreirreducible_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S U : Set X},
  IsPreirreducible S → IsOpen U → (S ∩ U).Nonempty → S ⊆ closure (S ∩ U)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zipWithMAux.eq_def : ∀ {α : Type u} {β : Type u_1} {γ : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (bs : Array β)
  (f : α → β → m γ) (i : ℕ) (cs : Array γ),
  as.zipWithMAux bs f i cs =
    if h : i < as.size then
      have a := as[i];
      if h : i < bs.size then
        have b := bs[i];
        do
        let __do_lift ← f a b
        as.zipWithMAux bs f (i + 1) (cs.push __do_lift)
      else pure cs
    else pure cs
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.instCompleteSpace : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  [CompleteSpace 𝕜] [CompleteSpace A], CompleteSpace (WithLp 1 (Unitization 𝕜 A))
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.ofFractionRing.injEq : ∀ {K : Type u} [inst : CommRing K] (toFractionRing toFractionRing_1 : FractionRing (Polynomial K)),
  ({ toFractionRing := toFractionRing } = { toFractionRing := toFractionRing_1 }) = (toFractionRing = toFractionRing_1)
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.cases : Lean.MVarId → Lean.Expr → Array Aesop.CtorNames → Aesop.Script.TacticBuilder
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.angleDiff_pos : ∀ {x y : Circle}, x ≠ y → 0 < x.angleDiff y
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.commRingEquiv_single_one_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M),
  MonoidAlgebra.commRingEquiv (MonoidAlgebra.single 1 (MonoidAlgebra.single m 1)) = MonoidAlgebra.single m 1
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supported_mono : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  {s t : Set M}, s ⊆ t → MonoidAlgebra.supported R S s ≤ MonoidAlgebra.supported R S t
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Sub α] (M N : Matrix m n α),
  (M - N).transpose = M.transpose - N.transpose
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {a₁ : ℤ × M} (a₂ : ℤ × M) {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M},
  (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval → (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_add : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x), (c1 + c2).deg = c1.deg + c2.deg
-- Mathlib.Data.List.Cycle
Cycle.subsingleton_nil : ∀ {α : Type u_1}, Cycle.nil.Subsingleton
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natMod : ∀ {a b a' b' c : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' →
    Mathlib.Meta.NormNum.IsNat b b' → a'.mod b' = c → Mathlib.Meta.NormNum.IsNat (a % b) c
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `descPochhammer S n` is at least `(s-n+1)^n` on `[n-1, ∞)`.  -/
pow_le_descPochhammer_eval : ∀ {S : Type u_1} [inst : Ring S] [inst_1 : PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S},
  ↑n - 1 ≤ s → (s - ↑n + 1) ^ n ≤ Polynomial.eval s (descPochhammer S n)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.isOrdered.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (t : RBTree.RBNode α) (l r : Option α),
  RBTree.RBNode.isOrdered cmp t l r =
    match t with
    | RBTree.RBNode.nil =>
      match l, r with
      | some l, some r => decide (cmp l r = Ordering.lt)
      | x, x_1 => true
    | RBTree.RBNode.node c a v b => RBTree.RBNode.isOrdered cmp a l (some v) && RBTree.RBNode.isOrdered cmp b (some v) r
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csSup_mem : ∀ {s : Set ℤ}, s.Nonempty → BddAbove s → sSup s ∈ s
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.nhds_eq_principal_Ici : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] (a : α),
  nhds a = Filter.principal (Set.Ici a)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.funext : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [Infinite R] {p q : Polynomial R},
  (∀ (r : R), Polynomial.eval r p = Polynomial.eval r q) → p = q
-- Mathlib.FieldTheory.FinTrdeg
finite_of_algebraicIndependent : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FinTrdeg K L] {ι : Type u_3}
  {x : ι → L}, AlgebraicIndependent K x → Finite ι
-- Init.Data.BitVec.Lemmas
BitVec.replicate_append_self : ∀ {w n : ℕ} {x : BitVec w}, x ++ BitVec.replicate n x = BitVec.cast ⋯ (BitVec.replicate n x ++ x)
-- Mathlib.Topology.Instances.Irrational
Irrational.eventually_forall_le_dist_cast_div_of_denom_le : ∀ {x : ℝ}, Irrational x → ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in nhds 0, ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
-- Mathlib.Order.WithBot
WithTop.lt_def' : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop α}, x < y ↔ (y = ⊤ ∧ ∃ a, x = ↑a) ∨ ∃ b, ∃ a < b, y = ↑b ∧ x = ↑a
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f g : α →Co β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Order.WithBot
WithBot.exists_coe_le : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithBot α → Prop}, (∃ x, ↑a ≤ x ∧ p x) ↔ ∃ b, a ≤ b ∧ p ↑b
-- Mathlib.Data.Set.Function
Set.preimage_invFun_of_notMem : ∀ {α : Type u_1} {β : Type u_2} [n : Nonempty α] {f : α → β},
  Function.Injective f → ∀ {s : Set α}, Classical.choice n ∉ s → Function.invFun f ⁻¹' s = f '' s
-- Mathlib.Logic.Nontrivial.Defs
/-- Predicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension.  -/
Nontrivial : Type u_3 → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inr_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g))
      (CategoryTheory.Limits.PreservesPushout.iso G f g).inv =
    CategoryTheory.Limits.pushout.inr (G.map f) (G.map g)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and `Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]`
of monoids, `RestrictedProduct.mapAlongMonoidHom` gives a monoid homomorphism between them.
The data needed is a function `f : ι₂ → ι₁` such that `𝓕₂` tends to `𝓕₁` along `f`, and monoid
homomorphisms `φ j : R₁ (f j) → R₂ j` sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s.
 -/
RestrictedProduct.mapAlongMonoidHom : {ι₁ : Type u_3} →
  {ι₂ : Type u_4} →
    (R₁ : ι₁ → Type u_5) →
      (R₂ : ι₂ → Type u_6) →
        {𝓕₁ : Filter ι₁} →
          {𝓕₂ : Filter ι₂} →
            {S₁ : ι₁ → Type u_7} →
              {S₂ : ι₂ → Type u_8} →
                [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)] →
                  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] →
                    {B₁ : (i : ι₁) → S₁ i} →
                      {B₂ : (j : ι₂) → S₂ j} →
                        (f : ι₂ → ι₁) →
                          Filter.Tendsto f 𝓕₂ 𝓕₁ →
                            [inst_2 : (i : ι₁) → Monoid (R₁ i)] →
                              [inst_3 : (i : ι₂) → Monoid (R₂ i)] →
                                [inst_4 : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] →
                                  [inst_5 : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)] →
                                    (φ : (j : ι₂) → R₁ (f j) →* R₂ j) →
                                      (∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) →
                                        RestrictedProduct (fun i => R₁ i) (fun i => ↑(B₁ i)) 𝓕₁ →*
                                          RestrictedProduct (fun j => R₂ j) (fun j => ↑(B₂ j)) 𝓕₂
-- Init.Data.List.TakeDrop
List.take_eq_nil_iff : ∀ {α : Type u_1} {l : List α} {k : ℕ}, List.take k l = [] ↔ k = 0 ∨ l = []
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} (Q : CategoryTheory.MorphismProperty C) [W.HasOfPrecompProperty Q],
  W' ≤ Q → W.HasOfPrecompProperty W'
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instOrientedOrd : ∀ {rel : ℤ → ℤ → Prop} {n m : ℤ}, Std.OrientedOrd (Std.Time.Internal.Bounded rel n m)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexRange_repr' : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (x : M) {bi : M} {i : ι} (h : b i = bi), (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- The constant sequence `X` is Følner if `X` has finite measure.  -/
IsFoelner.univ_of_isFiniteMeasure : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} [NeZero μ] [MeasureTheory.IsFiniteMeasure μ],
  IsFoelner G μ l fun x => Set.univ
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
/-- The heart of a t-structure, as the property of objects
that are both `≤ 0` and `≥ 0`.  -/
CategoryTheory.Triangulated.TStructure.heart : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → CategoryTheory.ObjectProperty C
-- Mathlib.Data.Finset.Interval
Finset.Icc_eq_image_powerset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α},
  s ⊆ t → Finset.Icc s t = Finset.image (fun x => s ∪ x) (t \ s).powerset
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_sup : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (I : Submodule R A) (N P : Submodule R M), I • (N ⊔ P) = I • N ⊔ I • P
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.ext_iff : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {φ ψ : ρ.Equiv σ}, φ = ψ ↔ ⇑φ = ⇑ψ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_eq_getValue! : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  [inst_3 : Inhabited β] {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.get! t k = Std.Internal.List.getValue! k t.toListModel
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_gt : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι}, MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | ↑i < τ ω}
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on augmented simplicial objects.  -/
CategoryTheory.SimplicialObject.Augmented.whiskeringObj : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u_1) →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C)
            (CategoryTheory.SimplicialObject.Augmented D)
-- Init.Data.BitVec.Lemmas
BitVec.sub_sub : ∀ {n : ℕ} (a b c : BitVec n), a - b - c = a - (b + c)
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.SplitIf.getSimprocs : ℕ → Bool → Lean.MetaM (Array Lean.Meta.Simprocs)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {B : Rep.{u, u, u} k G} (n : ℕ),
  groupCohomology.map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n =
    CategoryTheory.CategoryStruct.id (groupCohomology B n)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_sSup_of_mem : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)} {s : Submonoid M}, s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv_eq_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜}, iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun x => 1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.toSimplexCategory_map_δ : ∀ {n : ℕ} (i : Fin (n + 2)),
  SimplexCategoryGenRel.toSimplexCategory.map (SimplexCategoryGenRel.δ i) = SimplexCategory.δ i
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumber_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Fintype α]
  [inst_3 : Fintype β] (e : α ≃ β), ruzsaSzemerediNumber α = ruzsaSzemerediNumber β
-- Mathlib.Algebra.Homology.Homotopy
/-- A homotopy `h` between chain maps `f` and `g` consists of components `h i j : C.X i ⟶ D.X j`
which are zero unless `c.Rel j i`, satisfying the homotopy condition.
 -/
Homotopy : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → (C ⟶ D) → (C ⟶ D) → Type (max u_1 v)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.liftMagma_symm_apply : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Add M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A]
  [inst_5 : SMulCommClass R A A] (F : AddMonoidAlgebra R M →ₙₐ[R] A),
  (AddMonoidAlgebra.liftMagma R).symm F = F.toMulHom.comp (AddMonoidAlgebra.ofMagma R M)
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of the reverse direction of `SimpleGraph.degree_eq_zero`. -/
SimpleGraph.IsIsolated.degree_eq_zero : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], G.IsIsolated v → G.degree v = 0
-- Mathlib.NumberTheory.Fermat
Nat.two_lt_fermatNumber : ∀ (n : ℕ), 2 < n.fermatNumber
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.DHashMap.Raw.Const.insertMany m l},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.insertMany m l) k h' = Std.DHashMap.Raw.Const.get m k ⋯
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.trivialFunctor_map_hom : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] {X Y : ModuleCat k} (f : X ⟶ Y),
  Rep.Hom.hom ((Rep.trivialFunctor k G).map f) = { toLinearMap := ModuleCat.Hom.hom f, isIntertwining' := ⋯ }
-- Mathlib.Data.Set.Card
Set.ncard_le_ncard_iff_ncard_sdiff_le_ncard_sdiff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_le_ncard_iff_ncard_sdiff_le_ncard_sdiff._auto_1 →
    autoParam t.Finite Set.ncard_le_ncard_iff_ncard_sdiff_le_ncard_sdiff._auto_3 →
      (s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard)
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.prod_left_iff : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
  IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
-- Mathlib.Data.Semiquot
Semiquot.mk'.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (s : Set α) (val : Trunc ↑s), sizeOf { s := s, val := val } = 1 + sizeOf val
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.map_adj_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v w : V},
  G'.Adj (f v) (f w) ↔ G.Adj v w
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.charFunDual_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : StrongDual ℝ E),
  MeasureTheory.charFunDual (ProbabilityTheory.stdGaussian E) L = Complex.exp (-↑‖L‖ ^ 2 / 2)
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two one-preserving morphisms `f`, `g`,
`f / g` is the one-preserving morphism sending `x` to `f x / g x`.  -/
OneHom.instDiv : {M : Type u_2} → {N : Type u_3} → [inst : One M] → [inst_1 : DivisionMonoid N] → Div (OneHom M N)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.Hom.add_mul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R : C} [inst_3 : CategoryTheory.RingObj R] {X : C} (a b c : X ⟶ R),
  (a + b) * c = a * c + b * c
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.intermediateFieldEquivSubgroup.congr_simp : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [inst_4 : IsGalois F E],
  IsGalois.intermediateFieldEquivSubgroup = IsGalois.intermediateFieldEquivSubgroup
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.face.eq_1 : ∀ {n : ℕ} (i j : Fin (n + 2)) (h : j ≠ i),
  SSet.horn.face i j h = SSet.yonedaEquiv (CategoryTheory.Subfunctor.lift (SSet.stdSimplex.δ j) ⋯)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.flatten_pure : ∀ {α : Type u} (s : Stream'.WSeq α), Stream'.WSeq.flatten (Computation.pure s) = s
-- Mathlib.Order.Hom.Basic
OrderHom.uliftLeftMap_uliftRightMap_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β),
  f.uliftLeftMap.uliftRightMap = f.uliftMap
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_zero : ∀ {α : Type u_1} [inst : DecidableEq α], Multiset.toFinsupp 0 = 0
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldlM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (n : ℕ) (f : α → Fin n → m α) (x : α) (i : ℕ),
  Fin.foldlM.loop✝ n f x i =
    if h : i < n then do
      let x ← f x ⟨i, h⟩
      Fin.foldlM.loop✝ n f x (i + 1)
    else pure x
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a * b`
semiconjugates `x` to `z`.  -/
SemiconjBy.mul_left : ∀ {S : Type u_1} [inst : Semigroup S] {a b x y z : S}, SemiconjBy a y z → SemiconjBy b x y → SemiconjBy (a * b) x z
-- Mathlib.Data.Stream.Defs
/-- Interleave two streams.  -/
Stream'.«term_⋈_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslateData.mk.injEq : ∀ (ignoreArgsAttr : Lean.NameMapExtension (List ℕ)) (doTranslateAttr : Lean.NameMapExtension Bool)
  (unfoldBoundaries? : Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt)
  (translations : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo) (attrName : Lean.Name)
  (changeNumeral isDual : Bool) (guessNameExt : Mathlib.Tactic.GuessName.GuessNameExt)
  (ignoreArgsAttr_1 : Lean.NameMapExtension (List ℕ)) (doTranslateAttr_1 : Lean.NameMapExtension Bool)
  (unfoldBoundaries?_1 : Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt)
  (translations_1 : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo) (attrName_1 : Lean.Name)
  (changeNumeral_1 isDual_1 : Bool) (guessNameExt_1 : Mathlib.Tactic.GuessName.GuessNameExt),
  ({ ignoreArgsAttr := ignoreArgsAttr, doTranslateAttr := doTranslateAttr, unfoldBoundaries? := unfoldBoundaries?,
        translations := translations, attrName := attrName, changeNumeral := changeNumeral, isDual := isDual,
        guessNameExt := guessNameExt } =
      { ignoreArgsAttr := ignoreArgsAttr_1, doTranslateAttr := doTranslateAttr_1,
        unfoldBoundaries? := unfoldBoundaries?_1, translations := translations_1, attrName := attrName_1,
        changeNumeral := changeNumeral_1, isDual := isDual_1, guessNameExt := guessNameExt_1 }) =
    (ignoreArgsAttr = ignoreArgsAttr_1 ∧
      doTranslateAttr = doTranslateAttr_1 ∧
        unfoldBoundaries? = unfoldBoundaries?_1 ∧
          translations = translations_1 ∧
            attrName = attrName_1 ∧ changeNumeral = changeNumeral_1 ∧ isDual = isDual_1 ∧ guessNameExt = guessNameExt_1)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- In the space `ι → ℝ`, the Hausdorff measure coincides exactly with the Lebesgue measure.  -/
MeasureTheory.hausdorffMeasure_pi_real : ∀ {ι : Type u_4} [inst : Fintype ι], MeasureTheory.Measure.hausdorffMeasure ↑(Fintype.card ι) = MeasureTheory.volume
-- Mathlib.Algebra.Algebra.Basic
Algebra.coe_algebraMap_ofSubsemiring : ∀ {R : Type u_1} [inst : CommSemiring R] {C : Type u_4} [inst_1 : SetLike C R] [inst_2 : SubsemiringClass C R] (S : C),
  ⇑(algebraMap (↥S) R) = Subtype.val
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.upper : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RxcIterator α β → α