mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Regular
TopologicalSpace.IsTopologicalBasis.nhds_basis_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {B : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis B → ∀ (x : X), (nhds x).HasBasis (fun s => x ∈ s ∧ s ∈ B) closure
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the month to the given `month` value.
The day is rolled over to the next valid month if necessary.
 -/
Std.Time.DateTime.withMonthRollOver : Std.Time.DateTime → Std.Time.Month.Ordinal → Std.Time.DateTime
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_terminates_of_head_tail_terminates : ∀ {α : Type u} (s : Stream'.WSeq α) [T : s.tail.head.Terminates], s.head.Terminates
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrictHom.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Type u_5} [inst_1 : SetLike S M] [inst_2 : SubmonoidClass S M] (M' : S)
  (A : Type u_6) [inst_3 : CommMonoid A],
  MonoidHom.domRestrictHom M' A = { toFun := fun f => f.domRestrict M', map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toNonUnitalStarAlgHom_toStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [inst_5 : Star A₁] [inst_6 : Star A₂] (e : A₁ ≃⋆ₐ[R] A₂),
  e.toStarAlgHom.toNonUnitalStarAlgHom = e.toNonUnitalStarAlgHom
-- Mathlib.RingTheory.ClassGroup.Basic
QuotientGroup.congr.congr_simp : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (G' : Subgroup G) (H' : Subgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e e_1 : G ≃* H) (e_e : e = e_1) (he : Subgroup.map (↑e) G' = H'),
  QuotientGroup.congr G' H' e he = QuotientGroup.congr G' H' e_1 ⋯
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.finrank_le_one_add_finrank_fixedSubmodule_dilatransvection : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V],
  ∀ e ∈ LinearEquiv.dilatransvections K V, Module.finrank K V ≤ 1 + Module.finrank K ↥(↑e).fixedSubmodule
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The underlying object of a comonoid object.  -/
CategoryTheory.Comon.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Comon C → C
-- Mathlib.Algebra.Lie.Weights.RootSystem
_private.Mathlib.Algebra.Lie.Weights.RootSystem.0.LieAlgebra.IsKilling.chainLength_aux : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero →
    ∀ {x : L}, x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β) → ∃ n, n • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆
-- Mathlib.Data.FP.Basic
FP.toRat : [C : FP.FloatCfg] → (f : FP.Float) → f.isFinite = true → ℚ
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} {n : ℕ},
  (∀ i < n, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i, ⋃ (_ : i < n), s i)
-- Mathlib.Algebra.Group.Basic
div_eq_iff_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a / b = c ↔ a = c * b
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.comp.eq_4 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithTerminal C) (_Y : C),
  CategoryTheory.WithTerminal.comp =
    match (motive := (x x_1 x_2 : CategoryTheory.WithTerminal C) → x.Hom x_1 → x_1.Hom x_2 → x.Hom x_2) x,
      CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      fun f g => CategoryTheory.CategoryStruct.comp f g
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => fun _f _g => PUnit.unit
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => fun f _g => PEmpty.elim f
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => fun _f g => PEmpty.elim g
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star =>
      fun x x_1 => PUnit.unit
-- Lean.Meta.Tactic.Clear
/-- Try to clear the given fvars from the local context. Returns the new goal and
the hypotheses that were cleared.

Does not require the `hyps` to be given in the order in which they
appear in the local context.
 -/
Lean.MVarId.tryClearMany' : Lean.MVarId → Array Lean.FVarId → Lean.MetaM (Lean.MVarId × Array Lean.FVarId)
-- Init.Data.Format.Macro
Std.termF!_ : Lean.ParserDescr
-- Mathlib.Tactic.Ring.Common
/-- Inverts a polynomial `va` to get a normalized result polynomial.

* `0⁻¹ = 0`
* `a⁻¹ = (a⁻¹)` if `a` is a nontrivial sum
 -/
Mathlib.Tactic.Ring.Common.ExSum.evalInv : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            (dsα : Q(Semifield «$α»)) →
              {a : Q(«$α»)} →
                Option Q(CharZero «$α») →
                  Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                    Mathlib.Tactic.AtomM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a»⁻¹))
-- Mathlib.RingTheory.Localization.Defs
/-- To show `j` and `k` agree on the whole localization, it suffices to show they agree
on the image of the base ring, if they preserve `1` and `*`.  -/
IsLocalization.ext : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {P : Type u_4} [inst_4 : Monoid P] (j k : S → P),
  j 1 = 1 →
    k 1 = 1 →
      (∀ (a b : S), j (a * b) = j a * j b) →
        (∀ (a b : S), k (a * b) = k a * k b) → (∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)) → j = k
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.total : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α}, IsUpperSet s → IsUpperSet t → s ⊆ t ∨ t ⊆ s
-- Mathlib.Data.DFinsupp.Interval
/-- Pointwise `Finset.Icc` bundled as a `DFinsupp`.  -/
DFinsupp.rangeIcc : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [inst_1 : (i : ι) → PartialOrder (α i)] →
        [(i : ι) → LocallyFiniteOrder (α i)] → (Π₀ (i : ι), α i) → (Π₀ (i : ι), α i) → Π₀ (i : ι), Finset (α i)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_zero : ∀ {α : Type u_1} {x : MeasurableSpace α}, MeasureTheory.Measure.real 0 = 0
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass : ∀ {E : Type u_3} [inst : AddGroup E], NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd'_hom_app_f : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n₁ n₂ n₁₂ : ℤ)
  (h : n₁ + n₂ = n₁₂) (X : CochainComplex C ℤ) (i : ℤ),
  ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).hom.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).hom
-- Mathlib.Combinatorics.Graph.Basic
Graph.edgeSet_noEdge : ∀ {α : Type u_1} (vertexSet : Set α) (β : Type u_3), (Graph.noEdge vertexSet β).edgeSet = ∅
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.prodMap_toFun : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : Monoid D] [inst_4 : TopologicalSpace A] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace C]
  [inst_7 : TopologicalSpace D] (f : A →ₜ* C) (g : B →ₜ* D) (i : A × B), (f.prodMap g) i = (f i.1, g i.2)
-- Mathlib.RingTheory.Flat.Localization
Localization.flat : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Module.Flat R S] (p : Submonoid S), Module.Flat R (Localization p)
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.ZMod.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.BigOperators.Option
Finset.mul_prod_eq_prod_insertNone : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : α → M) (x : M) (s : Finset α),
  x * ∏ i ∈ s, f i = ∏ i ∈ Finset.insertNone s, i.elim x f
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNeg : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → Neg (CompactlySupportedContinuousMap α β)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.ext_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} {x y : G.CompleteEquipartiteSubgraph r t}, x = y ↔ x.parts = y.parts
-- Init.Data.Array.Zip
Array.zip_of_prod : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {xs : Array (α × β)},
  Array.map Prod.fst xs = as → Array.map Prod.snd xs = bs → xs = as.zip bs
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The pushforward of an indexed collection of submodule `p i ⊆ M₁ i` by `f : M₁ → M₂`.

Note that this is not a submodule - it is not closed under addition.  -/
MultilinearMap.map : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Ring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [Nonempty ι] → MultilinearMap R M₁ M₂ → ((i : ι) → Submodule R (M₁ i)) → SubMulAction R M₂
-- Mathlib.Algebra.Order.Monovary
antivaryOn_iff_forall_mul_nonpos : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_toSubmodule : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L),
  ↑(LieIdeal.map f I) = ⇑f '' ↑I → ↑(LieIdeal.map f I) = Submodule.map ↑f ↑I
-- Mathlib.Probability.Density
Real.hasPDF_iff : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.SFinite ℙ],
  MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔
    AEMeasurable X ℙ ∧ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous MeasureTheory.volume
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The equivalence `LeftExtension L F ≌ LeftExtension L F'` induced by
a natural isomorphism `F ≅ F'`.  -/
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (L : CategoryTheory.Functor C D) →
              {F F' : CategoryTheory.Functor C H} → (F ≅ F') → (L.LeftExtension F ≌ L.LeftExtension F')
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_5 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 y : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.descFunLift F s (x_1.add y) =
    CommRingCat.Colimits.descFunLift F s x_1 + CommRingCat.Colimits.descFunLift F s y
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- Given a functor `F : C ⥤ D`, this is the property of objects `Y : D` such
that `F` is dense at `Y`.  -/
CategoryTheory.Functor.isDenseAt : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_fderiv_apply_const_with_param : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] {f : α → E → F} [inst_7 : MeasurableSpace α]
  [OpensMeasurableSpace α] [inst_9 : MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F]
  [inst_12 : MeasurableSpace F] [BorelSpace F],
  Continuous (Function.uncurry f) → ∀ (y : E), Measurable fun p => (fderiv 𝕜 (f p.1) p.2) y
-- Init.Data.List.Lemmas
List.foldr_cons_nil : ∀ {α : Type u_1} {l : List α}, List.foldr List.cons [] l = l
-- Mathlib.Algebra.GCDMonoid.Basic
instUniqueNormalizationMonoid : {α : Type u_1} → [inst : CommMonoidWithZero α] → [Subsingleton αˣ] → Unique (NormalizationMonoid α)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects colimits, then `F.rightOp : C ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β},
  (Std.ExtDHashMap.Const.getThenInsertIfNew? m k v).1 = Std.ExtDHashMap.Const.get? m k
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `continuousAt_inv_iff`. -/
ContinuousAt.of_inv : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f⁻¹ x → ContinuousAt f x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.isClosedEmbedding_subtype : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), IsClosed ↑p → Topology.IsClosedEmbedding ⇑p.subtype
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finprod_mem_inter_mul_sdiff`. -/
finprod_mem_inter_mul_diff : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α} (t : Set α),
  s.Finite → (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- The homeomorphism `quasispectrum S a ≃ₜ quasispectrum R a` induced by
`QuasispectrumRestricts a f`.  -/
QuasispectrumRestricts.homeomorph : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Semifield R] →
        [inst_1 : Field S] →
          [inst_2 : NonUnitalRing A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Module R A] →
                [inst_5 : Module S A] →
                  [IsScalarTower R S A] →
                    [inst_7 : TopologicalSpace R] →
                      [inst_8 : TopologicalSpace S] →
                        [ContinuousSMul R S] →
                          [IsScalarTower S A A] →
                            [SMulCommClass S A A] →
                              {a : A} →
                                {f : C(S, R)} →
                                  QuasispectrumRestricts a ⇑f → ↑(quasispectrum S a) ≃ₜ ↑(quasispectrum R a)
-- Std.Http.Internal.LowerCase
_private.Std.Http.Internal.LowerCase.0.Std.Http.Internal.IsLowerCase.Char.toLower_idempotent : ∀ (c : Char), c.toLower.toLower = c.toLower
-- Mathlib.Analysis.Analytic.OfScalars
/-- If `‖c n.succ‖ / ‖c n‖` is unbounded, then the radius of convergence is zero.  -/
FormalMultilinearSeries.ofScalars_radius_eq_zero_of_tendsto : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) [NormOneClass E],
  Filter.Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) Filter.atTop Filter.atTop →
    (FormalMultilinearSeries.ofScalars E c).radius = 0
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange.equiv.congr_simp : ∀ {ι : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e e_1 : M ≃ N) (e_e : e = e_1)
  (hf : e 0 = 0), Finsupp.mapRange.equiv e hf = Finsupp.mapRange.equiv e_1 ⋯
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.piecewise_div : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Div (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ f₂ g₁ g₂ : (i : I) → f i), s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_nat_mul_pi : ∀ (n : ℕ), Real.tan (↑n * Real.pi) = 0
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.not_isPrincipal_iff : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  ¬Ordinal.IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vadd_midpoint : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (v v' : V) (p p' : P),
  midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p')
-- Mathlib.Algebra.Lie.CartanExists
_private.Mathlib.Algebra.Lie.CartanExists.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly.eq_1 : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x y : L),
  LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y =
    Polynomial.map
      (↑(MvPolynomial.aeval fun i =>
          Polynomial.C (((Module.Free.chooseBasis R L).repr y) i) * Polynomial.X +
            Polynomial.C (((Module.Free.chooseBasis R L).repr x) i)))
      ((↑(LieModule.toEnd R L M)).polyCharpoly (Module.Free.chooseBasis R L))
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
/-- Mapping `fun ε x => x * Real.exp (- (ε * x * x))`. By composition, it can be used to transform
functions into bounded functions.
 -/
Real.mulExpNegMulSq : ℝ → ℝ → ℝ
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} {x y : M.Hom N}, x.hom = y.hom → x = y
-- Mathlib.RingTheory.Algebraic.Defs
/-- An element of an R-algebra is transcendental over R if it is not algebraic over R.  -/
Transcendental : (R : Type u) → {A : Type v} → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → A → Prop
-- Mathlib.Data.Prod.Basic
Prod.exists' : ∀ {α : Type u_1} {β : Type u_2} {p : α → β → Prop}, (∃ x, p x.1 x.2) ↔ ∃ a b, p a b
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.has_kernels : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasKernels C
-- Aesop.Forward.State
Aesop.VariableMap.mk : Lean.PHashMap Aesop.PremiseIndex Aesop.InstMap → Aesop.VariableMap
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A subcomplex is a closed subspace of a CW complex that is the union of open cells of the
CW complex.  -/
Topology.RelCWComplex.Subcomplex : {X : Type u_1} → [t : TopologicalSpace X] → (C : Set X) → {D : Set X} → [Topology.RelCWComplex C D] → Type u_1
-- Std.Do.WP.Sound
/-- A `wp`-provable postcondition refines the post-run computation `prog.run r : m α`
via `Internal.Ensures`.
 -/
Std.Do.ReaderT.ensures_of_wp_run : ∀ {m : Type u → Type u_1} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WP m ps] [Std.Do.WPSound m ps]
  {α ρ : Type u} {prog : ReaderT ρ m α} (r : ρ) (P : α → Prop),
  (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.mayThrow fun a => ⌜P a⌝) r) → Std.Do.Internal.Ensures P (prog.run r)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.triangle_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ.comp φ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) h
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.inverse_of_rightInverse.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g g_1 : N →ₗ[R] P} (e_g : g = g_1) (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  {h h_1 : P → N} (e_h : h = h_1) (hfg : Function.Exact ⇑f ⇑g) (hgh : Function.RightInverse h ⇑g),
  rTensor.inverse_of_rightInverse Q hfg hgh = rTensor.inverse_of_rightInverse Q ⋯ ⋯
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The sine of the angle between two vectors, multiplied by the
product of their norms.  -/
InnerProductGeometry.sin_angle_mul_norm_mul_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  Real.sin (InnerProductGeometry.angle x y) * (‖x‖ * ‖y‖) = √(inner ℝ x x * inner ℝ y y - inner ℝ x y * inner ℝ x y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Cell.ofOption.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Cell.ofOption k none = Std.DTreeMap.Internal.Cell.empty
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.liftOfRightInverseAux_comp_apply : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (x : G₁),
  (f.liftOfRightInverseAux f_neg hf g hg) (f x) = g x
-- Mathlib.Data.Finset.PImage
/-- Image of `s : Finset α` under a partially defined function `f : α →. β`.  -/
Finset.pimage : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → (f : α →. β) → [(x : α) → Decidable (f x).Dom] → Finset α → Finset β
-- Init.Data.UInt.Bitwise
UInt64.xor_neg_one : ∀ {a : UInt64}, a ^^^ -1 = ~~~a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_le_minD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k ≠ ∅ → ∀ {fallback : α}, (cmp (t.minD fallback) ((t.erase k).minD fallback)).isLE = true