mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Fin
LinearEquiv.finTwoArrow.eq_1 : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearEquiv.finTwoArrow R M =
    { toFun := (finTwoArrowEquiv M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (finTwoArrowEquiv M).invFun,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.isGaussian_iff_charFun_eq : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.IsGaussian μ ↔
    ∀ (t : E),
      MeasureTheory.charFun μ t =
        Complex.exp
          ((∫ (x : E), ↑((fun x => inner ℝ t x) x) ∂μ) * Complex.I -
            ↑(ProbabilityTheory.variance (fun x => inner ℝ t x) μ) / 2)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq)
  {v : β k},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → ∀ {h' : k' ∈ ↑(t.insertMany l ⋯)}, (↑(t.insertMany l ⋯)).get k' h' = cast ⋯ v
-- Mathlib.Data.Int.Cast.Lemmas
MonoidHom.apply_mint : ∀ (α : Type u_3) [inst : Group α] (f : Multiplicative ℤ →* α) (n : Multiplicative ℤ),
  f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryLE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option ((a : α) × β a)
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.exists_gcf_pair_rat_eq_of_nth_contsAux : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ),
  ∃ conts, (GenContFract.of v).contsAux n = GenContFract.Pair.map Rat.cast conts
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The non-unital subsemiring of elements `x : R` such that `f x = g x`  -/
NonUnitalRingHom.eqSlocus : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      {F : Type u_1} →
        [inst_1 : FunLike F R S] →
          [inst_2 : NonUnitalNonAssocSemiring S] → [NonUnitalRingHomClass F R S] → F → F → NonUnitalSubsemiring R
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.instCategoryULiftHomULiftOfSmallCategory : (J : Type) →
  [hJ : CategoryTheory.SmallCategory J] →
    CategoryTheory.Category.{u_1, u_2} (CategoryTheory.ULiftHom (ULift.{u_2, 0} J))
-- Mathlib.Algebra.Order.Positive.Field
Positive.coe_inv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K] (x : { x // 0 < x }),
  ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.Data.Nat.Choose.Factorization
Nat.multiplicity_choose_aux : ∀ {p n b k : ℕ},
  Nat.Prime p →
    k ≤ n →
      ∑ i ∈ Finset.Ico 1 b, n / p ^ i =
        ∑ i ∈ Finset.Ico 1 b, k / p ^ i + ∑ i ∈ Finset.Ico 1 b, (n - k) / p ^ i +
          {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
-- Mathlib.Data.NNReal.Defs
NNReal.zpow : Pow NNReal ℤ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α}, Std.DHashMap.Raw.Const.get? (m₁.diff m₂) k = if k ∈ m₂ then none else Std.DHashMap.Raw.Const.get? m₁ k
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.map_inv_hom_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map e.inv) (CategoryTheory.CategoryStruct.comp (F.map e.hom) h) = h
-- Mathlib.Topology.Separation.Hausdorff
/-- A continuous surjective map from a compact space to a Hausdorff space is a quotient map.  -/
Topology.IsQuotientMap.of_surjective_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [T2Space Y]
  {f : X → Y}, Function.Surjective f → Continuous f → Topology.IsQuotientMap f
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.coe_mulActionFiber_smul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (g : G) (e : ↑(f ⁻¹' {x})),
  ↑(g • e) = g • ↑e
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.mul₀_of_isBoundedUnder` -/
TendstoLocallyUniformlyOn.fun_mul₀_of_isBoundedUnder : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {s : Set X} {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (f y) 0) →
        (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (g y) 0) →
          TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 * G i i_1) (fun i => f i * g i) l s
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_ne_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (s : Set α),
  μ s ≠ ⊤
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.mulOp_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (a : Mᵐᵒᵖ),
  (AddMonoidHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.membership : {α : Type u} → Membership α (Stream'.WSeq α)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.colimitCommGroup : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommGrpCat) → CommGroup ↑(CommGrpCat.FilteredColimits.G F)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.next' : {ι : Type} →
  {elem idx : outParam Type} →
    {inst : DecidableEq idx} →
      {inst_1 : DecidableEq elem} →
        [self : Std.Internal.Parsec.Input ι elem idx] → (it : ι) → Std.Internal.Parsec.Input.hasNext it = true → ι
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is integrable on a set `s` and nonzero there, then the measurable hull of `s` is
well behaved: the restriction of the measure to `toMeasurable μ s` coincides with its restriction
to `s`.  -/
MeasureTheory.IntegrableOn.restrict_toMeasurable : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → (∀ x ∈ s, ‖f x‖ₑ ≠ 0) → μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.inductionOn₃ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (f : l.Germ β) (g : l.Germ γ)
  (h : l.Germ δ) {p : l.Germ β → l.Germ γ → l.Germ δ → Prop},
  (∀ (f : α → β) (g : α → γ) (h : α → δ), p ↑f ↑g ↑h) → p f g h
-- Mathlib.Order.BoundedOrder.Basic
ite_ne_bot : ∀ {α : Type u} [inst : Bot α] {p : Prop} [inst_1 : Decidable p] {a b : α},
  (p → a ≠ ⊥) → (¬p → b ≠ ⊥) → (if p then a else b) ≠ ⊥
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_insert_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b < a → insert a (Set.Ioo b a) = Set.Ioc b a
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.liftFromOver_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (X_1 : CategoryTheory.Functor J (CategoryTheory.Over X)) {X_2 Y : CategoryTheory.WithTerminal J}
  (f : X_2 ⟶ Y),
  (CategoryTheory.WithTerminal.liftFromOver.obj X_1).map f =
    match X_2, Y, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      CategoryTheory.Over.Hom.left (X_1.map (CategoryTheory.WithTerminal.down f))
    | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => (X_1.obj x).hom
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id X
-- Lean.Meta.Tactic.Grind.Util
/-- In the `grind` tactic, during `Expr` internalization, we don't expect to find `Expr.mdata`.
This function ensures `Expr.mdata` is not found during internalization.
Recall that we do not internalize `Expr.lam` children.
Recall that we still have to process `Expr.forallE` because of `ForallProp.lean`.
Moreover, we may not want to reduce `p → q` to `¬p ∨ q` when `(p q : Prop)`.
 -/
Lean.Meta.Grind.eraseIrrelevantMData : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Algebra.Lie.TraceForm
/-- See also `LieModule.traceForm_eq_sum_finrank_nsmul'` for an expression omitting the zero
weights.  -/
LieModule.traceForm_eq_sum_finrank_nsmul : ∀ (K : Type u_2) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : Field K] [inst_4 : LieAlgebra K L] [inst_5 : Module K M] [inst_6 : LieModule K L M]
  [inst_7 : FiniteDimensional K M] [inst_8 : LieRing.IsNilpotent L] [inst_9 : LieModule.LinearWeights K L M]
  [LieModule.IsTriangularizable K L M],
  LieModule.traceForm K L M =
    ∑ χ,
      Module.finrank K ↥(LieModule.genWeightSpace M ⇑χ) •
        (LieModule.Weight.toLinear K L M χ).smulRight (LieModule.Weight.toLinear K L M χ)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init ↑m = forIn (↑m).toArray init fun a b => f a.fst a.snd b
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Pos.find?_char_eq_find?_beq : ∀ {c : Char} {s : String} {pos : s.Pos}, pos.find? c = pos.find? fun x => x == c
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff : ∀ {X : Type u} {ι : Type u_1} {Y : ι → Type u} {f : (i : ι) → Y i ⟶ X},
  CategoryTheory.Presieve.ofArrows Y f ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : (fun X => X) X), ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (f i))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Var
Lean.Meta.Grind.Arith.Linear.mkVar : Lean.Expr → optParam Bool true → Lean.Meta.Grind.Arith.Linear.LinearM Lean.Grind.Linarith.Var
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev?.eq_1 : ∀ {s : String.Slice} (pos : s.Pos), pos.prev? = if h : pos = s.startPos then none else some (pos.prev h)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A] (S : NonUnitalSubalgebra R A), S.starClosure.toNonUnitalSubalgebra = S ⊔ star S
-- Init.Data.Range.Polymorphic.UInt
UInt16.upwardEnumerableLE_ofBitVec : ∀ {x y : BitVec 16},
  Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (α : CategoryTheory.Abelian.Ext X Y n) (m : ℕ) (hm : n + 1 = m),
  ∃ f, ∃ (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0), R.extMk f m hm hf = α
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.instInhabited : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → Inhabited (X ≅ X)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = 0` induces `l : cokernel f ⟶ W` such that
`cokernel.π f ≫ l = k`.  -/
CategoryTheory.Limits.cokernel.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            {W : C} →
              (k : Y ⟶ W) →
                CategoryTheory.CategoryStruct.comp f k = 0 →
                  { l // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) l = k }
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceδ_naturality_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [inst_3 : F.ShiftSequence ℤ]
  (T T' : CategoryTheory.Pretriangulated.Triangle C) (φ : T ⟶ T') (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : A}
  (h_1 : (F.shift n₁).obj T'.obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.shift n₀).map φ.hom₃)
      (CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T' n₀ n₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h)
      (CategoryTheory.CategoryStruct.comp ((F.shift n₁).map φ.hom₁) h_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver.eq_1 : ∀ (p : ℕ → Prop), Int.Internal.Linear.OrOver 0 p = False
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.image_Iio_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictAntiOn f (Set.Iic b) → f '' Set.Iio b ⊆ Set.Ioi (f b)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_le_size_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} {ρ : Type v} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, m.size ≤ (m.insertMany l).size
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [inst_2 : DecidableEq β] {b : β}, (insert b s).gcd f = gcd (f b) (s.gcd f)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_mul_le_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → (a⁻¹ * b ≤ 1 ↔ b ≤ a)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Init.System.IO
IO.Process.Stdio.piped.sizeOf_spec : sizeOf IO.Process.Stdio.piped = 1
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBotCoeff.eq_1 : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  LieModule.chainBotCoeff α β = LieModule.chainTopCoeff (-α) β
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_max!_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, k ∈ t → (cmp k t.max!).isLE = true
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.FormallyUnramified
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_piecewise : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) {s : Set α} {t : Set β} [inst : (x : α) → Decidable (x ∈ s)]
  [inst_1 : (y : β) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s ⋯ ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
/-- If `f : X ⟶ Y` is locally of finite presentation, flat and has smooth fibers, then `f` is
smooth.  -/
AlgebraicGeometry.Smooth.of_smooth_fiberToSpecResidueField : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f]
  [AlgebraicGeometry.Flat f],
  (∀ (y : ↥Y), AlgebraicGeometry.Smooth (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y)) →
    AlgebraicGeometry.Smooth f
-- Mathlib.Data.Sigma.Order
Sigma.LT.fiber : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LT (α i)] (i : ι) (a b : α i), a < b → ⟨i, a⟩.LT ⟨i, b⟩
-- Lean.Elab.AssertExists
Lean.Elab.Command.AssertExists.mk.sizeOf_spec : ∀ (isDecl : Bool) (givenName modName : Lean.Name),
  sizeOf { isDecl := isDecl, givenName := givenName, modName := modName } =
    1 + sizeOf isDecl + sizeOf givenName + sizeOf modName
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix.sizeOf_spec : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs s c₁ c₂) =
    1 + sizeOf lhs + sizeOf s + sizeOf c₁ + sizeOf c₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
isLittleO_log_rpow_atTop : ∀ {r : ℝ}, 0 < r → Real.log =o[Filter.atTop] fun x => x ^ r
-- Init.Data.Array.Lemmas
Array.any_iff_exists : ∀ {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : ℕ},
  as.any p start stop = true ↔ ∃ i, ∃ (x : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_iff_isCompact_closure_image_closedBall : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  [T2Space M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : ℝ},
  0 < r → (IsCompactOperator ⇑f ↔ IsCompact (closure (⇑f '' Metric.closedBall 0 r)))
-- Mathlib.Topology.UniformSpace.Basic
SetRel.id.eq_1 : ∀ {α : Type u_1}, SetRel.id = {(a₁, a₂) | a₁ = a₂}
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_natCast_nonneg : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] (n : ℕ),
  0 ≤ ArchimedeanClass.mk ↑n
-- Mathlib.Data.Real.Basic
CauSeq.congr_simp : ∀ {α : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (β : Type u_4)
  [inst_3 : Ring β] (abv abv_1 : β → α), abv = abv_1 → CauSeq β abv = CauSeq β abv_1
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Computes the semantic tokens in the range provided by `p`.  -/
Lean.Server.FileWorker.handleSemanticTokensRange : Lean.Lsp.SemanticTokensRangeParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.SemanticTokens)
-- Init.Data.Array.Zip
Array.zipWith_comm_of_comm : ∀ {α : Type u_1} {β : Type u_2} {f : α → α → β},
  (∀ (x y : α), f x y = f y x) → ∀ {xs ys : Array α}, Array.zipWith f xs ys = Array.zipWith f ys xs
-- Mathlib.Topology.Algebra.Group.Basic
/-- Addition from the right in a topological additive group as a homeomorphism.  -/
Homeomorph.addRight : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [SeparatelyContinuousAdd G] → G → G ≃ₜ G
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.isoSheafify_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D}
  (hP : CategoryTheory.Presheaf.IsSheaf J P), (J.isoSheafify hP).hom = J.toSheafify P
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_erase_mul : ∀ {α : Type u_3} [inst : Monoid α] [inst_1 : DecidableEq α] (s : Multiset α) {a : α},
  a ∈ s →
    ∀ (comm : {x | x ∈ s}.Pairwise Commute)
      (comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1) ⋯),
      (s.erase a).noncommProd comm' * a = s.noncommProd comm
-- Batteries.Control.ForInStep.Lemmas
ForInStep.done_bindList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β)) (a : β)
  (l : List α), ForInStep.bindList f l (ForInStep.done a) = pure (ForInStep.done a)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapWithPostcondition_eq_toList_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n γ} {it : Std.IterM m β},
  (Std.IterM.mapWithPostcondition f it).toList =
    (Std.IterM.filterMapWithPostcondition (fun x => Std.Iterators.PostconditionT.map some (f x)) it).toList
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₂'_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.X₃ = S.L₃.X₂
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.not_vlt_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), ¬x <ᵥ 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coeFn_injective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂], Function.Injective DFunLike.coe
-- Batteries.Control.AlternativeMonad
LawfulAlternative.toLawfulApplicative : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m], LawfulApplicative m
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The ring homomorphism associated to an inclusion of subrings.  -/
Subring.inclusion : {R : Type u} → [inst : NonAssocRing R] → {S T : Subring R} → S ≤ T → ↥S →+* ↥T
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_map : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R →⋆* S) (x : ↥(unitary R)), ↑((Unitary.map f) x) = f ↑x