mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasStrictFDerivAt.continuousMultilinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] {G : Type u_4} [inst_6 : NormedAddCommGroup G]
  [inst_7 : NormedSpace 𝕜 G] [inst_8 : DecidableEq ι] {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F}
  {g : (i : ι) → G → E i} {f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : (i : ι) → G →L[𝕜] E i},
  HasStrictFDerivAt f f' x →
    (∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x) →
      HasStrictFDerivAt (fun x => (f x) fun x_1 => g x_1 x)
        ((ContinuousMultilinearMap.apply 𝕜 E F fun x_1 => g x_1 x) ∘SL f' +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL g' i)
        x
-- Init.Data.Nat.Log2
_private.Init.Data.Nat.Log2.0.Nat.log2_rec_irrel : ∀ {n k k' : ℕ},
  n ≤ k →
    n ≤ k' →
      Nat.rec (motive := fun x => ℕ → ℕ) (fun x => 0) (fun x ih n => Bool.rec 0 (ih (n / 2)).succ (Nat.ble 2 n)) k n =
        Nat.rec (motive := fun x => ℕ → ℕ) (fun x => 0) (fun x ih n => Bool.rec 0 (ih (n / 2)).succ (Nat.ble 2 n)) k' n
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdCongr_apply : ∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : PseudoEMetricSpace α']
  [inst_3 : PseudoEMetricSpace β'] (f : α ≃ᵢ α') (g : β ≃ᵢ β') (a : WithLp p (α × β)),
  (IsometryEquiv.withLpProdCongr p f g) a = WithLp.toLp p (Prod.map (⇑f) (⇑g) a.ofLp)
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_indicator_apply_of_subset : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s t : Set α} {f : α → M} {a : α},
  s ⊆ t → 0 ≤ f a → s.indicator f a ≤ t.indicator f a
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_fmod_unique : ∀ {a b r q : ℤ}, 0 < b → (a.fdiv b = q ∧ a.fmod b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_toENat : Cardinal.toENat Cardinal.continuum = ⊤
-- Mathlib.Tactic.DuplicateDecls
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.instLTModuleKey : LT Mathlib.Tactic.DuplicateDecls.ModuleKey✝
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.instHashable : Hashable Lean.Meta.LazyDiscrTree.Key
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.eq_normS_nc_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.ext_iff : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  {η η' : ApplicativeTransformation F G},
  η = η' ↔ ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
-- Mathlib.Algebra.Category.BialgCat.Monoidal
/-- `forget₂ (BialgCat R) (AlgCat R)` as a monoidal functor.  -/
BialgCat.instMonoidalAlgCatForget₂BialgHomCarrierAlgHomCarrier : (R : Type u) → [inst : CommRing R] → (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).Monoidal
-- Mathlib.Data.List.Sort
List.sortedLE_iff_getElem_le_getElem_of_le : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedLE ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i ≤ j → l[i] ≤ l[j]
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getGT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getGT! k = t₂.getGT! k
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_le : ∀ (n : ℕ) {k m : ℕ}, k ≤ m → k.descFactorial n ≤ m.descFactorial n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- Equip the "additive circle" `ℝ ⧸ (ℤ ∙ T)` with, as a standard measure, the Haar measure of total
mass `T`  -/
AddCircle.measureSpace : (T : ℝ) → [hT : Fact (0 < T)] → MeasureTheory.MeasureSpace (AddCircle T)
-- Init.SimpLemmas
iff_self_and : ∀ {p q : Prop}, (p ↔ p ∧ q) ↔ p → q
-- Lean.Elab.MutualDef
Lean.Elab.Term.AsyncBodyInfo : Type
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.closure_mul_le : ∀ {M : Type u_3} [inst : Monoid M] (S T : Set M), Submonoid.closure (S * T) ≤ Submonoid.closure S ⊔ Submonoid.closure T
-- Init.SimpLemmas
Bool.false_or : ∀ (b : Bool), (false || b) = b
-- Lean.DocString.Markdown
/-- Concatenates a array of lines, where each line is an array of rendered inlines. The last line of one
piece is glued onto the first line of the next via `glueInlineBoundary` (so `.text "a"` followed by
`.text "b"` yields one line `"ab"`, but two adjacent `.code` spans get a U+200B between them).
 -/
Lean.Doc.joinInlines : Array (Array String) → Array String
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
CFC.log_le_log : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  a ≤ b → autoParam (IsStrictlyPositive a) CFC.log_le_log._auto_1 → CFC.log a ≤ CFC.log b
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey_cons_perm.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((v : β) → motive (some v)) → motive x
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃* G / M`.  -/
QuotientGroup.quotientQuotientEquivQuotient : {G : Type u} →
  [inst : Group G] →
    (N : Subgroup G) →
      [nN : N.Normal] →
        (M : Subgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalBinderInfo_qq : Lean.Meta.ReduceEval Lean.BinderInfo
-- Mathlib.Data.Set.Finite.Basic
/-- Gives a `Set.Finite` for the `Finset` coerced to a `Set`.
This is a wrapper around `Set.toFinite`.  -/
Finset.finite_toSet : ∀ {α : Type u} (s : Finset α), (↑s).Finite
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.MinIndexableMode.yes.sizeOf_spec : sizeOf Lean.Meta.Grind.MinIndexableMode.yes = 1
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyGE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option α
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_sup : ∀ {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Finsubgraph), ↑(G₁ ⊔ G₂) = ↑G₁ ⊔ ↑G₂
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instNonUnitalCommSemiring : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : StarRing A] →
          [inst_3 : Module R A] →
            [inst_4 : IsScalarTower R A A] →
              [inst_5 : SMulCommClass R A A] → NonUnitalCommSemiring ↥(NonUnitalStarSubalgebra.center R A)
-- Mathlib.Algebra.Group.Action.Pi
Pi.vaddAssocClass' : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → VAdd M (α i)]
  [inst_1 : (i : ι) → VAdd (α i) (β i)] [inst_2 : (i : ι) → VAdd M (β i)] [∀ (i : ι), VAddAssocClass M (α i) (β i)],
  VAddAssocClass M ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `Polynomial.map` as a `RingHom`.  -/
Polynomial.mapRingHom : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → Polynomial R →+* Polynomial S
-- Mathlib.Data.Real.Embedding
Archimedean.embedRealFun.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : One M] (x : M),
  Archimedean.embedRealFun x = sSup (Archimedean.ratLt' x)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.mk.inj : ∀ {ι : Type uι} {E : Type uE} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {H : Type uH}
  {inst_2 : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type uM} {inst_3 : TopologicalSpace M}
  {inst_4 : ChartedSpace H M} {s : Set M} {toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤}
  {locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)} {nonneg' : ∀ (i : ι) (x : M), 0 ≤ (toFun i) x}
  {sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1} {sum_le_one' : ∀ (x : M), ∑ᶠ (i : ι), (toFun i) x ≤ 1}
  {toFun_1 : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤}
  {locallyFinite'_1 : LocallyFinite fun i => Function.support ⇑(toFun_1 i)}
  {nonneg'_1 : ∀ (i : ι) (x : M), 0 ≤ (toFun_1 i) x} {sum_eq_one'_1 : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun_1 i) x = 1}
  {sum_le_one'_1 : ∀ (x : M), ∑ᶠ (i : ι), (toFun_1 i) x ≤ 1},
  { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
      { toFun := toFun_1, locallyFinite' := locallyFinite'_1, nonneg' := nonneg'_1, sum_eq_one' := sum_eq_one'_1,
        sum_le_one' := sum_le_one'_1 } →
    toFun = toFun_1
-- Mathlib.Algebra.BigOperators.Pi
Prod.fst_prod : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Finset ι}
  {f : ι → M × N}, (∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1
-- Mathlib.Data.DFinsupp.Defs
/-- `DFinsupp.mapRange` as an `AddMonoidHom`.  -/
DFinsupp.mapRange.addMonoidHom : {ι : Type u} →
  {β₁ : ι → Type v₁} →
    {β₂ : ι → Type v₂} →
      [inst : (i : ι) → AddZeroClass (β₁ i)] →
        [inst_1 : (i : ι) → AddZeroClass (β₂ i)] → ((i : ι) → β₁ i →+ β₂ i) → (Π₀ (i : ι), β₁ i) →+ Π₀ (i : ι), β₂ i
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.aeval_comp_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) {A : Type u_5} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] (f : σ → A), (MvPolynomial.aeval f).comp (MvPolynomial.expand p) = MvPolynomial.aeval (f ^ p)
-- Init.Data.Array.Count
Array.count_flatMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {xs : Array α} {f : α → Array β} {x : β},
  Array.count x (Array.flatMap f xs) = (Array.map (Array.count x ∘ f) xs).sum
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_add_right : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Add β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j + f k) μ
-- Mathlib.Data.Nat.Factorization.Defs
Nat.pow_succ_factorization_not_dvd : ∀ {n p : ℕ}, n ≠ 0 → Nat.Prime p → ¬p ^ (n.factorization p + 1) ∣ n
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.instInhabitedContext : Inhabited Lean.Elab.Term.CollectPatternVars.Context
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instAdd : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddMonoid Y] → Add (Function.locallyFinsuppWithin U Y)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_le_mk : ∀ (α : Type u) [Infinite α], Cardinal.aleph0 ≤ Cardinal.mk α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_of_X_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → W'.addX P Q = 0
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.StrongHomClass.toEquiv_toFun : ∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : EquivLike F M N] [inst_3 : L.StrongHomClass F M N] (a : F) (a_1 : M),
  (FirstOrder.Language.StrongHomClass.toEquiv a) a_1 = a a_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.cons_not_rev : ∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool}, FreeGroup.Red.Step ((x, !b) :: (x, b) :: L) L
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_iff_dvd_of_dvd_add : ∀ {a b c : ℤ}, a ∣ b + c → (a ∣ b ↔ a ∣ c)
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A variant of `Matrix.toLin'_submatrix` that keeps around `LinearEquiv`s.  -/
Matrix.toLin'_reindex : ∀ {R : Type u_1} [inst : CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5}
  [inst_1 : DecidableEq n] [inst_2 : Fintype n] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (e₁ : k ≃ m) (e₂ : l ≃ n)
  (M : Matrix k l R),
  Matrix.toLin' ((Matrix.reindex e₁ e₂) M) =
    ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ Matrix.toLin' M ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolution : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G],
  HasCompactSupport f → HasCompactSupport g → HasCompactSupport (MeasureTheory.convolution f g L μ)
-- Mathlib.Order.Preorder.Chain
IsMaxChain.isChain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxChain r s → IsChain r s
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- For any `n`, we have `log_stirlingSeq 1 - log_stirlingSeq n ≤ 12⁻¹`.  -/
Stirling.log_stirlingSeq_bounded_aux : ∀ (n : ℕ), Real.log (Stirling.stirlingSeq 1) - Real.log (Stirling.stirlingSeq (n + 1)) ≤ 12⁻¹
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.DTreeMap.Raw.Const.alter t k f},
  (Std.DTreeMap.Raw.Const.alter t k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Std.Do.PostCond
Std.Do.instInhabitedPostCond : {ps : Std.Do.PostShape} → {α : Type u} → Inhabited (Std.Do.PostCond α ps)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_pair : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι] {a b : ι},
  a ≠ b → ∑ x ∈ {a, b}, f x = f a + f b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.label : Lean.Lsp.SignatureInformation → String
-- Init.Data.SInt.Basic
instAddInt32 : Add Int32
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.mkDefaultParams : Lean.Grind.Config → Lean.MetaM Lean.Meta.Grind.Params
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.op.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β],
  AddEquiv.op =
    {
      toFun := fun f =>
        { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop,
          left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ },
      invFun := fun f =>
        { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op,
          left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
/-- Base change commutes with finite products.  -/
IsBaseChange.pi : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_3}
  [Finite ι] {M : ι → Type u_4} {M' : ι → Type u_5} [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → AddCommMonoid (M' i)] [inst_6 : (i : ι) → Module R (M i)] [inst_7 : (i : ι) → Module R (M' i)]
  [inst_8 : (i : ι) → Module S (M' i)] [inst_9 : ∀ (i : ι), IsScalarTower R S (M' i)] (f : (i : ι) → M i →ₗ[R] M' i),
  (∀ (i : ι), IsBaseChange S (f i)) → IsBaseChange S (LinearMap.pi fun i => f i ∘ₗ LinearMap.proj i)
-- Mathlib.Data.Nat.Pairing
Set.iInter_unpair : ∀ {α : Type u_1} (f : ℕ → ℕ → Set α), ⋂ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⋂ i, ⋂ j, f i j
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageOneHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : DecidableEq β] [inst_2 : One β]
  [inst_3 : FunLike F α β] [inst_4 : OneHomClass F α β] (f : F) (s : Finset α),
  (Finset.imageOneHom f) s = Finset.image (⇑f) s
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.eq_bot_iff_isIsolated : ∀ {V : Type u} (G : SimpleGraph V), G = ⊥ ↔ ∀ (v : V), G.IsIsolated v
-- Mathlib.Computability.RE
ComputablePred.to_re : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, ComputablePred p → REPred p
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.localization_away_comap_range : ∀ {R : Type u} [inst : CommSemiring R] (S : Type v) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R)
  [IsLocalization.Away r S], Set.range (PrimeSpectrum.comap (algebraMap R S)) = ↑(PrimeSpectrum.basicOpen r)
-- Mathlib.Order.Cofinal
IsCofinal.of_isEmpty : ∀ {α : Type u_1} [inst : LE α] [IsEmpty α] {s : Set α}, IsCofinal s
-- Mathlib.Order.CompleteBooleanAlgebra
/-- **Alias** of `Function.completeDistribLatticeMinimalAxioms`.

---

Pullback a `CompleteDistribLattice.MinimalAxioms` along an injection.  -/
Function.Injective.completeDistribLatticeMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  CompleteDistribLattice.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
        (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
          (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
            (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
              (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → CompleteDistribLattice.MinimalAxioms α
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.toFormula.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.toFormula =
    match x, x_1 with
    | _n, FirstOrder.Language.BoundedFormula.falsum => FirstOrder.Language.BoundedFormula.falsum
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => t₁.equal t₂
    | _n, FirstOrder.Language.BoundedFormula.rel R ts => R.formula ts
    | _n, φ₁.imp φ₂ => FirstOrder.Language.BoundedFormula.imp φ₁.toFormula φ₂.toFormula
    | _n, φ.all =>
      (FirstOrder.Language.BoundedFormula.relabel
          (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) φ.toFormula).all
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.GrothendieckTopology.close_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X) (x : C) (f : x ⟶ X), (J₁.close S).arrows f = J₁.Covers S f
-- Mathlib.RingTheory.AdicCompletion.Functoriality
surjective_of_mk_map_comp_surjective : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {S : Type u_6} [inst_1 : CommRing S] (f : R →+* S)
  [IsPrecomplete I R] [haus : IsHausdorff (Ideal.map f I) S],
  Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map f I)).comp f) → Function.Surjective ⇑f
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The submodule of self-adjoint matrices with respect to the bilinear form corresponding to
the matrix `J`.  -/
selfAdjointMatricesSubmodule : {R : Type u_1} →
  {n : Type u_11} → [inst : CommRing R] → [Fintype n] → Matrix n n R → [DecidableEq n] → Submodule R (Matrix n n R)
-- Mathlib.Data.EReal.Operations
EReal.instNoZeroDivisors : NoZeroDivisors EReal
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.mk_zsmul : ∀ {M : Type u_1} [inst : SubNegMonoid M] (a : M) (n : ℤ), DomAddAct.mk (n • a) = n • DomAddAct.mk a
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.fibrations_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.fibrations Cᵒᵖ = (HomotopicalAlgebra.cofibrations C).op
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_c_eq_zero' : ∀ {R : Type u_1} {d : R} [inst : Semiring R], { a := 0, b := 0, c := 0, d := d }.toPoly.degree ≤ 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp S.homologyπ h.homologyIso.hom =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.π
-- Mathlib.Analysis.Convex.Combination
affineCombination_eq_centerMass : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {ι : Type u_8}
  {t : Finset ι} {p : ι → E} {w : ι → R}, ∑ i ∈ t, w i = 1 → (Finset.affineCombination R t p) w = t.centerMass w p
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.match_21.eq_1 : ∀ (aig : Std.Sat.AIG ℕ) (upper : ℕ) (h : upper < aig.decls.size) (state : Std.Sat.AIG.toCNF.State✝ aig)
  (lhs rhs : Std.Sat.AIG.Fanin) (this : lhs.gate < upper ∧ rhs.gate < upper)
  (motive : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out lhs.gate ⋯ } → Sort u_1)
  (lstate : Std.Sat.AIG.toCNF.State✝ aig) (hlstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state lstate lhs.gate ⋯)
  (h_1 :
    (lstate : Std.Sat.AIG.toCNF.State✝ aig) →
      (hlstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state lstate lhs.gate ⋯) → motive ⟨lstate, hlstate⟩),
  (match ⟨lstate, hlstate⟩ with
    | ⟨lstate, hlstate⟩ => h_1 lstate hlstate) =
    h_1 lstate hlstate
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_sup_generateFrom : ∀ {α : Type u_1} {s t : Set (Set α)},
  MeasurableSpace.generateFrom s ⊔ MeasurableSpace.generateFrom t = MeasurableSpace.generateFrom (s ∪ t)
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.one_def : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X : C}, 1 = CategoryTheory.CategoryStruct.id X
-- Lean.Meta.Constructions.BRecOn
_private.Lean.Meta.Constructions.BRecOn.0.Lean.buildBelowMinorPremise.go : Lean.Level → Array Lean.Expr → Array Lean.Expr → List Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Module.ULift
ULift.addAction.eq_1 : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M],
  ULift.addAction = { toVAdd := ULift.vaddLeft, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mapComp_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.mapComp F G).inv.app X =
    (match X with
      | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj a)))
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Ioi : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b : G₀), (fun x => a * x) '' Set.Ioi b = Set.Ioi (a * b)
-- Mathlib.Data.Finset.BooleanAlgebra
/-- Note this is a special case of `(Finset.image_preimage f univ _).symm`.  -/
Finset.univ_filter_mem_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α → β) [inst_1 : Fintype β]
  [inst_2 : DecidablePred fun y => y ∈ Set.range f] [inst_3 : DecidableEq β],
  {y | y ∈ Set.range f} = Finset.image f Finset.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_empty : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty.isEmpty = true
-- Mathlib.Order.SuccPred.Basic
WithBot.orderSucc_coe : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] (a : α),
  Order.succ ↑a = ↑(Order.succ a)
-- Init.Data.List.Find
List.findSome?_replicate_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  (f a).isSome = true → List.findSome? f (List.replicate n a) = if n = 0 then none else f a