mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.symmetry'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) h) =
    h
-- Mathlib.Topology.Algebra.Module.Star
continuous_decomposeProdAdjoint : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousStar A]
  [ContinuousConstSMul R A], Continuous ⇑(StarModule.decomposeProdAdjoint R A)
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand.congr_simp : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p p_1 : ℕ) (e_p : p = p_1) (hp : p ≠ 0),
  MvPowerSeries.expand p hp = MvPowerSeries.expand p_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- A `Fan` gives a `Cofan` in the opposite category.  -/
CategoryTheory.Limits.Fan.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} → {Z : α → C} → CategoryTheory.Limits.Fan Z → CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.instIsPushout' : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : CommMonoid M] [inst_8 : Algebra S B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower R S B] [Algebra.IsPushout R A S B],
  Algebra.IsPushout R (MonoidAlgebra A M) S (MonoidAlgebra B M)
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState.mk : ℕ → ℕ → Std.BarrierState✝
-- Mathlib.Data.Multiset.Count
Multiset.count_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α) (s : Multiset α),
  Multiset.count a (b ::ₘ s) = Multiset.count a s + if a = b then 1 else 0
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.instModule : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} → [inst : Semiring R] → [inst_1 : Semiring S] → [Module R S] → Module R (AddMonoidAlgebra S M)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.iInf_eq_zero_iff : ∀ {ι : Sort u_1} {f : ι → Cardinal.{u_2}}, ⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_reProdIm : ∀ (s t : Set ℝ), frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_inv_inv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [inst : Inv γ],
  Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.isIso_π_terminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [inst_2 : CategoryTheory.Limits.HasTerminal J] (F : CategoryTheory.Functor J C)
  [inst_3 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F (⊤_ J))
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.ext : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂},
  (∀ (x : M), e x = e' x) → e = e'
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instSigmaFiniteForallVolume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : ι → Type u_4} [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume], MeasureTheory.SigmaFinite MeasureTheory.volume
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_union : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω},
  s.Finite →
    Disjoint t u →
      (ProbabilityTheory.uniformOn s) (t ∪ u) = (ProbabilityTheory.uniformOn s) t + (ProbabilityTheory.uniformOn s) u
-- Mathlib.NumberTheory.PythagoreanTriples
_private.Mathlib.NumberTheory.PythagoreanTriples.0.coprime_sq_sub_sq_add_of_even_odd : ∀ {m n : ℤ}, m.gcd n = 1 → m % 2 = 0 → n % 2 = 1 → (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
-- Init.Data.Int.Order
Int.le_antisymm_iff : ∀ {a b : ℤ}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.of_equivalence : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {J' : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} J'] (e : J ≌ J'),
  CategoryTheory.IsCardinalFiltered J' κ
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.goodδ.congr_simp : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  Besicovitch.goodδ E = Besicovitch.goodδ E
-- Mathlib.Algebra.Star.Module
star_intCast_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StarAddMonoid M] (n : ℤ) (x : M), star (↑n • x) = ↑n • star x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.isLowerSet_toLowerSet_preimage : ∀ {α : Type u_1} [inst : Preorder α] {s : Set (Topology.WithLowerSet α)},
  IsLowerSet (⇑Topology.WithLowerSet.toLowerSet ⁻¹' s) ↔ IsOpen s
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddGroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [AddGroup Y] → AddGroup (LocallyConstant X Y)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.factorThru_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P X E : C} [inst_1 : CategoryTheory.Projective P] (f : P ⟶ X)
  (e : E ⟶ X) [inst_2 : CategoryTheory.Epi e],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.factorThru f e) e = f
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquiv_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D],
  (CategoryTheory.Equivalence.symmEquiv C D).inverse = CategoryTheory.Equivalence.symmEquivInverse C D
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `EMetricSpace` instance on the product of two emetric spaces, using the `L^p`
edistance, and having as uniformity the product uniformity.  -/
WithLp.instProdEMetricSpace : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) → [hp : Fact (1 ≤ p)] → [EMetricSpace α] → [EMetricSpace β] → EMetricSpace (WithLp p (α × β))
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_sub : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddGroup (G i)] [inst_3 : ∀ (i : ι), AddSubgroupClass (S i) (G i)]
  (i : ι) (r s : G i),
  RestrictedProduct.single A i (r - s) = RestrictedProduct.single A i r - RestrictedProduct.single A i s
-- Mathlib.Algebra.Lie.Normalizer
LieSubalgebra.coe_normalizer_eq_normalizer : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L), ↑H.toLieSubmodule.normalizer = H.normalizer.toSubmodule
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₀_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C) {X_1 Y : Fin 1} (x : X_1 ⟶ Y),
  (CategoryTheory.ComposableArrows.mk₀ X).map x = CategoryTheory.CategoryStruct.id X
-- Mathlib.Data.Set.Countable
Set.not_countable_univ_iff : ∀ {α : Type u}, ¬Set.univ.Countable ↔ Uncountable α
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- **Alias** of `AlgebraicGeometry.tilde.toStalk`.

---

If `x` is a point of `Spec R`, this is the morphism of `R`-modules from `M` to the stalk of
`M^~` at `x`.
 -/
ModuleCat.Tilde.toStalk : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)) →
      ModuleCat.of ↑R ↑M ⟶ ModuleCat.of ↑R ↑((AlgebraicGeometry.tilde M).presheaf.stalk x)
-- Mathlib.Analysis.Calculus.MeanValue
/-- If a function has zero Fréchet derivative at every point of a convex set,
then it is a constant on this set.  -/
Convex.is_const_of_fderivWithin_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E} {x y : E},
  Convex ℝ s → DifferentiableOn 𝕜 f s → (∀ x ∈ s, fderivWithin 𝕜 f s x = 0) → x ∈ s → y ∈ s → f x = f y
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.right.sizeOf_spec : ∀ {ι : Type v} [inst : SizeOf ι] (i j : ι), sizeOf (CategoryTheory.Pairwise.Hom.right i j) = 1 + sizeOf i + sizeOf j
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_trim : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Type u_5} {m m0 : MeasurableSpace X}
  {μ : MeasureTheory.Measure X} (hm : m ≤ m0) {f : X → E},
  MeasureTheory.StronglyMeasurable f →
    ∀ {s : Set X}, MeasurableSet s → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y),
  AlgebraicGeometry.AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 => CompactSpace ↥X) f ↔
    QuasiSeparatedSpace ↥X
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.t1Space : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [ContinuousAdd G], IsClosed {0} → T1Space G
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_5} {x : MeasurableSpace γ}
  {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable g ν →
    MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [AlgebraicGeometry.IsProper g],
  AlgebraicGeometry.IsProper (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsProper f
-- Init.Data.Option.Array
Option.toArray_join : ∀ {α : Type u_1} {o : Option (Option α)}, o.join.toArray = Array.flatMap Option.toArray o.toArray
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) {hc : k' ∈ m.modify k f},
  (m.modify k f)[k'] = if heq : (k == k') = true then f m[k] else m[k']
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.range_eq_univ : ∀ {𝕜 : 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) [I.Boundaryless],
  Set.range ↑I = Set.univ
-- Lean.Compiler.IR.Basic
Lean.IR.instReprArg.repr : Lean.IR.Arg → ℕ → Std.Format
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.instAddCancelCommMonoid : {α : Type u_1} → AddCancelCommMonoid (Multiset α)
-- Init.Data.Vector.Attach
Vector.toList_unattach : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n}, xs.unattach.toList = xs.toList.unattach
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_smul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A)
  {α : Type u_4} [inst_2 : SMul α A] [inst_3 : SMulMemClass σ α A] (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x)
  (m : α), (m • c).deg = c.deg
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.castAdd m) (Finset.Icc i j) = Finset.Icc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_lt_iff`.

---

The edist to a set is `< r` iff there exists a point in the set at edistance `< r`  -/
EMetric.infEdist_lt_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal},
  Metric.infEDist x s < r ↔ ∃ y ∈ s, edist x y < r
-- Init.Data.String.Lemmas.Basic
_private.Init.Data.String.Lemmas.Basic.0.String.Slice.Pos.nextn.eq_def : ∀ {s : String.Slice} (p : s.Pos) (n : ℕ),
  p.nextn n =
    match n with
    | 0 => p
    | n.succ => if h : p ≠ s.endPos then (p.next h).nextn n else p
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.Pseudofunctor B C} (θ : G ⟶ H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h).hom (θ.app c)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f
          (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f
            (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft f
              (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.whiskerRight (θ.naturality g).hom (H.map h)))
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.units_mem_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ pinGroup Q ↔ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Raw.Const.ofList l).getKeyD k' fallback = k
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- Multiplication and division by a non-zero ordinal form a Galois connection.  -/
Ordinal.mul_div_gc : ∀ {a : Ordinal.{u_4}}, a ≠ 0 → GaloisConnection (fun x => a * x) fun x => x / a
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingSubgroup_iff_subset_fixedBy : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {m : M},
  m ∈ fixingSubgroup M s ↔ s ⊆ MulAction.fixedBy α m
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a commutative
ring.  -/
Algebra.adjoinCommRingOfComm : (R : Type uR) →
  {A : Type uA} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] → {s : Set A} → (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → CommRing ↥(Algebra.adjoin R s)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- For every element `e` of an independent set `I`,
there is a cocircuit whose intersection with `I` is `{e}`.  -/
Matroid.Indep.exists_isCocircuit_inter_eq_mem : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α}, M.Indep I → e ∈ I → ∃ K, M.IsCocircuit K ∧ K ∩ I = {e}
-- Batteries.Util.ProofWanted
/-- The trivial constructor; carries no information.  -/
ProofWanted.mk : {α : Sort u} → ProofWanted α
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.neg_sub' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y), -(a - b) = -a + b
-- Mathlib.Topology.Inseparable
Specializes.mem_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, x ⤳ y → IsOpen s → y ∈ s → x ∈ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_nonneg`.  -/
add_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_ofENat : ∀ (n : ℕ∞), Cardinal.toNat ↑n = n.toNat
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instFaithfulTopCatToContinuousGeneratedByCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  (TopCat.toContinuousGeneratedByCat X).Faithful
-- Mathlib.Topology.Compactness.Lindelof
hasBasis_coclosedLindelof : ∀ {X : Type u} [inst : TopologicalSpace X],
  (Filter.coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_sumInl : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.relabel Sum.inl φ = FirstOrder.Language.BoundedFormula.castLE ⋯ φ
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.mul : ∀ {𝕜 : 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] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'},
  MDiffAt[s] p z → MDiffAt[s] q z → MDiffAt[s] (p * q) z
-- Lean.Server.Requests
Lean.Server.RequestM.asTask : {α : Type} → Lean.Server.RequestM α → Lean.Server.RequestM (Lean.Server.RequestTask α)
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instComonObj : {X : SFinKer} → CategoryTheory.ComonObj X
-- Mathlib.Tactic.ReduceModChar.Ext
/-- `@[reduce_mod_char]` is an attribute that tags lemmas for preprocessing and cleanup in the
`reduce_mod_char` tactic  -/
reduceModCharExt : Lean.Meta.SimpExtension
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.sigmaFinite_tprod : ∀ {δ : Type u_4} {X : δ → Type u_5} [inst : (i : δ) → MeasurableSpace (X i)] (l : List δ)
  (μ : (i : δ) → MeasureTheory.Measure (X i)) [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.tprod l μ)
-- Mathlib.Analysis.CStarAlgebra.Basic
IsSelfAdjoint.nnnorm_pow_two_pow : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E},
  IsSelfAdjoint x → ∀ (n : ℕ), ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.isoOfHomotopyEquiv_hom : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D),
  (HomotopyCategory.isoOfHomotopyEquiv f).hom = (HomotopyCategory.quotient V c).map f.hom
-- Mathlib.Analysis.Normed.Group.Hom
/-- The fundamental property of the operator norm: `‖f x‖ ≤ ‖f‖ * ‖x‖`.  -/
NormedAddGroupHom.le_opNorm : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) (x : V₁), ‖f x‖ ≤ ‖f‖ * ‖x‖
-- Init.Data.SInt.Lemmas
Int8.toInt32_le : ∀ {a b : Int8}, a.toInt32 ≤ b.toInt32 ↔ a ≤ b
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {t : Set Y} [CompactSpace ↑t] [inst_4 : TopologicalSpace X]
  [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)] (f : X → Y → E) (g : C(↑t, E)),
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ t) →
    MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMap.mkD (t.domRestrict (f x)) g) μ
-- Mathlib.Topology.Bases
/-- If `β` is a second-countable space, then its induced topology via
`f` on `α` is also second-countable.  -/
TopologicalSpace.secondCountableTopology_induced : ∀ (α : Type u_1) (β : Type u_2) [t : TopologicalSpace β] [SecondCountableTopology β] (f : α → β),
  SecondCountableTopology α
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- `a ↦ a ^ p` is operator monotone for `p ∈ [0,1]`.  -/
CFC.monotone_rpow : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : ℝ},
  p ∈ Set.Icc 0 1 → Monotone fun a => a ^ p
-- Mathlib.SetTheory.Cardinal.Basic
/-- See also `Cardinal.aleph0_le_mul_iff'`.  -/
Cardinal.aleph0_le_mul_iff' : ∀ {a b : Cardinal.{u}}, Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ Cardinal.aleph0 ≤ b ∨ Cardinal.aleph0 ≤ a ∧ b ≠ 0
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_monomial : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.eval₂Hom f g) ((MvPolynomial.monomial d) r) = f r * d.prod fun i k => g i ^ k
-- Mathlib.Data.List.Perm.Subperm
/-- See also `List.subperm_ext_iff`.  -/
List.subperm_iff_count : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₁.Subperm l₂ ↔ ∀ (a : α), List.count a l₁ ≤ List.count a l₂
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.replaceFVarS.tacticBuilder : Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.Expr → Lean.MVarId × Lean.FVarId × Bool → Aesop.Script.TacticBuilder
-- Mathlib.Algebra.BigOperators.Balance
Fintype.expect_balance : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f : ι → G),
  (Finset.univ.expect fun x => Fintype.balance f x) = 0
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_mul_iff_of_isSuccLimit : ∀ {a b c : Ordinal.{u_4}}, Order.IsSuccLimit c → (a < b * c ↔ ∃ c' < c, a < b * c')
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.image_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (f : F ⟶ F') (G' : CategoryTheory.Subfunctor F'), G.image f ≤ G' ↔ G ≤ G'.preimage f
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.apply_mem_toSubmodule : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (self : Subrepresentation ρ) (g : G) ⦃v : W⦄,
  v ∈ self.toSubmodule → (ρ g) v ∈ self.toSubmodule
-- Mathlib.Order.CompleteBooleanAlgebra
sSup_symmDiff_le : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α},
  s.Nonempty → ∀ {a : α}, symmDiff (sSup s) a ≤ sSup ((fun x => symmDiff x a) '' s)