mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (M : Λ → Turing.TM2.Stmt Γ Λ σ) (S : Finset Λ),
  Turing.TM2.stmts M S = Finset.insertNone (S.biUnion fun q => Turing.TM2.stmts₁ (M q))
-- Mathlib.Algebra.Star.Unitary
Unitary.smul_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : Monoid A] [inst_2 : MulAction R A] [SMulCommClass R A A]
  [IsScalarTower R A A] [inst_5 : StarMul R] [inst_6 : StarMul A] [StarModule R A] (r : ↥(unitary R)) {a : A},
  a ∈ unitary A → r • a ∈ unitary A
-- Mathlib.Order.Category.Lat
Lat.ext_iff : ∀ {X Y : Lat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.neg : {M N : SemiNormedGrp} → Neg (M ⟶ N)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFaithfulArrowArrowForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q W : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative],
  (CategoryTheory.MorphismProperty.Arrow.forget P Q W).Faithful
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop}
  (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
-- Std.Async.Process
Std.IO.Process.instReprResourceUsageStats : Repr Std.IO.Process.ResourceUsageStats
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationAdjunctionLeft_unit_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (X : CategoryTheory.Functor C D)
  (x : C),
  ((CategoryTheory.evaluationAdjunctionLeft D c).unit.app X).app x = CategoryTheory.Limits.Pi.lift fun g => X.map g
-- Mathlib.Computability.MyhillNerode
Language.leftQuotient_append : ∀ {α : Type u} (L : Language α) (x y : List α), L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.isLittleO_of_lt_exps_right : ∀ {left right : Tactic.ComputeAsymptotics.Basis} {t1 t2 : Tactic.ComputeAsymptotics.Monomial},
  Tactic.ComputeAsymptotics.WellFormedBasis (left ++ right) →
    List.length t1.unit = List.length left + List.length right →
      List.length t2.unit = List.length right →
        t1.coef ≠ 0 →
          List.replicate (List.length left) 0 ++ t2.unit < t1.unit →
            t2.toFun right =o[Filter.atTop] t1.toFun (left ++ right)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.comp : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g₀ g₁ : C(Y, Z)} {f₀ f₁ : C(X, Y)},
  g₀.Homotopic g₁ → f₀.Homotopic f₁ → (g₀.comp f₀).Homotopic (g₁.comp f₁)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If a linear map has a retraction, then the map it induces on exterior powers is injective.  -/
exteriorPower.map_injective : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (g : N →ₗ[R] M),
  g ∘ₗ f = LinearMap.id → Function.Injective ⇑(exteriorPower.map n f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  [inst_3 : Inhabited α], (↑m).WF → ∀ {k : α}, m.contains k = true → m.getKey! k = k
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.comp_tensorRId_eq : ∀ {R : Type uR} {M₁ : Type uM₁} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Invertible 2] (Q₁ : QuadraticForm R M₁),
  QuadraticMap.comp Q₁ ↑(TensorProduct.rid R M₁) = Q₁.tmul QuadraticMap.sq
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Context for the `AbstractM` monad used to implement `abstractGroundMismatches?`  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.Context : Type
-- Std.Data.HashMap.Raw
/-- Returns an array of all keys present in the hash map in some order.  -/
Std.HashMap.Raw.keysArray : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Array α
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_pow : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (f : (i : ι) → E i →L[𝕜] E i) (n : ℕ),
  PiTensorProduct.mapL (f ^ n) = PiTensorProduct.mapL f ^ n
-- Mathlib.NumberTheory.Height.Projectivization
/-- Extension for the `positivity` tactic: `Projectivization.mulHeight` is always positive.  -/
Mathlib.Meta.Positivity.evalProjMulHeight : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.id_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData),
  (CategoryTheory.ShortComplex.RightHomologyMapData.id h).φH = CategoryTheory.CategoryStruct.id h.H
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Default delaborator for applications.
 -/
Lean.PrettyPrinter.Delaborator.delabApp : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {p : α × β},
  Std.ExtDTreeMap.Const.insertMany t (p :: l) = Std.ExtDTreeMap.Const.insertMany (t.insert p.1 p.2) l
-- Aesop.Tree.Data
Aesop.GoalState.provenByNormalization : Aesop.GoalState
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x : ↑(Set.Icc 0 1)},
  ↑x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_le_sq₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀],
  0 ≤ a → 0 ≤ b → (a ^ 2 ≤ b ^ 2 ↔ a ≤ b)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {β : ι → Type u_10} {m : (x : ι) → MeasurableSpace (β x)} {f : (x : ι) → Ω → β x},
  ProbabilityTheory.Kernel.iIndepFun f κ 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The configuration translation.  -/
Turing.TM0to1.trCfg : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {Λ : Type u_2} →
      [inst_1 : Inhabited Λ] →
        Turing.TM0.Machine Γ Λ → Turing.TM0.Cfg Γ Λ → Turing.TM1.Cfg Γ (Turing.TM0to1.Λ' Γ Λ) Unit
-- Mathlib.Data.Set.Piecewise
Set.piecewise_insert_self : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) {j : α}
  [inst : (i : α) → Decidable (i ∈ insert j s)], (insert j s).piecewise f g j = f j
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.piToPiTop_map : ∀ {I : Type u} (X : I → TopCat) {X_1 Y : (i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))}
  (p : X_1 ⟶ Y), (FundamentalGroupoidFunctor.piToPiTop X).map p = Path.Homotopic.pi p
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.disconnect_objs : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C), S.disconnect.objs = S.objs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_eq_get! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {a : α} {h : Std.DTreeMap.Internal.Impl.contains a t = true},
      Std.DTreeMap.Internal.Impl.Const.get t a h = Std.DTreeMap.Internal.Impl.Const.get! t a
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.reflects_cofiltered_limits : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] (J : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsCofiltered J],
  CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.logDeriv_exp : logDeriv Complex.exp = 1
-- Init.Data.Function
Function.RightInverse.surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse g f → Function.Surjective f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₂.contains k = false → (m₁.diff m₂).get! k = m₁.get! k
-- Mathlib.Algebra.CubicDiscriminant
/-- The structure representing a cubic polynomial.  -/
Cubic : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {f g : E.Hom F} →
            (H : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i)) →
              (a : (i : E.I₀) → E.X i ⟶ F.Y (H i)) →
                (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₁ (H i)) = f.h₀ i) →
                  (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₂ (H i)) = g.h₀ i) →
                    CategoryTheory.PreOneHypercover.Homotopy f g
-- Std.Time.Zoned.Database.TzIf
/-- Represents the header of a TZif file, containing metadata about the file's structure.
 -/
Std.Time.TimeZone.TZif.Header : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.vec : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig len) → aig.RefVec self.w
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_snd_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) (j : ℕ) (hj : j < k),
  (F.intervalGapsWithin h a b ↑j).2 = ((F.orderEmbOfFin h) ⟨j, hj⟩).1
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_bot_of_ne : ∀ {V : Type u_1} {u v : V}, u ≠ v → ⊥.edist u v = ⊤
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  [hi : Inhabited β] {f : β → β},
  (t.modify k f)[k']! = if cmp k k' = Ordering.eq then (Option.map f t[k]?).get! else t[k']!
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.taylorEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (r : R),
  Polynomial.taylorEquiv r =
    { toFun := (↑↑(Polynomial.taylorAlgHom r).toRingHom).toFun, invFun := ⇑(Polynomial.taylorAlgHom (-r)),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Config.mk.injEq : ∀ (verbose enforceUnfoldReducible enforceFoldProjs verbose_1 enforceUnfoldReducible_1 enforceFoldProjs_1 : Bool),
  ({ verbose := verbose, enforceUnfoldReducible := enforceUnfoldReducible, enforceFoldProjs := enforceFoldProjs } =
      { verbose := verbose_1, enforceUnfoldReducible := enforceUnfoldReducible_1,
        enforceFoldProjs := enforceFoldProjs_1 }) =
    (verbose = verbose_1 ∧ enforceUnfoldReducible = enforceUnfoldReducible_1 ∧ enforceFoldProjs = enforceFoldProjs_1)
-- Init.Data.String.Lemmas.Basic
String.singleton_ne_empty : ∀ {c : Char}, String.singleton c ≠ ""
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_eq_zero : ∀ {M : Type u_5} [inst : AddCommMonoid M] {s : Multiset M}, (∀ x ∈ s, x = 0) → s.sum = 0
-- Mathlib.Algebra.Module.LocalizedModule.Int
IsLocalizedModule.isInteger_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') {a : R} {x : M'},
  IsLocalizedModule.IsInteger f x → IsLocalizedModule.IsInteger f (a • x)
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.mem_fintsupport_iff : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) (i : ι),
  i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport ⇑(ρ i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k k' : α} {f : β k → β k},
  (t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.C_injective : ∀ {R : Type u_1} [inst : Semiring R], Function.Injective ⇑PowerSeries.C
-- Init.Data.UInt.Bitwise
UInt16.xor_zero : ∀ {a : UInt16}, a ^^^ 0 = a
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A vector space with a nonzero vector `v` has dimension 1 iff `v` spans.
 -/
finrank_eq_one_iff_of_nonzero : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V),
  v ≠ 0 → (Module.finrank K V = 1 ↔ K ∙ v = ⊤)
-- Mathlib.Data.PFunctor.Univariate.M
/-- similar to `isubtree` but returns the data at the end of the path instead
of the whole subtree  -/
PFunctor.M.iselect : {F : PFunctor.{uA, uB}} → [DecidableEq F.A] → [Inhabited F.M] → PFunctor.Approx.Path F → F.M → F.A
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.finsetMap : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {s : Finset α},
  G.IsClique ↑s → (SimpleGraph.map (⇑f) G).IsClique ↑(Finset.map f s)
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.polynomial_map_coe : ∀ {U : Type u_2} {V : Type u_3} [inst : CommSemiring U] [inst_1 : CommSemiring V] {φ : U →+* V} {f : Polynomial U},
  ↑(Polynomial.map φ f) = (PowerSeries.map φ) ↑f
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The free-forgetful adjunction for additive monoids.  -/
AddMonCat.adj : AddMonCat.free ⊣ CategoryTheory.forget AddMonCat
-- Init.Data.Function
Function.Injective.ne_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {x y : α} {z : β}, f y = z → (f x ≠ z ↔ x ≠ y)
-- Lean.Meta.Eqns
/-- The equational theorem for a definition can be private even if the definition itself is not.
So un-private the name here when looking for a declaration
 -/
Lean.Meta.declFromEqLikeName : Lean.Environment → Lean.Name → Option (Lean.Name × String)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [inst_2 : CategoryTheory.IsIso h.unit]
  (X : C), h.whiskerLeftLCounitIsoOfIsIsoUnit.inv.app X = L.map (h.unit.app X)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_negPart_inj : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a b : α} [AddLeftMono α], a⁺ = b⁺ ∧ a⁻ = b⁻ ↔ a = b
-- Mathlib.Topology.Separation.Hausdorff
isClosed_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {f g : Y → X},
  Continuous f → Continuous g → IsClosed {y | f y = g y}
-- Mathlib.CategoryTheory.Action.Basic
/-- Restricting scalars along a monoid isomorphism induces an equivalence of categories.  -/
Action.resEquiv : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_3} → {H : Type u_4} → [inst_1 : Monoid G] → [inst_2 : Monoid H] → G ≃* H → (Action V H ≌ Action V G)
-- Init.Data.List.Attach
List.foldr_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : List (Subtype P)} {f : α → β → β} {x : β},
  List.foldr f x xs.unattach =
    List.foldr
      (fun x s =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint s (f x) (binderNameHint h () (f (wfParam x) s))))
      x xs
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.degree 0 = 0
-- Mathlib.Order.BoundedOrder.Lattice
max_top_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] (a : α), max ⊤ a = ⊤
-- Mathlib.RingTheory.Valuation.Integers
_private.Mathlib.RingTheory.Valuation.Integers.0.Valuation.term𝓞 : Lean.ParserDescr
-- Mathlib.RingTheory.Algebraic.Integral
instIsAlgebraicMvPolynomialOfNoZeroDivisors_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] {σ : Type u_4} [NoZeroDivisors S],
  Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, a ∉ m → m.getKeyD a fallback = fallback
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasEigenvalue.exists_hasEigenvector : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.HasEigenvalue μ → ∃ v, f.HasEigenvector μ v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (k, v) ∈ t.toList ↔ t.getKey? k = some k ∧ t[k]? = some v
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Transports a `CompStruct` between edges `e₀₁`, `e₁₂` and `e₀₂` to a `CompStruct` between edges
`f₀₁`, `f₁₂` and `f₀₂` along equalities of 1-simplices `eᵢⱼ.edge = fᵢⱼ.edge`.  -/
SSet.Edge.CompStruct.ofEq : {X : SSet} →
  {x₀ x₁ x₂ y₀ y₁ y₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {f₀₁ : SSet.Edge y₀ y₁} →
        {e₁₂ : SSet.Edge x₁ x₂} →
          {f₁₂ : SSet.Edge y₁ y₂} →
            {e₀₂ : SSet.Edge x₀ x₂} →
              {f₀₂ : SSet.Edge y₀ y₂} →
                e₀₁.CompStruct e₁₂ e₀₂ →
                  e₀₁.edge = f₀₁.edge → e₁₂.edge = f₁₂.edge → e₀₂.edge = f₀₂.edge → f₀₁.CompStruct f₁₂ f₀₂
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).f₁₃ = F.map sq.f₁₃
-- Mathlib.Control.Traversable.Lemmas
Traversable.map_eq_traverse_id : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {β γ : Type u} (f : β → γ),
  Functor.map f = Id.run ∘ traverse (pure ∘ f)
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_eq_top : ∀ {n : ℕ∞}, ↑n = ⊤ ↔ n = ⊤
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι),
  c.prev j = i →
    ∀ (hk : c.next j = k) {A : C} (x₂ x₂' : A ⟶ K.X j) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0)
      (hx₂' : CategoryTheory.CategoryStruct.comp x₂' (K.d j k) = 0),
      CategoryTheory.CategoryStruct.comp (K.liftCycles x₂ k hk hx₂) (K.homologyπ j) =
          CategoryTheory.CategoryStruct.comp (K.liftCycles x₂' k hk hx₂') (K.homologyπ j) ↔
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₁,
              CategoryTheory.CategoryStruct.comp π x₂ =
                CategoryTheory.CategoryStruct.comp π x₂' + CategoryTheory.CategoryStruct.comp x₁ (K.d i j)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsInitial.uniqueUpToIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I I' : C} (hI : CategoryTheory.Limits.IsInitial I)
  (hI' : CategoryTheory.Limits.IsInitial I'), (hI.uniqueUpToIso hI').inv = hI'.to I
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_toSlice_iff : ∀ {s : String}, s.toSlice.isEmpty = true ↔ s = ""
-- Mathlib.Data.Finset.Image
/-- If a `Finset` of a subtype is converted to the main type with
`Embedding.subtype`, the result does not contain any value that does
not satisfy the property of the subtype.  -/
Finset.notMem_map_subtype_of_not_property : ∀ {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α},
  ¬p a → a ∉ Finset.map (Function.Embedding.subtype fun x => p x) s
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.updateLazy.unsafe_1 : IO.Ref ProofWidgets.RefreshComponent.RefreshState → BaseIO ProofWidgets.RefreshComponent.RefreshState
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.public : {α : Type} → Lean.VisibilityMap✝ α → α
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instOne : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoidWithOne (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] → One (PiTensorProduct R fun i => A i)
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.term : Lean.Term → Lean.Expr → Aesop.ElabRuleTerm
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.inclusion_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Core C),
  (CategoryTheory.Core.inclusion C).obj self = self.of
-- Mathlib.Order.Monotone.Defs
monotone_iff_apply₂ : ∀ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [inst : (i : ι) → Preorder (β i)] [inst_1 : Preorder α]
  {f : α → (i : ι) → β i}, Monotone f ↔ ∀ (i : ι), Monotone fun x => f x i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Equation.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.Equation P = ((MvPolynomial.eval P) W'.polynomial = 0)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_toNNReal_iff : ∀ {r p : ℝ}, 0 ≤ p → (r.toNNReal ≤ p.toNNReal ↔ r ≤ p)
-- Mathlib.Data.Set.Operations
Set.mem_image2_of_mem : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β},
  a ∈ s → b ∈ t → f a b ∈ Set.image2 f s t
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_range : ∀ {M : Type u_1} [inst : AddMonoid M] {M' : Type u_3} [inst_1 : AddMonoid M'] [AddMonoid.FG M] (f : M →+ M'),
  AddMonoid.FG ↥(AddMonoidHom.mrange f)
-- Lean.Meta.LitValues
_private.Lean.Meta.LitValues.0.Lean.Meta.getRatValue?.getRatValueNum? : Lean.Expr → Lean.MetaM (Option ℚ)