mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_fold : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M),
  ∑ i ∈ s, f i = Finset.fold (fun x1 x2 => x1 + x2) 0 f s
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_imp : ∀ {σs : List (Type u)} {P' Q' : Std.Do.SPred σs}, P' ∧ (P' → Q') ⊢ₛ P' ∧ Q'
-- Init.Data.UInt.Lemmas
UInt8.ofFin_bitVecToFin : ∀ (n : BitVec 8), UInt8.ofFin n.toFin = { toBitVec := n }
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertManyIfNew_list : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑↑(m.insertManyIfNew l)).buckets).Perm
      (Std.Internal.List.insertListIfNew (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Init.Data.List.Sublist
List.Sublist.head_mem : ∀ {α : Type u_1} {ys xs : List α}, ys.Sublist xs → ∀ (h : ys ≠ []), ys.head h ∈ xs
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_zpow₀ : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → GroupWithZero (G i)] [inst_7 : GroupWithZero C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  [∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f) (z : ℤ),
  DirectLimit.lift f (fun x => ⇑(g x)) h (x ^ z) = DirectLimit.lift f (fun x => ⇑(g x)) h x ^ z
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mk : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : Zero R] →
        [inst_2 : TopologicalSpace X] →
          [inst_3 : TopologicalSpace R] → (toContinuousMap : C(X, R)) → toContinuousMap 0 = 0 → ContinuousMapZero X R
-- Mathlib.Order.Minimal
minimal_and_iff_left_of_imp : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α],
  (∀ ⦃x : α⦄, P x → Q x) → (Minimal (fun x => Q x ∧ P x) x ↔ Q x ∧ Minimal P x)
-- Lean.Elab.ConfigEval.Util
_private.Lean.Elab.ConfigEval.Util.0.Lean.Elab.ConfigEval.planDerivation.tryInst : Lean.Name →
  (Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)) →
    Array Lean.Expr →
      Lean.ExprSet → Lean.Expr → Lean.Meta.SynthInstance.Instance → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instIsOrderedAddMonoid : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  IsOrderedAddMonoid (LieSubalgebra R L)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- Constructor for `BifibrantObject C`.  -/
HomotopicalAlgebra.BifibrantObject.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C] →
          [inst_4 : CategoryTheory.Limits.HasTerminal C] →
            (X : C) →
              [HomotopicalAlgebra.IsCofibrant X] →
                [HomotopicalAlgebra.IsFibrant X] → HomotopicalAlgebra.BifibrantObject C
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- **Alias** of `Mathlib.Tactic.BicategoryCoherence.bicategoryCoherence`.

---

Coherence tactic for bicategories.  -/
Mathlib.Tactic.BicategoryCoherence.bicategory_coherence : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.smul.eq_1 : ∀ (t : Tactic.ComputeAsymptotics.Monomial) (c : ℝ), t.smul c = { coef := c * t.coef, unit := t.unit }
-- Mathlib.Algebra.Notation.Indicator
Set.comp_indicator_const : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] {s : Set α} (c : M) (f : M → N),
  f 0 = 0 → (fun x => f (s.indicator (fun x => c) x)) = s.indicator fun x => f c
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins_eq_fill : ∀ {α : Type u_1} {c₀ : RBTree.RBColor} {n₀ : ℕ} {c : RBTree.RBColor} {n : ℕ} {path : RBTree.RBNode.Path α}
  {t : RBTree.RBNode α},
  RBTree.RBNode.Path.Balanced c₀ n₀ path c n → t.Balanced c n → path.ins t = (path.fill t).setBlack
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_le_iff_le_comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {I : Ideal R} {K : Ideal S} [inst_3 : RingHomClass F R S], Ideal.map f I ≤ K ↔ I ≤ Ideal.comap f K
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.go.eq_1 : ∀ (acc s a : String) (as : List String),
  String.intercalate.go✝ acc s (a :: as) = String.intercalate.go✝ (acc ++ s ++ a) s as
-- Init.Data.Range.Polymorphic.Instances
Std.Rxc.instIsAlwaysFiniteOfLawfulHasSize : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α], Std.Rxc.IsAlwaysFinite α
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.tendsto_integral_Ici_zero : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E},
  Filter.Tendsto a l Filter.atTop → Filter.Tendsto (fun i => ∫ (x : ℝ) in Set.Ici (a i), f x ∂μ) l (nhds 0)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The isomorphism between `incl ⋙ lift F _ _` with `F`.  -/
CategoryTheory.WithTerminal.inclLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → F.obj x ⟶ Z) →
              (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) →
                CategoryTheory.WithTerminal.incl.comp (CategoryTheory.WithTerminal.lift F M hM) ≅ F
-- Mathlib.Data.Sum.Order
/-- `Equiv.sumComm` promoted to an order isomorphism.  -/
OrderIso.sumComm : (α : Type u_10) → (β : Type u_11) → [inst : LE α] → [inst_1 : LE β] → α ⊕ β ≃o β ⊕ α
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact : @AlgebraicGeometry.QuasiSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.QuasiCompact
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_terminal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [inst_2 : CategoryTheory.Limits.HasTerminal C],
  P (⊤_ C)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
Diffeomorph.mfderivToContinuousLinearEquiv_coe : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {x : M} (Φ : Diffeomorph I J M N n)
  (hn : n ≠ 0), ↑(Φ.mfderivToContinuousLinearEquiv hn x) = mfderiv% ⇑Φ x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.WorkspaceSymbolParams.mk.injEq : ∀ (query query_1 : String), ({ query := query } = { query := query_1 }) = (query = query_1)
-- Mathlib.Data.Finset.Grade
Multiset.covBy_iff : ∀ {α : Type u_1} {s t : Multiset α}, s ⋖ t ↔ ∃ a, a ::ₘ s = t
-- Mathlib.Analysis.Complex.Schwarz
/-- **Alias** of `Complex.norm_le_norm_of_mapsTo_ball`.

---

The **Schwarz Lemma**.
Let `f : E → F` be a complex analytic on an open ball with center at the origin.
If `f` sends this ball to the closed ball with center `0` of the same radius and `f 0 = 0`,
then for any point `z` of this disk we have `‖f z‖ ≤ ‖z‖`.  -/
Complex.norm_le_norm_of_mapsTo_ball_self : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R : ℝ} {f : E → F} {z : E},
  DifferentiableOn ℂ f (Metric.ball 0 R) →
    Set.MapsTo f (Metric.ball 0 R) (Metric.closedBall 0 R) → f 0 = 0 → ‖z‖ < R → ‖f z‖ ≤ ‖z‖
-- Init.Data.Nat.ToString
Nat.isDigit_digitChar : ∀ {n : ℕ}, n.digitChar.isDigit = decide (n < 10)
-- Mathlib.Order.MinMax
max_right_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max (max a b) c = max (max a c) b
-- Mathlib.Topology.Compactness.Compact
Set.Finite.isCompact_biUnion : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set ι} {f : ι → Set X},
  s.Finite → (∀ i ∈ s, IsCompact (f i)) → IsCompact (⋃ i ∈ s, f i)
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (toContinuousMap : C(α, β))
  (map_open' : IsOpenMap toContinuousMap.toFun) (toContinuousMap_1 : C(α, β))
  (map_open'_1 : IsOpenMap toContinuousMap_1.toFun),
  ({ toContinuousMap := toContinuousMap, map_open' := map_open' } =
      { toContinuousMap := toContinuousMap_1, map_open' := map_open'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_sigmaUncurry : ∀ {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8}
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)], Measurable Sigma.uncurry
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context.uvars : Lean.Elab.Term.Do.ToTerm.Context → Array Lean.Elab.Term.Do.Var
-- Mathlib.Algebra.Group.Submonoid.Units
instIsLocalHomSubtypeMemSubmonoidEqLocusMMonoidHomSubtype : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (f g : M →* N), IsLocalHom (f.eqLocusM g).subtype
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule.mk : Lean.EffectiveImport →
  Array (Lean.ModuleData × Lean.CompactedRegion) →
    Array (Lean.ModuleData × Lean.CompactedRegion) → Bool → Lean.ImportedModule✝
-- Std.Do.SPred.DerivedLaws
/-- A generalization of `pure_intro` exploiting `IsPure`.  -/
Std.Do.SPred.Tactic.Pure.intro : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs} {φ : Prop} [Std.Do.SPred.Tactic.IsPure Q φ], φ → P ⊢ₛ Q
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below.base : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} (α : F), IsSolvableByRad.below ⋯
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eval_cons : ∀ {R : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : SMul R M] (p : R × M) (l : Mathlib.Tactic.Module.NF R M),
  (p ::ᵣ l).eval = p.1 • p.2 + l.eval
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- If `G : C ⥤ D` is cover dense and full, then the
map `(P ⟶ Q) → (G.op ⋙ P ⟶ G.op ⋙ Q)` is bijective when `Q` is a sheaf.  -/
CategoryTheory.Functor.whiskerLeft_obj_map_bijective_of_isCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] {A : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_4, u_4} A] (P Q : CategoryTheory.Functor Dᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf K Q →
    Function.Bijective ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
-- Mathlib.Control.Monad.Writer
WriterT.run_mk : ∀ {M : Type u → Type v} {α ω : Type u} (cmd : M (α × ω)), (WriterT.mk cmd).run = cmd
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Ioi_eq_Ioi_iInf : ∀ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ι → R}, ⋃ i, Set.Ioi (f i) = Set.Ioi (⨅ i, f i)
-- Mathlib.Logic.Equiv.Defs
Equiv.ofUnique_symm_apply : ∀ (α : Sort u) (β : Sort v) [inst : Unique α] [inst_1 : Unique β] (a : β), (Equiv.ofUnique α β).symm a = default a
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.ExchangeProperty.encard_sdiff_le_aux`. -/
Matroid.ExchangeProperty.encard_diff_le_aux : ∀ {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α},
  Matroid.ExchangeProperty IsBase → IsBase B₁ → IsBase B₂ → (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from rings to additive commutative groups preserves all limits.
 -/
RingCat.forget₂AddCommGroup_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ RingCat AddCommGrpCat)
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_rii : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_rii._auto_1)
  {t : Std.DTreeMap α β cmp}, Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_add : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (x y : ↥S), ↑(x + y) = ↑x + ↑y
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.measurableEquiv_comp_right : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨}
  {κ : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.SFinite P] [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.HasCondDistrib Y X κ P →
    ∀ (f : 𝓧 ≃ᵐ 𝓩), ProbabilityTheory.HasCondDistrib Y (⇑f ∘ X) (κ.comap ⇑f.symm ⋯) P
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramNatTrans_zero : ∀ {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 : CategoryTheory.Preadditive D] (X : C) (P Q : CategoryTheory.Functor Cᵒᵖ D), J.diagramNatTrans 0 X = 0
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) {X : AlgebraicGeometry.Scheme} [inst : X.Over S]
  (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))),
  ↑((AlgebraicGeometry.AffineSpace.homOverEquiv S).symm v) = AlgebraicGeometry.AffineSpace.homOfVector (X ↘ S) v
-- Std.Sync.Channel
Std.CloseableChannel.instReprError.repr : Std.CloseableChannel.Error → ℕ → Std.Format
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsDenseInducing.isUniformInducing_extend : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] [CompleteSpace β] [CompleteSpace γ] {i : α → β} {f : α → γ} (hid : IsDenseInducing i),
  IsUniformInducing i → IsUniformInducing f → IsUniformInducing (hid.extend f)
-- Mathlib.Util.SleepHeartbeats
/-- do nothing for at least n heartbeats  -/
tacticSleep_heartbeats_ : Lean.ParserDescr
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Init.Data.Array.Attach
Array.filterMap_attachWith : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {q : α → Prop} {xs : Array α} {f : { x // q x } → Option β}
  (H : ∀ x ∈ xs, q x),
  stop = (xs.attachWith q H).size →
    Array.filterMap f (xs.attachWith q H) 0 stop =
      Array.filterMap
        (fun x =>
          match x with
          | ⟨x, h⟩ => f ⟨x, ⋯⟩)
        xs.attach
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.cast_smul_eq_mul : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {R' : Type u_3}
  [inst : HSMul R' A A] {r' : R'} {r r'' : R},
  r = r'' → (∀ (a : A), r • a = r' • a) → ∀ (a : A), r' • a = ((algebraMap R A) r'' + 0) * a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.TreeMap.Raw.ofList l cmp).getKey? k = none
-- Mathlib.RingTheory.Henselian
HenselianLocalRing.TFAE : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsLocalRing R],
  [HenselianLocalRing R,
      ∀ (f : Polynomial R),
        f.Monic →
          ∀ (a₀ : IsLocalRing.ResidueField R),
            (Polynomial.aeval a₀) f = 0 →
              (Polynomial.aeval a₀) (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (IsLocalRing.residue R) a = a₀,
      ∀ {K : Type u} [inst_2 : Field K] (φ : R →+* K),
        Function.Surjective ⇑φ →
          ∀ (f : Polynomial R),
            f.Monic →
              ∀ (a₀ : K),
                Polynomial.eval₂ φ a₀ f = 0 →
                  Polynomial.eval₂ φ a₀ (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE
-- Mathlib.NumberTheory.MulChar.Basic
/-- If `a` is a unit and `n : ℤ`, then `(χ ^ n) a = χ (a ^ n)`.  -/
MulChar.zpow_apply_coe : ∀ {R : Type u_4} [inst : CommGroupWithZero R] {R' : Type u_5} [inst_1 : CommRing R'] (χ : MulChar R R') (n : ℤ)
  (a : Rˣ), (χ ^ n) ↑a = χ ↑(a ^ n)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.IsLinear.linear : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} {inst : Semiring R} {inst_1 : TopologicalSpace F}
  {inst_2 : TopologicalSpace B} {inst_3 : AddCommMonoid F} {inst_4 : Module R F}
  {inst_5 : (x : B) → AddCommMonoid (E x)} {inst_6 : (x : B) → Module R (E x)}
  {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj} [self : Bundle.Pretrivialization.IsLinear R e],
  ∀ b ∈ e.baseSet, IsLinearMap R fun x => (↑e ⟨b, x⟩).2
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_pos_of_pos : ∀ {q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], 0 < q → 0 < ↑q
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_base_mul : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → p.maxPowDvdDiv (p * n) = (padicValNat p n + 1, n.divMaxPow p)
-- Mathlib.Algebra.Order.Round
/-- Away from the points with fractional part `1 / 2`, `round x = ⌈2 * x⌉ / 2`.  -/
round_eq_half_ceil_two_mul : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] {x : α},
  2 * Int.fract x ≠ 1 → round x = ⌈2 * x⌉ / 2
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
_private.Mathlib.NumberTheory.RamificationInertia.HilbertTheory.0.IsDecompositionField.instances : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [inst_6 : Algebra A K]
  [IsFractionRing A K] [inst_8 : Algebra A L] [IsScalarTower A K L] [inst_10 : Algebra B L] [IsScalarTower A B L]
  [IsFractionRing B L] [inst_13 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5)
  (𝓞D : Type u_6) [inst_15 : Field D] [inst_16 : Algebra D L] [IsDecompositionField K L P D] [inst_18 : CommRing 𝓞D]
  [inst_19 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_21 : Algebra 𝓞D B] [inst_22 : Algebra 𝓞D L]
  [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B]
  [Module.Finite A B] [Module.IsTorsionFree A B] [inst_30 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B]
  [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p],
  p ≠ ⊥ →
    Module.Finite 𝓞D B ∧
      Module.IsTorsionFree 𝓞D B ∧ Module.IsTorsionFree A 𝓞D ∧ IsGaloisGroup Gal(L/K) A B ∧ IsGaloisGroup ⋯ 𝓞D B ∧ 𝓟D ≠ ⊥
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.instBEqDefaultClause : {numVarsSucc : ℕ} → BEq (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc)
-- Init.Data.Nat.Div.Lemmas
Nat.div_mod_eq_div : ∀ {a b c : ℕ}, a < c → a / b % c = a / b
-- Mathlib.Data.Nat.Choose.Sum
Finset.sum_antidiagonal_choose_add : ∀ (d n : ℕ), ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.isPiSystem_Ici_rat : IsPiSystem (⋃ a, {Set.Ici ↑a})
-- Init.Prelude
instDecidableEqUInt8 : DecidableEq UInt8
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsContained.not_cliqueFree_card : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α],
  (SimpleGraph.completeGraph α).IsContained G → ¬G.CliqueFree (Fintype.card α)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_mapId_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.swap B C).mapId x).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1))
-- Mathlib.Analysis.CStarAlgebra.Fuglede
/-- **Fuglede–Putnam–Rosenblum**: If `a` and `b` are normal elements in a C⋆-algebra `A` which
are interwined by `x`, then `star a` and `star b` are also intertwined by `x`.  -/
SemiconjBy.star_right : ∀ {A : Type u_2} [inst : NonUnitalCStarAlgebra A] {a b x : A},
  IsStarNormal a → IsStarNormal b → SemiconjBy x a b → SemiconjBy x (star a) (star b)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_id_limit : ∀ {o : Ordinal.{u}}, (∀ a < o, Order.succ a < o) → (o.bsup fun x x_1 => x) = o
-- Mathlib.Data.List.Lex
List.Lex.isOrderConnected : ∀ {α : Type u} (r : α → α → Prop) [IsOrderConnected α r] [Std.Trichotomous r], IsOrderConnected (List α) (List.Lex r)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.app_shift : ∀ {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₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C),
  τ.app ((CategoryTheory.shiftFunctor C a).obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X))
        ((CategoryTheory.Functor.commShiftIso F₂ a).inv.app X))
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact
instPreservesFiniteLimitsModuleCatRestrictScalars : ∀ {R : Type u} [inst : CommRing R] {R' : Type u'} [inst_1 : CommRing R'] (f : R →+* R'),
  CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.inl_biprodComparison'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj (X ⊞ Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (F.biprodComparison' X Y) h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.biprod.inl) h
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.eq_symm_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) (f : α → α) (g : α → β), f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g