mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_1 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1)
  (decl : Lean.Compiler.LCNF.LetDecl pu)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.let decl with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_1 decl
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `isPGroup_iff_pow_pow_eq_one`. -/
IsPGroup.exists_pow_pow_eq_one : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ (g : G), ∃ k, g ^ p ^ k = 1
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.ConcreteCategory.forget_map_eq_ofHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Module.NatInt
/-- `nsmul` is equal to any other module structure via a cast.  -/
Nat.cast_smul_eq_nsmul : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ) (b : M),
  ↑n • b = n • b
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.mk : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α},
  (∀ ⦃a : α⦄, a ∉ u → f a = a) →
    (∀ ⦃a : α⦄, a ∈ u → P.Rel a (f a)) → (∀ ⦃a b : α⦄, P.Rel a b → f a = f b) → P.IsRepFun f
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_of_assemble₂_eq_some : ∀ {w x : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₂ w x = some c → ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = false
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mkIso'_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f : M.X ≅ N.X) [inst_2 : CategoryTheory.IsComonHom f.hom],
  (CategoryTheory.Comon.mkIso' f).inv.hom = f.inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ : Std.DTreeMap.Raw α β cmp} {l : List ((a : α) × β a)},
  (t₁.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) t₁ l)
-- Init.Prelude
/-- `LT α` is the typeclass which supports the notation `x < y` where `x y : α`. -/
LT : Type u → Type u
-- Mathlib.GroupTheory.ArchimedeanDensely
OrderAddMonoidIso.addArchimedean : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] (e : α ≃+o β) [Archimedean α], Archimedean β
-- Std.Http.Protocol.H1.Reader
/-- Closes the reader, transitioning to the closed state.
 -/
Std.Http.Protocol.H1.Reader.close : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_of_tendsto_aux : ∀ (f : CircleDeg1Lift) {τ' : ℝ}, Filter.Tendsto f.transnumAuxSeq Filter.atTop (nhds τ') → f.translationNumber = τ'
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct a morphism `AddMon.mk G ⟶ AddMon.mk H` from a  map `f : G ⟶ H` and a `IsAddMonHom f`
instance.  -/
CategoryTheory.AddMon.ofHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : C} →
        [inst_2 : CategoryTheory.AddMonObj A] →
          [inst_3 : CategoryTheory.AddMonObj B] →
            (f : A ⟶ B) → [CategoryTheory.IsAddMonHom f] → { X := A, addMon := inst_2 } ⟶ { X := B, addMon := inst_3 }
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Transport an exact pairing across an isomorphism in the first argument.  -/
CategoryTheory.exactPairingCongrLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X X' Y : C} → [CategoryTheory.ExactPairing X' Y] → (X ≅ X') → CategoryTheory.ExactPairing X Y
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.comp_id : ∀ {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q), (RootPairing.Equiv.id Q).comp f = f
-- Std.Async.System
/-- OS build.
 -/
Std.Async.System.OSInfo.version : Std.Async.System.OSInfo → String
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_inv : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (e : x = y),
  (AlgebraicGeometry.Scheme.residueFieldCongr e).inv = (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom
-- Mathlib.Algebra.Group.Defs
DivInvOneMonoid.mk : {G : Type u_2} → [toDivInvMonoid : DivInvMonoid G] → 1⁻¹ = 1 → DivInvOneMonoid G
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.denote.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign : α → Bool) (entry : Std.Sat.AIG.Entrypoint α),
  ⟦assign, entry⟧ = (Std.Sat.AIG.denote.go entry.ref.gate entry.aig.decls assign ⋯ ⋯ ^^ entry.ref.invert)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w : ℕ} {discr : aig.Ref}
  {lhs rhs : aig.RefVec w} {discr_1 : aig.Ref} {lhs_1 rhs_1 : aig.RefVec w},
  { discr := discr, lhs := lhs, rhs := rhs } = { discr := discr_1, lhs := lhs_1, rhs := rhs_1 } →
    discr = discr_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.CategoryTheory.Square
/-- The functor `(C ⥤ D) ⥤ Square C ⥤ Square D`.  -/
CategoryTheory.Square.mapFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Square D))
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_zero : Ordinal.veblen 0 = fun a => Ordinal.omega0 ^ a
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `AddMonoid.Coprod M N →+ N`.  -/
AddMonoid.Coprod.snd : {M : Type u_1} → {N : Type u_2} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → AddMonoid.Coprod M N →+ N
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_join_le_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R T : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet P R) T →
    Lean.Order.PartialOrder.rel (Lean.Order.meet Q R) T →
      Lean.Order.PartialOrder.rel (Lean.Order.meet (Lean.Order.join P Q) R) T
-- Aesop.Tree.AddRapp
Aesop.AddRapp.mk : Aesop.RuleApplication → Aesop.GoalRef → Aesop.RegularRule → Aesop.Percent → Aesop.AddRapp
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm_comp_self : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.PB.eq_1 : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R],
  LieAlgebra.Orthogonal.PB l R = Matrix.fromBlocks 1 0 0 (LieAlgebra.Orthogonal.PD l R)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
CategoryTheory.yonedaCommRingObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : C) [inst_3 : CategoryTheory.CommRingObj R] (X : Cᵒᵖ),
  (CategoryTheory.yonedaCommRingObj R).obj X = CommRingCat.of (Opposite.unop X ⟶ R)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- We can prove two cocone points `(s : Cocone F).pt` and `(t : Cocone G).pt` are isomorphic if
* both cocones are colimit cocones
* their indexing categories are equivalent via some `e : J ≌ K`,
* the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`.

This is the most general form of uniqueness of cocone points,
allowing relabelling of both the indexing category (up to equivalence)
and the functor (up to natural isomorphism).
 -/
CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cocone F} →
                {G : CategoryTheory.Functor K C} →
                  {t : CategoryTheory.Limits.Cocone G} →
                    CategoryTheory.Limits.IsColimit s →
                      CategoryTheory.Limits.IsColimit t → (e : J ≌ K) → (e.functor.comp G ≅ F) → (s.pt ≅ t.pt)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.equivAddOpposite_apply : ∀ {M : Type u_2} [inst : AddMonoid M] (f : M →ₑ[id] M), AddActionHom.End.equivAddOpposite f = AddOpposite.op (f 0)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsZeroApply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), IsZeroApply (UniformConvergenceCLM σ F 𝔖) E F
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.hf : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (self : SingularManifold X k I), Continuous self.f
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_true : Encodable.encode true = 1
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- Consider a pushout square involving types `X₁`, `X₂`, `X₃` and `X₄`:
```
     t
 X₁  ⟶  X₂
l|     |r  \
 v   b  v   \ r'
 X₃  ⟶  X₄   \
  \       k\  |
   \ b'     v v
    \______> X₅
```
Let `k : X₄ ⟶ X₅`, `r' : X₂ ⟶ X₅` and `b' : X₃ ⟶ X₅` be such
that `r ≫ k = r'` and `b ≫ k = b'`. Assume that
the outer square is a pullback, that `r'` is a monomorphism
and that `b'` is injective on the complement of the range of `l`,
then `k : X₄ ⟶ X₅` is a monomorphism.  -/
CategoryTheory.Limits.Types.mono_of_isPushout_of_isPullback : ∀ {X₁ X₂ X₃ X₄ X₅ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} {k : X₄ ⟶ X₅},
  CategoryTheory.IsPushout t l r b →
    ∀ {r' : X₂ ⟶ X₅} {b' : X₃ ⟶ X₅},
      CategoryTheory.IsPullback t l r' b' →
        CategoryTheory.CategoryStruct.comp r k = r' →
          CategoryTheory.CategoryStruct.comp b k = b' →
            ∀ [hr' : CategoryTheory.Mono r'],
              (∀ (x₃ y₃ : X₃),
                  x₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l) →
                    y₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l) →
                      (CategoryTheory.ConcreteCategory.hom b') x₃ = (CategoryTheory.ConcreteCategory.hom b') y₃ →
                        x₃ = y₃) →
                CategoryTheory.Mono k
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.mem_stabilizer_mk_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] (φ : K →+* ℂ) (σ : Gal(K/k)),
  σ ∈ MulAction.stabilizer Gal(K/k) (NumberField.InfinitePlace.mk φ) ↔ σ = 1 ∨ NumberField.ComplexEmbedding.IsConj φ σ
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousAt.coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F} {z : Z},
  ContinuousAt f z → ContinuousAt (fun z => ⇑(f z)) z
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.of_union_cover : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t u : Set α},
  MeasurableSet s →
    MeasurableSet t →
      Set.univ ⊆ s ∪ t → MeasurableSet (Subtype.val ⁻¹' u) → MeasurableSet (Subtype.val ⁻¹' u) → MeasurableSet u
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.map_id : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C : ConvexCone R M), ConvexCone.map LinearMap.id C = C
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.eq_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (f : HomologicalComplex.homotopyCofiber φ ⟶ K) (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  f =
    HomologicalComplex.homotopyCofiber.desc φ
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ) f)
      ((Homotopy.ofEq ⋯).trans
        (((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated monoids is finitely generated.  -/
Prod.instMonoidFG : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] [Monoid.FG M] [Monoid.FG N], Monoid.FG (M × N)
-- Mathlib.Topology.Compactness.Lindelof
cluster_point_of_Lindelof : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X] (f : Filter X) [f.NeBot] [CountableInterFilter f],
  ∃ x, ClusterPt x f
-- Mathlib.Algebra.GradedMonoid
/-- If all grades are the same type and themselves form a monoid, then there is a trivial grading
structure.  -/
Monoid.gMonoid : (ι : Type u_1) → {R : Type u_2} → [inst : AddMonoid ι] → [Monoid R] → GradedMonoid.GMonoid fun x => R
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_const : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} (x : ℂ) [inst : Γ.HasDetOne], ⇑(ModularForm.const x) = Function.const UpperHalfPlane x
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instOne : (M : Type u_4) → [inst : MulOne M] → One (Monoid.End M)
-- Mathlib.Algebra.Lie.OfAssociative
/-- A Lie module is *faithful* if the associated map `L → End M` is injective.  -/
LieModule.IsFaithful : (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] → [LieModule R L M] → Prop
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux2.eq_2 : ∀ (o₂ : ONote), o₂.opowAux2 (ONote.zero, 1) = 1
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.star_vec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : Star R] (x : Matrix m n R), star x.vec = (x.map star).vec
-- Mathlib.Computability.TuringMachine.Tape
/-- Given two `BlankRel` lists, there exists (constructively) a common meet.  -/
Turing.BlankRel.below : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {l₁ l₂ : List Γ} → Turing.BlankRel l₁ l₂ → { l // Turing.BlankExtends l l₁ ∧ Turing.BlankExtends l l₂ }
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- The `MonoidWithZero` version of `div_eq_div_iff_mul_eq_mul`.  -/
Commute.div_eq_div_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c d : G₀},
  Commute b d → b ≠ 0 → d ≠ 0 → (a / b = c / d ↔ a * d = c * b)
-- Std.Sat.AIG.CachedLemmas
/-- `AIG.mkAtomCached` never shrinks the underlying AIG.
 -/
Std.Sat.AIG.mkAtomCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (var : α),
  aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.one_toNat : Cardinal.toNat 1 = 1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mk.injEq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (toNonUnitalSubsemiring : NonUnitalSubsemiring A)
  (smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier)
  (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring A)
  (smul_mem'_1 : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring_1.carrier → c • x ∈ toNonUnitalSubsemiring_1.carrier),
  ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, smul_mem' := smul_mem'_1 }) =
    (toNonUnitalSubsemiring = toNonUnitalSubsemiring_1)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instAddCommGroup : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → AddCommGroup (SlashInvariantForm Γ k)
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `dist_eq_norm_sub'`. -/
dist_eq_norm' : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), dist a b = ‖b - a‖
-- Init.Data.Vector.Lemmas
Vector.toArray_cast : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} (h : n = m), (Vector.cast h xs).toArray = xs.toArray
-- Mathlib.Analysis.Convex.PathConnected
Path.segment_add_segment : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a b c d : E), (Path.segment a b).add (Path.segment c d) = Path.segment (a + c) (b + d)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- `gramSchmidt` produces linearly independent vectors when given linearly independent vectors.  -/
InnerProductSpace.gramSchmidt_linearIndependent : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E},
  LinearIndependent 𝕜 f → LinearIndependent 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f)
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.coe_iInf : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} {S : ι → Submonoid M}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.RepresentationTheory.Basic
Representation.norm.eq_1 : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : AddCommMonoid V] [inst_4 : Module k V] (ρ : Representation k G V), ρ.norm = ∑ g, ρ g
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_inv : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R), ↑A⁻¹ = (↑A).adjugate
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (fallback : β),
  Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k fallback =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if compare a k = Ordering.eq then some b else none)
          l).getD
      (Std.DTreeMap.Internal.Impl.Const.getD t k fallback)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, l.contains k = false → k ∈ t.insertManyIfNewUnit l → k ∈ t
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.add b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_5 a b
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.homCongr_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y),
  (α.homCongr β) f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f β.hom)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ofCore_map_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X Y : C} (g : X ⟶ Y) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Profunctor.ofCore P).map g).app X_1 = P.map g (CategoryTheory.CategoryStruct.id (Opposite.unop X_1))