mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x i x_1 : ℤ),
  ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).inv.f i).f x_1 =
    CategoryTheory.CategoryStruct.id ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))
-- Mathlib.Topology.Homotopy.Equiv
Homeomorph.coe_toHomotopyEquiv : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  ⇑h.toHomotopyEquiv.toFun = ⇑h
-- Mathlib.Order.Filter.NAry
Filter.map₂_mono_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g₁ g₂ : Filter β},
  g₁ ≤ g₂ → Filter.map₂ m f g₁ ≤ Filter.map₂ m f g₂
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso_inv_iCycles_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C}
  (h : (K.extend e).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv
      (CategoryTheory.CategoryStruct.comp ((K.extend e).iCycles j') h) =
    CategoryTheory.CategoryStruct.comp (K.iCycles j) (CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv h)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_eq_getD : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β} {h' : a ∈ m}, m[a] = m.getD a fallback
-- Mathlib.Data.Nat.EvenOddRec
Nat.evenOddRec_zero : ∀ {P : ℕ → Sort u_1} (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  Nat.evenOddRec h0 h_even h_odd 0 = h0
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.maxDegree_of_subsingleton : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Subsingleton V], G.maxDegree = 0
-- Mathlib.GroupTheory.Coset.Basic
orbit_subgroup_eq_self_of_mem : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → MulAction.orbit (↥s) a = ↑s
-- Mathlib.Data.Matrix.Composition
Matrix.comp_map_map : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (R' : Type u_6)
  (M : Matrix I J (Matrix K L R)) (f : R → R'),
  (Matrix.comp I J K L R') (M.map fun M' => M'.map f) = ((Matrix.comp I J K L R) M).map f
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- **Alias** of `MeromorphicAt.MeromorphicOn.codiscreteWithin_setOfPred_ne_zero`.

---

Variant of the principle of isolated zeros, formulated in terms of orders: If `f` is nowhere locally
constant zero, then its zero set is discrete within its domain of meromorphicity.
 -/
MeromorphicAt.MeromorphicOn.codiscreteWithin_setOf_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  MeromorphicOn f U → (∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤) → ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ 0
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertIfNew_eq_insertIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), m.insertIfNew a b = m.insertIfNewₘ a b
-- Mathlib.FieldTheory.Isaacs
Field.nonempty_algHom_of_aeval_eq_zero_subset : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  {p | ∃ x, (Polynomial.aeval x) p = 0} ⊆ {p | ∃ y, (Polynomial.aeval y) p = 0} → Nonempty (E →ₐ[F] K)
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex that was constructed using `CWComplex.mkFiniteType` is of finite type.  -/
Topology.CWComplex.finiteType_mkFiniteType : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) → IsClosed A)
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C), Topology.RelCWComplex.FiniteType C
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.isSeparated_insert_of_notMem : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X},
  x ∉ s → (Metric.IsSeparated ε (insert x s) ↔ Metric.IsSeparated ε s ∧ ∀ y ∈ s, ε < edist x y)
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.map_eq_zero_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N) {m : M}, f m = 0 ↔ ∃ s, ↑s * m = 0
-- Mathlib.Data.List.Sublists
List.sublists'_nil : ∀ {α : Type u}, [].sublists' = [[]]
-- Lean.Util.PPExt
Lean.formatRawGoal : Lean.MVarId → Std.Format
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.exists_isPath : ∀ {V : Type u} {G : SimpleGraph V}, G.Preconnected → ∀ (u v : V), ∃ p, p.IsPath
-- Mathlib.Data.List.Sort
List.SortedLT.nodup : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT → l.Nodup
-- Mathlib.GroupTheory.Coxeter.Length
_private.Mathlib.GroupTheory.Coxeter.Length.0.CoxeterSystem.isReduced_take_and_drop : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B},
  cs.IsReduced ω → ∀ (j : ℕ), cs.IsReduced (List.take j ω) ∧ cs.IsReduced (List.drop j ω)
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_add : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R) (n : ℕ),
  WittVector.init n (x + y) = WittVector.init n (WittVector.init n x + WittVector.init n y)
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- Given a sequence of continuous linear maps which converges pointwise and for which the
domain is barrelled, the Banach-Steinhaus theorem is used to guarantee that the limit map
is a *continuous* linear map as well.

This actually works for any *countably generated* filter instead of `atTop : Filter ℕ`,
but the proof ultimately goes back to sequences.  -/
WithSeminorms.continuousLinearMapOfTendsto : {α : Type u_1} →
  {κ : Type u_3} →
    {𝕜₁ : Type u_4} →
      {𝕜₂ : Type u_5} →
        {E : Type u_6} →
          {F : Type u_7} →
            [inst : NontriviallyNormedField 𝕜₁] →
              [inst_1 : NontriviallyNormedField 𝕜₂] →
                {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
                  [RingHomIsometric σ₁₂] →
                    [inst_3 : AddCommGroup E] →
                      [inst_4 : AddCommGroup F] →
                        [inst_5 : Module 𝕜₁ E] →
                          [inst_6 : Module 𝕜₂ F] →
                            [inst_7 : UniformSpace E] →
                              [inst_8 : UniformSpace F] →
                                [IsUniformAddGroup E] →
                                  [IsUniformAddGroup F] →
                                    [ContinuousSMul 𝕜₁ E] →
                                      [BarrelledSpace 𝕜₁ E] →
                                        [ContinuousSMul 𝕜₂ F] →
                                          {q : SeminormFamily 𝕜₂ F κ} →
                                            WithSeminorms q →
                                              [T2Space F] →
                                                {l : Filter α} →
                                                  [l.IsCountablyGenerated] →
                                                    [l.NeBot] →
                                                      (g : α → E →SL[σ₁₂] F) →
                                                        {f : E → F} →
                                                          Filter.Tendsto (fun n x => (g n) x) l (nhds f) → E →SL[σ₁₂] F
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.coe_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {S : Type u_5} [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M] [inst_10 : IsScalarTower S (↥F) M]
  (s : S) (x : ↥(F.extendRight M)), ↑(s • x) = s • ↑x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtDHashMap.Const.unitOfList l = Std.ExtDHashMap.Const.insertManyIfNewUnit ∅ l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α}
  (h₁ : (List.map Prod.fst l).contains k = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) = true},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKey k h' = t.getKey k ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- A `BitVec` variable, referred to through an index.
 -/
Std.Tactic.BVDecide.BVExpr.var : {w : ℕ} → ℕ → Std.Tactic.BVDecide.BVExpr w
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is filtered or empty, and we have a right adjoint functor `R : C ⥤ D`, then `D` is
filtered or empty.  -/
CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D) [R.IsRightAdjoint],
  CategoryTheory.IsFilteredOrEmpty D
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ},
  MvPowerSeries.IsWeightedHomogeneous w f p ↔ f = (MvPowerSeries.weightedHomogeneousComponent w p) f
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instCanLiftMultiplicativeExpNeOfNat : ∀ {M : Type u_4}, CanLift (WithZero (Multiplicative M)) M WithZero.exp fun x => x ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
_private.Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct.0.CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan.match_1_3.eq_1 : ∀ (motive : (i j : CategoryTheory.Limits.WalkingPair) → i ≠ j → Sort u_1)
  (hij : CategoryTheory.Limits.WalkingPair.left ≠ CategoryTheory.Limits.WalkingPair.right)
  (h_1 :
    (hij : CategoryTheory.Limits.WalkingPair.left ≠ CategoryTheory.Limits.WalkingPair.right) →
      motive CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.WalkingPair.right hij)
  (h_2 :
    (hij : CategoryTheory.Limits.WalkingPair.right ≠ CategoryTheory.Limits.WalkingPair.left) →
      motive CategoryTheory.Limits.WalkingPair.right CategoryTheory.Limits.WalkingPair.left hij),
  (match CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.WalkingPair.right, hij with
    | CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.WalkingPair.right, hij => h_1 hij
    | CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WalkingPair.left, hij => h_2 hij) =
    h_1 hij
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.threeAPFree_image_sphere : ∀ {n d k : ℕ}, ThreeAPFree ↑(Finset.image (⇑(Behrend.map (2 * d - 1))) (Behrend.sphere n d k))
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_insert_zero : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), PrimeSpectrum.zeroLocus (insert 0 s) = PrimeSpectrum.zeroLocus s
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a...b` by
varying the lower bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a`, the statement holds for the empty range `a...b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, the
statement holds for nonempty ranges `a...b` if it holds for the smaller range
`(a + 1)...b`.

The following is an example reproving `length_toList_rco`.

```
example (a b : Int) : (a...b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_rco_left
  case base =>
    simp [Int.toList_rco_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step =>
    simp only [Int.toList_rco_eq_cons, List.length_cons, *]; omega
``` -/
Int.induct_rco_left : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a → motive a b) → (∀ (a b : ℤ), a < b → motive (a + 1) b → motive a b) → ∀ (a b : ℤ), motive a b
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.Additive.of_isZero : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}, CategoryTheory.Limits.IsZero F → F.Additive
-- Mathlib.GroupTheory.Nilpotent
/-- n-ary products of nilpotent groups are nilpotent.  -/
Group.isNilpotent_pi : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [Finite η] [∀ (i : η), Group.IsNilpotent (Gs i)],
  Group.IsNilpotent ((i : η) → Gs i)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.zero : Nat.Primrec' fun x => 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.Equation.baseChange : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) {x y : A}, (W.baseChange A).Equation x y → (W.baseChange B).Equation (f x) (f y)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.vcomp_right : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g)
  (θ₁ θ₂ : CategoryTheory.FreeBicategory.Hom₂ g h) (a_1 : CategoryTheory.FreeBicategory.Rel θ₁ θ₂),
  CategoryTheory.FreeBicategory.Rel.below a_1 → motive θ₁ θ₂ a_1 → CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
lt_of_mabs_lt : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a b : α}, |a|ₘ < b → a < b
-- Lean.Server.Requests
Lean.Language.SnapshotTree.collectMessagesInRange : Lean.Language.SnapshotTree → Lean.Syntax.Range → Lean.Server.ServerTask Lean.MessageLog
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.restr_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t),
  ↑h.restr.symm = ↑e.symm
-- Init.Prelude
/-- The homogeneous version of `HOrElse`: `a <|> b : α` where `a b : α`.
Because `b` is "lazy" in this notation, it is passed as `Unit → α` to the
implementation so it can decide when to evaluate it.
 -/
OrElse : Type u → Type u
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The empty set is cospherical.  -/
EuclideanGeometry.cospherical_empty : ∀ {P : Type u_2} [inst : MetricSpace P] [Nonempty P], EuclideanGeometry.Cospherical ∅
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_commonIntTangents_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s₁ s₂ : EuclideanGeometry.Sphere P},
  as ∈ s₁.commonIntTangents s₂ ↔ as ∈ s₁.commonTangents s₂ ∧ ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
-- Lean.Parser.Basic
Lean.Parser.setLhsPrec : ℕ → Lean.Parser.Parser
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The downward **local LYM inequality**, with cancelled denominators. `𝒜` takes up less of `α^(r)`
(the finsets of card `r`) than `∂𝒜` takes up of `α^(r - 1)`.  -/
Finset.card_mul_le_card_shadow_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  Set.Sized r ↑𝒜 → 𝒜.card * r ≤ 𝒜.shadow.card * (Fintype.card α - r + 1)
-- Mathlib.Topology.Category.TopPair
/-- The proof that the homotopies fit into a commutative square with the maps of the pairs.  -/
TopPair.Homotopy.w_apply : ∀ {X Y : TopPair} {f g : X ⟶ Y} (self : TopPair.Homotopy f g)
  (x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj TopPair.snd TopCat.I)),
  self.fst (TopCat.I.homeomorph x.2, (CategoryTheory.ConcreteCategory.hom TopPair.map) x.1) =
    (CategoryTheory.ConcreteCategory.hom TopPair.map) (self.snd (TopCat.I.homeomorph x.2, x.1))
-- Mathlib.Order.Hom.BoundedLattice
/-- `id` as a `SupBotHom`.  -/
SupBotHom.id : (α : Type u_2) → [inst : Max α] → [inst_1 : Bot α] → SupBotHom α α
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.ae_of_ae_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) {μ : MeasureTheory.Measure α} {P : α → Prop},
  (∀ᵐ (x : α) ∂μ.trim hm, P x) → ∀ᵐ (x : α) ∂μ, P x
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_le_iff_of_le_aleph0 : ∀ {c c' : Cardinal.{u}}, c ≤ Cardinal.aleph0 → (Cardinal.toENat c ≤ Cardinal.toENat c' ↔ c ≤ c')
-- Init.Data.Random
instRandomGenStdGen : RandomGen StdGen
-- Mathlib.RingTheory.Multiplicity
emultiplicity_lt_iff_not_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, emultiplicity a b < ↑k ↔ ¬a ^ k ∣ b
-- Aesop.Forward.State
Aesop.ForwardState.mk.inj : ∀ {ruleStates : Lean.PHashMap Aesop.RuleName Aesop.RuleState}
  {hyps : Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex))}
  {patSubsts : Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution))}
  {ruleStates_1 : Lean.PHashMap Aesop.RuleName Aesop.RuleState}
  {hyps_1 : Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex))}
  {patSubsts_1 : Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution))},
  { ruleStates := ruleStates, hyps := hyps, patSubsts := patSubsts } =
      { ruleStates := ruleStates_1, hyps := hyps_1, patSubsts := patSubsts_1 } →
    ruleStates = ruleStates_1 ∧ hyps = hyps_1 ∧ patSubsts = patSubsts_1
-- Init.Data.String.Termination
String.Pos.le_iff_remainingBytes_le : ∀ {s : String} (p q : s.Pos), p ≤ q ↔ q.remainingBytes ≤ p.remainingBytes
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- See Note [custom simps projection].  -/
LinearMap.BilinForm.Isometry.Simps.apply : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} → {B₂ : LinearMap.BilinForm R M₂} → (B₁ →bᵢ B₂) → M₁ → M₂
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A commuting square induces a morphism of kernels.  -/
CategoryTheory.Limits.kernel.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {X' Y' : C} →
              (f' : X' ⟶ Y') →
                [inst_3 : CategoryTheory.Limits.HasKernel f'] →
                  (p : X ⟶ X') →
                    (q : Y ⟶ Y') →
                      CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f' →
                        (CategoryTheory.Limits.kernel f ⟶ CategoryTheory.Limits.kernel f')
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.CreatesColimitsOfShape J F], CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiableAt_ofComplex : ∀ {z : ℂ}, 0 < z.im → MDiffAt ↑UpperHalfPlane.ofComplex z
-- Mathlib.Algebra.Module.Equiv.Basic
/-- If a linear map has an inverse, it is a linear equivalence.  -/
LinearEquiv.ofLinearMap : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (f : M →ₛₗ[σ₁₂] M₂) →
                              (g : M₂ →ₛₗ[σ₂₁] M) → f ∘ₛₗ g = LinearMap.id → g ∘ₛₗ f = LinearMap.id → M ≃ₛₗ[σ₁₂] M₂
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.extendFunctor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : HomologicalComplex C c} (φ : X ⟶ Y),
  (e.extendFunctor C).map φ = HomologicalComplex.extendMap φ e
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct X] [∀ (i : ι), CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)]
  (s :
    {i j : ι} →
      i ≠ j →
        CategoryTheory.Limits.PullbackCone (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j))
  (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij))
  (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt),
  CategoryTheory.Limits.CoproductDisjoint X
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `J` is `u`-small, `CommSemiRingCat.{u}` has limits of shape `J`.  -/
CommSemiRingCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J CommSemiRingCat
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.map_surjective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  (self : IsAdjoinRoot S f), Function.Surjective ⇑self.map
-- Mathlib.Analysis.Normed.Group.Basic
preimage_add_ball : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E) (r : ℝ),
  (fun x => b + x) ⁻¹' Metric.ball a r = Metric.ball (a - b) r