mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Util.AtLocation
/-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).

In the wildcard case (`*`), filter out all dependent and/or non-`Prop` hypotheses.

Assumes `proc` is not surrounded by backticks.  -/
Mathlib.Tactic.transformAtNondepPropLocation : (Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) →
  String →
    Lean.Elab.Tactic.Location →
      optParam Mathlib.Tactic.BehaviorIfUnchanged Mathlib.Tactic.BehaviorIfUnchanged.error →
        optParam Bool false → optParam Lean.Meta.Simp.Context default → Lean.Elab.Tactic.TacticM Unit
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State.mk.sizeOf_spec : ∀ (varMap : Lean.Meta.KExprMap ℕ) (vars : Array Lean.Expr),
  sizeOf { varMap := varMap, vars := vars } = 1 + sizeOf varMap + sizeOf vars
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The additive congruence relation generated by a normal additive subgroup.  -/
QuotientAddGroup.con : {G : Type u_1} → [inst : AddGroup G] → (N : AddSubgroup G) → [nN : N.Normal] → AddCon G
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_subrel : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (a : α),
  Ordinal.type (Subrel r fun x => r x a) = (Ordinal.typein r).toRelEmbedding a
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.WidePushoutShape.fintypeHom : {J : Type v} → (j j' : CategoryTheory.Limits.WidePushoutShape J) → Fintype (j ⟶ j')
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_iSup_of_directed : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → Submonoid M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Lean.CoreM
Lean.maxHeartbeats : Lean.Option ℕ
-- Lean.Level
Lean.Level.instQuoteMkStr1 : Lean.Quote Lean.Level `level
-- Mathlib.RingTheory.Multiplicity
multiplicity_of_one_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, ¬IsUnit a → multiplicity a 1 = 0
-- Init.Data.String.Basic
String.Slice.str_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceFrom pos).str = s.str
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- If a weak equalizer of `f` and `g` exists, we can access an arbitrary choice of such by
saying `weakEqualizer f g`.  -/
CategoryTheory.Limits.weakEqualizer : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} → (f g : X ⟶ Y) → [CategoryTheory.Limits.HasWeakEqualizer f g] → C
-- Mathlib.RingTheory.Finiteness.Descent
Module.Finite.of_finite_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} [inst : CommRing R] (T : Type u_3) [inst_1 : CommRing T] [inst_2 : Algebra R T] {M : Type u_4}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.FaithfullyFlat R T] [Module.Finite T (TensorProduct R T M)],
  Module.Finite R M
-- Init.Data.List.ToArray
List.findIdx_toArray : ∀ {α : Type u_1} {as : List α} {p : α → Bool}, Array.findIdx p as.toArray = List.findIdx p as
-- Init.Data.List.Zip
/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths.  -/
List.zip_replicate' : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : ℕ},
  (List.replicate n a).zip (List.replicate n b) = List.replicate n (a, b)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- Standard formula for the discriminant of a cubic polynomial.  -/
Polynomial.discr_of_degree_eq_three : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  f.degree = 3 →
    f.discr =
      f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
          27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
        18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.trans : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H},
  e ∈ G → e' ∈ G → e.trans e' ∈ G
-- Init.Data.UInt.Lemmas
USize.le_iff_toNat_le : ∀ {a b : USize}, a ≤ b ↔ a.toNat ≤ b.toNat
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sdiff_eq_prod_sdiff_iff : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq ι] [inst_1 : CancelCommMonoid M] {s t : Finset ι} {f : ι → M},
  ∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurve.isIntegralCurveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v → ∀ (s : Set ℝ), IsIntegralCurveOn γ v s
-- Mathlib.Geometry.Euclidean.Simplex
Affine.Simplex.Equilateral.acuteAngled : ∀ {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 : ℕ} {s : Affine.Simplex ℝ P n}, s.Equilateral → s.AcuteAngled
-- Std.Data.ExtTreeMap.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.ExtTreeMap.mergeWith : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (α → β → β → β) → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Translating a `Cont` continuation to a `Cont'` continuation simply entails dropping all the
data. This data is instead encoded in `trContStack` in the configuration.  -/
Turing.PartrecToTM2.trCont : Turing.ToPartrec.Cont → Turing.PartrecToTM2.Cont'
-- Mathlib.Algebra.Group.Action.Basic
smul_inv' : ∀ {M : Type u_2} {A : Type u_3} [inst : Monoid M] [inst_1 : Group A] [inst_2 : MulDistribMulAction M A] (r : M) (x : A),
  r • x⁻¹ = (r • x)⁻¹
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- The adjacency matrix of `G` is an adjacency matrix.  -/
SimpleGraph.isAdjMatrix_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Zero α] [inst_2 : One α],
  (SimpleGraph.adjMatrix α G).IsAdjMatrix
-- Init.Data.String.Pattern.String
String.Slice.Pattern.BackwardSliceSearcher.instBackwardPattern : {pat : String.Slice} → String.Slice.Pattern.BackwardPattern pat
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.fixedField_eq_iff_fixingSubgroup_eq : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [IsGalois F E] {K : IntermediateField F E} {H : Subgroup Gal(E/F)},
  IntermediateField.fixedField H = K ↔ K.fixingSubgroup = H
-- Mathlib.GroupTheory.OrderOfElement
multiplesEquivMultiples.eq_1 : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Finite G] {x y : G} (h : addOrderOf x = addOrderOf y),
  multiplesEquivMultiples h = (finEquivMultiples ⋯).symm.trans ((finCongr h).trans (finEquivMultiples ⋯))
-- Init.Data.List.Scan.Lemmas
List.scanlM_map : ∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α₁ → α₂} {g : β → α₂ → m β} {as : List α₁},
  List.scanlM g init (List.map f as) = List.scanlM (fun x1 x2 => g x1 (f x2)) init as
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousOn_iff_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  UpperHemicontinuous (s.domRestrict f) ↔ UpperHemicontinuousOn f s
-- Mathlib.Data.PNat.Basic
instAddLeftStrictMonoPNat : AddLeftStrictMono ℕ+
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Data.Nat.Cast.Defs
two_add_two_eq_four : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 2 + 2 = 4
-- Mathlib.GroupTheory.Finiteness
Subgroup.fg_iff_add_fg : ∀ {G : Type u_3} [inst : Group G] (P : Subgroup G), P.FG ↔ (Subgroup.toAddSubgroup P).FG
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.instCategoryCostructuredArrow_1 : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (S : CategoryTheory.Functor C D) →
          (T : D) → CategoryTheory.Category.{v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)
-- Init.Prelude
/-- Lifts a type or proposition to a higher universe level.

`PULift α` wraps a value of type `α`. It is a generalization of
`PLift` that allows lifting values whose type may live in `Sort s`.
It also subsumes `PLift`.
 -/
PULift : Sort s → Sort (max s r 1)
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyLE.countable_bUnion`. -/
EventuallyLE.countable_bUnion : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) → ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
-- Init.Data.BitVec.Lemmas
BitVec.clz_eq_reverse_ctz : ∀ {w : ℕ} {x : BitVec w}, x.clz = x.reverse.ctz
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.spine.eq_1 : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (h : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := h })),
  X.spine m h Δ =
    {
      vertex := fun i =>
        (CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.Hom.tr ({ len := 0 }.const { len := m } i) ⋯ h).op))
          Δ,
      arrow := fun i =>
        (CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ h).op))
          Δ,
      arrow_src := ⋯, arrow_tgt := ⋯ }
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_gamma : ∀ (o : Ordinal.{u_1}), o.gamma.invVeblen₁ = o.gamma
-- Mathlib.Data.Stream.Defs
/-- Given an initial value `a : α` and functions `f : α → β` and `g : α → α`,
`corecOn a f g` creates a stream by repeatedly:
1. Applying `f` to the current value to get the next stream element
2. Applying `g` to get the next value to process

This is equivalent to `corec f g a`.  -/
Stream'.corecOn : {α : Type u} → {β : Type v} → α → (α → β) → (α → α) → Stream' β
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.map_vsub : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (p1 p2 : P),
  e.linearIsometryEquiv (p1 -ᵥ p2) = e p1 -ᵥ e p2
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_eq_empty : ∀ {α : Type u_1} [inst : LE α] {s : LowerSet α}, ↑s = ∅ ↔ s = ⊥
-- Mathlib.NumberTheory.Dioph
Poly.sub_apply : ∀ {α : Type u_1} (f g : Poly α) (x : α → ℕ), (f - g) x = f x - g x
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The pole divisor of `f₁ + f₂` is smaller than or equal to the sum of the pole divisors of `f₁` and
`f₂`, respectively.
 -/
MeromorphicOn.negPart_divisor_add_le_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (MeromorphicOn.divisor (f₁ + f₂) U)⁻ ≤ (MeromorphicOn.divisor f₁ U)⁻ + (MeromorphicOn.divisor f₂ U)⁻
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.List.filterMapM_cons.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive __do_lift
-- Mathlib.FieldTheory.AbelRuffini
splits_X_pow_sub_one_of_X_pow_sub_C : ∀ {F : Type u_3} [inst : Field F] {E : Type u_4} [inst_1 : Field E] (i : F →+* E) (n : ℕ) {a : F},
  a ≠ 0 →
    (Polynomial.map i (Polynomial.X ^ n - Polynomial.C a)).Splits → (Polynomial.map i (Polynomial.X ^ n - 1)).Splits
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₁.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.u₁✝ S = FermatLastTheoremForThreeGen.Solution.u₁✝ S_1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.val_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp}, (↑t).toList = t.toList
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α}, a • s = ∅ ↔ s = ∅
-- Init.Data.List.Scan.Lemmas
List.head?_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β}, (List.scanr f b l).head? = some (List.foldr f b l)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_comm_of_commute : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {M N : Submodule R A}, (∀ m ∈ M, ∀ n ∈ N, Commute m n) → M * N = N * M
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Two affine maps which agree on a set, agree on its affine span.  -/
AffineMap.eqOn_affineSpan : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {V₂ : Type u_8} {P₂ : Type u_9} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] {s : Set P₁} {f g : P₁ →ᵃ[k] P₂}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(affineSpan k s)
-- Mathlib.Algebra.Group.Action.Sigma
/-- This is not an instance because `i` becomes a metavariable.  -/
Sigma.FaithfulSMul' : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] (i : ι) [FaithfulSMul M (α i)],
  FaithfulSMul M ((i : ι) × α i)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.FormatType.match_1.splitter : (motive : Std.Time.FormatString → Sort u_1) →
  (x : Std.Time.FormatString) →
    ((entry : Std.Time.Modifier) →
        (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.modifier entry :: xs)) →
      ((val : String) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.string val :: xs)) →
        (Unit → motive []) → motive x
-- Std.Http.Data.URI.Basic
/-- URI scheme identifier (e.g., "http", "https", "ftp").
 -/
Std.Http.URI.Scheme : Type
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.error.sizeOf_spec : ∀ (stx : Lean.TSyntax `tactic) (msg : Lean.MessageData),
  sizeOf (Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx msg) = 1 + sizeOf stx + sizeOf msg
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
/-- Affine homeomorphism `(r • · +ᵥ c)` between a normed space and an add torsor over this space,
interpreted as an `OpenPartialHomeomorph` between `Metric.ball 0 1` and `Metric.ball c r`.  -/
OpenPartialHomeomorph.unitBallBall : {E : Type u_1} →
  [inst : SeminormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      {P : Type u_2} →
        [inst_2 : PseudoMetricSpace P] → [NormedAddTorsor E P] → P → (r : ℝ) → 0 < r → OpenPartialHomeomorph E P
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.visitLevels : List Lean.Level → Lean.CollectLevelParams.Visitor
-- Std.Async.ContextAsync
/-- Gets the cancellation reason if the context is cancelled. Returns `some reason` if cancelled, `none` otherwise,
allowing you to distinguish between different cancellation types.
 -/
Std.Async.ContextAsync.getCancellationReason : Std.Async.ContextAsync (Option Std.CancellationReason)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.primesOver_ncard_ne_zero`. -/
primesOver_ncard_ne_zero : ∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  (p.primesOver B).ncard ≠ 0
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.union_iff : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ s' : Set (Set Ω)},
  ProbabilityTheory.CondIndepSets m' hm' (s₁ ∪ s₂) s' μ ↔
    ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ ∧ ProbabilityTheory.CondIndepSets m' hm' s₂ s' μ
-- Mathlib.Order.SuccPred.CompleteLinearOrder
/-- See `exists_eq_ciSup_of_not_isSuccLimit` for the `ConditionallyCompleteLinearOrder` version.  -/
exists_eq_ciSup_of_not_isSuccPrelimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
  ¬Order.IsSuccPrelimit (⨆ i, f i) → ∃ i, f i = ⨆ i, f i
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_eq_of_eqOn : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {f g : α → α'},
  Set.EqOn f g G.vertexSet → Graph.map f G = Graph.map g G
-- Lean.Data.Json.Printer
Lean.Json.instToString : ToString Lean.Json
-- Mathlib.Order.LatticeIntervals
Set.Icc.coe_sup : ∀ {α : Type u_1} {a b : α} [inst : SemilatticeSup α] {x y : ↑(Set.Icc a b)}, ↑(x ⊔ y) = ↑x ⊔ ↑y
-- Mathlib.Topology.Sheaves.LocallySurjective
TopCat.Sheaf.isLocallySurjective_iff_epi : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Balanced (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C)]
  [(Opens.grothendieckTopology ↑X).HasSheafCompose (CategoryTheory.forget C)]
  [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C]
  [(Opens.grothendieckTopology ↑X).WEqualsLocallyBijective C]
  [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization C] {F G : TopCat.Sheaf C X}
  (φ : F ⟶ G), TopCat.Presheaf.IsLocallySurjective φ.hom ↔ CategoryTheory.Epi φ
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.digits_append_zeroes_append_digits : ∀ {b k m n : ℕ},
  1 < b → 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.pow_iff_pos : ∀ {n : ℕ} {S : Type u_5} [inst : MonoidWithZero S] {x : S}, n ≠ 0 → (IsNilpotent (x ^ n) ↔ IsNilpotent x)
-- Mathlib.Algebra.BigOperators.Finprod
Nat.cast_finprod : ∀ {ι : Type u_3} [Finite ι] {R : Type u_7} [inst : CommSemiring R] (f : ι → ℕ), ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)
-- Std.Data.Internal.List.Defs
Std.Internal.List.DistinctKeys.mk : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a == b) = false) (Std.Internal.List.keys l) → Std.Internal.List.DistinctKeys l
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.star_mem_star_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] (S : NonUnitalSubalgebra R A) (x : A),
  star x ∈ star S ↔ x ∈ S
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Submonoids of monoid `M` are isomorphic to additive submonoids of `Additive M`.  -/
Submonoid.toAddSubmonoid : {M : Type u_1} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toArray_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.keys.toArray = t.keysArray
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Precomposing `f` with `Prod.snd` is `C^n` at `x : E × F`  -/
ContDiffAt.snd'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : F → G} {x : E × F},
  ContDiffAt 𝕜 n f x.2 → ContDiffAt 𝕜 n (fun x => f x.2) x
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mapEquiv_symm : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (g : M ≃ₗ[R] N),
  (DividedPowerAlgebra.mapEquiv g).symm = DividedPowerAlgebra.mapEquiv g.symm
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- If `m₁ s = op (m₂ s)` for all `s`, then the same is true for `m₁.trim` and `m₂.trim`.  -/
MeasureTheory.OuterMeasure.trim_op : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α} {op : ENNReal → ENNReal},
  (∀ (s : Set α), m₁ s = op (m₂ s)) → ∀ (s : Set α), m₁.trim s = op (m₂.trim s)
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_mem_unitary_mul : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] {U : E} (A : E),
  U ∈ unitary E → ‖U * A‖ = ‖A‖
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[t] f x f' → s ⊆ t → HasMFDerivAt[s] f x f'
-- Lean.Meta.Sym.InstantiateS
/-- Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
 -/
Lean.Meta.Sym.betaRevS : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulReflectLT_iff_mulPosReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α],
  PosMulReflectLT α ↔ MulPosReflectLT α
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mk.injEq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (f : ι → ι')
  (injective_f : Function.Injective f) (rel : ∀ {i₁ i₂ : ι}, c.Rel i₁ i₂ → c'.Rel (f i₁) (f i₂)) (f_1 : ι → ι')
  (injective_f_1 : Function.Injective f_1) (rel_1 : ∀ {i₁ i₂ : ι}, c.Rel i₁ i₂ → c'.Rel (f_1 i₁) (f_1 i₂)),
  ({ f := f, injective_f := injective_f, rel := rel } = { f := f_1, injective_f := injective_f_1, rel := rel_1 }) =
    (f = f_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.foldM_eq_foldlM_toArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  m.WF → Std.HashMap.Raw.foldM f init m = Array.foldlM (fun a b => f a b.1 b.2) init m.toArray