mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.exists_set_linearIndependent_of_lt_lift_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {c : Cardinal.{w}},
  Cardinal.lift.{v, w} c < Cardinal.lift.{w, v} (Module.rank R M) →
    ∃ s, Cardinal.lift.{w, v} (Cardinal.mk ↑s) = Cardinal.lift.{v, w} c ∧ LinearIndepOn R id s
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_mul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] (s t : Set α),
  ↑(lowerClosure s) * t = ↑(lowerClosure (s * t))
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isUniformEmbedding_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] (𝕜' : Type u_5) [inst_8 : NontriviallyNormedField 𝕜']
  [inst_9 : NormedAlgebra 𝕜' 𝕜] [inst_10 : Module 𝕜' E] [inst_11 : IsScalarTower 𝕜' 𝕜 E] [inst_12 : Module 𝕜' F]
  [inst_13 : IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E],
  IsUniformEmbedding (ContinuousAlternatingMap.restrictScalars 𝕜')
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.avgRisk_eq_lintegral_lintegral_lintegral : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ],
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) [inst_2 : ProbabilityTheory.IsFiniteKernel P]
      (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [ProbabilityTheory.IsSFiniteKernel κ] (π : MeasureTheory.Measure Θ)
      [inst_4 : MeasureTheory.IsFiniteMeasure π],
      ProbabilityTheory.avgRisk ℓ P κ π =
        ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x ∂κ x ∂π.bind ⇑P
-- Mathlib.Analysis.InnerProductSpace.NormPow
norm_fderiv_norm_id_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x : E) {p : ℝ},
  1 < p → ‖fderiv ℝ (fun x => ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.fixedBy_zero_eq_univ : ∀ (α : Type u_1) (M : Type u_3) [inst : AddMonoid M] [inst_1 : AddAction M α], AddAction.fixedBy α 0 = Set.univ
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
disjoint_ball_closedBall_iff : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} {δ ε : ℝ},
  0 < δ → 0 ≤ ε → (Disjoint (Metric.ball x δ) (Metric.closedBall y ε) ↔ δ + ε ≤ dist x y)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.toContinuousInf : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α], ContinuousSup α
-- Mathlib.Geometry.Euclidean.MongePoint
/-- In the case of a triangle, altitudes are the same thing as Monge
planes.  -/
Affine.Triangle.altitude_eq_mongePlane : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Affine.Simplex.altitude t i₁ = Affine.Simplex.mongePlane t i₂ i₃
-- Init.PropLemmas
Bool.dite_else_true : ∀ {p : Prop} [inst : Decidable p] {x : p → Bool}, (if h : p then x h else true) = true ↔ ∀ (h : p), x h = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instMax : {R : Type u} → {M : Type v} → [inst : SMul R M] → Max (SubMulAction R M)
-- Mathlib.Order.Grade
instGradeBoundedOrderOrderDual : {𝕆 : Type u_1} →
  {α : Type u_3} → [inst : Preorder 𝕆] → [inst_1 : Preorder α] → [GradeBoundedOrder 𝕆 α] → GradeBoundedOrder 𝕆ᵒᵈ αᵒᵈ
-- Init.Core
Std.LeftIdentity.mk : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → β} {o : outParam α}, Std.LeftIdentity op o
-- Mathlib.RingTheory.Algebraic.Defs
/-- An element `x` is transcendental over `R` if and only if for any polynomial `p`,
`Polynomial.aeval x p = 0` implies `p = 0`. This is similar to `algebraicIndependent_iff`.  -/
transcendental_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A},
  Transcendental R x ↔ ∀ (p : Polynomial R), (Polynomial.aeval x) p = 0 → p = 0
-- Mathlib.RingTheory.Jacobson.Radical
Ring.map_jacobson_of_ker_le : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] {f : R →+* R₂} [inst_2 : RingHomSurjective f],
  RingHom.ker f ≤ Ring.jacobson R → Submodule.map f.toSemilinearMap (Ring.jacobson R) = Ring.jacobson R₂
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Transport a `HasExactColimitsOfShape` along an equivalence of the shape.

Note: When `C` has finite limits, this lemma holds with the equivalence replaced by a final
functor, see `hasExactColimitsOfShape_of_final` below.
 -/
CategoryTheory.HasExactColimitsOfShape.of_domain_equivalence : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {J' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : CategoryTheory.Category.{v_2, u_2} J'] (e : J ≌ J')
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C],
  CategoryTheory.HasExactColimitsOfShape J' C
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.functor_obj : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ) (A : Rep.{u, u, u} k G),
  (groupCohomology.functor k G n).obj A = groupCohomology A n
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₁ = φ.unop.hom₃.op
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The natural transformation of relative homology functors in a morphism of
`HomologyPretheory`s.  -/
TopPair.HomologyPretheory.Hom.homₚ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} → {HP HP' : TopPair.HomologyPretheory C c} → HP.Hom HP' → (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffAt.rpow_const_of_ne : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {p : ℝ} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → f x ≠ 0 → ContDiffAt ℝ n (fun x => f x ^ p) x
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Two equivalent partial equivs coincide on the source.  -/
PartialEquiv.EqOnSource.eqOn : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → Set.EqOn (↑e) (↑e') e.source
-- Init.SizeOf
Lean.ParserDescr.node.sizeOf_spec : ∀ (kind : Lean.SyntaxNodeKind) (prec : ℕ) (p : Lean.ParserDescr),
  sizeOf (Lean.ParserDescr.node kind prec p) = 1 + sizeOf kind + sizeOf prec + sizeOf p
-- Mathlib.RepresentationTheory.Basic
/-- The natural `k`-linear `G`-representation on `k[Gⁿ]` induced by left multiplication in `G`.  -/
Representation.diagonal : (k : Type u_1) →
  [inst : Semiring k] →
    (G : Type u_2) → [inst_1 : Monoid G] → (n : ℕ) → Representation k G (MonoidAlgebra k (Fin n → G))
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_series_hasSum_exp' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp x)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_zero_of_lt : ∀ {n k : ℕ}, n < k → n.choose k = 0
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_sub : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddGroup M] (f g : ι →₀ M), (f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp
-- Lean.Meta.Sym.AlphaShareBuilder
/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing.  -/
Lean.Meta.Sym.Internal.mkAppRangeS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → ℕ → ℕ → Array Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.le_transfiniteCompositions : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W ≤ CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W
-- Mathlib.FieldTheory.JacobsonNoether
/-- Jacobson-Noether theorem: For a non-commutative division algebra `D`
that is algebraic over a field `L`, if the center of
`D` coincides with `L`, then there exist an element `x` of `D \ L`
that is separable over `L`.  -/
JacobsonNoether.exists_separable_and_not_isCentral' : ∀ {L : Type u_2} {D : Type u_3} [inst : Field L] [inst_1 : DivisionRing D] [inst_2 : Algebra L D]
  [Algebra.IsAlgebraic L D] [Algebra.IsCentral L D], ⊥ ≠ ⊤ → ∃ x ∉ ⊥, IsSeparable L x
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_deleteMin_lt : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {s' s : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s') → s'.size < s.size
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAt_iff_isLongestRevMatchAt_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt p pos pos' ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt (fun x => decide (p x)) pos pos'
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.prod_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type w} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type v'}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type w'} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') (x : ModelProd H H'), ↑(I.prod I') x = (↑I x.1, ↑I' x.2)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAdd_symm : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v : V₁), (AffineEquiv.constVAdd k P₁ v).symm = AffineEquiv.constVAdd k P₁ (-v)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplex_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), Φ.shortComplex.X₂ = CategoryTheory.Functor.id C
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.mono : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε δ : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj],
  G.FarFromTriangleFree ε → δ ≤ ε → G.FarFromTriangleFree δ
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Subgroup.IsFinitelyNormallyGenerated.eq_1 : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G),
  N.IsFinitelyNormallyGenerated = ∃ S, S.Finite ∧ Subgroup.normalClosure S = N
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.State.mk.sizeOf_spec : ∀ (set : Lean.PHashSet Lean.Meta.Sym.AlphaKey), sizeOf { set := set } = 1 + sizeOf set
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The morphism `mappingCone φ₁ ⟶ mappingCone φ₂` that is induced by a commutative square.  -/
CochainComplex.mappingCone.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} →
          (φ₁ : K₁ ⟶ L₁) →
            (φ₂ : K₂ ⟶ L₂) →
              (a : K₁ ⟶ K₂) →
                (b : L₁ ⟶ L₂) →
                  CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂ →
                    (CochainComplex.mappingCone φ₁ ⟶ CochainComplex.mappingCone φ₂)
-- Mathlib.Data.List.Sigma
List.dlookup_kunion_left : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  a ∈ l₁.keys → List.dlookup a (l₁.kunion l₂) = List.dlookup a l₁
-- Mathlib.LinearAlgebra.RootSystem.Basic
RootPairing.equiv_of_mapsTo.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p p_1 : M →ₗ[R] N →ₗ[R] R) (e_p : p = p_1)
  (root root_1 : ι ↪ M) (e_root : root = root_1) (coroot coroot_1 : ι ↪ N) (e_coroot : coroot = coroot_1) (i i_1 : ι),
  i = i_1 →
    ∀
      (h :
        ∀ (i : ι),
          Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root))
      (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2),
      RootPairing.equiv_of_mapsTo p root coroot i h hp = RootPairing.equiv_of_mapsTo p_1 root_1 coroot_1 i_1 ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- At `-n` for `n ∈ ℕ`, the Gamma function is undefined; by convention we assign it the value 0.  -/
Complex.Gamma_neg_nat_eq_zero : ∀ (n : ℕ), Complex.Gamma (-↑n) = 0
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_X : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (a : D.J), D.oneHypercover.X a = D.U a
-- Mathlib.Order.KrullDimension
Order.krullDim_withBot : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim (WithBot α) = Order.krullDim α + 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.var.injEq : ∀ (i i_1 : Lean.Grind.CommRing.Var), (Lean.Grind.CommRing.Expr.var i = Lean.Grind.CommRing.Expr.var i_1) = (i = i_1)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] {p : ↑unitInterval},
  MeasureTheory.IsProbabilityMeasure (unitInterval.toNNReal p • μ + unitInterval.toNNReal (unitInterval.symm p) • ν)
-- Mathlib.Analysis.Complex.Convex
/-- The slit plane is star-convex at a positive number.  -/
Complex.starConvex_slitPlane : ∀ {z : ℂ}, 0 < z → StarConvex ℝ z Complex.slitPlane
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Locally uniform convergence implies convergence in the compact-open topology.  -/
ContinuousMap.tendsto_of_tendstoLocallyUniformly : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
  {p : Filter ι} {F : ι → C(α, β)}, TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p → Filter.Tendsto F p (nhds f)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` is `C^k` at `x`, so is its coefficient `b.localFrameCoeff e i` in the local frame
near `x` induced by `e` and `b`  -/
contMDiffAt_localFrameCoeff : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  {x : M} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  x ∈ e.baseSet →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) x →
      ∀ (i : ι),
        ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) k
          ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x
-- Mathlib.Algebra.Group.Units.Basic
Units.inv_mul_eq_inv_mul_iff : ∀ {α : Type u} [inst : CommMonoid α] (a c : α) (b d : αˣ), ↑b⁻¹ * a = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- If `c` is a pushout cocone, then `c.op.unop` is isomorphic to `c`.  -/
CategoryTheory.Limits.PushoutCocone.opUnopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} → {f : X ⟶ Y} → {g : X ⟶ Z} → (c : CategoryTheory.Limits.PushoutCocone f g) → c.op.unop ≅ c
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sUnion_empty : ∅.sUnion = ∅
-- Mathlib.Analysis.InnerProductSpace.Continuous
_private.Mathlib.Analysis.InnerProductSpace.Continuous.0.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonUnitalNonAssocSemiring : {n : Type u_2} →
  {A : Type u_5} → [Fintype n] → [NonUnitalNonAssocSemiring A] → NonUnitalNonAssocSemiring (CStarMatrix n n A)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The current value of the variable store  -/
Turing.TM1.Cfg.var : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → [inst : Inhabited Γ] → Turing.TM1.Cfg Γ Λ σ → σ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f t[k]?).isSome = true else k' ∈ t
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaEquivSigma_apply : ∀ {α : Type u_2} (β : α → Type u_1) (a : (i : α) ×' β i), (Equiv.psigmaEquivSigma β) a = ⟨a.fst, a.snd⟩
-- Mathlib.Topology.Connected.Clopen
/-- A pairwise disjoint cover by clopens partitions the connected components.  -/
ConnectedComponents.equivOfIsClopen : {α : Type u} →
  [inst : TopologicalSpace α] →
    {ι : Type u_3} →
      {U : ι → Set α} →
        (∀ (i : ι), IsClopen (U i)) →
          Pairwise (Function.onFun Disjoint U) →
            ⋃ i, U i = Set.univ → ConnectedComponents α ≃ (i : ι) × ConnectedComponents ↑(U i)
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.exists_ball_subset_forall_le_norm_circleMap_sub : ∀ {R : ℝ} {w c : ℂ},
  w ∈ Metric.ball c R →
    ∃ d > 0, Metric.ball w d ⊆ Metric.ball c R ∧ ∀ x ∈ Metric.ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Expr.toSeq'.match_1.splitter : (motive : Lean.Grind.AC.Expr → Sort u_1) →
  (e : Lean.Grind.AC.Expr) →
    ((x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Expr.var x)) →
      ((a b : Lean.Grind.AC.Expr) → motive (a.op b)) → motive e
-- Mathlib.Data.Nat.BinaryRec
/-- For a predicate `motive : Nat → Sort u`, if instances can be
constructed for natural numbers of the form `bit b n`,
they can be constructed for any given natural number.  -/
Nat.bitCasesOn : {motive : ℕ → Sort u} → (n : ℕ) → ((b : Bool) → (n : ℕ) → motive (Nat.bit b n)) → motive n
-- Mathlib.RingTheory.PiTensorProduct
SemiconjBy.tprod : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  {a₁ a₂ a₃ : (i : ι) → A i},
  SemiconjBy a₁ a₂ a₃ →
    SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)
-- Mathlib.Order.Category.PartOrd
PartOrd.ext : ∀ {X Y : PartOrd} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_same₂₄ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c : ℤ), IsEllipticNet.atomRel W a b c b = W b * W 0 * IsEllipticNet.atom W c a
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_tfae : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y),
  [CategoryTheory.Mono (L.map f), P.monoModSerre f,
      ∀ ⦃Z : C⦄ (z : Z ⟶ X), CategoryTheory.CategoryStruct.comp (L.map z) (L.map f) = 0 → L.map z = 0].TFAE
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} (self : S.BindStruct R h) {Z_1 : C}
  (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp self.g (CategoryTheory.CategoryStruct.comp self.f h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.E.sizeOf_spec : ∀ {B : Type v} [inst : SizeOf B] (a : B), sizeOf (CartanMatrix.Generators.E a) = 1 + sizeOf a
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.State.mk.inj : ∀ {visited : Array Lean.Expr} {checked : Std.HashSet Lean.Expr} {visited_1 : Array Lean.Expr}
  {checked_1 : Std.HashSet Lean.Expr},
  { visited := visited, checked := checked } = { visited := visited_1, checked := checked_1 } →
    visited = visited_1 ∧ checked = checked_1
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instModuleOfIsScalarTower : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddCommMonoid X] →
            [inst_3 : Module R X] →
              {R₀ : Type u_3} →
                [inst_4 : Semiring R₀] →
                  [inst_5 : Module R₀ X] →
                    [inst_6 : Module R₀ R] →
                      [IsScalarTower R₀ R X] → [IsScalarTower R₀ R R] → Module R₀ (OreLocalization S X)
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_3.eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (pw₁ : Lean.Grind.CommRing.Power)
  (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : (x : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit x)
  (h_2 : (x : Lean.Grind.CommRing.Mon) → motive x Lean.Grind.CommRing.Mon.unit)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ with
    | Lean.Grind.CommRing.Mon.unit, x => h_1 x
    | x, Lean.Grind.CommRing.Mon.unit => h_2 x
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
    h_3 pw₁ m₁ pw₂ m₂
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.mk : {X : Type u_3} →
  [toPseudoMetricSpace : PseudoMetricSpace X] →
    [toCompleteSpace : CompleteSpace X] → TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace X
-- Mathlib.Algebra.Group.Finsupp
Finsupp.induction₂ : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M),
  motive 0 → (∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + fun₀ | a => b)) → motive f