mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.Module
/-- [Stacks Tag 00NZ](https://stacks.math.columbia.edu/tag/00NZ) -/
Module.free_of_flat_of_isLocalRing : ∀ {R : Type u_1} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup P] [inst_2 : Module R P] [IsLocalRing R]
  [Module.Finite R P] [Module.Flat R P], Module.Free R P
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveTermGoal.mk.sizeOf_spec : ∀ (toInteractiveGoalCore : Lean.Widget.InteractiveGoalCore) (range : Lean.Lsp.Range)
  (term : Lean.Server.WithRpcRef Lean.Elab.TermInfo),
  sizeOf { toInteractiveGoalCore := toInteractiveGoalCore, range := range, term := term } =
    1 + sizeOf toInteractiveGoalCore + sizeOf range + sizeOf term
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), logDeriv id x = 1 / x
-- Mathlib.Topology.NhdsWithin
nhdsWithin_le_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, nhdsWithin a s ≤ nhds a
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.maxCombinationSize : ℕ
-- Mathlib.RingTheory.Artinian.Module
/-- A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.  -/
set_has_minimal_iff_artinian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.mk.sizeOf_spec : ∀ (levelParams : Array Lean.Name) (proof : Lean.Expr) (numParams : ℕ) (patterns : List Lean.Expr)
  (symbols : List Lean.HeadIndex) (origin : Lean.Meta.Grind.Origin) (kind : Lean.Meta.Grind.EMatchTheoremKind)
  (minIndexable : Bool) (cnstrs : List Lean.Meta.Grind.EMatchTheoremConstraint),
  sizeOf
      { levelParams := levelParams, proof := proof, numParams := numParams, patterns := patterns, symbols := symbols,
        origin := origin, kind := kind, minIndexable := minIndexable, cnstrs := cnstrs } =
    1 + sizeOf levelParams + sizeOf proof + sizeOf numParams + sizeOf patterns + sizeOf symbols + sizeOf origin +
          sizeOf kind +
        sizeOf minIndexable +
      sizeOf cnstrs
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isStrongLimit_beth : ∀ {o : Ordinal.{u_1}}, (Cardinal.beth o).IsStrongLimit ↔ Order.IsSuccPrelimit o
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Directed.sequence.match_3.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.UInt.Bitwise
UInt64.toNat_xor : ∀ (a b : UInt64), (a ^^^ b).toNat = a.toNat ^^^ b.toNat
-- Init.Data.BitVec.Bitblast
BitVec.divRec_succ : ∀ {w : ℕ} (m : ℕ) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w),
  BitVec.divRec (m + 1) args qr = BitVec.divRec m args (BitVec.divSubtractShift args qr)
-- Init.Data.List.Attach
List.getLast?_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H).getLast? = xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.termination : Lean.Elab.PreDefinition → Lean.Elab.TerminationHints
-- Std.Http.Data.Headers.Name
/-- Standard Server header name
 -/
Std.Http.Header.Name.server : Std.Http.Header.Name
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_natCast_lt_lift : ∀ {o : Ordinal.{u}} {n : ℕ}, Ordinal.omega ↑n < Ordinal.lift.{v, u} o ↔ Ordinal.omega ↑n < o
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the pure predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.any`.
 -/
Std.Iter.Total.any : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.IteratorLoop α Id Id] → [Std.Iterators.Finite α Id] → (β → Bool) → Std.Iter.Total β → Bool
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_injective : ∀ (p : ENNReal) {V : Type u_4}, Function.Injective (WithLp.toLp p)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffAt.snd : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : N → M × M'} {x : N}, ContMDiffAt J (I.prod I') n f x → ContMDiffAt J I' n (fun x => (f x).2) x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ),
  MeasureTheory.StronglyMeasurable (MeasureTheory.AEStronglyMeasurable.mk f hf)
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_eq_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {x : ↑(Set.Ioc 0 1)},
  ↑x = 1 ↔ x = 1
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceTo_next : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).endPos},
  String.Pos.ofSliceTo (p.next h) = (String.Pos.ofSliceTo p).next ⋯
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instFaithfulUlift : ∀ (R : Type u) [inst : Ring R], (FGModuleCat.ulift R).Faithful
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- Any cusp form for `𝒮ℒ` is `O(Δ)` at the cusp `i∞`.  -/
CuspForm.exp_decay_isBigO_discriminant : ∀ {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k),
  ⇑f =O[UpperHalfPlane.atImInfty] ModularForm.discriminant
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.mk.injEq : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ} (max : ℕ)
  (map : Std.HashMap α ℕ) (inv1 : Std.Sat.AIG.RelabelNat.State.Inv1 max map)
  (inv2 : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map) (max_1 : ℕ) (map_1 : Std.HashMap α ℕ)
  (inv1_1 : Std.Sat.AIG.RelabelNat.State.Inv1 max_1 map_1) (inv2_1 : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map_1),
  ({ max := max, map := map, inv1 := inv1, inv2 := inv2 } =
      { max := max_1, map := map_1, inv1 := inv1_1, inv2 := inv2_1 }) =
    (max = max_1 ∧ map = map_1)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_union_add_inter_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (f : α → M) (s t : Set α) (a : α),
  (s ∪ t).indicator f a + (s ∩ t).indicator f a = s.indicator f a + t.indicator f a
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.sum_eq_iSup_of_lift_mk_le_iSup : ∀ {ι : Type u} {f : ι → Cardinal.{max u v}},
  Cardinal.aleph0 ≤ Cardinal.mk ι → Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ ⨆ i, f i → Cardinal.sum f = ⨆ i, f i
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] {a a' : α} {f : α →₀ M},
  (Finsupp.erase a f) a' = if a' = a then 0 else f a'
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTop_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (β : LieModule.Weight R L M),
  LieModule.chainTop 0 β = β
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C}
  (h : Opposite.unop (CategoryTheory.Limits.pullback f.op g.op) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f.op g.op).unop h
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- The (limit) fan expressing that `U.power α` is a product of copies of
`U` indexed by `α`.  -/
CategoryTheory.Limits.FormalCoproduct.powerFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Limits.FormalCoproduct C) →
      (α : Type) → [CategoryTheory.Limits.HasProductsOfShape α C] → CategoryTheory.Limits.Fan fun x => U
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_nsmul_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : AddMonoid Z] [inst_4 : ContinuousAdd Z] (f : C(X × Y, Z)) (n : ℕ) (x : X),
  (n • f).curry x = n • f.curry x
-- Mathlib.NumberTheory.Multiplicity
padicValNat.pow_two_sub_pow : ∀ {x y : ℕ},
  y < x →
    2 ∣ x - y →
      ¬2 ∣ x →
        ∀ {n : ℕ},
          n ≠ 0 →
            Even n → padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommSemiRingCat.FilteredColimits.colimitCommSemiring : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommSemiRingCat) → CommSemiring ↑(CommSemiRingCat.FilteredColimits.R F)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound : Type
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.mk.injEq : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing N] [inst_2 : LieAlgebra R N]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (L : Type u_5) (instLieRing : LieRing L)
  (instLieAlgebra : LieAlgebra R L) (incl : N →ₗ⁅R⁆ L) (proj : L →ₗ⁅R⁆ M)
  (IsExtension : LieAlgebra.IsExtension incl proj) (L_1 : Type u_5) (instLieRing_1 : LieRing L_1)
  (instLieAlgebra_1 : LieAlgebra R L_1) (incl_1 : N →ₗ⁅R⁆ L_1) (proj_1 : L_1 →ₗ⁅R⁆ M)
  (IsExtension_1 : LieAlgebra.IsExtension incl_1 proj_1),
  ({ L := L, instLieRing := instLieRing, instLieAlgebra := instLieAlgebra, incl := incl, proj := proj,
        IsExtension := IsExtension } =
      { L := L_1, instLieRing := instLieRing_1, instLieAlgebra := instLieAlgebra_1, incl := incl_1, proj := proj_1,
        IsExtension := IsExtension_1 }) =
    (L = L_1 ∧ instLieRing ≍ instLieRing_1 ∧ instLieAlgebra ≍ instLieAlgebra_1 ∧ incl ≍ incl_1 ∧ proj ≍ proj_1)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.isPiSystem : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetSemiring C → IsPiSystem C
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsReducedSpecOfIsReducedCarrier : ∀ {R : CommRingCat} [H : IsReduced ↑R], AlgebraicGeometry.IsReduced (AlgebraicGeometry.Spec R)
-- Mathlib.Order.Basic
Sum.elim_le_const_iff : ∀ {β : Type u_3} {α₁ : Type u_5} {α₂ : Type u_6} [inst : LE β] {b : β} {u₁ : α₁ → β} {u₂ : α₂ → β},
  Sum.elim u₁ u₂ ≤ Function.const (α₁ ⊕ α₂) b ↔ u₁ ≤ Function.const α₁ b ∧ u₂ ≤ Function.const α₂ b
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapWhiskerRight_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fₗ Gₗ Hₗ : CategoryTheory.Functor C E} (α : Fₗ ⟶ Gₗ) (β : Gₗ ⟶ Hₗ)
  (H : CategoryTheory.Functor D E'),
  CategoryTheory.Join.mapWhiskerRight (CategoryTheory.CategoryStruct.comp α β) H =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapWhiskerRight α H)
      (CategoryTheory.Join.mapWhiskerRight β H)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.lintegral_nnnorm_condExpL2_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0},
  MeasurableSet s →
    μ s ≠ ⊤ →
      ∀ (f : ↥(MeasureTheory.Lp ℝ 2 μ)),
        ∫⁻ (x : α) in s, ↑‖↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isPartialOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsPartialOrder β s],
  IsPartialOrder α r
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.finsuppSum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : Type u_3} [inst_1 : Zero β]
  {f : ι →₀ β} (g : ι → β → R), (∀ i ∈ f.support, g i (f i) ∈ I) → f.sum g ∈ I
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sdiff_eq_sub : ∀ {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [inst : AddCommGroup G] [inst_1 : DecidableEq ι] {f : ι → G},
  s₁ ⊆ s₂ → ∑ x ∈ s₂ \ s₁, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A presieve `R` has pullbacks along `f` if for every `h` in `R`, the pullback
with `f` exists.  -/
CategoryTheory.Presieve.HasPullbacks : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Presieve X → {Y : C} → (Y ⟶ X) → Prop
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments by duplicating the first argument. Used for `smul`.  -/
Simps.copySecond : Simps.findArgType
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.isImage_source_target_of_disjoint : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β),
  Disjoint e.source e'.source → Disjoint e.target e'.target → e.IsImage e'.source e'.target
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_injective : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  Function.Injective ⇑f → Function.Injective ⇑(MvPolynomial.map f)
-- Mathlib.Topology.Sheaves.Limits
TopCat.instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{v_1, w} J] →
        [CategoryTheory.Limits.HasLimitsOfShape J C] →
          (X : TopCat) → CategoryTheory.CreatesLimitsOfShape J (TopCat.Sheaf.forget C X)
-- Mathlib.Topology.Separation.Regular
/-- A topological space is said to be a *normal space* if any two disjoint closed sets
have disjoint open neighborhoods.  -/
NormalSpace : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.mkQ.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G] (n : ℕ), ModN.mkQ n = ↑((LinearMap.lsmul ℤ G) ↑n).range.mkQ
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.inclLift_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (x : C),
  (CategoryTheory.WithTerminal.inclLift F M hM).hom.app x =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithTerminal.incl.obj x with
      | CategoryTheory.WithTerminal.of x => F.obj x
      | CategoryTheory.WithTerminal.star => Z)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The kernel of a divided power morphism, as a `SubDPIdeal`.  -/
DividedPowers.DPMorphism.ker : {A : Type u_1} →
  [inst : CommRing A] →
    {I : Ideal A} →
      (hI : DividedPowers I) →
        {B : Type u_2} →
          [inst_1 : CommRing B] → {J : Ideal B} → (hJ : DividedPowers J) → hI.DPMorphism hJ → hI.SubDPIdeal
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Enter foralls recursively, creating a telescope for binders which are instances of concern
and instantiating all other bvars with `sorry`. The only free variables therefore arise from
instances of concern which we want to track the usage of.

By instantiating ordinary binders with `sorry`, `collectFVarsOutsideOfProofs` can use the
computed field accessed by `hasFVar` (in constant time) to avoid traversing any subexpressions
that do not contain a free variable for an instance of concern, which helps performance.

Used fvarIds (i.e., instances of concern) are recorded in the `StateRefT`'s `FVarIdSet`; the
returned `Array InstanceOfConcern` records all instances of concern that have been introduced,
used or not.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Lean.Expr.collectUnnecessaryInstanceBinderIdxsWhere.go : (Lean.Expr → Bool) →
  Lean.Expr →
    ℕ →
      Array Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern✝ →
        StateRefT' IO.RealWorld Lean.FVarIdSet Lean.MetaM
          (Array Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern✝)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop} {X Y : C}
  {x : X ⟶ Y} (t : CategoryTheory.MorphismProperty.sourceLocalClosure K P x),
  (∀ ⦃X Y : C⦄ (x : X ⟶ Y) (t : CategoryTheory.MorphismProperty.sourceLocalClosure K P x),
      CategoryTheory.MorphismProperty.sourceLocalClosure.below t → motive x t) →
    motive x t
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.intro' : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} {K : Set α},
  IsCompact K → IsClosed K → (∀ x ∉ K, f x = 1) → HasCompactMulSupport f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.liftOn.congr_simp : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α : Type u_3} (x x_1 : LocalizedModule S M),
  x = x_1 →
    ∀ (f f_1 : M × ↥S → α) (e_f : f = f_1) (wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'),
      x.liftOn f wd = x_1.liftOn f_1 ⋯
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.mk : Lean.Declaration →
  Array Lean.Expr → ℤ → Array Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.Command.FinalizeInductiveDecl✝
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysArray.isEmpty = m.isEmpty
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasProd_nat_add_iff' : ∀ {G : Type u_2} [inst : CommGroup G] {g : G} [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ),
  HasProd (fun n => f (n + k)) (g / ∏ i ∈ Finset.range k, f i) ↔ HasProd f g
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_pair : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [CompleteSpace F]
  {μ : MeasureTheory.Measure α} [CompleteSpace E] {f : α → E} {g : α → F},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ⨍ (x : α), (f x, g x) ∂μ = (⨍ (x : α), f x ∂μ, ⨍ (x : α), g x ∂μ)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_setOfPred_eq : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [Finite ι] {F : Type u_5} {G : Type u_6}
  [inst_2 : FunLike F (ι → ℕ) M] [AddMonoidHomClass F (ι → ℕ) M] [inst_4 : FunLike G (ι → ℕ) M]
  [AddMonoidHomClass G (ι → ℕ) M] (a b : M) (f : F) (g : G), IsSemilinearSet {x | a + f x = b + g x}
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.mk.injEq : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] (toEquiv : α ≃ β)
  (uniformContinuous_toFun : UniformContinuous toEquiv.toFun)
  (uniformContinuous_invFun : UniformContinuous toEquiv.invFun) (toEquiv_1 : α ≃ β)
  (uniformContinuous_toFun_1 : UniformContinuous toEquiv_1.toFun)
  (uniformContinuous_invFun_1 : UniformContinuous toEquiv_1.invFun),
  ({ toEquiv := toEquiv, uniformContinuous_toFun := uniformContinuous_toFun,
        uniformContinuous_invFun := uniformContinuous_invFun } =
      { toEquiv := toEquiv_1, uniformContinuous_toFun := uniformContinuous_toFun_1,
        uniformContinuous_invFun := uniformContinuous_invFun_1 }) =
    (toEquiv = toEquiv_1)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j / f k) κ μ
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaObjObjEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {Y : Cᵒᵖ}, CategoryTheory.shrinkYonedaObjObjEquiv = (equivShrink ((CategoryTheory.yoneda.obj X).obj Y)).symm
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coe_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] [inst_3 : Nontrivial R]
  {x : ↑(Set.Ico 0 1)}, ↑x ≠ 0 ↔ x ≠ 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Icc : ∀ {n : ℕ} (i j : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Icc i j) = Finset.Icc j.rev i.rev
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_of_mem_nhds : ∀ {𝕜 : 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 : Set M},
  s ∈ nhds x → mfderiv[s] f x = mfderiv% f x
-- Std.Data.DHashMap.Raw
/-- Returns a list of all keys present in the hash map in some order.  -/
Std.DHashMap.Raw.keys : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → List α
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.single m r` is injective in `m` if `r ≠ 0`. For injectivity in `r`, see
`MonoidAlgebra.single_injective`.  -/
MonoidAlgebra.single_left_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R},
  r ≠ 0 → Function.Injective fun m => MonoidAlgebra.single m r
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h_def : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : DecidableEq ι] (i : ↥b.support),
  RootPairing.GeckConstruction.h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x => ↑(P.pairingIn ℤ x ↑i))