mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Algebraic.Defs
/-- A subalgebra is algebraic if and only if it is algebraic as an algebra.  -/
Subalgebra.isAlgebraic_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.IsAlgebraic ↔ Algebra.IsAlgebraic R ↥S
-- Mathlib.Algebra.CharP.Defs
ringExpChar.eq_one : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [CharZero R], ringExpChar R = 1
-- Mathlib.RingTheory.DualNumber
DualNumber.fst_eq_zero_iff_eps_dvd : ∀ {R : Type u_1} [inst : Semiring R] {x : DualNumber R}, TrivSqZeroExt.fst x = 0 ↔ DualNumber.eps ∣ x
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.mem_invtSubmodule_iff : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E}
  {U : Submodule R E}, LinearMap.IsProj U f → (U ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [Inhabited α] {k : α} {f : β → β} {hc : k ∈ Std.ExtDTreeMap.Const.modify t k f},
  (Std.ExtDTreeMap.Const.modify t k f).getKey k hc = k
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpCacheKey.mk.sizeOf_spec : ∀ (variant : Lean.Name) (args : Lean.Elab.Tactic.Grind.DSimpArgs),
  sizeOf { variant := variant, args := args } = 1 + sizeOf variant + sizeOf args
-- Mathlib.NumberTheory.Harmonic.Int
harmonic_pos : ∀ {n : ℕ}, n ≠ 0 → 0 < harmonic n
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.opEquiv_apply : ∀ {M : Type u_2} [inst : Add M] (x : AddSubsemigroup M), AddSubsemigroup.opEquiv x = x.op
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.μ_pullback_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {f : R ⟶ X} (R_1 S : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) R_1 S))
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj R_1 S).hom f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj R_1).hom
        ((CategoryTheory.Over.pullback f).obj S).hom)
      (CategoryTheory.Limits.pullback.snd S.hom f)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.spanOp.match_1.splitter : (motive : CategoryTheory.Limits.WalkingSpan → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingSpan) →
    (Unit → motive none) →
      (Unit → motive (some CategoryTheory.Limits.WalkingPair.left)) →
        (Unit → motive (some CategoryTheory.Limits.WalkingPair.right)) → motive x
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_one : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M) (x : α), birkhoffSum f g 1 x = g x
-- Init.Data.Nat.Bitwise.Basic
/-- A helper for implementing bitwise operators on `Nat`.

Each bit of the resulting `Nat` is the result of applying `f` to the corresponding bits of the input
`Nat`s, up to the position of the highest set bit in either input.
 -/
Nat.bitwise : (Bool → Bool → Bool) → ℕ → ℕ → ℕ
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_sup : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s t : NonUnitalSubring R) (f : F),
  NonUnitalSubring.map f (s ⊔ t) = NonUnitalSubring.map f s ⊔ NonUnitalSubring.map f t
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.map_addUnits : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (y : ↥S), IsAddUnit (f ↑y)
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_div : ∀ {α : Type u_1} [inst : Div α] (a b : αᵒᵈ), OrderDual.ofDual (a / b) = OrderDual.ofDual a / OrderDual.ofDual b
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- Given a function `f` that approximates a linear equivalence on an open set `s`,
returns an open partial homeomorphism with `toFun = f` and `source = s`.  -/
ApproximatesLinearOn.toOpenPartialHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                (f : E → F) →
                  {f' : E ≃L[𝕜] F} →
                    (s : Set E) →
                      {c : NNReal} →
                        [CompleteSpace E] →
                          ApproximatesLinearOn f (↑f') s c →
                            Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → IsOpen s → OpenPartialHomeomorph E F
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.full_whiskeringRight_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] [F.Full],
  ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Full
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : ℕ) (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n)
  (size : ℕ) (k : α) (v : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β) (n : ℕ),
  x = Std.DTreeMap.Internal.Impl.inner size k v l r →
    x_1 = n →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
        | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) ≍
        h_2 size k v l r n
-- Mathlib.CategoryTheory.Localization.Predicate
/-- the functor `L` inverts `W`  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.inverts : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E), W.IsInvertedBy L
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom
      CategoryTheory.Limits.prod.fst =
    CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Three Subgroups Lemma** (via the Hall-Witt identity)  -/
AddSubgroup.addCommutator_addCommutator_eq_bot_of_rotate : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ H₃ : AddSubgroup G},
  ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥ → ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥ → ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaUncurry_apply : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : ι) (j : α i), δ i j) (i : ι) (j : α i),
  f.sigmaUncurry ⟨i, j⟩ = (f i) j
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Compute the discrimination trees for the theorems in the current file.  -/
Mathlib.Tactic.ClickSuggestions.computeModuleDiscrTrees : Mathlib.Tactic.ClickSuggestions.Choice → Option Lean.Name → Lean.CoreM Mathlib.Tactic.ClickSuggestions.PreDiscrTrees
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swapCompInr_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : D), (CategoryTheory.Sum.swapCompInr C D).hom.app X = CategoryTheory.CategoryStruct.id (Sum.inl X)
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.subtype_comp_inclusion : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p q : Submodule R M) (h : p ≤ q), q.subtype ∘ₗ Submodule.inclusion h = p.subtype
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((_ : α) × β)}
  {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
          k ∈ List.map Prod.fst toInsert →
            Std.Internal.List.getKey! k' (Std.Internal.List.insertListConst l toInsert) = k
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.not_isComplex_iff_isReal : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, ¬w.IsComplex ↔ w.IsReal
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ)
  {X Y : SimplexCategory} (f : X ⟶ Y),
  ((CategoryTheory.simplicialCosimplicialEquiv C).functor.obj F).map f = ((Opposite.unop F).map f.op).op
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.del.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (x_1 : RBTree.RBNode α) →
        (x_2 : RBTree.RBColor) →
          ((t : RBTree.RBNode α) → (x : RBTree.RBColor) → motive RBTree.RBNode.Path.root t x) →
            ((c : RBTree.RBColor) →
                (parent : RBTree.RBNode.Path α) →
                  (y : α) →
                    (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.red) →
              ((c : RBTree.RBColor) →
                  (a : RBTree.RBNode α) →
                    (y : α) →
                      (parent : RBTree.RBNode.Path α) →
                        (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.red) →
                ((c : RBTree.RBColor) →
                    (parent : RBTree.RBNode.Path α) →
                      (y : α) →
                        (b a : RBTree.RBNode α) →
                          motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.black) →
                  ((c : RBTree.RBColor) →
                      (a : RBTree.RBNode α) →
                        (y : α) →
                          (parent : RBTree.RBNode.Path α) →
                            (b : RBTree.RBNode α) →
                              motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.black) →
                    motive x x_1 x_2
-- Init.Prelude
/-- Helper function we use to create binder names that do not need to be unique.  -/
Lean.Name.simpMacroScopes : Lean.Name → Lean.Name
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.val_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (a b : GroupLike R A), ↑(a * b) = ↑a * ↑b
-- Mathlib.RingTheory.Nilpotent.Lemmas
nilradical_le_prime : ∀ {R : Type u_1} [inst : CommSemiring R] (J : Ideal R) [H : J.IsPrime], nilradical R ≤ J
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.awayToAwayLeft.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x x_1 : R) (e_x : x = x_1) [inst_4 : IsLocalization.Away x S] (y y_1 : R) (e_y : y = y_1)
  [inst_5 : Algebra R P] [inst_6 : IsLocalization.Away (y * x) P],
  IsLocalization.Away.awayToAwayLeft x y = IsLocalization.Away.awayToAwayLeft x_1 y_1
-- Init.Data.UInt.Bitwise
UInt8.toBitVec_and : ∀ (a b : UInt8), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.quasiIso_shift_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ),
  QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ) ↔ QuasiIso φ
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_pow : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (l : Mathlib.Tactic.FieldSimp.NF M) (r : ℕ),
  (l ^ r).eval = Mathlib.Tactic.FieldSimp.zpow' l.eval ↑r
-- Batteries.Data.List.Lemmas
List.findIdxsValues_eq_zip_filter_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ},
  List.findIdxsValues p xs s = (List.findIdxs p xs s).zip (List.filter p xs)
-- Mathlib.NumberTheory.LucasLehmer
/-- We construct the ring `X q` as ℤ/qℤ + √3 ℤ/qℤ.  -/
LucasLehmer.X : ℕ → Type
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.fst_of_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set α} {t : Set β},
  Bornology.IsBounded (s ×ˢ t) → t.Nonempty → Bornology.IsBounded s
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The map `Φ.toSucc X : X ⟶ Φ.Succ X`, as an element in `Arrow C`.  -/
CategoryTheory.SmallObject.SuccStruct.toSuccArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.SmallObject.SuccStruct C → C → CategoryTheory.Arrow C
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  (isMin : (a : α) → IsMax a → motive a) (succ : (a : α) → ¬IsMin a → motive (Order.pred a))
  (isSuccLimit : (a : α) → Order.IsPredLimit a → motive a),
  Order.isPredLimitRecOn b isMin succ isSuccLimit =
    Order.isPredPrelimitRecOn b succ fun a ha => if h : IsMax a then isMin a h else isSuccLimit a ⋯
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for subtraction on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalSub : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.unitCofork_π : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))],
  (CategoryTheory.Monad.MonadicityInternal.unitCofork A).π =
    G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
-- Mathlib.Algebra.Group.End
Equiv.Perm.coe_inv : ∀ {α : Type u_4} (f : Equiv.Perm α), ⇑f⁻¹ = ⇑(Equiv.symm f)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_natDegree_le_one_of_monic : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree ≤ 1 → f.Monic → f.Splits
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      Std.Internal.List.maxKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback =
        (Std.Internal.List.maxKey? l).elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.sub_mul_left_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (y - x * z) ↔ IsRelPrime x y
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- If `f : E → F` is surjective and `F` is finite-dimensional,
`f` has a continuous right inverse.  -/
ContinuousLinearMap.HasRightInverse.of_surjective_of_finiteDimensional : ∀ {𝕜 : Type u_7} [inst : NontriviallyNormedField 𝕜] {E : Type u_8} {F : Type u_9} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜 F] [IsTopologicalAddGroup F]
  [ContinuousSMul 𝕜 F] [T2Space F] {f : E →L[𝕜] F} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F],
  Function.Surjective ⇑f → f.HasRightInverse
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- If `F` is a normed `ℂ`-algebra and `x : F`, then there is a complex number `z` such that
`‖x - algebraMap ℂ F z‖ = 0` (whence `x = algebraMap ℂ F z`).  -/
NormedAlgebra.Complex.exists_norm_sub_smul_one_eq_zero : ∀ {F : Type u_1} [inst : NormedRing F] [NormOneClass F] [NormMulClass F] [inst_3 : NormedAlgebra ℂ F] (x : F),
  ∃ z, ‖x - (algebraMap ℂ F) z‖ = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.isAddMonHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} (self : M.Hom N), CategoryTheory.IsAddMonHom self.hom
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A section `s` of `V` is differentiable at `x ∈ e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
mdifferentiableAt_iff_localFrameCoeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {x' : M}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  x' ∈ e.baseSet →
    (MDiffAt (T% s) x' ↔ ∀ (i : ι), MDiffAt ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x')
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.isScalarTower : ∀ {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [inst : SMul T R] [inst_1 : SMul T M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : SMul T S] [IsScalarTower T S R] [IsScalarTower T S M],
  IsScalarTower T S (TrivSqZeroExt R M)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablePartitionSet_eq_iff : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] {n : ℕ} (a : α) {s : Set α},
  s ∈ MeasurableSpace.countablePartition α n → (MeasurableSpace.countablePartitionSet n a = s ↔ a ∈ s)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.one_le_mul_inv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a : M} (u : Mˣ), 1 ≤ a * ↑u⁻¹ ↔ ↑u ≤ a
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.medial_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [inst_5 : CharZero k] (s : Affine.Simplex k P n)
  (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S),
  (s.restrict S hS).medial = s.medial.restrict S ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.rlp_monomorphisms : (CategoryTheory.MorphismProperty.monomorphisms SSet).rlp = SSet.modelCategoryQuillen.I.rlp
-- Lean.Environment
Lean.OLeanLevel.adjustFileName : System.FilePath → Lean.OLeanLevel → System.FilePath
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
_private.Mathlib.Analysis.CStarAlgebra.Module.Defs.0.CStarModule.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.Data.Finset.Basic
Equiv.Finset.union_symm_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ s) (hi' : i ∈ s ∪ t),
  (Equiv.Finset.union s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F], IsBoundedLinearMap 𝕜 fun x => 0
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instOrdPosition.ord : Lean.Lsp.Position → Lean.Lsp.Position → Ordering
-- Std.Http.Data.URI.Basic
/-- A domain name represented as a validated, lowercase-normalized string.
Only ASCII alphanumeric characters, hyphens, and dots are allowed.
Each label cannot start or end with `-` and is limited to 63 characters.
Internationalized domain names must be converted to punycode before use.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2
 -/
Std.Http.URI.DomainName : Type
-- Lean.Structure
Lean.StructureResolutionOrderResult.mk.inj : ∀ {resolutionOrder : Array Lean.Name} {conflicts : Array Lean.StructureResolutionOrderConflict}
  {resolutionOrder_1 : Array Lean.Name} {conflicts_1 : Array Lean.StructureResolutionOrderConflict},
  { resolutionOrder := resolutionOrder, conflicts := conflicts } =
      { resolutionOrder := resolutionOrder_1, conflicts := conflicts_1 } →
    resolutionOrder = resolutionOrder_1 ∧ conflicts = conflicts_1
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_sup_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (K₁ K₂ : TopologicalSpace.Compacts G),
  (interior U).Nonempty →
    MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (K₁ ⊔ K₂) ≤
      MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.ext : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] {f g : A ≃⋆+* B}, (∀ (a : A), f a = g a) → f = g
-- Mathlib.Algebra.Order.Field.Basic
/-- For the single implications with fewer assumptions, see `one_div_lt_one_div_of_lt` and
`lt_of_one_div_lt_one_div`  -/
one_div_lt_one_div_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (1 / a < 1 / b ↔ b < a)
-- Mathlib.CategoryTheory.Iso
/-- Notation for an isomorphism in a category.  -/
CategoryTheory.«term_≅_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α},
  LowerSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≤ y) → f x ≤ y
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.toLieSubalgebra.congr_simp : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {h h_1 : L}
  (e_h : h = h_1) {e e_1 : L} (e_e : e = e_1) {f f_1 : L} (e_f : f = f_1) (t : IsSl2Triple h e f),
  IsSl2Triple.toLieSubalgebra R t = IsSl2Triple.toLieSubalgebra R ⋯