mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_smul_measure_of_ne_zero : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} {c : NNReal},
  c ≠ 0 → MeasureTheory.lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.lpNorm f p μ
-- Mathlib.Data.Set.Prod
/-- **Alias** of the reverse direction of `Set.offDiag_eq_empty`. -/
Set.Subsingleton.offDiag_eq_empty : ∀ {α : Type u_1} {s : Set α}, s.Subsingleton → s.offDiag = ∅
-- Mathlib.Data.Finset.Sort
/-- Given a `Fintype` `α` of cardinality `k`, the map `orderIsoFinOfCardEq s h` is the increasing
bijection between `Fin k` and `α` as an `OrderIso`. Here, `h` is a proof that the cardinality of `α`
is `k`. We use this instead of an iso `Fin (Fintype.card α) ≃o α` to avoid casting issues in further
uses of this function.  -/
Fintype.orderIsoFinOfCardEq : (α : Type u_1) → [inst : LinearOrder α] → [inst_1 : Fintype α] → {k : ℕ} → Fintype.card α = k → Fin k ≃o α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- If `φ : W.RightFraction X Y` and `L` is a functor which inverts `W`, this is the
induced morphism `L.obj X ⟶ L.obj Y`  -/
CategoryTheory.MorphismProperty.RightFraction.map : {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] →
        {W : CategoryTheory.MorphismProperty C} →
          {X Y : C} → W.RightFraction X Y → (L : CategoryTheory.Functor C D) → W.IsInvertedBy L → (L.obj X ⟶ L.obj Y)
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.lift_unique : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : AddZeroClass β] (f : WithZero α →+ β),
  f = WithZero.lift ((↑f).comp WithZero.coeAddHom)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Eventually.natCast_atTop : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atTop, p x) → ∀ᶠ (n : ℕ) in Filter.atTop, p ↑n
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.instSubsingleton : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [Subsingleton R],
  Subsingleton (HahnSeries Γ R)
-- Mathlib.Order.Irreducible
not_supPrime_bot : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α], ¬SupPrime ⊥
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.instCommMagma.eq_1 : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : IsMulCommutative M],
  IsMulCommutative.instCommMagma = { toMul := inst, mul_comm := ⋯ }
-- Init.Data.SInt.Lemmas
Int16.ofNat_add : ∀ (a b : ℕ), Int16.ofNat (a + b) = Int16.ofNat a + Int16.ofNat b
-- Lean.Parser.Term
Lean.Parser.Term.unop.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Internal.Order.MonadTail
_private.Init.Internal.Order.MonadTail.0.ST.bind.eq_1 : ∀ {σ α β : Type} (x : ST σ α) (f : α → ST σ β) (s : Void σ),
  x.bind f s =
    match x s with
    | { val := x, state := s } => f x s
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.addChar_of_value_at_one.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] (r r_1 : R) (e_r : r = r_1)
  (hr : Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0)),
  PadicInt.addChar_of_value_at_one r hr = PadicInt.addChar_of_value_at_one r_1 ⋯
-- Std.Data.DHashMap.Raw
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DHashMap.Raw.Const.beq : {α : Type u} →
  {β : Type v} →
    [BEq α] → [Hashable α] → [BEq β] → (Std.DHashMap.Raw α fun x => β) → (Std.DHashMap.Raw α fun x => β) → Bool
-- Mathlib.Order.Hom.Lattice
InfHom.subtypeVal.eq_1 : ∀ {β : Type u_3} [inst : SemilatticeInf β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)),
  InfHom.subtypeVal Psup = { toFun := Subtype.val, map_inf' := ⋯ }
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tildeEquiv_functor : ∀ {R : CommRingCat},
  AlgebraicGeometry.tildeEquiv.functor =
    (SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf).lift (AlgebraicGeometry.tilde.functor R) ⋯
-- Mathlib.CategoryTheory.Square
CategoryTheory.NatTrans.mapSquare_app_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C),
  ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₂ = τ.app sq.X₂
-- Init.Data.Option.Lemmas
Function.comp.eq_1 : ∀ {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) (x : α), (f ∘ g) x = f (g x)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSubtype.match_1.splitter : (n : ℕ) →
  (P : Fin (n + 1) → Prop) →
    (inst : DecidablePred P) →
      (motive : Fin (Fin.countP fun x => decide (P x.succ)) → Sort u_1) →
        (x : Fin (Fin.countP fun x => decide (P x.succ))) →
          ((k : ℕ) → (hk : k < Fin.countP fun x => decide (P x.succ)) → motive ⟨k, hk⟩) → motive x
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.localizerMorphism_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.localizerMorphism C).functor = HomotopicalAlgebra.FibrantObject.ι
-- Mathlib.Data.Seq.Basic
Stream'.Seq.cons_append : ∀ {α : Type u} (a : α) (s t : Stream'.Seq α), (Stream'.Seq.cons a s).append t = Stream'.Seq.cons a (s.append t)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roc.count_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] {r : Std.Roc α},
  r.iter.length = r.size
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary **rearrangement inequality**.  -/
mul_add_mul_le_mul_add_mul' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R]
  [AddLeftMono R] [AddLeftReflectLE R], b ≤ a → d ≤ c → a * d + b * c ≤ a * c + b * d
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMapZero.induction_on_of_compact : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} [inst_1 : Fact (0 ∈ s)] [CompactSpace ↑s]
  {p : ContinuousMapZero (↑s) 𝕜 → Prop},
  p 0 →
    p (ContinuousMapZero.id s) →
      p (star (ContinuousMapZero.id s)) →
        (∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f + g)) →
          (∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f * g)) →
            (∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p f → p (r • f)) →
              (∀ (f : ContinuousMapZero (↑s) 𝕜), (∃ᶠ (g : ContinuousMapZero (↑s) 𝕜) in nhds f, p g) → p f) →
                ∀ (f : ContinuousMapZero (↑s) 𝕜), p f
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSemigroup : {α : Type u_1} → [Semigroup α] → Semigroup (Colex α)
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_inter_self : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α}, t ∈ nhdsWithin x (s ∩ t)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_of_subsingleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [h : Subsingleton E] (f : E → F) (s : Set E) (x : E), HasFDerivWithinAt f 0 s x
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coe_smul`. -/
TestFunction.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k}, (cmp k (t.insert k v).maxKey!).isLE = true
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeriesStep.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = { carrier := {x | ∀ (y : G), ⁅x, y⁆ ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Topology.Order.Monotone
/-- A monotone function continuous at the supremum of a nonempty set sends this supremum to
the supremum of the image of this set.  -/
Monotone.map_csSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousAt f (sSup A) →
    Monotone f →
      A.Nonempty → autoParam (BddAbove A) Monotone.map_csSup_of_continuousAt._auto_1 → f (sSup A) = sSup (f '' A)
-- Mathlib.Logic.Relation
Relation.Comp.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ),
  Relation.Comp r p a c = ∃ b, r a b ∧ p b c
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X₁ X₂ Y : C} {n : ℕ}
  (e : CategoryTheory.Abelian.Ext X₁ Y n × CategoryTheory.Abelian.Ext X₂ Y n),
  CategoryTheory.Abelian.Ext.biprodAddEquiv.symm e =
    (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.fst).comp e.1 ⋯ +
      (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.snd).comp e.2 ⋯
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.nonempty_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C)
  (a : α) [(P a).Nonempty], (⨆ a, P a).Nonempty
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Finset.map (Fin.addNatEmb m) (Finset.uIcc i j) = Finset.uIcc (i.addNat m) (j.addNat m)
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- [Stacks Tag 090P](https://stacks.math.columbia.edu/tag/090P) (part (1)) -/
Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn : ∀ {K : Type u_3} [inst : Field K] {x : K} {R : Subring K},
  x ∉ R → ∀ [IsIntegrallyClosedIn (↥R) K], ∃ V, R ≤ V.toSubring ∧ x ∉ V
-- Init.Data.Vector.FinRange
_private.Init.Data.Vector.FinRange.0.Vector.finRange.eq_1 : ∀ (n : ℕ), Vector.finRange n = Vector.ofFn fun i => i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, (m.insertManyIfNewUnit l).contains k = (m.contains k || l.contains k)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.condition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.fst f g) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.snd f g) g
-- Batteries.Data.Array.Merge
_private.Batteries.Data.Array.Merge.0.Array.mergeDedupWith.go.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The isometry between `ℂ` and a two-dimensional real inner product space given by a basis.  -/
Complex.isometryOfOrthonormal : {F : Type u_5} →
  [inst : NormedAddCommGroup F] → [inst_1 : InnerProductSpace ℝ F] → OrthonormalBasis (Fin 2) ℝ F → ℂ ≃ₗᵢ[ℝ] F
-- Init.Data.List.Find
List.findIdx?_subtype : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.findIdx? f l = List.findIdx? g l.unattach
-- Mathlib.GroupTheory.Divisible
DivisibleBy.surjective_smul : ∀ (A : Type u_1) (α : Type u_2) [inst : AddMonoid A] [inst_1 : SMul α A] [inst_2 : Zero α] [DivisibleBy A α] {n : α},
  n ≠ 0 → Function.Surjective fun a => n • a
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_div : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (x y : ↥(selfAdjoint R)), ↑(x / y) = ↑x / ↑y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {f : α → β → γ} {k : α}, (Std.TreeMap.map f t).getKey! k = t.getKey! k
-- Mathlib.Order.SuccPred.LinearLocallyFinite
iterate_pred_toZ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι}, ∀ i < i0, Order.pred^[(-toZ i0 i).toNat] i0 = i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {combined : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig combined → ℕ
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlCommand.evalCommandMHtml : Lean.Term → Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM ProofWidgets.Html)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod_comp_inl_inr : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] [ContinuousAdd M₁] [inst_12 : ContinuousAdd M₂] (f : M × M₁ →L[R] M₂),
  (f ∘SL ContinuousLinearMap.inl R M M₁).coprod (f ∘SL ContinuousLinearMap.inr R M M₁) = f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_support_eq_support_drop_min : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ),
  (p.drop n).support = List.drop (min n p.length) p.support
-- Mathlib.Data.Sym.Sym2
Set.mem_sym2_iff_subset : ∀ {α : Type u_1} {s : Set α} {z : Sym2 α}, z ∈ s.sym2 ↔ ↑z ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_inv_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.op =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.op X)).hom
-- Mathlib.Topology.Order.IsLUB
IsLUB.frequently_nhds_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsLUB s a → s.Nonempty → ∃ᶠ (x : α) in nhds a, x ∈ s
-- Mathlib.RingTheory.Invariant.Basic
instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u_3}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (H : Subgroup G)
  [inst_6 : H.Normal], SMulCommClass (G ⧸ H) A ↥(FixedPoints.subalgebra A B ↥H)
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A gcf terminates if its sequence terminates.  -/
GenContFract.Terminates : {α : Type u_1} → GenContFract α → Prop
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.terminatedAt_iff_partNum_none : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ}, g.TerminatedAt n ↔ g.partNums.get? n = none
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symmEquiv_symm_apply_symm_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Add P] [inst_1 : Add Q] (h : Q ≃+ P) (a : Q),
  ((AddEquiv.symmEquiv P Q).symm h).symm a = h a
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_inv : ∀ {a b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ x ∈ Set.uIcc a b, f x ≠ 0) → ContinuousOn f (Set.uIcc a b) → IntervalIntegrable (fun x => (f x)⁻¹) μ a b
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.of_subsingleton_top : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Subsingleton S], A.LinearDisjoint B
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.return : {pu : Lean.Compiler.LCNF.Purity} → Lean.FVarId → Lean.Compiler.LCNF.Code pu
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.rangeKerLift_surjective : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H),
  Function.Surjective ⇑(QuotientGroup.rangeKerLift φ)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filterMap.go.eq_2 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a))
  (acc : Std.DHashMap.Internal.AssocList α γ) (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.filterMap.go✝ f acc (Std.DHashMap.Internal.AssocList.cons a b es) =
    match f a b with
    | none => Std.DHashMap.Internal.AssocList.filterMap.go✝ f acc es
    | some v' => Std.DHashMap.Internal.AssocList.filterMap.go✝ f (Std.DHashMap.Internal.AssocList.cons a v' acc) es
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.inv_measure_univ_smul_eq_self : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  (μ Set.univ)⁻¹ • μ = μ
-- Mathlib.Probability.ProbabilityMassFunction.Integrals
PMF.integral_eq_tsum : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [CompleteSpace E] (p : PMF α) (f : α → E),
  MeasureTheory.Integrable f p.toMeasure → ∫ (a : α), f a ∂p.toMeasure = ∑' (a : α), (p a).toReal • f a
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt_dvd_iff_of_ne_one : ∀ {p : ℕ}, p ≠ 1 → ∀ (n : ℕ) (a : ℤ), ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.inverseImage_quotient_isomorphisms : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι),
  (CategoryTheory.MorphismProperty.isomorphisms (HomotopyCategory V c)).inverseImage (HomotopyCategory.quotient V c) =
    HomologicalComplex.homotopyEquivalences V c
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The chosen cokernels and kernels of the limits API give a `RightHomologyData`  -/
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : CategoryTheory.Limits.HasCokernel S.f] →
          [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)] → S.RightHomologyData
-- Mathlib.Data.List.Basic
List.ext_getElem?' : ∀ {α : Type u} {l₁ l₂ : List α}, (∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]?) → l₁ = l₂
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂TriangEnvelopeOfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C], P.triangEnvelope.IsTriangulatedClosed₂
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftHomologyIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.leftHomologyIso.hom (CategoryTheory.ShortComplex.homologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) S₂.leftHomologyIso.hom
-- Mathlib.Topology.Algebra.Group.Units
Units.toMulEquiv_mapContinuousMulEquiv : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Monoid M]
  [inst_3 : Monoid N] (f : M ≃ₜ* N), ↑(Units.mapContinuousMulEquiv f) = Units.mapEquiv ↑f
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f) (s : TopologicalSpace.Compacts α), ↑(TopologicalSpace.Compacts.map f hf s) = f '' ↑s
-- Mathlib.Topology.Constructions
Pi.continuous_precomp : ∀ {X : Type u} {ι : Type u_5} [inst : TopologicalSpace X] {ι' : Type u_9} (φ : ι' → ι), Continuous fun x => x ∘ φ
-- Init.Data.Array.Lemmas
Array.getElem?_size_le : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.size ≤ i → xs[i]? = none
-- Init.Control.Except
/-- Use a monadic action that may return an exception's value as an action in the transformed monad that
may throw the corresponding exception.

This is the inverse of `ExceptT.run`.
 -/
ExceptT.mk : {ε : Type u} → {m : Type u → Type v} → {α : Type u} → m (Except ε α) → ExceptT ε m α
-- Mathlib.RingTheory.MvPowerSeries.Derivative
_private.Mathlib.RingTheory.MvPowerSeries.Derivative.0.MvPowerSeries.pderivFun_smul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (r : R) (f : MvPowerSeries σ R),
  MvPowerSeries.pderivFun i (r • f) = r • MvPowerSeries.pderivFun i f
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.coeff_sum_eq : ∀ {𝕜 : 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] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} [inst_13 : Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : (x : M) → V x),
  x ∈ u → t x = ∑ i, (hs.coeff i x) (t x) • s i x
-- Mathlib.Geometry.Euclidean.Projection
/-- The `orthogonalProjection` lies in the given subspace.  -/
EuclideanGeometry.orthogonalProjection_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ s
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_of_nonneg_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulMono α β], 0 ≤ a → b ≤ 0 → a • b ≤ 0