mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ')
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (y : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η).app S).snd.app y =
    η.right.app (S.snd.obj y)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- C2.1.3 in [Elephant]  -/
CategoryTheory.Presieve.isSheafFor_iff_generate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.IsSheafFor P R ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.generate R).arrows
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.isRoot_of_eval₂_map_eq_zero : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ {r : R}, Polynomial.eval₂ f (f r) p = 0 → p.IsRoot r
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The odd part of the Hurwitz zeta function, i.e. the meromorphic function of `s` which agrees
with `1 / 2 * ∑' (n : ℤ), sign (n + a) / |n + a| ^ s` for `1 < re s`  -/
HurwitzZeta.hurwitzZetaOdd : UnitAddCircle → ℂ → ℂ
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mulInvariantVectorField.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] (v : GroupLieAlgebra I G) (g : G),
  mulInvariantVectorField v g = ((mfderiv% fun x => g * x) 1) v
-- Mathlib.Analysis.Analytic.Basic
/-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as
a power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a neighborhood of `0`.  -/
HasFPowerSeriesAt : {𝕜 : 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] → (E → F) → FormalMultilinearSeries 𝕜 E F → E → Prop
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.continuous_integral_continuousMap : ∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] [inst_2 : MeasurableSpace X]
  [inst_3 : OpensMeasurableSpace X] {F : Type u_3} [inst_4 : FunLike F X ℝ] [ContinuousMapClass F X ℝ] (f : F),
  Continuous fun μ => ∫ (x : X), f x ∂↑μ
-- Init.Data.List.Lemmas
List.filterMap_cons_none : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {a : α} {l : List α},
  f a = none → List.filterMap f (a :: l) = List.filterMap f l
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'_inv_app_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = (X.XIsoOfEq hk).inv
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.polyToMatrix_cornerAddX : ∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  (M : Matrix m m S) [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] (k : m) [inst_4 : Fintype n]
  (f : S →+* Matrix n n R), f.polyToMatrix (Algebra.Norm.Transitivity.cornerAddX M k k k) = (-f (M k k)).charmatrix
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.filterMapₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β)
  (f : (a : α) → β a → Option (δ a)),
  m.filterMapₘ f =
    ⟨Std.DHashMap.Internal.withComputedSize
        (Std.DHashMap.Internal.updateAllBuckets (↑m).buckets fun l => Std.DHashMap.Internal.AssocList.filterMap f l),
      ⋯⟩
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.coe_srangeRestrict : ∀ {M : Type u_1} [inst : Add M] {N : Type u_5} [inst_1 : Add N] (f : M →ₙ+ N) (x : M), ↑(f.srangeRestrict x) = f x
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.abs : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [inst : NormedAddCommGroup β]
  [inst_1 : Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f : α → β},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun a => |f a|) μ
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In a linearly ordered semiring with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`),
sums of squares are non-negative.
 -/
IsSumSq.nonneg : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {s : R},
  IsSumSq s → 0 ≤ s
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_set_normalizer_iff'' : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G} {g : G},
  g ∈ AddSubgroup.normalizer S ↔ ∀ (h : G), h ∈ S ↔ -g + h + g ∈ S
-- Lean.Linter.UnusedVariables
/-- Visit a `PersistentHashMap.Entry`, collecting all fvars in it into `fvarUses`  -/
_private.Lean.Linter.UnusedVariables.0.Lean.Linter.UnusedVariables.visitAssignments.visitEntry : IO.Ref (Std.HashSet USize) →
  IO.Ref (Std.HashSet Lean.FVarId) →
    Lean.PersistentHashMap.Entry Lean.MVarId Lean.Expr (Lean.PersistentHashMap.Node Lean.MVarId Lean.Expr) →
      Lean.MonadCacheT Lean.Expr Unit IO Unit
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.deleteElem_eq_self : ∀ {α : Type u_1} {M : Matroid α} {e : α}, e ∉ M.E → M.delete {e} = M
-- Mathlib.GroupTheory.OrderOfElement
/-- If each prime factor of
`addOrderOf y` has higher multiplicity in `addOrderOf x`, and `x` commutes with `y`,
then `x + y` has the same order as `x`.  -/
AddCommute.addOrderOf_add_eq_left_of_forall_prime_mul_dvd : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
  AddCommute x y →
    IsOfFinAddOrder x →
      (∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf y → p * addOrderOf y ∣ addOrderOf x) → addOrderOf (x + y) = addOrderOf x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.IsIso g] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
/-- The multiplicative action on an affine subspace corresponding to applying the action to every
element.

This is available as an instance in the `Pointwise` locale.

TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineSubspace k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`.  -/
AffineSubspace.mulAction : {M : Type u_1} →
  {k : Type u_2} →
    {V : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : Monoid M] →
              [inst_4 : DistribMulAction M V] → [SMulCommClass M k V] → MulAction M (AffineSubspace k V)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_algHomOfDvd : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hgf : g ∣ f),
  ⇑(AdjoinRoot.algHomOfDvd R f g hgf) = ⇑(AdjoinRoot.liftAlgHom f (Algebra.ofId S (AdjoinRoot g)) (AdjoinRoot.root g) ⋯)
-- Init.System.FilePath
System.FilePath.mk.sizeOf_spec : ∀ (toString : String), sizeOf { toString := toString } = 1 + sizeOf toString
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instDistribSMulOfMulActionHomClass : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Nonempty ι] →
                    [inst_5 : (i : ι) → AddZeroClass (G i)] →
                      [inst_6 : (i : ι) → DistribSMul R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] →
                          [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] →
                            DistribSMul R (DirectLimit G f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).minKey?.isSome = true
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
HomotopyCategory.mappingConeCompTriangleh_distinguished : ∀ {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₃)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C],
  CochainComplex.mappingConeCompTriangleh f g ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMulActionOfContinuousConstSMul : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_3} →
      {M : Type u_5} →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : Monoid R] → [inst_3 : MulAction R M] → [ContinuousConstSMul R M] → MulAction R C(α, M)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The associator isomorphism: `(f ≫ g) ≫ h ≅ f ≫ g ≫ h`  -/
CategoryTheory.Bicategory.termα_ : Lean.ParserDescr
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.leftInverse_symm : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (e : A ≃⋆* B),
  Function.LeftInverse ⇑e.symm ⇑e
-- Mathlib.GroupTheory.Transfer
Subgroup.leftTransversals.smul_diff_smul : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (S T : H.LeftTransversal) [inst_2 : H.FiniteIndex] (g : G),
  Subgroup.leftTransversals.diff ϕ (g • S) (g • T) = Subgroup.leftTransversals.diff ϕ S T
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Nodup.notMem : ∀ {α : Type u_1} {s : Multiset α} {a : α}, (a ::ₘ s).Nodup → a ∉ s
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Colex.wellFoundedLT_of_finite : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [Finite α] [inst_3 : LT N] [WellFoundedLT N],
  WellFoundedLT (Colex (α →₀ N))
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.isHamiltonianCycle_rotate : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a v : α} {p : G.Walk a a} (hv : v ∈ p.support),
  (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
-- Mathlib.CategoryTheory.PEmpty
CategoryTheory.instIsEmptyDiscrete : ∀ (α : Type u_1) [IsEmpty α], IsEmpty (CategoryTheory.Discrete α)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If ∠ABC = 0, then (dist A C) = abs ((dist A B) - (dist B C)).  -/
EuclideanGeometry.dist_eq_abs_sub_dist_of_angle_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = 0 → dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|
-- Lean.Meta.Tactic.Grind.Beta
_private.Lean.Meta.Tactic.Grind.Beta.0.Lean.Meta.Grind.isPropagateBetaTarget.go : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.instNegIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Preadditive C] → {X Y : C} → Neg (X ≅ Y)
-- Mathlib.Analysis.Analytic.Composition
/-- Source set in the change of variables to compute the composition of partial sums of formal
power series.
See also `comp_partialSum`.  -/
FormalMultilinearSeries.compPartialSumSource : ℕ → ℕ → ℕ → Finset ((n : ℕ) × (Fin n → ℕ))
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mem_range_embedding_iff' : ∀ {n : ℕ} (c : Composition n) {j : Fin n} {i : Fin c.length}, j ∈ Set.range ⇑(c.embedding i) ↔ i = c.index j
-- Mathlib.Algebra.Module.FinitePresentation
LinearEquiv.finitePresentation_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N),
  Module.FinitePresentation R M ↔ Module.FinitePresentation R N
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.whiskerLeft_apply : ∀ {R : Type u} [inst : CommSemiring R] (L : SemimoduleCat R) {M N : SemimoduleCat R} (f : M ⟶ N) (l : ↑L) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f)) (l ⊗ₜ[R] m) =
    l ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom f) m
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteCoproducts F] →
            (J : Type w) → [Finite J] → CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance
`< r` of a point in the other set.  -/
Metric.exists_dist_lt_of_hausdorffDist_lt : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α} {r : ℝ},
  x ∈ s → Metric.hausdorffDist s t < r → Metric.hausdorffEDist s t ≠ ⊤ → ∃ y ∈ t, dist x y < r
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- A Turing machine "statement" is just a command to either move
left or right, or write a symbol on the tape.  -/
Turing.TM0.Stmt : Type u_1 → Type u_1
-- Mathlib.Order.Bounds.Basic
glb_Ioi_eq_self_or_Ioi_eq_Ici : ∀ {γ : Type u_3} [inst : PartialOrder γ] {j : γ} (i : γ), IsGLB (Set.Ioi i) j → j = i ∨ Set.Ioi i = Set.Ici j
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.printDefLike : String →
  Lean.Name →
    List Lean.Name →
      Lean.Expr → Lean.Expr → optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe → Lean.CoreM Lean.MessageData
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- **Alias** of `SimpleGraph.isBridge_iff_not_isEdgeReachable_two`.

---

An edge is a bridge iff its endpoints are not 2-edge-reachable.

The forward direction of this is true without assuming `u` and `v` are adjacent.
See `IsBridge.not_isEdgeReachable_two`.  -/
SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Adj u v → (G.IsBridge s(u, v) ↔ ¬G.IsEdgeReachable 2 u v)
-- Mathlib.Topology.Sets.Compacts
exists_positiveCompacts_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [LocallyCompactSpace α] {U : Set α}, IsOpen U → U.Nonempty → ∃ K, ↑K ⊆ U
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.directionOfNonempty.eq_1 : ∀ {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] {s : AffineSubspace k P} (h : (↑s).Nonempty),
  AffineSubspace.directionOfNonempty h = { carrier := ↑s -ᵥ ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the bottom and `𝟙 X` on the top is a pushout square.  -/
CategoryTheory.IsPushout.zero_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id X) 0 0 0
-- Init.Data.Rat.Lemmas
Rat.zero_den : Rat.den 0 = 1
-- Mathlib.Data.Fintype.Card
/-- A custom induction principle for fintypes. The base case is a subsingleton type,
and the induction step is for non-trivial types, and one can assume the hypothesis for
smaller types (via `Fintype.card`).

The major premise is `Fintype α`, so to use this with the `induction` tactic you have to give a name
to that instance and use that name.
 -/
Fintype.induction_subsingleton_or_nontrivial : ∀ {P : (α : Type u_4) → [Fintype α] → Prop} (α : Type u_4) [inst : Fintype α],
  (∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α) →
    (∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
        (∀ (β : Type u_4) [inst_2 : Fintype β], Fintype.card β < Fintype.card α → P β) → P α) →
      P α
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_unsat : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  p.isUnsatDiseq_k = true → Int.Internal.Linear.Poly.denote' ctx p ≠ 0 → False
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam.eq_1 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), Metric.diam s = (Metric.ediam s).toReal
-- Qq.AssertInstancesCommute
Qq.termAssumeInstancesCommute'_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Center
Set.addCenter_pi : ∀ {ι : Type u_2} {A : ι → Type u_3} [inst : (i : ι) → Add (A i)],
  Set.addCenter ((i : ι) → A i) = Set.univ.pi fun i => Set.addCenter (A i)
-- Mathlib.Data.NNRat.Defs
NNRat.num_one : NNRat.num 1 = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The identity functor on `C`, viewed as a functor from `C` to its
monoidal opposite, upgraded to a braided functor.  -/
CategoryTheory.MonoidalOpposite.instBraidedMopFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.mopFunctor C).Braided
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] [inst_2 : Group E]
  [IsTopologicalGroup E] [inst_4 : Group X] {f : E →* X},
  Topology.IsQuotientMap ⇑f → IsDiscrete ↑f.ker → IsQuotientCoveringMap ⇑f ↥f.ker
-- Mathlib.Data.Part
Part.bind_eq_bind : ∀ {α β : Type u_4} (f : Part α) (g : α → Part β), f >>= g = f.bind g
-- Mathlib.Data.Nat.Factorization.Basic
Nat.exists_factorization_lt_of_lt : ∀ {a b : ℕ}, a ≠ 0 → a < b → ∃ p, a.factorization p < b.factorization p
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_bsup : ∀ {ι : Type u} (r r' : ι → ι → Prop) [inst : IsWellOrder ι r] [inst_1 : IsWellOrder ι r'] (f : ι → Ordinal.{max u v}),
  (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').bsup (Ordinal.bfamilyOfFamily' r' f)
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence.  -/
CoalgEquivClass.instCoeToCoalgEquiv : {F : Type u_5} →
  {R : Type u_6} →
    {A : Type u_7} →
      {B : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : AddCommMonoid B] →
              [inst_3 : Module R A] →
                [inst_4 : Module R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] →
                      [inst_7 : EquivLike F A B] → [CoalgEquivClass F R A B] → CoeHead F (A ≃ₗc[R] B)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.isTrivial : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_iff_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  a ∈ t ↔ (Std.DTreeMap.Const.get? t a).isSome = true
-- Mathlib.RingTheory.LaurentSeries
RatFunc.single_one_eq_pow : ∀ {R : Type u_2} [inst : Semiring R] (n : ℕ), (HahnSeries.single ↑n) 1 = (HahnSeries.single 1) 1 ^ n
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.eq_of_le_of_card_ge : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [Finite ↥K], H ≤ K → Nat.card ↥K ≤ Nat.card ↥H → H = K
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is strictly monotone on a neighborhood of `a`
and the closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is
continuous at `a`.  -/
StrictMonoOn.continuousAt_of_closure_image_mem_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α}, StrictMonoOn f s → s ∈ nhds a → closure (f '' s) ∈ nhds (f a) → ContinuousAt f a
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonneg_of_mul_nonpos_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R]
  [AddRightReflectLE R] {a b : R}, a * b ≤ 0 → b < 0 → 0 ≤ a
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.fun_vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableVAdd₂ M X],
  Measurable f → Measurable g → Measurable fun i => f i +ᵥ g i
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.add : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x y : S},
  f.IsIntegralElem x → f.IsIntegralElem y → f.IsIntegralElem (x + y)
-- Mathlib.Data.Finset.Max
Finset.min'_le : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s), s.min' ⋯ ≤ x
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
/-- **Alias** of the reverse direction of `TwoSidedIdeal.one_mem_iff`. -/
TwoSidedIdeal.one_mem : ∀ {R : Type u_2} [inst : NonAssocRing R] (I : TwoSidedIdeal R), I = ⊤ → 1 ∈ I
-- Mathlib.Data.Quot
Quotient.map'_mk'' : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β) (h : ∀ (a b : α), s₁ a b → s₂ (f a) (f b))
  (x : α), Quotient.map' f h (Quotient.mk'' x) = Quotient.mk'' (f x)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingCoeff.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.trailingCoeff = p.coeff p.natTrailingDegree
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
/-- Composition of an open partial homeomorphism and its inverse is equivalent to the restriction of
the identity to the source  -/
OpenPartialHomeomorph.self_trans_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.trans e.symm ≈ OpenPartialHomeomorph.ofSet e.source ⋯
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.subsingleton_of_subsingleton : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Subsingleton n],
  Subsingleton (Matrix.SpecialLinearGroup n R)
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_pure : ∀ {α : Type u} [uniformSpace : UniformSpace α] {a : α}, Cauchy (pure a)
-- Init.Prelude
Subtype.mk : {α : Sort u} → {p : α → Prop} → (val : α) → p val → Subtype p