mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Pointwise
Filter.nsmul_mem_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] {f : Filter α} {s : Set α}, s ∈ f → ∀ (n : ℕ), n • s ∈ n • f
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_smul_measure_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  (c : ENNReal) (f : α → ε) (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_eq_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.minKey he = t.minKey!
-- Mathlib.Order.Filter.Defs
Filter.hnot_def : ∀ {α : Type u_1} {f : Filter α}, ￢f = Filter.principal f.kerᶜ
-- Mathlib.Topology.Algebra.IsOpenUnits
instIsOpenUnitsOfContinuousInv₀OfT1Space : ∀ {M : Type u_1} [inst : GroupWithZero M] [inst_1 : TopologicalSpace M] [ContinuousInv₀ M] [T1Space M], IsOpenUnits M
-- Mathlib.Algebra.Module.SpanRank
Ideal.lift_spanRank_map_eq_of_ringEquiv : ∀ {R : Type u} [inst : Semiring R] {T : Type v} [inst_1 : Semiring T] (f : R ≃+* T) (I : Ideal R),
  Cardinal.lift.{u, v} (Submodule.spanRank (Ideal.map f I)) = Cardinal.lift.{v, u} (Submodule.spanRank I)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.post_comp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor T D)
  (G : CategoryTheory.Functor D E),
  CategoryTheory.Over.post (F.comp G) = (CategoryTheory.Over.post F).comp (CategoryTheory.Over.post G)
-- Mathlib.Topology.Algebra.ConstMulAction
isClosedMap_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G), IsClosedMap fun x => c +ᵥ x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_sin : Measurable Real.sin
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMapCompIso_hom_app : ∀ {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [inst : Quiver V₁] [inst_1 : Quiver V₂] [inst_2 : Quiver V₃]
  (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) (X : CategoryTheory.Paths V₁),
  (CategoryTheory.Cat.freeMapCompIso F G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj (F.obj X))
-- Mathlib.Algebra.Order.Pi
Function.const_nonneg : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  0 ≤ Function.const β a ↔ 0 ≤ a
-- Mathlib.Order.Filter.Prod
Filter.prod_comm : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = Filter.map Prod.swap (g ×ˢ f)
-- Mathlib.Order.Compare
LT.lt.cmp_eq_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x < y → cmp x y = Ordering.lt
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.needMoreData.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {size size_1 : Option ℕ},
  Std.Http.Protocol.H1.Event.needMoreData size = Std.Http.Protocol.H1.Event.needMoreData size_1 → size = size_1
-- Mathlib.Tactic.GCongr.Core
/-- See if the term is `a = b` and the goal is `a ∼ b` or `b ∼ a`, with `∼` reflexive.  -/
Mathlib.Tactic.GCongr.exactRefl : Mathlib.Tactic.GCongr.ForwardExt
-- Mathlib.Geometry.Euclidean.Triangle
EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mul : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (a b c a' b' c' : P) (r : ℝ),
  EuclideanGeometry.angle a' b' c' = EuclideanGeometry.angle a b c →
    dist a' b' = r * dist a b → dist c' b' = r * dist c b → dist a' c' = r * dist a c
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_iff_lt_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a - b < c ↔ a < b + c
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleRing.isSemisimpleModule : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleRing R],
  IsSemisimpleModule R M
-- Mathlib.Data.ENat.Basic
/-- Convert a `ℕ∞` to a `ℕ` using a proof that it is not infinite.  -/
ENat.lift : (x : ℕ∞) → x < ⊤ → ℕ
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.isMaximal : ∀ {R : Type u_1} [inst : CommSemiring R] (self : MaximalSpectrum R), self.asIdeal.IsMaximal
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The identity is 1-Lipschitz.  -/
LipschitzWith.id : ∀ {α : Type u} [inst : PseudoEMetricSpace α], LipschitzWith 1 id
-- Lean.Parser.Term
Lean.Parser.Term.type.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Compiler.LCNF.Basic
/-- Partial application of a function.
 -/
Lean.Compiler.LCNF.LetValue.pap : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name →
    Array (Lean.Compiler.LCNF.Arg pu) →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_15 →
        Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.Finsupp.Single
Finsupp.support_single_ne_bot : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b : M} (i : α), b ≠ 0 → (fun₀ | i => b).support ≠ ⊥
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.not_matchesAt_of_get_ne : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  pos.get h ≠ c → ¬String.Slice.Pattern.Model.MatchesAt c pos
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' fallback : α} {f : β k → β k},
  m.WF →
    (m.modify k f).getKeyD k' fallback =
      if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.Elements.instHasInitialObjOppositeTypeFlipShrinkYonedaOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  (X : C), CategoryTheory.Limits.HasInitial (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.flip.obj (Opposite.op X)).Elements
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsAddRightInvariant.map_add_right_eq_self : ∀ {G : Type u_1} {inst : MeasurableSpace G} {inst_1 : Add G} {μ : MeasureTheory.Measure G}
  [self : μ.IsAddRightInvariant] (g : G), MeasureTheory.Measure.map (fun x => x + g) μ = μ
-- Mathlib.Topology.Constructions.SumProd
continuous_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.inr
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β →o γ) (f : α →o β) (a : NonemptyInterval α),
  NonemptyInterval.map g (NonemptyInterval.map f a) = NonemptyInterval.map (g.comp f) a
-- Mathlib.Analysis.Normed.Operator.CompleteCodomain
SeparatingDual.completeSpace_continuousLinearMap_iff : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [SeparatingDual 𝕜 E]
  [Nontrivial E], CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_comp : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} {o : Type u_6} [inst_1 : Fintype n] [inst_2 : Fintype o]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq o] (B : LinearMap.BilinForm R₁ (n → R₁))
  (l r : (o → R₁) →ₗ[R₁] n → R₁),
  LinearMap.BilinForm.toMatrix' (B.comp l r) =
    (LinearMap.toMatrix' l).transpose * LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' r
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ}, a ∉ Std.HashSet.Raw.emptyWithCapacity c
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_revMatchesAt_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔ String.Slice.Pattern.Model.RevMatchesAt pat.toSlice pos
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.minKey? = some km → (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.RingTheory.WittVector.Frobenius
/-- A key numerical identity needed for the proof of `WittVector.map_frobeniusPoly`.  -/
WittVector.map_frobeniusPoly.key₂ : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {n i j : ℕ},
  i ≤ n → j < p ^ (n - i) → j - multiplicity p (j + 1) + n = i + j + (n - i - multiplicity p (j + 1))
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivWithinAt_Ioi_iff_Ici`. -/
HasDerivWithinAt.Ici_of_Ioi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  HasDerivWithinAt f f' (Set.Ioi x) x → HasDerivWithinAt f f' (Set.Ici x) x
-- Init.Internal.Order.Basic
Lean.Order.coind_monotone_and : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ f₂ : α → Prop),
  Lean.Order.monotone f₁ → Lean.Order.monotone f₂ → Lean.Order.monotone fun x => f₁ x ∧ f₂ x
-- Mathlib.Algebra.Group.Defs
/-- Addition is commutative in a commutative additive magma.  -/
SubtractionCommMonoid.add_comm : ∀ {G : Type u} [self : SubtractionCommMonoid G] (a b : G), a + b = b + a
-- Mathlib.RepresentationTheory.Character
/-- The character of isomorphic representations is the same.  -/
FDRep.char_iso : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Monoid G] {V W : FDRep k G} (i : V ≅ W),
  V.character = W.character
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instPow_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], Colex.instPow_1 = inst
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.mk : Lean.Lsp.DocumentUri → Option Lean.Lsp.DeleteFile.Options → Option String → Lean.Lsp.DeleteFile
-- Init.System.FilePath
System.instCoeStringFilePath : Coe String System.FilePath
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The canonical cone over `diagram P` with point `P`.  -/
ProfiniteGrp.cone : (P : ProfiniteGrp.{u}) → CategoryTheory.Limits.Cone P.diagram
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorUnit_tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Dial C)).tgt = ⊤_ C
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedSymbolPriorities : Inhabited Lean.Meta.Grind.SymbolPriorities
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.HashMap.filter f m},
  (Std.HashMap.filter f m)[k] = m[k]
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (c.π.app j) (F.map f) = c.π.app j'
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_inter_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (f : Mathlib.Tactic.BicategoryLike.Atom₁)
  (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) (e_1 : Mathlib.Tactic.BicategoryLike.Mor₂)
  (f_1 : Mathlib.Tactic.BicategoryLike.Atom₁) (η_1 : Mathlib.Tactic.BicategoryLike.WhiskerLeft),
  (Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e f η =
      Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e_1 f_1 η_1) =
    (e = e_1 ∧ f = f_1 ∧ η = η_1)
-- Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
MeasureTheory.AEFinStronglyMeasurable.mk.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  [inst : TopologicalSpace β] [inst_1 : Zero β] (f f_1 : α → β) (e_f : f = f_1)
  (hf : MeasureTheory.AEFinStronglyMeasurable f μ) (a a_1 : α),
  a = a_1 → MeasureTheory.AEFinStronglyMeasurable.mk f hf a = MeasureTheory.AEFinStronglyMeasurable.mk f_1 ⋯ a_1
-- Init.Data.String.Slice
/-- Appends all the slices in a list of slices, in order.

Use `String.Slice.intercalate` to place a separator string between the strings in a list.

Examples:

* `String.Slice.join ["gr", "ee", "n"] = "green"`

* `String.Slice.join ["b", "", "l", "", "ue"] = "blue"`

* `String.Slice.join [] = ""`
 -/
String.Slice.join : List String.Slice → String
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prod_topology : ∀ {X Y : TopCat},
  (X ⨯ Y).str =
    TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst)) X.str ⊓
      TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd)) Y.str
-- Mathlib.Algebra.Category.BoolRing
/-- The underlying ring hom.  -/
BoolRing.Hom.hom' : {R : BoolRing} → {S : BoolRing} → R.Hom S → ↑R →+* ↑S
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- Given `h : F.IsEventuallyConstantFrom i₀`, this is the (limit) cocone for `F` whose
point is `F.obj i₀`.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom.cocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} → F.IsEventuallyConstantFrom i₀ → [CategoryTheory.IsFiltered J] → CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Category.Bipointed
bipointedToPointedFst_comp_forget : bipointedToPointedFst.comp (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed
-- Mathlib.Algebra.Notation.Support
Function.support_update_of_ne_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] [inst_1 : DecidableEq ι] (f : ι → M) (x : ι) {y : M},
  y ≠ 0 → Function.support (Function.update f x y) = insert x (Function.support f)
-- Mathlib.NumberTheory.PrimeCounting
Nat.prime_nth_prime : ∀ (n : ℕ), Nat.Prime (Nat.nth Nat.Prime n)
-- Mathlib.Analysis.Complex.Basic
Complex.restrictScalars_toSpanSingleton' : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (x : E),
  ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ x) =
    Complex.reCLM.smulRight x + Complex.I • Complex.imCLM.smulRight x
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform_idem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.mulDysonETransform e (Finset.mulDysonETransform e x) = Finset.mulDysonETransform e x
-- Init.Data.UInt.Basic
/-- Unsigned division for 8-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.div : UInt8 → UInt8 → UInt8
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_self : ∀ {a : ℤ}, a.fmod a = 0
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    Lean.Grind.Linarith.Expr.denote ctx lhs ≠ Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p ≠ 0
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_neg_one : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R), A ^ (-1) = A⁻¹
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.Iso.symm.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (I : X ≅ Y),
  I.symm = { hom := I.inv, inv := I.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Batteries.Data.List.Lemmas
List.insertP_nil : ∀ {α : Type u_1} (p : α → Bool) (a : α), List.insertP p a [] = [a]
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- Induction principle for finset families. To prove a statement for every finset family,
it suffices to prove it for
* the empty finset family.
* the finset family which only contains the empty finset.
* `ℬ ∪ {s ∪ {a} | s ∈ 𝒞}` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the
  ground type and `𝒜` and `ℬ` are families of finsets not containing `a`.
  Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you
  `𝒜 = ℬ ∪ {s ∪ {a} | s ∈ 𝒞}`, so that `ℬ = 𝒜.nonMemberSubfamily` and `𝒞 = 𝒜.memberSubfamily`.

This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.

See also `Finset.family_induction_on.`  -/
Finset.memberFamily_induction_on : ∀ {α : Type u_1} [inst : DecidableEq α] {p : Finset (Finset α) → Prop} (𝒜 : Finset (Finset α)),
  p ∅ →
    p {∅} →
      (∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (Finset.nonMemberSubfamily a 𝒜) → p (Finset.memberSubfamily a 𝒜) → p 𝒜) →
        p 𝒜
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_isLocal : RingHom.PropertyIsLocal @RingHom.FiniteType
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.countable_support : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  {f : α → G} [FirstCountableTopology G] [T1Space G], Summable f → (Function.support f).Countable
-- Mathlib.Algebra.Group.Defs
IsMulTorsionFree.pow_left_injective : ∀ {M : Type u_2} {inst : Monoid M} [self : IsMulTorsionFree M] ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun a => a ^ n
-- Mathlib.Data.Nat.ModEq
Nat.mod_modEq : ∀ (a n : ℕ), a % n ≡ a [MOD n]
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.overrideStatefulLspRequestHandler : String →
  Lean.Server.RequestHandlerCompleteness →
    (paramType : Type) →
      [Lean.FromJson paramType] →
        [Lean.Lsp.FileSource paramType] →
          (respType : Type) →
            [Lean.ToJson respType] →
              (stateType : Type) →
                [TypeName stateType] →
                  stateType →
                    (paramType → stateType → Lean.Server.RequestM (Lean.Server.LspResponse respType × stateType)) →
                      (Lean.Lsp.DidChangeTextDocumentParams → StateT stateType Lean.Server.RequestM Unit) → IO Unit
-- Mathlib.Topology.Category.TopPair
/-- Two maps of topological pairs being homotopic defines an equivalence relation.  -/
TopPair.Homotopic.equivalence : ∀ {X Y : TopPair}, Equivalence TopPair.Homotopic
-- Mathlib.Algebra.Algebra.Tower
Submodule.orderIsoOfAlgebraMapSurjective_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (h : Function.Surjective ⇑(algebraMap R S)) (N : Submodule S M),
  (Submodule.orderIsoOfAlgebraMapSurjective h) N = Submodule.restrictScalars R N
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_mul : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R), (I * J).radical = I.radical ⊓ J.radical
-- Lean.PrettyPrinter.Parenthesizer
/-- Adjust state and advance.  -/
Lean.PrettyPrinter.Parenthesizer.visitToken : Lean.PrettyPrinter.Parenthesizer
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertTimezone : Std.Time.TimeZone → Lean.MacroM (Lean.TSyntax `term)
-- Std.Sync.Mutex
/-- Waits until another thread calls `notifyOne` or `notifyAll`.  -/
Std.Condvar.wait : Std.Condvar → Std.BaseMutex → BaseIO Unit
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.irreducibleComponentι_apply : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X)
  [inst : AlgebraicGeometry.IsNoetherian X] (x : ↥(X.irreducibleComponent Z hZ)), (X.irreducibleComponentι Z hZ) x = ↑x
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensoring on the right, as a functor from `C` into endofunctors of `C`.

We later show this is a monoidal functor.
 -/
CategoryTheory.MonoidalCategory.tensoringRight : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Mathlib.Combinatorics.Graph.Basic
/-- **Alias** of `Graph.vertexSet_bouquet`. -/
Graph.bouquet_vertexSet : ∀ {α : Type u_1} {β : Type u_2} (v : α) (edgeSet : Set β), (Graph.bouquet v edgeSet).vertexSet = {v}
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.mk.sizeOf_spec : ∀ (eq : Bool) (lhs rhs : Nat.Internal.Linear.Expr),
  sizeOf { eq := eq, lhs := lhs, rhs := rhs } = 1 + sizeOf eq + sizeOf lhs + sizeOf rhs
-- Mathlib.Data.Nat.Sqrt
Nat.exists_mul_self' : ∀ (x : ℕ), (∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x
-- Mathlib.LinearAlgebra.Reflection
Module.invOn_reflection_of_mapsTo : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} {Φ : Set M} (h : f x = 2), Set.InvOn (⇑(Module.reflection h)) (⇑(Module.reflection h)) Φ Φ
-- Mathlib.Data.Part
Part.mem_bind : ∀ {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} {a : α} {b : β}, a ∈ f → b ∈ g a → b ∈ f.bind g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
/-- This map sends a pair `P`, `Q` of nonsingular points in affine coordinates on `W`
to a triple projectively equivalent to `![x(P) * x(Q), x(P) + x(Q), 1]`.

In more geometric terms, this is the map `Sym² W → Sym² ℙ¹ ≃ ℙ²` induced by `x : W → ℙ¹`.  -/
WeierstrassCurve.Affine.Point.sym2x : {R : Type u_1} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → W'.Point → W'.Point → Fin 3 → R
-- Mathlib.Data.PNat.Prime
PNat.fact_prime_three : Fact (PNat.Prime 3)
-- Mathlib.Data.Num.Bitwise
/-- Add an inactive bit at the end of a `SNum`. This mimics `ZNum.bit0`.  -/
SNum.bit0 : SNum → SNum
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.congr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  IsLocalMinOn f s a → f =ᶠ[nhdsWithin a s] g → a ∈ s → IsLocalMinOn g s a
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivWithinAt.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G},
  HasFDerivWithinAt f₂ f₂' s x → HasFDerivWithinAt (fun x => (f₂ x).1) (ContinuousLinearMap.fst 𝕜 F G ∘SL f₂') s x
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which antivary together, is unchanged by a permutation if and only if `f ∘ σ` and `g` antivary
together. Stated by permuting the entries of `f`.  -/
Antivary.sum_comp_perm_mul_eq_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Antivary f g → (∑ i, f (σ i) * g i = ∑ i, f i * g i ↔ Antivary (f ∘ ⇑σ) g)
-- Init.Data.Vector.Attach
Vector.unattach_attachWith : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector α n} {H : ∀ a ∈ xs, p a}, (xs.attachWith p H).unattach = xs