mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  (p.append p').support = p.support ++ p'.support.tail
-- Mathlib.Topology.ExtremallyDisconnected
/-- Lemma 2.2 in [Gleason, *Projective topological spaces*][gleason1958]:
in an extremally disconnected space, if $U_1$ and $U_2$ are disjoint open sets,
then $\overline{U_1}$ and $\overline{U_2}$ are also disjoint.  -/
ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen : ∀ {A : Type u} [inst : TopologicalSpace A] [ExtremallyDisconnected A] {U₁ U₂ : Set A},
  Disjoint U₁ U₂ → IsOpen U₁ → IsOpen U₂ → Disjoint (closure U₁) (closure U₂)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.TreeSet.Raw.ofList l cmp).contains k = l.contains k
-- Mathlib.Probability.Kernel.Category.Stoch
instDeterministicStochMkWideSubcategorySFinKerStochHomMkOfIsDeterministicCarrierObj : ∀ (X Y : Stoch) (κ : ProbabilityTheory.Kernel X.obj.carrier Y.obj.carrier) [ProbabilityTheory.IsDeterministic κ]
  [inst : ProbabilityTheory.IsMarkovKernel κ],
  CategoryTheory.Deterministic { hom := { hom := κ, property := ⋯ }, property := ⋯ }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : Inhabited α]
  [EquivBEq α] [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey! k = m₂.getKey! k
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_lift_fst_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : M ⟶ K) (β : M ⟶ L) (i : ι) {Z : C} (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h) =
    CategoryTheory.CategoryStruct.comp (α.f i) h
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.numLiterals_pos : ∀ {v : ℕ} {f : Std.Sat.CNF ℕ}, Std.Sat.CNF.VarMem v f → 0 < f.numLiterals
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_image : ∀ {f : PSet.{u} → PSet.{u}},
  (∀ (x y : PSet.{u}), x.Equiv y → (f x).Equiv (f y)) → ∀ {x y : PSet.{u}}, y ∈ PSet.image f x ↔ ∃ z ∈ x, y.Equiv (f z)
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.MethodsRefPointed : NonemptyType
-- Init.Prelude
/-- Gets the number of elements stored in an array.

This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as
its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
internal detail that's not observable by Lean code.
 -/
Array.size : {α : Type u} → Array α → ℕ
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instDecidableMem : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (key : α) → (map : Std.Internal.IndexMultiMap α β) → Decidable (key ∈ map)
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.addCommMonoid.eq_1 : ∀ {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.IsUnital m₁ e₁) [h : AddZeroClass X]
  (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d),
  EckmannHilton.addCommMonoid h₁ distrib =
    { toAdd := h.toAdd, add_assoc := ⋯, toZero := h.toZero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Init.SimpLemmas
cond_false : ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = b
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.prop_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α} {P : α → Prop} [inst : LE α], IsRelUpperSet s P → a ∈ s → P a
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticWith : {α : Type} → [BEq α] → BEq (Lean.Lsp.DiagnosticWith α)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.prod_snd : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β], LipschitzWith 1 Prod.snd
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_eq_zero_iff : ∀ {x : ℝ}, Real.artanh x = 0 ↔ x ≤ -1 ∨ x = 0 ∨ 1 ≤ x
-- Init.Data.BitVec.Lemmas
BitVec.srem_self : ∀ {w : ℕ} {x : BitVec w}, x.srem x = 0#w
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.brecOn.eq : ∀ {α : Type u} {motive : Ordnode α → Sort u_1} (t : Ordnode α) (F_1 : (t : Ordnode α) → Ordnode.below t → motive t),
  Ordnode.brecOn t F_1 = F_1 t (Ordnode.brecOn.go t F_1).2
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.abs_sub_ceil_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] {a : R},
  0 ≤ a → |a - ↑⌈a⌉₊| ≤ 1
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.withTop`.

---

The map `CardinalDirectedPoset κ → CardinalDirectedPoset κ` which sends
a partially ordered `κ`-filtered type `J` to `WithTop J`.  -/
CategoryTheory.CardinalFilteredPoset.withTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] → CategoryTheory.CardinalDirectedPoset κ → CategoryTheory.CardinalDirectedPoset κ
-- Std.Time.Format.DateFormat
Std.Time.instReprDayPeriodSymbols : Repr Std.Time.DayPeriodSymbols
-- Mathlib.Analysis.Seminorm
Seminorm.comp_smul_apply : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜]
  [inst_1 : SeminormedCommRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E]
  [inst_4 : AddCommGroup E₂] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂)
  (c : 𝕜₂) (x : E), (p.comp (c • f)) x = ‖c‖ * p (f x)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.map_id : ∀ {α : Type u_2} [inst : Preorder α] (c : OmegaCompletePartialOrder.Chain α), c.map OrderHom.id = c
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_ofNat_inv_pow : ∀ (x : ℂ) (n : ℕ) [inst : n.AtLeastTwo], (x ^ (OfNat.ofNat n)⁻¹) ^ OfNat.ofNat n = x
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_succ : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) (i : Fin m), Matrix.vecCons x u i.succ = u i
-- Init.Grind.Norm
Lean.Grind.not_ite : ∀ {p : Prop} {x : Decidable p} (q r : Prop), (¬if p then q else r) = if p then ¬q else ¬r
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentRegistrationOptions : Type
-- Std.Data.DTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the smallest key.
 -/
Std.DTreeMap.minKey : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → t.isEmpty = false → α
-- Mathlib.Probability.Distributions.Uniform
PMF.mem_support_uniformOfFinset_iff : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (a : α), a ∈ (PMF.uniformOfFinset s hs).support ↔ a ∈ s
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.imageι_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f),
  CategoryTheory.CategoryStruct.comp self.imageι (CategoryTheory.Limits.Cofork.π self.cokernelCofork) = 0
-- Batteries.Data.Array.Scan
Array.scanr_extract : ∀ {α : Type u_1} {β : Type u_2} {stop start : ℕ} {init : β} {f : α → β → β} {as : Array α},
  Array.scanr f init (as.extract stop start) = Array.scanr f init as start stop
-- Mathlib.Data.Nat.Count
Nat.count_add' : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (a b : ℕ),
  Nat.count p (a + b) = Nat.count (fun k => p (k + b)) a + Nat.count p b
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Corollary of the Lebesgue dominated convergence theorem: If a sequence of functions `F n` is
(eventually) uniformly bounded by a constant and converges (eventually) pointwise to a
function `f`, then the integrals of `F n` with respect to a vector measure `μ` with finite
variation converge to the integral of `f`.  -/
MeasureTheory.VectorMeasure.tendsto_integral_filter_of_norm_le_const : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F}
  {B : E →L[ℝ] F →L[ℝ] G} {l : Filter ι} [l.IsCountablyGenerated] {F_1 : ι → X → E}
  [MeasureTheory.IsFiniteMeasure μ.variation] {f : X → E},
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F_1 n) μ.variation) →
    (∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (a : X) ∂μ.variation, ‖F_1 n a‖ ≤ C) →
      (∀ᵐ (a : X) ∂μ.variation, Filter.Tendsto (fun n => F_1 n a) l (nhds (f a))) →
        Filter.Tendsto (fun n => ∫ᵛ (a : X), F_1 n a ∂[B; μ]) l (nhds ∫ᵛ (a : X), f a ∂[B; μ])
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.forMUncurried_eq_forM_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap.Raw α fun x => β} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF →
    ∀ {f : α × β → m' PUnit.{w + 1}},
      Std.DHashMap.Raw.Const.forMUncurried f m = (Std.DHashMap.Raw.Const.toList m).forM f
-- Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
MeasureTheory.Measure.MutuallySingular.compProd_of_right' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η]
  [MeasurableSpace.CountableOrCountablyGenerated α β] (μ ν : MeasureTheory.Measure α),
  (∀ᵐ (a : α) ∂ν, (κ a).MutuallySingular (η a)) → (μ.compProd κ).MutuallySingular (ν.compProd η)
-- Mathlib.Algebra.Polynomial.DenomsClearable
denomsClearable_C_mul_X_pow : ∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {i : R →+* K} {b : R} {bi : K} {N : ℕ}
  (a : R), bi * i b = 1 → ∀ {n : ℕ} (r : R), n ≤ N → DenomsClearable a b N (Polynomial.C r * Polynomial.X ^ n) i
-- Lean.Meta.NatInstTesters
Lean.Meta.DefEq.isInstLTNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_sin : ∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → Real.arcsin (Real.sin x) = x
-- Mathlib.Analysis.Convex.Basic
convex_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {ι : Type u_5} {s : Finset ι} (t : ι → Set E),
  (∀ i ∈ s, Convex 𝕜 (t i)) → Convex 𝕜 (∑ i ∈ s, t i)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.uset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5) (fvarId_1 : Lean.FVarId)
  (i_1 : ℕ) (y_1 : Lean.FVarId)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5),
  (Lean.Compiler.LCNF.CodeDecl.uset fvarId i y h = Lean.Compiler.LCNF.CodeDecl.uset fvarId_1 i_1 y_1 h_1) =
    (fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyδOfTriangle_homologyMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)),
  DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyδOfTriangle_homologyMap._auto_1),
      CategoryTheory.CategoryStruct.comp (CochainComplex.homologyδOfTriangle T n₀ n₁ h)
          (HomologicalComplex.homologyMap T.mor₁ n₁) =
        0
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.is_invariant_const : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : ℂ),
  SlashAction.map 0 A (Function.const UpperHalfPlane x) = Function.const UpperHalfPlane x
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.pretopology_inf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (P Q : CategoryTheory.MorphismProperty C) [inst_2 : P.IsMultiplicative] [inst_3 : P.IsStableUnderBaseChange]
  [inst_4 : Q.IsMultiplicative] [inst_5 : Q.IsStableUnderBaseChange],
  (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
_private.Mathlib.RepresentationTheory.Homological.TateCohomology.Basic.0.CochainComplex.ConnectData.X.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.Data.Int.Cast.Lemmas
/-- Additive homomorphisms from `ℤ` are defined by the image of `1`.  -/
zmultiplesHom : (β : Type u_4) → [inst : AddGroup β] → β ≃ (ℤ →+ β)
-- Aesop.Script.UScript
Aesop.Script.UScript.render : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Aesop.Script.TacticState → Aesop.Script.UScript → m (Array Lean.Syntax.Tactic)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_div_two_eq_sqrt : ∀ {x : ℝ} (r : ℝ), 0 ≤ x → x ^ (r / 2) = √x ^ r
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.of_restrictScalars : ∀ (R : Type u_4) [inst : CommRing R] (A : Type u_5) [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type u_6)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [Algebra.FormallyUnramified R A] [Algebra.FormallySmooth R B], Algebra.FormallySmooth A B
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderEmbedding.image_setOfPred_minimal`. -/
OrderEmbedding.image_setOf_minimal : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β},
  ⇑f '' {x | Minimal (fun x => x ∈ s) x} = {x | Minimal (fun x => x ∈ ⇑f '' s) x}
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.exists_companion' : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (self : QuadraticMap R M N),
  ∃ B, ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B x) y
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsLocalRingSubtypeMemSubalgebraOfFieldPrimeComplAsIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsLocalRing ↥(Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯)
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.mk : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m]
  [toLawfulMonad : LawfulMonad m],
  (∀ {α : Type u_1} (f : σ → α × σ),
      modifyGet f = do
        let z ← f <$> get
        set z.2
        pure z.1) →
    (∀ {α : Type u_1} (mx : m α),
        (do
            let _ ← get
            mx) =
          mx) →
      (∀ {α : Type u_1} (mx : σ → σ → m α),
          (do
              let s ← get
              let s' ← get
              mx s s') =
            do
            let s ← get
            mx s s) →
        (∀ {α : Type u_1} (mx : σ → PUnit.{u_1 + 1} → m α),
            (do
                let s ← get
                let u ← set s
                mx s u) =
              do
              let s ← get
              mx s PUnit.unit) →
          (∀ (s : σ),
              (do
                  set s
                  get) =
                do
                set s
                pure s) →
            (∀ (s s' : σ),
                (do
                    set s
                    set s') =
                  set s') →
              LawfulMonadStateOf σ m
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the left preserves `C^n` functions in a domain
at a point.  -/
ContDiffAt.continuousLinearMap_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {x : E} {n : WithTop ℕ∞} (g : F →L[𝕜] G),
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (⇑g ∘ f) x
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (a : L'.BoundedFormula α n),
  φ.onBoundedFormula.symm a = φ.invLHom.onBoundedFormula a
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `p` is `p⁻¹` if `p > 1`.

See also `padicNorm.padicNorm_p_of_prime` for a version assuming `p` is prime.  -/
padicNorm.padicNorm_p : ∀ {p : ℕ}, 1 < p → padicNorm p ↑p = (↑p)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.IsMonoidal.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [toContainsUnit : P.ContainsUnit] [toTensorLE : P.TensorLE P P], P.IsMonoidal
-- Mathlib.Topology.Instances.Matrix
/-- **Alias** of the reverse direction of `continuous_matrixOf`. -/
Continuous.matrixOf : ∀ {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace α]
  {f : α → m → n → R}, Continuous f → Continuous fun x => Matrix.of (f x)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const_ae : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {C : ENNReal},
  (∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ₑ ≤ C) → ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (v : β k), (t₁.insert k v).Equiv (t₂.insert k v)
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂]
  {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [Module.IsTorsionFree R₁ ↥F₁]
  [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L]
  [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B]
  [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁]
  [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [Module.IsTorsionFree R₁ B]
  [Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- Eta-expanded form of `iteratedDeriv_id` -/
iteratedDeriv_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜},
  iteratedDeriv n (fun x => x) x = if n = 0 then x else if n = 1 then 1 else 0
-- Init.Data.Nat.Lemmas
Nat.lt_mul_of_div_lt : ∀ {a c b : ℕ}, a / c < b → 0 < c → a < b * c
-- Mathlib.Tactic.Order
/-- Adds edges to the `≤`-graph using two types of facts:
1. Each fact `¬ (x < y)` allows to add the edge `(x, y)` when `y` is reachable from `x` in the
   graph.
2. Each fact `x ⊔ y = z` allows to add the edge `(z, s)` when `s` is reachable from both `x`
   and `y`.

We repeat the process until no more edges can be added.  -/
Mathlib.Tactic.Order.updateGraphWithNltInfSup : Mathlib.Tactic.Order.Graph → Array Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.AtomM Mathlib.Tactic.Order.Graph
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.group_smul_toList : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G)
  (w : HNNExtension.NormalWord d), (g • w).toList = w.toList
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_pi : ∀ (x : ℝ), Real.sin (x + Real.pi) = -Real.sin x
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_of_tendsto_measure_compl_closedBall : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : PseudoMetricSpace E]
  [ProperSpace E] {x : E},
  Filter.Tendsto (fun r => ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) Filter.atTop (nhds 0) →
    MeasureTheory.IsTightMeasureSet S
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- `ofMatrix` bundled as a star algebra equivalence.  -/
CStarMatrix.ofMatrixStarAlgEquiv : {n : Type u_2} →
  {A : Type u_5} →
    [inst : Fintype n] →
      [inst_1 : SMul ℂ A] → [inst_2 : Semiring A] → [inst_3 : StarRing A] → Matrix n n A ≃⋆ₐ[ℂ] CStarMatrix n n A
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_3} C₁₂]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  [inst_6 : F₁₂.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₁₂ : Type u_10} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (c₁₂ : ComplexShape ι₁₂) [inst_8 : TotalComplexShape c₁ c₂ c₁₂]
  [K₁.HasMapBifunctor K₂ F₁₂ c₁₂],
  (((CategoryTheory.GradedObject.mapBifunctor F₁₂ ι₁ ι₂).obj K₁.X).obj K₂.X).HasMap (c₁.π c₂ c₁₂)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (toMulEquiv : E ≃* E')
  (inl_comm : ⇑toMulEquiv ∘ ⇑S.inl = ⇑S'.inl) (rightHom_comm : ⇑S'.rightHom ∘ ⇑toMulEquiv = ⇑S.rightHom)
  (toMulEquiv_1 : E ≃* E') (inl_comm_1 : ⇑toMulEquiv_1 ∘ ⇑S.inl = ⇑S'.inl)
  (rightHom_comm_1 : ⇑S'.rightHom ∘ ⇑toMulEquiv_1 = ⇑S.rightHom),
  ({ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
      { toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 }) =
    (toMulEquiv = toMulEquiv_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mkIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (e : M.X ≅ N.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Mon.mkIso e one_f mul_f = CategoryTheory.Mon.mkIso' e