mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_curry_symm : ∀ {ι : Type u_6} {κ : Type u_7} {X : Type u_8} {mX : MeasurableSpace X} (μ : ι → κ → MeasureTheory.Measure X)
  [hμ : ∀ (i : ι) (j : κ), MeasureTheory.IsProbabilityMeasure (μ i j)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.curry ι κ X).symm)
      (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi fun j => μ i j) =
    MeasureTheory.Measure.infinitePi fun p => μ p.1 p.2
-- Lean.Parser.Term.Basic
/-- Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.

Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
 -/
Lean.Parser.Term.strictImplicitBinder : optParam Bool false → Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare (t.maxKeyD fallback) ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKeyD fallback)).isLE =
        true
-- Mathlib.Data.Finset.Lattice.Fold
/-- A version of `Finset.sup'_image` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.  -/
Finset.sup'_comp_eq_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : DecidableEq β] {s : Finset γ}
  {f : γ → β} (hs : s.Nonempty) (g : β → α), s.sup' hs (g ∘ f) = (Finset.image f s).sup' ⋯ g
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_eq_of_source_subset : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X}, e.source ⊆ s → e.restr s = e
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_right_self : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ (x \ y) = x ⊓ y
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTrivAt.eq_1 : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B),
  Z.localTrivAt b = Z.localTriv (Z.indexAt b)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections commute and are nested `P n (P m) = P (min n m)`.  -/
SchauderBasis.RankOneDecomposition.proj_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (self : SchauderBasis.RankOneDecomposition 𝕜 X) (n m : ℕ) (x : X),
  (self.P n) ((self.P m) x) = (self.P (min n m)) x
-- Lean.Elab.Do.ForwardSyntax
Lean.Elab.Do.ForwardArg.mk.inj : ∀ {binders : Array (Lean.TSyntax `Lean.Parser.Term.funBinder)} {body : Lean.DoSeq}
  {binders_1 : Array (Lean.TSyntax `Lean.Parser.Term.funBinder)} {body_1 : Lean.DoSeq},
  { binders := binders, body := body } = { binders := binders_1, body := body_1 } → binders = binders_1 ∧ body = body_1
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.hgate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (self : aig.Ref),
  self.gate < aig.decls.size
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Ici : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], (Finset.Ici a).Nonempty
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.min! ∈ t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insert k v}, (t.insert k v)[a] = if h₂ : cmp k a = Ordering.eq then v else t[a]
-- Mathlib.Tactic.FunProp.Types
/-- Discrimination tree indexing theorems.  -/
Mathlib.Meta.FunProp.GeneralTheorems.theorems : Mathlib.Meta.FunProp.GeneralTheorems → Lean.Meta.RefinedDiscrTree Mathlib.Meta.FunProp.GeneralTheorem
-- Mathlib.Algebra.Ring.Commute
/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
one's additive inverse.  -/
Units.inv_eq_self_iff : ∀ {R : Type u} [inst : Ring R] [NoZeroDivisors R] (u : Rˣ), u⁻¹ = u ↔ u = 1 ∨ u = -1
-- Mathlib.GroupTheory.Congruence.Defs
Con.toSetoid_bot : ∀ {M : Type u_1} [inst : Mul M], ⊥.toSetoid = ⊥
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- The isomorphism from multivariate power series to the adic completion of
multivariate polynomials with respect to the ideal spanned by all variables
when the index is finite.  -/
MvPowerSeries.toAdicCompletionAlgEquiv : (σ : Type u_3) →
  (R : Type u_4) →
    [Finite σ] →
      [inst : CommRing R] →
        MvPowerSeries σ R ≃ₐ[MvPolynomial σ R] AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- The universal set `Set.univ` in a totally separated space is totally separated.  -/
TotallySeparatedSpace.isTotallySeparated_univ : ∀ {α : Type u} {inst : TopologicalSpace α} [self : TotallySeparatedSpace α], IsTotallySeparated Set.univ
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two one-preserving morphisms `f`, `g`,
`f * g` is the one-preserving morphism sending `x` to `f x * g x`.  -/
OneHom.instMul : {M : Type u_2} → {N : Type u_3} → [inst : One M] → [inst_1 : MulOneClass N] → Mul (OneHom M N)
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.sum : ∀ {ι : Type u_1} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : ι → E → F} {s : Finset ι},
  (∀ i ∈ s, Function.HasTemperateGrowth (f i)) → Function.HasTemperateGrowth fun x => ∑ i ∈ s, f i x
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.instanceName : Lean.Meta.DefaultInstanceEntry → Lean.Name
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  (Std.DTreeMap.map f t).getD k fallback = (Option.map (f k) (t.get? k)).getD fallback
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_eq : ∀ (z w : UpperHalfPlane), dist z w = 2 * Real.arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.nonpos_of_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
  {a b : α}, b ≤ a → variationOnFromTo f s a b ≤ 0
-- Mathlib.Data.EReal.Inv
EReal.coe_abs : ∀ (x : ℝ), ↑(↑x).abs = ↑|x|
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.map : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {α β : Type u} {x : m α}
  {f : α → β} {Q : Std.Do.PostCond β ps}, ⦃(Std.Do.wp x).apply (fun a => Q.1 (f a), Q.2)⦄ (f <$> x) ⦃Q⦄
-- Mathlib.GroupTheory.Congruence.Basic
Con.quotientKerEquivOfRightInverse_symm_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P) (g : P → M)
  (hf : Function.RightInverse g ⇑f) (a : P), (Con.quotientKerEquivOfRightInverse f g hf).symm a = (Con.toQuotient ∘ g) a
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.isIso_sheafificationAdjunction_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Sheaf J D), CategoryTheory.IsIso ((CategoryTheory.sheafificationAdjunction J D).counit.app P)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.map_of_measurable : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : TopologicalSpace E]
  [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X : Ω → E} {F : Type u_5}
  [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid F] [inst_5 : Module ℝ F] [inst_6 : MeasurableSpace F]
  [OpensMeasurableSpace F] (L : E →L[ℝ] F),
  ProbabilityTheory.HasGaussianLaw X P → Measurable ⇑L → ProbabilityTheory.HasGaussianLaw (⇑L ∘ X) P
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.homInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] (M : CategoryTheory.AddMod D A), M.homInhabited = { default := M.id }
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_re : ∀ (r θ : ℝ), (circleMap 0 r θ).re = r * Real.cos θ
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a + x) ⁻¹' Set.Ioc b c = Set.Ioc (b - a) (c - a)
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.symm_symmMeasurableEquiv : unitInterval.symmMeasurableEquiv.symm = unitInterval.symmMeasurableEquiv
-- Mathlib.Data.Sym.Sym2
Set.sym2_univ : ∀ {α : Type u_1}, Set.univ.sym2 = Set.univ
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- **Alias** of `LinearMap.BilinForm.IsSymm.eq_iff`. -/
LinearMap.BilinForm.IsSymm.ortho_comm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm → ∀ {x y : M}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trPosNum.eq_def : ∀ (x : PosNum),
  Turing.PartrecToTM2.trPosNum x =
    match x with
    | PosNum.one => [Turing.PartrecToTM2.Γ'.bit1]
    | n.bit0 => Turing.PartrecToTM2.Γ'.bit0 :: Turing.PartrecToTM2.trPosNum n
    | n.bit1 => Turing.PartrecToTM2.Γ'.bit1 :: Turing.PartrecToTM2.trPosNum n
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ), ⌈↑n⌉ = ↑n
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] {M : Type u_3} [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] {χ₁ χ₂ : ↥H → R} {x : L} {m : M},
  x ∈ LieAlgebra.rootSpace H χ₁ → m ∈ LieModule.genWeightSpace M χ₂ → ⁅x, m⁆ ∈ LieModule.genWeightSpace M (χ₁ + χ₂)
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y p : R} {k : ℕ},
  Squarefree x → Prime p → p ^ (k + 1) ∣ x * y → p ^ k ∣ y
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for reverse monotonicity of multiplication on the right,
namely `a₁ * b ≤ a₂ * b → a₁ ≤ a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedCancelMonoid`.  -/
MulRightReflectLE : (M : Type u_1) → [Mul M] → [LE M] → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.keys_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool},
  (Std.DHashMap.filter f m).keys.Perm
    (List.filter
        (fun x_2 =>
          match x_2 with
          | ⟨x_3, h'⟩ => f x_3 (m.get x_3 ⋯))
        m.keys.attach).unattach
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabLam : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.ofIso_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] [inst_5 : AddCommGroup Z] [inst_6 : Module R Z]
  {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y} {Q₃ : QuadraticForm R Z} (e : QuadraticMap.IsometryEquiv Q₁ Q₂)
  (f : QuadraticMap.IsometryEquiv Q₂ Q₃),
  QuadraticModuleCat.ofIso (e.trans f) = QuadraticModuleCat.ofIso e ≪≫ QuadraticModuleCat.ofIso f
-- Qq.Macro
Qq.Impl.MVarSynth : Type
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.div_zero_subset : ∀ {α : Type u_1} [inst : GroupWithZero α] (s : Set α), s / 0 ⊆ 0
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom
      (CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp S.iCycles h
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNatHomeo_symm_apply : ∀ {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) [inst : Encodable ι]
  [inst_1 : (i : ι) → MetricSpace (Y i)] [inst_2 : TopologicalSpace X] [inst_3 : CompactSpace X]
  (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun x y => ∃ i, f i x ≠ f i y)
  (self : Metric.PiNatEmbed X Y f),
  (Metric.PiNatEmbed.toPiNatHomeo X Y f continuous_f separating_f).symm self = self.ofPiNat
-- Mathlib.Data.Vector3
Fin2.left.eq_def : ∀ (k x : ℕ) (x_1 : Fin2 x),
  Fin2.left k x_1 =
    match x, x_1 with
    | .(n + 1), Fin2.fz => Fin2.fz
    | .(n + 1), i.fs => (Fin2.left k i).fs
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.latticeEquiv_symm_apply : ∀ (L : PeriodPair) (x : ℤ × ℤ), ↑(L.latticeEquivProd.symm x) = ↑x.1 * L.ω₁ + ↑x.2 * L.ω₂
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.toTemperedDistribution.congr_simp : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)]
  (f f_1 : ↥(MeasureTheory.Lp F p μ)),
  f = f_1 → MeasureTheory.Lp.toTemperedDistribution f = MeasureTheory.Lp.toTemperedDistribution f_1
-- Mathlib.RingTheory.Valuation.Basic
/-- **Alias** of the forward direction of `Valuation.isEquiv_iff_val_sub_one_lt_one`. -/
Valuation.IsEquiv.val_sub_one_lt_one_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  v.IsEquiv v' → ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
-- Init.Data.Float.Float32
instNonemptyFloat32 : Nonempty Float32
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_addSubmonoid_closure : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R},
  Subsemiring.closure ↑(AddSubmonoid.closure s) = Subsemiring.closure s
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The constant map is multilinear when `ι` is empty.  -/
ContinuousMultilinearMap.constOfIsEmpty : (R : Type u) →
  {ι : Type v} →
    (M₁ : ι → Type w₁) →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → [IsEmpty ι] → M₂ → ContinuousMultilinearMap R M₁ M₂
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Rci.iter : {α : Type u_1} → Std.Rci α → Std.Iter α
-- Mathlib.Topology.Compactness.CountablyCompact
/-- If a sequential space is countably compact, then it is sequentially compact. We follow the proof
in [kremsater1972sequential].  -/
instSeqCompactSpaceOfSequentialSpaceOfCountablyCompactSpace : ∀ {E : Type u_2} [inst : TopologicalSpace E] [SequentialSpace E] [CountablyCompactSpace E], SeqCompactSpace E
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.of_subsingleton : ∀ {α : Type u_1} {s : Set α} {G : SimpleGraph α}, s.Subsingleton → G.IsClique s
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ofClass_apply : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B]
  [inst_4 : EquivLike F A B] [inst_5 : MulEquivClass F A B] [inst_6 : StarHomClass F A B] (f : F) (a : A),
  (StarMulEquiv.ofClass f) a = f a
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.eq_endPos_iff : ∀ {t₁ t₂ s : String} {p : s.Pos}, p.Splits t₁ t₂ → (p = s.endPos ↔ t₂ = "")
-- Mathlib.Analysis.Convex.LinearIsometry
StrictConvex.linearIsometry_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : SeminormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {s : Set F}, StrictConvex 𝕜 s → ∀ (e : E →ₗᵢ[𝕜] F), StrictConvex 𝕜 (⇑e ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f (CategoryTheory.CategoryStruct.id d) =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H0Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupCohomology.cocycles A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π A 0)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesIso₀ A).hom) x
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers : ∀ {K : Type u_1} [inst : Field K] {L : Type u_3} [inst_1 : NumberField K] [inst_2 : Field L] [inst_3 : NumberField L]
  [inst_4 : Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
  (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L))
  [inst_5 :
    Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)]
  [ContinuousSMul (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)]
  [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)],
  Module.Finite (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)
-- Mathlib.ModelTheory.Order
/-- A sentence indicating that an order is dense:
$\forall x, \forall y, x < y \to \exists z, x < z \wedge z < y$.  -/
FirstOrder.Language.denselyOrderedSentence : (L : FirstOrder.Language) → [L.IsOrdered] → L.Sentence
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.map_comp_C : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  (MvPolynomial.map f).comp MvPolynomial.C = MvPolynomial.C.comp f
-- Mathlib.Order.LatticeIntervals
Set.Icc.isCompl_iff : ∀ {α : Type u_1} {a b : α} [inst : Lattice α] [inst_1 : Fact (a ≤ b)] {x y : ↑(Set.Icc a b)},
  IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b
-- Mathlib.Algebra.Order.Star.Basic
/-- For a star projection `p`, we have `0 ≤ p ≤ 1`.  -/
IsStarProjection.mem_Icc : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {p : R},
  IsStarProjection p → p ∈ Set.Icc 0 1
-- Mathlib.Data.Set.Image
Set.preimage_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_eq_get : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {h : a ∈ t}, Std.ExtDTreeMap.Const.get t a h = t.get a h
-- Mathlib.Condensed.Discrete.Characterization
/-- A condensed object is *discrete* if it is constant as a sheaf, i.e. isomorphic to a constant sheaf.
 -/
Condensed.IsDiscrete : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] → Condensed C → Prop
-- Init.Data.Array.Lemmas
/-- Variant of `filterMap_eq_map` with `some ∘ f` expanded out to a lambda.  -/
Array.filterMap_eq_map' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {f : α → β},
  stop = as.size → Array.filterMap (fun x => some (f x)) as 0 stop = Array.map f as
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.iSup_lt_lift_of_isRegular : ∀ {ι : Type u} {f : ι → Cardinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} (Cardinal.mk ι) < c → (∀ (i : ι), f i < c) → iSup f < c
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_ofHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {p : ℤ} (φ : F ⟶ G),
  CochainComplex.HomComplex.δ 0 p (CochainComplex.HomComplex.Cochain.ofHom φ) = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv_comm₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom
      (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).mor₃ =
    (CochainComplex.mappingConeCompTriangle f g).mor₃
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.toAlgEquivAux_eq_proj_of_mem : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K)
  (L : FiniteGaloisIntermediateField k K) (hx : x ∈ L.toIntermediateField),
  InfiniteGalois.toAlgEquivAux✝ g x = ↑(((InfiniteGalois.proj L) g) ⟨x, hx⟩)
-- Lean.Setup
Lean.Import.mk.sizeOf_spec : ∀ (module : Lean.Name) (importAll isExported isMeta : Bool),
  sizeOf { module := module, importAll := importAll, isExported := isExported, isMeta := isMeta } =
    1 + sizeOf module + sizeOf importAll + sizeOf isExported + sizeOf isMeta
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain.addMonoidHom.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] {f f_1 : α → β} (e_f : f = f_1)
  (hf : Function.Injective f), Finsupp.comapDomain.addMonoidHom hf = Finsupp.comapDomain.addMonoidHom ⋯