mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Laurent
RatFunc.laurentAux_ofFractionRing_mk : ∀ {R : Type u} [inst : CommRing R] (r : R) (p : Polynomial R) (q : ↥(nonZeroDivisors (Polynomial R))),
  (RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } =
    { toFractionRing := Localization.mk ((Polynomial.taylor r) p) ⟨(Polynomial.taylor r) ↑q, ⋯⟩ }
-- Mathlib.RingTheory.WittVector.InitTail
/-- `WittVector.init n x` is polynomial in the coefficients of `x`.  -/
WittVector.init_isPoly : ∀ (p n : ℕ), WittVector.IsPoly p fun x x_1 => WittVector.init n
-- Init.Data.UInt.Lemmas
UInt16.mul_sub : ∀ {a b c : UInt16}, a * (b - c) = a * b - a * c
-- Aesop.Tree.Data
Aesop.MVarCluster.goals : Aesop.MVarCluster → Array Aesop.GoalRef
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.instCountableInterFilterAe : ∀ {α : Type u_1} {F : Type u_2} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  (μ : F), CountableInterFilter (MeasureTheory.ae μ)
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort.eq_1 : ∀ (x : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var x).sort = Lean.Grind.AC.Seq.var x
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mk.injEq : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (prop prop_1 : (X : B) → CategoryTheory.ObjectProperty ↑(F.obj X)),
  ({ prop := prop } = { prop := prop_1 }) = (prop = prop_1)
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_sub : ∀ {α : Type u_2} [inst : Sub α], CovariantClass (Filter α) (Filter α) (fun x1 x2 => x1 - x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.disjoint_incidenceFinset_of_disjoint : ∀ {V : Type u_1} (G H : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V]
  [inst_2 : Fintype ↑(H.neighborSet v)], Disjoint G H → Disjoint (G.incidenceFinset v) (H.incidenceFinset v)
-- Std.Time.Format
/-- Converts a date in the American format (`MM-dd-uuuu`) into a `String`.
 -/
Std.Time.PlainDate.toAmericanDateString : Std.Time.PlainDate → String
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallyDisconnected_of_isTotallySeparated : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsTotallySeparated s → IsTotallyDisconnected s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.unit : Lean.Grind.CommRing.Mon
-- Mathlib.SetTheory.ZFC.Class
Class.sInter_apply : ∀ {x : Class.{u}} {y : ZFSet.{u}}, x.sInter y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_mul : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x y : R), v (x * y) = v x + v y
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_map_eq : ∀ {R : Type u} {L : Type v} {L' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} (k : ℕ),
  Function.Surjective ⇑f → LieIdeal.map f (LieAlgebra.derivedSeries R L' k) = LieAlgebra.derivedSeries R L k
-- Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
CategoryTheory.Functor.reflects_precoherent : ∀ {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] (F : CategoryTheory.Functor C D)
  [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.EffectivelyEnough]
  [CategoryTheory.Precoherent D] [F.Full] [F.Faithful], CategoryTheory.Precoherent C
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- **Alias** of `MeasureTheory.SimpleFunc.lintegral_finsetSum`. -/
MeasureTheory.SimpleFunc.lintegral_finset_sum : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : MeasureTheory.SimpleFunc α ENNReal)
  (μ : ι → MeasureTheory.Measure α) (s : Finset ι), f.lintegral (∑ i ∈ s, μ i) = ∑ i ∈ s, f.lintegral (μ i)
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_mod : ∀ (a b : UInt8), (a % b).toUInt64 = a.toUInt64 % b.toUInt64
-- Init.Data.Order.Classes
Std.MinEqOr.min_eq_or : ∀ {α : Type u} {inst : Min α} [self : Std.MinEqOr α] (a b : α), a ⊓ b = a ∨ a ⊓ b = b
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.compileStxMatch : List Lean.Term → List Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Data.List.Basic
List.disjoint_reverse_left : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.reverse.Disjoint l₂ ↔ l₁.Disjoint l₂
-- Std.Data.DHashMap.RawLemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `get_insertIfNew`.  -/
Std.DHashMap.Raw.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β k}, a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isBool.sizeOf_spec : ∀ (val : Bool) (proof : Lean.Expr),
  sizeOf (Mathlib.Meta.NormNum.Result'.isBool val proof) = 1 + sizeOf val + sizeOf proof
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.id_apply : ∀ (M : AddCommMonCat) (x : ↑M), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- `Result` stores the information from a lemma that was successfully applied.  -/
Mathlib.Tactic.ClickSuggestions.Result : Type → Type
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsNotG2.pairingIn_mem_zero_one_two : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsNotG2]
  (i j : ι), P.pairingIn ℤ i j ∈ {-2, -1, 0, 1, 2}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_neg : ∀ (x : ℝ), Real.sinc (-x) = Real.sinc x
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.eq_6 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.black l v r with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_6 a x b (RBTree.RBNode.node RBTree.RBColor.black l v r) l v r ⋯
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.group.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Group G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieGroup I' n G],
  ContMDiffMap.group =
    { toMonoid := ContMDiffMap.monoid, inv := fun f => ⟨fun x => (f x)⁻¹, ⋯⟩, div := fun f g => ⟨⇑f / ⇑g, ⋯⟩,
      zpow := zpowRec, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_right_of_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R]
  [AddRightReflectLE R] {a b c : R}, c < 0 → (a * c ≤ b * c ↔ b ≤ a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β k}, (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (k : ℕ),
  (LinearMap.toMatrix v₁ v₁) f ^ k = (LinearMap.toMatrix v₁ v₁) (f ^ k)
-- Mathlib.Topology.MetricSpace.Dilation
/-- `DilationClass F α β r` states that `F` is a type of `r`-dilations.
You should extend this typeclass when you extend `Dilation`.  -/
DilationClass : (F : Type u_3) →
  (α : outParam (Type u_4)) →
    (β : outParam (Type u_5)) → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → [FunLike F α β] → Prop
-- Std.Data.HashMap.Lemmas
_private.Std.Data.HashMap.Lemmas.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_iUnion_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [inst : TopologicalSpace β] {m₀ : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : ι → Set α},
  MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ i, s i)) ↔
    ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))
-- Mathlib.Data.List.Basic
List.replicate_right_inj' : ∀ {α : Type u} {a b : α} {n : ℕ}, List.replicate n a = List.replicate n b ↔ n = 0 ∨ a = b
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.toSuccArrow_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C),
  (Φ.toSuccArrow X).left = X
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_left_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b c : α},
      a ∈ s → b ∈ s → c ∈ s → (variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0)
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_toOuterMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    (MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.sheafify (P.comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F)
      (CategoryTheory.CategoryStruct.comp (J.sheafifyCompIso F P).hom h) =
    CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F)) h
-- Mathlib.Algebra.Ring.Nat
Nat.instNonAssocSemiring : NonAssocSemiring ℕ
-- Std.Time.Date.PlainDate
/-- Subtracts `Year.Offset` from a `PlainDate`, clipping the day to the last valid day of the month.
 -/
Std.Time.PlainDate.subYearsClip : Std.Time.PlainDate → Std.Time.Year.Offset → Std.Time.PlainDate
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- **The Hahn decomposition theorem**: Given a signed measure `s`, there exist
complement measurable sets `i` and `j` such that `i` is positive, `j` is negative.  -/
MeasureTheory.SignedMeasure.exists_isCompl_positive_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  ∃ i j,
    MeasurableSet i ∧
      MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
        MeasurableSet j ∧
          MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ IsCompl i j
-- Mathlib.Order.PiLex
Pi.instOrderBotColexForallOfWellFoundedGT : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [WellFoundedGT ι] →
        [inst_2 : (a : ι) → PartialOrder (β a)] → [(a : ι) → OrderBot (β a)] → OrderBot (Colex ((a : ι) → β a))
-- Std.Data.ByteSlice
/-- Comparison function
 -/
ByteSlice.beq : ByteSlice → ByteSlice → Bool
-- Init.Prelude
/-- Changes the kind at the root of a `Syntax.node` to `k`.

Returns all other `Syntax` values unchanged.
 -/
Lean.Syntax.setKind : Lean.Syntax → Lean.SyntaxNodeKind → Lean.Syntax
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) h)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_sq : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : TopologicalSpace A] [inst_2 : StarRing A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A]
  [T2Space A] [inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), CFC.abs a ^ 2 = star a * a
-- Init.Data.List.MinMaxOn
List.apply_minOn_le_apply_minOn_of_subset : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : ys ⊆ xs) (hys : ys ≠ []), f (List.minOn f xs ⋯) ≤ f (List.minOn f ys hys)
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Discrete PUnit.{w + 1} × C} (f : X ⟶ Y),
  (CategoryTheory.prod.leftUnitor C).map f = f.2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insert_eq_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {p : (a : α) × β a},
  insert p t = t.insert p.fst p.snd
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivWithinAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {s : Set E}
  {f₂ : E → G} {f₂' : E →L[𝕜] G},
  HasFDerivWithinAt f₁ f₁' s x →
    HasFDerivWithinAt f₂ f₂' s x → HasFDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') s x
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuous_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f ↔ ∀ (x : α), UpperHemicontinuousAt f x
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.ext : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] {f g : M →ₗ⁅R,L⁆ N}, (∀ (m : M), f m = g m) → f = g
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
  (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ D hι u).W =
    ((⨆ i, (D i).W) ⊔ CategoryTheory.MorphismProperty.ofHoms fun x => CategoryTheory.CategoryStruct.id m) ⊔
      CategoryTheory.MorphismProperty.ofHoms fun x =>
        CategoryTheory.CategoryStruct.comp ((D x.fst).isTerminal.lift ⋯) (u x.fst)
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- **Alias** of `dvd_antisymm`. -/
Dvd.dvd.antisymm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b : α} [Subsingleton αˣ], a ∣ b → b ∣ a → a = b
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- ...factorizing `e` through `f`...  -/
CategoryTheory.EffectiveEpiStruct.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X}
  (self : CategoryTheory.EffectiveEpiStruct f) {W : C} (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
  CategoryTheory.CategoryStruct.comp f (self.desc e ⋯) = e
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- Auxiliary construction used to build the `Mul` instance and get distributivity of `+` and
`\smul`.  -/
GradedTensorProduct.mulHom : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [Module ι (Additive ℤˣ)] →
                                GradedTensorProduct R 𝒜 ℬ →ₗ[R]
                                  GradedTensorProduct R 𝒜 ℬ →ₗ[R] GradedTensorProduct R 𝒜 ℬ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_natCast_cpow_le_norm_natCast_cpow_iff : ∀ {n : ℕ}, 1 < n → ∀ {w z : ℂ}, ‖↑n ^ w‖ ≤ ‖↑n ^ z‖ ↔ w.re ≤ z.re
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.cases_on : ∀ {α : Type u} {P : WithZero α → Prop} (x : WithZero α), P 0 → (∀ (a : α), P ↑a) → P x
-- Mathlib.Data.PNat.Find
PNat.find_le_iff : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ+), PNat.find h ≤ n ↔ ∃ m ≤ n, p m
-- Lean.Structure
_private.Lean.Structure.0.Lean.instInhabitedStructureState : Inhabited Lean.StructureState✝
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_homologyIso_eq_left_homologyIso : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ :
    autoParam (n₀ + 1 = n₁)
      CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_homologyIso_eq_left_homologyIso._auto_1)
  (hn₂ :
    autoParam (n₁ + 1 = n₂)
      CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_homologyIso_eq_left_homologyIso._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).right.homologyIso =
    (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  k ∈ t → (f (Std.DTreeMap.Const.get? t k)).isSome = true → (Std.DTreeMap.Const.alter t k f).size = t.size
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Rat.toDyadic.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X},
  e.IsImage s t → x ∈ e.source → Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) t
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.continuous_mapGL : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] [inst_6 : Algebra R S]
  [IsTopologicalRing S] [ContinuousSMul R S], Continuous ⇑(Matrix.SpecialLinearGroup.mapGL S)