mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.StdBasis
Pi.basis_apply : ∀ {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [inst : Semiring R]
  [inst_1 : (i : η) → AddCommMonoid (Ms i)] [inst_2 : (i : η) → Module R (Ms i)] [inst_3 : Fintype η]
  [inst_4 : DecidableEq η] (s : (j : η) → Module.Basis (ιs j) R (Ms j)) (ji : (j : η) × ιs j),
  (Pi.basis s) ji = Pi.single ji.fst ((s ji.fst) ji.snd)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t = true → t.getKey? k = some k
-- Mathlib.Algebra.Group.Action.Defs
AddCommute.vadd_left_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : AddGroup G] {g : G} [inst_1 : Add H] [inst_2 : AddAction G H]
  [VAddCommClass G H H] [VAddAssocClass G H H] {a b : H}, AddCommute (g +ᵥ a) b ↔ AddCommute a b
-- Mathlib.Order.CompleteBooleanAlgebra
sSup_inf_sSup : ∀ {α : Type u} [inst : Order.Frame α] {s t : Set α}, sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_iso_of_essSurj_of_full : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.EssSurj] [R.functor.Full] [R.IsInduced] [L.functor.EssSurj]
  [W₂'.RespectsIso] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.HasRightResolutions ↔ B.HasRightResolutions
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.go : {α : Type u_1} → (α → α → Ordering) → Array α → Array α → ℕ → Ordering
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The orthocenter equals the Monge point.  -/
Affine.Triangle.orthocenter_eq_mongePoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P), t.orthocenter = Affine.Simplex.mongePoint t
-- Mathlib.CategoryTheory.Limits.Over
/-- Given an arrow `X ⟶ c.pt`, the diagram `J ⥤ C` can be lifted to `Under X ⥤ C`, and
the cone `c` also lifts to the diagram on `Under`.  -/
CategoryTheory.Under.liftCone : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            {X : C} →
              (f : X ⟶ c.pt) →
                CategoryTheory.Limits.Cone
                  (CategoryTheory.Under.lift F
                    (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f) c.π))
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_eq_zero_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, Multiset.Ico a b = 0 ↔ ¬a < b
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.map_subst : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] {a : MvPowerSeries τ R},
  PowerSeries.HasSubst a →
    ∀ {h : R →+* S} (f : PowerSeries R),
      (MvPowerSeries.map h) (PowerSeries.subst a f) =
        PowerSeries.subst ((MvPowerSeries.map h) a) ((PowerSeries.map h) f)
-- Mathlib.Algebra.Order.Module.Defs
IsStrictOrderedModule.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [inst_4 : Zero β] [toPosSMulStrictMono : PosSMulStrictMono α β] [toSMulPosStrictMono : SMulPosStrictMono α β],
  IsStrictOrderedModule α β
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Converse of pons asinorum**, vector angle form.  -/
InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x (x - y) = InnerProductGeometry.angle y (y - x) →
    InnerProductGeometry.angle x y ≠ Real.pi → ‖x‖ = ‖y‖
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_mul_def : ∀ {R : Type u} [inst : Add R] (x y : Tropical R), x * y = Tropical.trop (Tropical.untrop x + Tropical.untrop y)
-- Init.Data.List.Lemmas
List.head_mem : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head h ∈ l
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.colimit_sound : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j'),
  (CategoryTheory.ConcreteCategory.hom (F.map f)) x = x' →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x'
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_antitone_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f g : Filter β} {p : β → Prop} {u : β → α},
  f ≤ g → Filter.bliminf u g p ≤ Filter.bliminf u f p
-- Mathlib.Order.Filter.SmallSets
Filter.monotone_smallSets : ∀ {α : Type u_1}, Monotone Filter.smallSets
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.uniqueHomToTrivial_default_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Comon C), default.hom = CategoryTheory.ComonObj.counit
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The basis of the `unitLattice` obtained by mapping `basisModTorsion` via `logEmbedding`.  -/
NumberField.Units.basisUnitLattice : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → Module.Basis (Fin (NumberField.Units.rank K)) ℤ ↥(NumberField.Units.unitLattice K)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_diff_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.IsFibrant
    (HomotopicalAlgebra.CofibrantObject.ι.obj (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.obj X))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The morphism to `K.cycles i` that is induced by a "cycle", i.e. a morphism
to `K.X i` whose postcomposition with the differential is zero.  -/
HomologicalComplex.liftCycles' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            {i : ι} →
              [inst_2 : K.HasHomology i] →
                {A : C} →
                  (k : A ⟶ K.X i) →
                    (j : ι) → c.Rel i j → CategoryTheory.CategoryStruct.comp k (K.d i j) = 0 → (A ⟶ K.cycles i)
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.mk.inj : ∀ {α : Type u} {inner inner_1 : Std.HashMap.Raw α Unit}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_algebraMap : ∀ (R : Type uR) {S : Type uS} (A : Type uA) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (s : Set S),
  Algebra.adjoin R (⇑(algebraMap S A) '' s) = Subalgebra.map (IsScalarTower.toAlgHom R S A) (Algebra.adjoin R s)
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.add.sizeOf_spec : ∀ (e : Lean.Expr) (k : ℕ), sizeOf (Lean.Meta.Sym.Offset.add e k) = 1 + sizeOf e + sizeOf k
-- Mathlib.Order.Lattice
OrderDual.instSemilatticeInf : (α : Type u_1) → [h : SemilatticeSup α] → SemilatticeInf αᵒᵈ
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_le : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.dedup ≤ s
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel.refl : ∀ {R : Type u} [inst : Rack R] {a : Rack.PreEnvelGroup R}, Rack.PreEnvelGroupRel R a a
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Power.denote.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k),
  (k = 0 → False) →
    (k = 1 → False) →
      (match k with
        | 0 => h_1 ()
        | 1 => h_2 ()
        | k => h_3 k) =
        h_3 k
-- Batteries.Data.String.Lemmas
String.rawEndPos_mk : ∀ (cs : List Char), (String.ofList cs).rawEndPos = { byteIdx := String.utf8Len cs }
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.yang_baxter' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
      (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y Z).hom X)) =
    CategoryTheory.monoidalComp
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z))
      (CategoryTheory.monoidalComp
        (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
          (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y)
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (β_ X Y).hom)))
        (CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y) X)))
-- Batteries.Lean.EStateM
EStateM.run'_fromStateM : ∀ {σ α ε : Type} (x : StateM σ α) (s : σ), (EStateM.fromStateM x).run' s = some (StateT.run' x s)
-- Mathlib.MeasureTheory.Measure.AddContent
_private.Mathlib.MeasureTheory.Measure.AddContent.0.MeasureTheory.AddContent.supClosureFun.eq_1 : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] (m : MeasureTheory.AddContent G C)
  (s : Set α),
  MeasureTheory.AddContent.supClosureFun✝ m s =
    if h : ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s = ⋃₀ ↑J then ∑ s ∈ h.choose, m s else 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_zero_inj : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}},
  Order.IsNormal f → 0 < f 0 → (Ordinal.veblenWith f o₁ 0 = Ordinal.veblenWith f o₂ 0 ↔ o₁ = o₂)
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `smul_finsum` for a version that works even when the support of `f` is not finite,
but with slightly stronger typeclass requirements.  -/
smul_finsum' : ∀ {ι : Type u_3} {R : Type u_7} {M : Type u_8} [inst : AddCommMonoid M] [inst_1 : DistribSMul R M] (c : R) {f : ι → M},
  Function.HasFiniteSupport f → c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.insert k).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Order.Filter.Map
Filter.instLawfulApplicative : LawfulApplicative Filter
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H ≤ K → ((H.subgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.cond_false : ∀ {w : ℕ} (discr : Bool) (lhs rhs : BitVec w), (discr || (bif discr then lhs else rhs) == rhs) = true
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Monoid.End M` is equivalent to `AddMonoid.End (Additive M)`.  -/
MulEquiv.Monoid.End : {M : Type u_4} → [inst : Monoid M] → Monoid.End M ≃* AddMonoid.End (Additive M)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.of_image_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  ↑e '' (e.source ∩ s) = e.target ∩ t → e.IsImage s t
-- Mathlib.Order.Filter.NAry
Filter.HasBasis.map₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : Filter α} {g : Filter β} {ι : Type u_11} {ι' : Type u_12}
  {p : ι → Prop} {q : ι' → Prop} {s : ι → Set α} {t : ι' → Set β} (m : α → β → γ),
  f.HasBasis p s →
    g.HasBasis q t → (Filter.map₂ m f g).HasBasis (fun i => p i.1 ∧ q i.2) fun i => Set.image2 m (s i.1) (t i.2)
-- Mathlib.Condensed.Explicit
/-- A condensed object satisfies the equalizer condition.  -/
Condensed.equalizerCondition : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (X : Condensed A),
  CategoryTheory.regularTopology.EqualizerCondition X.obj
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_ne_zero_trans : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, H.relIndex K ≠ 0 → K.relIndex L ≠ 0 → H.relIndex L ≠ 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map.eq_1 : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (n : ℕ),
  groupCohomology.map f φ n = HomologicalComplex.homologyMap (groupCohomology.cochainsMap f φ) n
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_smul_le : ∀ {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (s : S) (x : HahnSeries Γ R)
  [inst_2 : SMulZeroClass S R], (s • x).cardSupp ≤ x.cardSupp
-- Mathlib.Data.List.Sigma
List.lookupAll_sublist : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)),
  (List.map (Sigma.mk a) (List.lookupAll a l)).Sublist l
-- Mathlib.Algebra.Group.Defs
/-- A commutative multiplicative magma is a type with a multiplication which commutes.  -/
CommMagma : Type u → Type u
-- Mathlib.Data.ENat.Basic
ENat.self_le_mul_left : ∀ {c : ℕ∞} (a : ℕ∞), c ≠ 0 → a ≤ c * a
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : InfSet α], sInfHom.instInhabited α = { default := sInfHom.id α }
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The norm of the `0` operator is `0`.  -/
ContinuousLinearMap.opNorm_zero : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}, ‖0‖ = 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Roi α → Std.DTreeMap.Internal.Const.RoiSliceData α β
-- Init.Data.List.Find
List.idxOf_eq_length : ∀ {α : Type u_1} {a : α} [inst : BEq α] [LawfulBEq α] {l : List α}, a ∉ l → List.idxOf a l = l.length
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.mk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T} {A B : T}
  (f : A ⟶ B) (hf : P f), (CategoryTheory.MorphismProperty.Arrow.mk f hf).hom = f
-- Lean.Meta.Match.SolveOverlap
/-- `fvarId` refers to the local declaration selected for the application of the `injection` tactic.  -/
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.subgoal : Lean.FVarId → Lean.MVarId → Lean.Meta.Match.InjectionAnyResult✝
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- **Alias** of `mvfderiv_add`. -/
extDerivFun_add : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g g' : M → F} {x : M}, MDiffAt g x → MDiffAt g' x → d% (g + g') x = d% g x + d% g' x
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_ι_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.eTruncLTι (WithBotTop.coe n) = t.truncLTι n
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
/-- A semilinear equivalence from `V` to `W` determines an isomorphism of general linear
groups.  -/
LinearMap.GeneralLinearGroup.congrLinearEquiv : {R₁ : Type u_3} →
  {R₂ : Type u_4} →
    {M₁ : Type u_6} →
      {M₂ : Type u_7} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M₁] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R₁ →+* R₂} →
                      {σ₂₁ : R₂ →+* R₁} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] →
                            (M₁ ≃ₛₗ[σ₁₂] M₂) → LinearMap.GeneralLinearGroup R₁ M₁ ≃* LinearMap.GeneralLinearGroup R₂ M₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.of_forall_contains_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  (∀ (k : α), t₁.contains k = t₂.contains k) → t₁.Equiv t₂
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_nnratCast : ∀ {K : Type u_1} [inst : RCLike K] (q : ℚ≥0), ‖↑q‖ = ↑q
-- Std.Time.Duration
/-- Negates a `Duration`, flipping its second and nanosecond values.
 -/
Std.Time.Duration.neg : Std.Time.Duration → Std.Time.Duration
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.liftCycles_homologyπ_eq_zero_of_boundary : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : A ⟶ S.X₂) (x : A ⟶ S.X₁)
  (hx : k = CategoryTheory.CategoryStruct.comp x S.f),
  CategoryTheory.CategoryStruct.comp (S.liftCycles k ⋯) S.homologyπ = 0
-- Mathlib.Data.Set.Pairwise.Chain
IsChain.pairwise_iUnion₂ : ∀ {α : Type u_1} {c : Set (Set α)} {r : α → α → Prop},
  IsChain (fun x1 x2 => x1 ⊆ x2) c → ((⋃ s ∈ c, s).Pairwise r ↔ ∀ s ∈ c, s.Pairwise r)
-- Mathlib.RingTheory.Henselian
/-- A ring `R` that is `I`-adically complete is Henselian at `I`.  -/
IsAdicComplete.henselianRing : ∀ (R : Type u_1) [inst : CommRing R] (I : Ideal R) [IsAdicComplete I R], HenselianRing R I
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_empty : ∀ {α : Type u} [BEq α] [Hashable α], ∅.isEmpty = true
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.mapIso_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ≅ g b),
  (CategoryTheory.Limits.biproduct.mapIso p).hom = CategoryTheory.Limits.biproduct.map fun b => (p b).hom
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
/-- `continuousMapPresheaf` is isomorphic to the composition of the forgetful
functor to `TopCat` and the yoneda embedding.  -/
AlgebraicGeometry.continuousMapPresheafIsoUlift : (T : Type v) →
  [inst : TopologicalSpace T] →
    AlgebraicGeometry.continuousMapPresheaf T ≅
      AlgebraicGeometry.Scheme.forgetToTop.op.comp
        (TopCat.uliftFunctor.op.comp (CategoryTheory.yoneda.obj (TopCat.of (ULift.{u_1, v} T))))
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_eq_singleton_of_subsingleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α], 0 ≤ ε → Metric.closedBall x ε = {x}
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb →
    ∀ {p : β → Prop}, (∀ᵐ (x : β) ∂μb, p x) → ∀ᵐ (x : α) ∂μa, p (f x)
-- Mathlib.ModelTheory.LanguageMap
/-- A language equivalence maps the symbols of one language to symbols of another bijectively.  -/
FirstOrder.Language.LEquiv : FirstOrder.Language → FirstOrder.Language → Type (max (max (max u_1 u_2) u_3) u_4)
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRci.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Rci α) → Decidable (x = x_1)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_add`. -/
SkewMonoidAlgebra.toFinsupp_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a b : SkewMonoidAlgebra k G), (a + b).coeff = a.coeff + b.coeff
-- Init.Data.UInt.Lemmas
UInt8.toUSize_mod_256 : ∀ (n : UInt8), n.toUSize % 256 = n.toUSize
-- Mathlib.Algebra.Ring.Defs
mul_sub_left_distrib : ∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
-- Mathlib.Order.Basic
compare_of_injective_eq_compareOfLessAndEq : ∀ {α : Type u_2} {β : Type u_3} (a b : α) [inst : LinearOrder β] [inst_1 : DecidableEq α] (f : α → β)
  (inj : Function.Injective f) [inst_2 : Decidable (a < b)], compare (f a) (f b) = compareOfLessAndEq a b
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_two_inv : Real.binEntropy 2⁻¹ = Real.log 2
-- Mathlib.Logic.Denumerable
Nat.Subtype.ofNat_surjective : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s], Function.Surjective (Nat.Subtype.ofNat s)
-- Init.Data.UInt.Lemmas
UInt8.ofInt_one : UInt8.ofInt 1 = 1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.tprod_cons : ∀ {δ : Type u_4} {X : δ → Type u_5} [inst : (i : δ) → MeasurableSpace (X i)] (i : δ) (l : List δ)
  (μ : (i : δ) → MeasureTheory.Measure (X i)),
  MeasureTheory.Measure.tprod (i :: l) μ = (μ i).prod (MeasureTheory.Measure.tprod l μ)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.mem_addSubmonoid_iff : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddZeroClass β] {f : α → β},
  f ∈ HasCompactSupport.addSubmonoid α β ↔ HasCompactSupport f
-- Mathlib.Data.ENNReal.Operations
/-- Weaker version of `ENNReal.sub_eq_of_eq_add_rev` assuming that `a = b + c` itself is finite
rather than `b`.  -/
ENNReal.sub_eq_of_eq_add_rev' : ∀ {a b c : ENNReal}, a ≠ ⊤ → a = b + c → a - b = c
-- Init.Data.String.Basic
String.Slice.Pos.next_eq_nextFast : @String.Slice.Pos.next = @String.Slice.Pos.nextFast