mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.div_ae_eq_one : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : Group β] (f g : α → β),
  f / g =ᵐ[μ] 1 ↔ f =ᵐ[μ] g
-- Mathlib.Analysis.BoundedVariation
eVariationOn_bilinear_comp_le : ∀ {α : Type u_2} [inst : LinearOrder α] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedAddCommGroup G]
  [inst_6 : NormedSpace ℝ G] {s : Set α} {f : α → E} {g : α → F} {C D : ENNReal},
  (∀ x ∈ s, ‖f x‖ₑ ≤ C) →
    (∀ x ∈ s, ‖g x‖ₑ ≤ D) →
      ∀ (B : E →L[ℝ] F →L[ℝ] G),
        eVariationOn (fun x => (B (f x)) (g x)) s ≤ ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_empty_notMem_affineSpan_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)},
  i ≠ j → s.touchpoint ∅ i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points)
-- Mathlib.FieldTheory.AbelRuffini
gal_X_pow_isSolvable : ∀ {F : Type u_1} [inst : Field F] (n : ℕ), Group.IsSolvable (Polynomial.X ^ n).Gal
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_inverse_obj_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).hom =
    CategoryTheory.CategoryStruct.comp (i.hom.app X.left) X.hom
-- Mathlib.Algebra.BigOperators.Fin
/-- A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f (Fin.last n)` plus the remaining sum  -/
Fin.sum_univ_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M), ∑ i, f i = ∑ i, f i.castSucc + f (Fin.last n)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s : Set E} {x v : E}, IsOpen s → x ∈ s → lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Strong normalized GCD monoid: a `NormalizedGCDMonoid` whose `normalize` function is a
monoid homomorphism.  -/
StrongNormalizedGCDMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Type u_2
-- Std.Sat.AIG.LawfulOperator
_private.Std.Sat.AIG.LawfulOperator.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_3 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs_1 rhs_1 : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.gate lhs_1 rhs_1 → motive (Std.Sat.AIG.Decl.gate lhs_1 rhs_1)),
  (match elem : Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs_1 rhs_1 => h_3 lhs_1 rhs_1 elem) =
    h_3 lhs rhs ⋯
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ {i j : ι}, i ≤ j → MeasurableSet {ω | τ ω = ↑i}
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.input.sizeOf_spec : sizeOf Lean.Meta.Grind.SplitSource.input = 1
-- Lean.Meta.CongrTheorems
/-- `fvarId` is an equality for "type casting."  -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.hyp : Lean.FVarId → Lean.Meta.EqInfo✝
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult.mk.inj : ∀ {us : List Lean.Level} {args : Array Lean.Expr} {unresolvedInsts : Array Lean.MVarId} {us_1 : List Lean.Level}
  {args_1 : Array Lean.Expr} {unresolvedInsts_1 : Array Lean.MVarId},
  { us := us, args := args, unresolvedInsts := unresolvedInsts } =
      { us := us_1, args := args_1, unresolvedInsts := unresolvedInsts_1 } →
    us = us_1 ∧ args = args_1 ∧ unresolvedInsts = unresolvedInsts_1
-- Mathlib.Data.Complex.Basic
Complex.ofReal_intCast : ∀ (n : ℤ), ↑↑n = ↑n
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- Constructor for `Derivation.Universal` in the case `F` is the identity functor.  -/
PresheafOfModules.Derivation'.Universal.mk : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
        {φ' : S' ⟶ R} →
          {d : M.Derivation' φ'} →
            (desc :
                {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                  M'.Derivation' φ' → (M ⟶ M')) →
              (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
                  (d' : M'.Derivation' φ'), PresheafOfModules.Derivation.postcomp d (desc d') = d') →
                (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (α β : M ⟶ M'),
                    PresheafOfModules.Derivation.postcomp d α = PresheafOfModules.Derivation.postcomp d β → α = β) →
                  PresheafOfModules.Derivation.Universal d
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α}
  (h₁ : (List.map Sigma.fst l).contains k = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(t.insertMany! l) = true},
  (↑(t.insertMany! l)).getKey k h' = t.getKey k ⋯
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.meromorphicOn_sphere_comp_sub_const_iff_meromorphicOn_sphere`

---

`MeromorphicOn` is invariant under translation, special case where the set is a sphere.  -/
MeromorphicOn.meromorphicOn_sphere_fun_comp_sub_const_iff_meromorphicOn_sphere : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (fun x => f (x - c)) (Metric.sphere c R) ↔ MeromorphicOn f (Metric.sphere 0 R)
-- Init.Data.Nat.Gcd
Nat.gcd_comm : ∀ (m n : ℕ), m.gcd n = n.gcd m
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  (φ :
    CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶
      CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D)),
  CategoryTheory.Nerve.nerveFunctor₂.map (CategoryTheory.nerve.functorOfNerveMap φ).toCatHom = φ
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.ne_one : ∀ {α : Type u_2} {f : Equiv.Perm α}, f.IsCycle → f ≠ 1
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.mk : Lean.BinderInfo → Bool → Array ℕ → Bool → Bool → Bool → Bool → Bool → Lean.Meta.ParamInfo
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The 0th homotopy "group" is in bijection with `ZerothHomotopy`.  -/
HomotopyGroup.pi0EquivZerothHomotopy : {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → HomotopyGroup.Pi 0 X x ≃ ZerothHomotopy X
-- Mathlib.Data.Set.Lattice
Set.compl_iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α), (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.hcomp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H I : CategoryTheory.Functor D E} (α : F ≅ G) (β : H ≅ I), (CategoryTheory.NatIso.hcomp α β).hom = α.hom ◫ β.hom
-- Mathlib.Order.Hom.CompleteLattice
Equiv.toOrderIsoSet_symm_apply : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) (s : Set β), (RelIso.symm e.toOrderIsoSet) s = ⇑e.symm '' s
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommRing : {R : Type u_1} →
  [inst : TopologicalSpace R] → [inst_1 : CommRing R] → [IsTopologicalRing R] → CommRing (SeparationQuotient R)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_const : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddZeroClass G]
  [inst_2 : Add H] [AddConstMapClass F G H a b] (f : F), f a = f 0 + b
-- Aesop.Tree.Data
Aesop.TreeSpec.mk.injEq : ∀ (Goal Rapp MVarCluster : Type) (introGoal : Aesop.GoalData Rapp MVarCluster → Goal)
  (elimGoal : Goal → Aesop.GoalData Rapp MVarCluster) (introRapp : Aesop.RappData Goal MVarCluster → Rapp)
  (elimRapp : Rapp → Aesop.RappData Goal MVarCluster) (introMVarCluster : Aesop.MVarClusterData Goal Rapp → MVarCluster)
  (elimMVarCluster : MVarCluster → Aesop.MVarClusterData Goal Rapp) (Goal_1 Rapp_1 MVarCluster_1 : Type)
  (introGoal_1 : Aesop.GoalData Rapp_1 MVarCluster_1 → Goal_1)
  (elimGoal_1 : Goal_1 → Aesop.GoalData Rapp_1 MVarCluster_1)
  (introRapp_1 : Aesop.RappData Goal_1 MVarCluster_1 → Rapp_1)
  (elimRapp_1 : Rapp_1 → Aesop.RappData Goal_1 MVarCluster_1)
  (introMVarCluster_1 : Aesop.MVarClusterData Goal_1 Rapp_1 → MVarCluster_1)
  (elimMVarCluster_1 : MVarCluster_1 → Aesop.MVarClusterData Goal_1 Rapp_1),
  ({ Goal := Goal, Rapp := Rapp, MVarCluster := MVarCluster, introGoal := introGoal, elimGoal := elimGoal,
        introRapp := introRapp, elimRapp := elimRapp, introMVarCluster := introMVarCluster,
        elimMVarCluster := elimMVarCluster } =
      { Goal := Goal_1, Rapp := Rapp_1, MVarCluster := MVarCluster_1, introGoal := introGoal_1, elimGoal := elimGoal_1,
        introRapp := introRapp_1, elimRapp := elimRapp_1, introMVarCluster := introMVarCluster_1,
        elimMVarCluster := elimMVarCluster_1 }) =
    (Goal = Goal_1 ∧
      Rapp = Rapp_1 ∧
        MVarCluster = MVarCluster_1 ∧
          introGoal ≍ introGoal_1 ∧
            elimGoal ≍ elimGoal_1 ∧
              introRapp ≍ introRapp_1 ∧
                elimRapp ≍ elimRapp_1 ∧ introMVarCluster ≍ introMVarCluster_1 ∧ elimMVarCluster ≍ elimMVarCluster_1)
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.addRight.congr_simp : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c c_1 : G),
  c = c_1 → IsometryEquiv.addRight c = IsometryEquiv.addRight c_1
-- Mathlib.Data.List.Sort
/-- The list obtained from an antitone tuple is sorted.  -/
List.SortedGE.antitone : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedGE → Antitone f
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.irreducible_pow_sup_of_le`. -/
irreducible_pow_sup_of_le : ∀ {T : Type u_4} [inst : CommRing T] [IsDedekindDomain T] {I J : Ideal T},
  Irreducible J → ∀ (n : ℕ), ↑n ≤ emultiplicity J I → J ^ n ⊔ I = J ^ n
-- Lean.Data.Lsp.CodeActions
/-- An array of diagnostics known on the client side overlapping the range
provided to the `textDocument/codeAction` request. They are provided so
that the server knows which errors are currently presented to the user
for the given range. There is no guarantee that these accurately reflect
the error state of the resource. The primary parameter
to compute code actions is the provided range.
 -/
Lean.Lsp.CodeActionContext.diagnostics : Lean.Lsp.CodeActionContext → Array Lean.Lsp.Diagnostic
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.neg_eq_self_iff : ∀ {θ : Real.Angle}, -θ = θ ↔ θ = 0 ∨ θ = ↑Real.pi
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instInhabited : {A : Type u_1} → [inst : Monoid A] → [inst_1 : TopologicalSpace A] → Inhabited (PontryaginDual A)
-- Mathlib.Data.Complex.Basic
Complex.mk_eq_add_mul_I : ∀ (a b : ℝ), { re := a, im := b } = ↑a + ↑b * Complex.I
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mk_as : ∀ {C : Type u} (a : CategoryTheory.LocallyDiscrete C), { as := a.as } = a
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMax.eq_3 : ∀ {α : Type u_1} (size : ℕ) (l : Ordnode α) (x_1 : α) (sz : ℕ) (l' : Ordnode α) (y : α) (r' : Ordnode α),
  (Ordnode.node size l x_1 (Ordnode.node sz l' y r')).eraseMax = l.balanceL x_1 (Ordnode.node sz l' y r').eraseMax
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.realSpace K},
  x ≠ 0 →
    x ∈ NumberField.mixedEmbedding.fundamentalCone.compactSet K →
      x ∈
        ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis ''
          closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.filterMap_equiv_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a},
  t.WF → (Std.DTreeMap.Raw.filterMap (fun k v => some (f k v)) t).Equiv (Std.DTreeMap.Raw.map f t)
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.throwNotCommRing : {α : Type} → Lean.Meta.Grind.Arith.Linear.LinearM α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sieve₀_eq_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F),
  E.sieve₀ = F.sieve₀
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffOn.rpow_const_of_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {p : ℝ} {m : ℕ},
  ContDiffOn ℝ (↑m) f s → ↑m ≤ p → ContDiffOn ℝ (↑m) (fun x => f x ^ p) s
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.guardMinColumn : (min : ℕ) → optParam String (toString "expected column at least " ++ toString min) → Lean.Parser.ParserFn
-- Mathlib.Order.Fin.Basic
/-- A function `f` on `Fin (n + 1)` is strictly antitone if and only if `f (i + 1) < f i`
for all `i`.  -/
Fin.strictAnti_iff_succ_lt : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  StrictAnti f ↔ ∀ (i : Fin n), f i.succ < f i.castSucc
-- Mathlib.Tactic.ITauto
/-- The context during proof search is a map from propositions to proof values.  -/
Mathlib.Tactic.ITauto.Context : Type
-- Lean.Data.NameMap.Basic
Lean.NameSet.instSDiff : SDiff Lean.NameSet
-- Lean.Elab.DeprecatedArg
_private.Lean.Elab.DeprecatedArg.0.Lean.Elab.addDeprecatedArgEntry : Lean.Elab.DeprecatedArgState → Lean.Elab.DeprecatedArgEntry → Lean.Elab.DeprecatedArgState
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.mem_span_iff_linearCombination : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M)
  (x : M), x ∈ Submodule.span R s ↔ ∃ l, (Finsupp.linearCombination R Subtype.val) l = x
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.size.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        ((sz : ℕ) →
            (k : α) →
              (v : β k) →
                (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r)) →
          (Unit → motive Std.DTreeMap.Internal.Impl.leaf) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_symm : ∀ {V : Type u} (G : SimpleGraph V) {u v : V}, G.Adj u v → G.Adj v u
-- Lean.Meta.AppBuilder
/-- Returns `@of_eq_false p h`  -/
Lean.Meta.mkOfEqFalseCore : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The constant map is alternating when `ι` is empty.  -/
AlternatingMap.constOfIsEmpty : (R : Type u_1) →
  [inst : Semiring R] →
    (M : Type u_2) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → (ι : Type u_7) → [IsEmpty ι] → N → M [⋀^ι]→ₗ[R] N
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `1` is `1`.  -/
padicNorm.one : ∀ {p : ℕ}, padicNorm p 1 = 1
-- Init.Data.List.Lemmas
List.getElem_replace : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [inst_1 : LawfulBEq α] {l : List α} {i : ℕ} (h : i < l.length),
  (l.replace a b)[i] = if (l[i] == a) = true then if a ∈ List.take i l then a else b else l[i]
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- If a function is linearly approximated by a continuous linear map with a (possibly nonlinear)
right inverse, then it is locally onto: a ball of an explicit radius is included in the image
of the map.  -/
ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse : ∀ {𝕜 : 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] {f : E → F}
  [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F},
  ApproximatesLinearOn f f' s c →
    ∀ (f'symm : f'.NonlinearRightInverse) {ε : ℝ} {b : E},
      0 ≤ ε →
        Metric.closedBall b ε ⊆ s →
          Set.SurjOn f (Metric.closedBall b ε) (Metric.closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sumInr_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (x : F.I₀), (E.sumInr F).h₀ x = CategoryTheory.CategoryStruct.id (F.X x)
-- Mathlib.Data.Nat.GCD.Prime
Nat.Prime.dvd_lcm : ∀ {p a b : ℕ}, Nat.Prime p → (p ∣ a.lcm b ↔ p ∣ a ∨ p ∣ b)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.mk : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {W : CategoryTheory.MorphismProperty C} {X : C},
  W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X) → F.HasPointwiseRightDerivedFunctorAt W X
-- Init.Data.Nat.Lemmas
Nat.pred_sub : ∀ (n m : ℕ), n.pred - m = (n - m).pred
-- Lean.Parser.Attr
Lean.Parser.Attr.default_instance : Lean.Parser.Parser
-- Mathlib.Analysis.Oscillation
/-- If `oscillation f x < ε` at every `x` in a compact set `K`, then there exists `δ > 0` such
that the oscillation of `f` on `ball x δ` is less than `ε` for every `x` in `K`.  -/
IsCompact.uniform_oscillation : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : PseudoEMetricSpace E] {K : Set E},
  IsCompact K →
    ∀ {f : E → F} {ε : ENNReal},
      (∀ x ∈ K, oscillation f x < ε) → ∃ δ > 0, ∀ x ∈ K, Metric.ediam (f '' Metric.eball x (ENNReal.ofReal δ)) ≤ ε
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_toEquiv_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), ⇑(↑f).symm = ⇑f.symm
-- Std.Time.DateTime
/-- Creates a new `DateTime` out of a `Timestamp` and a `TimeZone`.
 -/
Std.Time.DateTime.ofTimestampWithZone : Std.Time.Timestamp → Std.Time.TimeZone → Std.Time.DateTime
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `N` is a normal subgroup of `G` and `IsGaloisGroup N B C`, then `G` acts on `B`.
For `g : G` and `x : B`, `g • x` is the unique element of `B` whose image in `C` is
`g • algebraMap B C x`, see `algebraMap_smulOfNormal`.  -/
IsGaloisGroup.smulOfNormal : (G : Type u_1) →
  [inst : Group G] →
    (B : Type u_3) →
      (C : Type u_4) →
        [inst_1 : Semiring C] →
          [inst_2 : MulSemiringAction G C] →
            (N : Subgroup G) →
              [inst_3 : CommSemiring B] → [inst_4 : Algebra B C] → [N.Normal] → [IsGaloisGroup (↥N) B C] → SMul G B
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c = Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c_1) = (c = c_1)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_preimage_re : ∀ (s : Set ℝ), frontier (Complex.re ⁻¹' s) = Complex.re ⁻¹' frontier s
-- Mathlib.Geometry.Euclidean.Projection
/-- The characteristic property of the orthogonal projection, for a point given in the relevant
subspace. This form is typically more convenient to use than
`inter_eq_singleton_orthogonalProjection`.  -/
EuclideanGeometry.orthogonalProjection_eq_iff_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P} {q : ↥s},
  (EuclideanGeometry.orthogonalProjection s) p = q ↔ p -ᵥ ↑q ∈ s.directionᗮ
-- Mathlib.Order.Category.BddOrd
BddOrd.comp_apply : ∀ {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toPartOrd),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.Language.Basic
/-- The immediately available element of the snapshot tree node.  -/
Lean.Language.SnapshotTree.element : Lean.Language.SnapshotTree → Lean.Language.Snapshot
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_smul_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (s : S)
  (f : AdicCompletion I M) (n : ℕ), ↑(s • f) n = s • ↑f n
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.CategoryStruct.comp S.abelianImageToKernel
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) =
    0
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.mk.injEq : ∀ (ref : Lean.Syntax) (hasExpose : Bool) (cls : Lean.Term) (ref_1 : Lean.Syntax) (hasExpose_1 : Bool)
  (cls_1 : Lean.Term),
  ({ ref := ref, hasExpose := hasExpose, cls := cls } = { ref := ref_1, hasExpose := hasExpose_1, cls := cls_1 }) =
    (ref = ref_1 ∧ hasExpose = hasExpose_1 ∧ cls = cls_1)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.mk.injEq : ∀ (f : Std.Format) (indent : ℤ) (activeTags : ℕ) (f_1 : Std.Format) (indent_1 : ℤ) (activeTags_1 : ℕ),
  ({ f := f, indent := indent, activeTags := activeTags } =
      { f := f_1, indent := indent_1, activeTags := activeTags_1 }) =
    (f = f_1 ∧ indent = indent_1 ∧ activeTags = activeTags_1)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.sum_ite_eq_ite_exists : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] (p : ι → Prop) [inst_2 : DecidablePred p],
  (∀ (i j : ι), p i → p j → i = j) → ∀ (a : M), (∑ i, if p i then a else 0) = if ∃ i, p i then a else 0
-- Mathlib.Order.BoundedOrder.Basic
le_bot_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≤ ⊥ ↔ a = ⊥