mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.cons.inj : ∀ {a b a_1 b_1 : Mathlib.Deriving.Encodable.S✝},
  Mathlib.Deriving.Encodable.S.cons✝ a b = Mathlib.Deriving.Encodable.S.cons✝ a_1 b_1 → a = a_1 ∧ b = b_1
-- Lean.Meta.DiscrTree.Main
/-- TODO: add hook for users adding their own functions for controlling `shouldAddAsStar`
Different `DiscrTree` users may populate this set using, for example, attributes.

Remark: we currently tag "offset" terms as star to avoid having to add special
support for offset terms.
Example, suppose the discrimination tree contains the entry
`Nat.succ ?m |-> v`, and we are trying to retrieve the matches for `Expr.lit (Literal.natVal 1) _`.
In this scenario, we want to retrieve `Nat.succ ?m |-> v`
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.shouldAddAsStar : Lean.Name → Lean.Expr → Lean.MetaM Bool
-- Lean.Util.Trace
Lean.crossEmoji : String
-- Mathlib.Topology.Basic
/-- If `g` tends to some `𝓝 x` along `f`, then it tends to `𝓝 (Filter.limUnder f g)`. We formulate
this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for types
without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify this
instance with any other instance.  -/
tendsto_nhds_limUnder : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {f : Filter α} {g : α → X}
  (h : ∃ x, Filter.Tendsto g f (nhds x)), Filter.Tendsto g f (nhds (f.limUnder g))
-- Mathlib.Algebra.Category.FGModuleCat.Limits
/-- Finite limits of finite-dimensional vector spaces are finite dimensional,
because we can realise them as subobjects of a finite product.  -/
FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG : ∀ {J : Type} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [inst_2 : Ring k]
  [IsNoetherianRing k] (F : CategoryTheory.Functor J (FGModuleCat k)),
  Module.Finite k ↑(CategoryTheory.Limits.limit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos : Lean.PrettyPrinter.Delaborator.DelabM Lean.Options
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.val_mem_ofUnits_iff_mem : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gˣ) (x : Gˣ), ↑x ∈ H.ofUnits ↔ x ∈ H
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.le_add_tsub_swap : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  AddLECancellable b → a ≤ b + a - b
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_zero : Nat.minFac 0 = 2
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_atTop_iff_eventually_exists : ∀ {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {α : Type u_17} [inst_2 : SemilatticeSup α]
  [Nonempty α] {f : α → E} {g : α → F},
  f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_span_mul_finite_of_mem_span_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Mul A] [inst_3 : Module R A]
  {S S' : Set A} {x : A}, x ∈ Submodule.span R (S * S') → ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ Submodule.span R (↑T * ↑T')
-- Lean.Util.Recognizers
Lean.Expr.isIte : Lean.Expr → Bool
-- Lean.DocString.Types
Lean.Doc.Inline.bold.inj : ∀ {i : Type u} {content content_1 : Array (Lean.Doc.Inline i)},
  Lean.Doc.Inline.bold content = Lean.Doc.Inline.bold content_1 → content = content_1
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonAssocCommRingWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [NonAssocCommRing α] → NonAssocCommRing (WithConv (Matrix m n α))
-- Init.Data.Repr
instReprProdOfReprTuple : {α : Type u_1} → {β : Type u_2} → [Repr α] → [ReprTuple β] → Repr (α × β)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- A ring isomorphism `R ≃+* R'` induces an isomorphism on their class groups.  -/
ClassGroup.mulEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      {R' : Type u_3} → [inst_2 : CommRing R'] → [inst_3 : IsDomain R'] → R ≃+* R' → ClassGroup R ≃* ClassGroup R'
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A standard Borel space is a measurable space arising as the Borel sets of some Polish topology.
This is useful in situations where a space has no natural topology or
the natural topology in a space is non-Polish.

To endow a standard Borel space `α` with a compatible Polish topology, use
`letI := upgradeStandardBorel α`. One can then use `eq_borel_upgradeStandardBorel α` to
rewrite the `MeasurableSpace α` instance to `borel α t`, where `t` is the new topology.  -/
StandardBorelSpace : (α : Type u_1) → [MeasurableSpace α] → Prop
-- Mathlib.Algebra.Notation.Defs
/-- `a -ᵥ b` computes the difference of `a` and `b`. The meaning of this notation is
type-dependent, but it is intended to be used for additive torsors. 

Conventions for notations in identifiers:

 * The recommended spelling of `-ᵥ` in identifiers is `vsub`. -/
«term_-ᵥ_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryD_eq_getEntryDₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a),
  l.getEntryD k fallback = Std.DTreeMap.Internal.Impl.getEntryDₘ k l fallback
-- Mathlib.Order.Concept
Order.IsExtent.inter : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s s' : Set α},
  Order.IsExtent r s → Order.IsExtent r s' → Order.IsExtent r (s ∩ s')
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ofArchimedean_injective : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {R : Type u_2}
  [inst_3 : LinearOrder R] [inst_4 : CommRing R] [inst_5 : IsStrictOrderedRing R] [inst_6 : Archimedean R]
  (f : R →+*o K), Function.Injective ⇑(ArchimedeanClass.FiniteResidueField.ofArchimedean f)
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.Algebra.Algebra.Hom
AlgHom.map_smul_of_tower : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) {R' : Type u_1} [inst_5 : SMul R' A]
  [inst_6 : SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A), φ (r • x) = r • φ x
-- Mathlib.Probability.Process.Predictable
/-- A discrete process `u` is predictable iff `u (n + 1)` is `𝓕 n`-measurable for all `n` and
`u 0` is `𝓕 0`-measurable.  -/
MeasureTheory.IsStronglyPredictable.iff_measurable_add_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E},
  MeasureTheory.IsStronglyPredictable 𝓕 u ↔
    MeasureTheory.StronglyMeasurable (u 0) ∧ ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.sum : ∀ {𝕜 : 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]
  {L : Filter (E × E)} {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L) → HasFDerivAtFilter (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.irreducibleSpace : ∀ {R : Type u} [inst : CommSemiring R] [IsDomain R], IrreducibleSpace (PrimeSpectrum R)
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.Equiv.trans : ∀ {self : Batteries.UnionFind} {a b c : ℕ}, self.Equiv a b → self.Equiv b c → self.Equiv a c
-- Mathlib.Data.List.Sigma
List.notMem_keys_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)},
  l.NodupKeys → a ∉ (List.kerase a l).keys
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_symm_X : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (c : S₁),
  (MvPolynomial.sumAlgEquiv R S₁ S₂).symm (MvPolynomial.X c) = MvPolynomial.X (Sum.inl c)
-- Mathlib.GroupTheory.Sylow
/-- A `p`-subgroup with index indivisible by `p` is a Sylow subgroup.  -/
IsPGroup.toSylow : {p : ℕ} →
  {G : Type u_1} → [inst : Group G] → [Fact (Nat.Prime p)] → {P : Subgroup G} → IsPGroup p ↥P → ¬p ∣ P.index → Sylow p G
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_toArray_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} {v : β}, (k, v) ∈ t.toArray ↔ t[k]? = some v
-- Mathlib.Data.Set.Card
Set.one_lt_ncard_iff : ∀ {α : Type u_1} {s : Set α},
  autoParam s.Finite Set.one_lt_ncard_iff._auto_1 → (1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b)
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instTypeNameSemanticTokensState : TypeName Lean.Server.FileWorker.SemanticTokensState
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C]
  {F G : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts F]
  [CategoryTheory.Limits.PreservesFiniteProducts G],
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f →
    ∀ {X : C}, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X)))
-- Mathlib.Analysis.Calculus.FDeriv.Pow
hasFDerivWithinAt_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ) {x : 𝔸} {s : Set 𝔸},
  HasFDerivWithinAt (fun x => x ^ n)
    (∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸) s x
-- Mathlib.NumberTheory.Divisors
Nat.one_mem_divisors : ∀ {n : ℕ}, 1 ∈ n.divisors ↔ n ≠ 0
-- Mathlib.Data.Num.Bitwise
instInhabitedNzsNum : Inhabited NzsNum
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.mk : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {m' : MeasurableSpace Ω'} {mE : MeasurableSpace E} [inst : TopologicalSpace E] [inst_1 : OpensMeasurableSpace E]
  {X : (i : ι) → Ω i → E} {l : Filter ι} {Z : Ω' → E} {μ : (i : ι) → MeasureTheory.Measure (Ω i)}
  [inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {μ' : autoParam (MeasureTheory.Measure Ω') MeasureTheory.TendstoInDistribution._auto_1}
  [inst_3 : MeasureTheory.IsProbabilityMeasure μ'] (forall_aemeasurable : ∀ (i : ι), AEMeasurable (X i) (μ i))
  (aemeasurable_limit :
    autoParam (AEMeasurable Z μ') MeasureTheory.TendstoInDistribution.aemeasurable_limit._autoParam),
  Filter.Tendsto (fun n => ⟨MeasureTheory.Measure.map (X n) (μ n), ⋯⟩) l (nhds ⟨MeasureTheory.Measure.map Z μ', ⋯⟩) →
    MeasureTheory.TendstoInDistribution X l Z μ μ'
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, (p.next h).prev ⋯ = p
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_inf_principal_iff : ∀ {α : Type u} {β : Type v} {F : Filter α} {s : Set α} {f g : α → β},
  f =ᶠ[F ⊓ Filter.principal s] g ↔ ∀ᶠ (x : α) in F, x ∈ s → f x = g x
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- If a pair of measures `HaveLebesgueDecomposition`, then `rnDeriv` chooses the
measurable function from `HaveLebesgueDecomposition`, otherwise it returns the zero function.
For sigma-finite measures, `μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)`.  -/
MeasureTheory.Measure.rnDeriv : {α : Type u_2} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → α → ENNReal
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE USize
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMultispan.functorExt.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MultispanShape} (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) (i : J.R)
  (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right i)),
  (match CategoryTheory.Limits.WalkingMultispan.right i with
    | CategoryTheory.Limits.WalkingMultispan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMultispan.right i => h_2 i) =
    h_2 i
-- Mathlib.Data.Rat.Init
/-- The numerator of a nonnegative rational.  -/
NNRat.num : ℚ≥0 → ℕ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyGT! k = t₂.getKeyGT! k
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (a : α), a • ∅ = ∅
-- Std.Data.DHashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `fallback`.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.Raw.getEntryD : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → α → (a : α) × β a → (a : α) × β a
-- Lean.DocString.Parser
/-- Parses as `p`, but discards the result.
 -/
Lean.Doc.Parser.ignoreFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.denote.match_1.eq_1 : ∀ (motive : Nat.Internal.Linear.Poly → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (k : ℕ) → (v : Nat.Internal.Linear.Var) → (p : List (ℕ × Nat.Internal.Linear.Var)) → motive ((k, v) :: p)),
  (match [] with
    | [] => h_1 ()
    | (k, v) :: p => h_2 k v p) =
    h_1 ()
-- Init.Data.List.Basic
List.map.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : List α),
  List.map f x =
    match x with
    | [] => []
    | a :: as => f a :: List.map f as
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.mk.inj : ∀ {w : ℕ} {lhs rhs : Std.Tactic.BVDecide.BVExpr w} {w_1 : ℕ} {lhs_1 rhs_1 : Std.Tactic.BVDecide.BVExpr w_1},
  { w := w, lhs := lhs, rhs := rhs } = { w := w_1, lhs := lhs_1, rhs := rhs_1 } → w = w_1 ∧ lhs ≍ lhs_1 ∧ rhs ≍ rhs_1
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic) (based condition)  -/
MulAction.IsPreprimitive.of_isTrivialBlock_of_notMem_fixedPoints : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {a : X},
  a ∉ MulAction.fixedPoints G X →
    (∀ ⦃B : Set X⦄, a ∈ B → MulAction.IsBlock G B → MulAction.IsTrivialBlock B) → MulAction.IsPreprimitive G X
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixState.mk.injEq : ∀ (goals goals_1 : Array Lean.MVarId), ({ goals := goals } = { goals := goals_1 }) = (goals = goals_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mapRelations.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η η_1 : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)), η = η_1 → P.mapRelations F η = P.mapRelations F η_1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.insphere_center : ∀ {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), s.insphere.center = s.incenter
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle**. Let `f : E → F` be a function between complex normed spaces.
Suppose that the codomain `F` is a strictly convex space, `f` is complex differentiable on a set
`s`, `f` is continuous on the closure of `s`, the norm of `f` takes it maximum on `s` at `z`, and
`w` is a point such that the closed ball with center `z` and radius `dist w z` is included in `s`,
then `f w = f z`.  -/
Complex.eq_of_isMaxOn_of_ball_subset : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {s : Set E} {z w : E},
  DiffContOnCl ℂ f s → IsMaxOn (norm ∘ f) s z → Metric.ball z (dist w z) ⊆ s → f w = f z
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- If a topological space admits an atlas with locally connected charts, then the space itself is
locally connected.  -/
ChartedSpace.locallyConnectedSpace : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [LocallyConnectedSpace H], LocallyConnectedSpace M
-- Init.Data.Array.MapIdx
Array.getElem_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α} {i : ℕ} (h : i < (Array.mapIdx f xs).size),
  (Array.mapIdx f xs)[i] = f i xs[i]
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀.eq_1 : ∀ {α : Type u_1} [inst : Zero α] (a : WithTop α), a.untop₀ = WithTop.untopD 0 a
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.homQuotientZPowOfHom_id : ∀ {A : Type u} [inst : CommGroup A] (n : ℤ),
  QuotientGroup.homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id (A ⧸ (zpowGroupHom n).range)
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` respects isomorphism, so does `Locally P`.  -/
RingHom.locally_respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.withBRecOnArgs.go.go2.eq_def : ∀ (ctx : Lean.Meta.IndPredBelow.Context✝) (newMinors : Array Lean.Expr) (belowCtorName : Lean.Name)
  (minorArgs : Array Lean.Expr) (j : ℕ) (vars args : Array Lean.Expr),
  Lean.Meta.IndPredBelow.withBRecOnArgs.go.go2✝ ctx newMinors belowCtorName minorArgs j vars args =
    if h : j < minorArgs.size then do
      let type ← Lean.Meta.inferType minorArgs[j]
      match Lean.Meta.IndPredBelow.isIH✝ type ctx with
        | some i' => do
          let __do_lift ← liftM (Lean.mkFreshUserName `ih)
          Lean.Meta.withLocalDeclD __do_lift (Lean.Meta.IndPredBelow.ihTypeToBelowType✝ type ctx) fun newIH => do
              let proof ←
                Lean.Meta.forallTelescope type fun args body =>
                    have proof := (body.updateFn newMinors[i']!).app (Lean.mkAppN newIH args);
                    Lean.Meta.mkLambdaFVars args proof
              Lean.Meta.IndPredBelow.withBRecOnArgs.go.go2✝ ctx newMinors belowCtorName minorArgs (j + 1)
                  (vars.push newIH) ((args.push newIH).push proof)
        | x =>
          Lean.Meta.IndPredBelow.withBRecOnArgs.go.go2✝ ctx newMinors belowCtorName minorArgs (j + 1)
            (vars.push minorArgs[j]) (args.push minorArgs[j])
    else
      have belowCtor :=
        Lean.Expr.const belowCtorName (List.map Lean.Level.param (Lean.Meta.IndPredBelow.Context.levelParams✝ ctx));
      have proof :=
        Lean.mkAppN
          (Lean.mkAppN (Lean.mkAppN belowCtor (Lean.Meta.IndPredBelow.Context.params✝ ctx))
            (Lean.Meta.IndPredBelow.Context.motives✝ ctx))
          args;
      Lean.Meta.mkLambdaFVars vars proof
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ γ) ≃ᵤ (α →ᵤ β)` by
post-composing.  -/
UniformFun.congrRight : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → [inst : UniformSpace β] → [inst_1 : UniformSpace γ] → γ ≃ᵤ β → UniformFun α γ ≃ᵤ UniformFun α β
-- Mathlib.Data.Finset.Image
Finset.image_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
  (Finset.image f s).Nonempty ↔ s.Nonempty
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.Gamma_inv_mul_ordinaryHypergeometricSeries_eq : ∀ {a b c : ℂ},
  (∀ (k : ℕ), c ≠ -↑k) →
    ∀ {n : ℕ},
      (Complex.Gamma c)⁻¹ * (ordinaryHypergeometricSeries ℂ a b c).coeff n = (a.regularizedGaussHGFunSeries b c).coeff n
-- Mathlib.Analysis.Convolution
/-- The integral over `Ioi 0` of a forward convolution of two functions is equal to the product
of their integrals over this set. (Compare `integral_convolution` for the two-sided convolution.)  -/
MeasureTheory.integral_posConvolution : ∀ {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ E'] [inst_5 : NormedSpace ℝ F]
  [CompleteSpace E] [CompleteSpace E'] [CompleteSpace F] {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasureTheory.NullSingletonClass ν] {f : ℝ → E} {g : ℝ → E'},
  MeasureTheory.IntegrableOn f (Set.Ioi 0) ν →
    MeasureTheory.IntegrableOn g (Set.Ioi 0) μ →
      ∀ (L : E →L[ℝ] E' →L[ℝ] F),
        ∫ (x : ℝ) in Set.Ioi 0, ∫ (t : ℝ) in 0..x, (L (f t)) (g (x - t)) ∂ν ∂μ =
          (L (∫ (x : ℝ) in Set.Ioi 0, f x ∂ν)) (∫ (x : ℝ) in Set.Ioi 0, g x ∂μ)
-- Lean.Compiler.ExternAttr
/-- We say a Lean function marked as `[extern "<c_fn_name>"]` is for all backends, and it is implemented using `extern "C"`.
Thus, there is no name mangling.  -/
Lean.isExternC : Lean.Environment → Lean.Name → Bool
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.restrict_dirac' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  MeasurableSet s →
    ∀ [inst_1 : Decidable (a ∈ s)],
      (MeasureTheory.Measure.dirac a).restrict s = if a ∈ s then MeasureTheory.Measure.dirac a else 0
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_pow_left`. -/
Equiv.Perm.SameCycle.of_pow_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle ((f ^ n) x) y → f.SameCycle x y
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.val_zero : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), ↑0 = 0