mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.map_fun : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Hom M N)
  {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
-- Lean.Elab.Tactic.Omega.Frontend
/-- The trivial `MetaProblem`, with no facts to process and a trivial `Problem`.  -/
Lean.Elab.Tactic.Omega.MetaProblem.trivial : Lean.Elab.Tactic.Omega.MetaProblem
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_top : ∀ {R : Type u_2} [inst : NonAssocSemiring R], ⊤.unop = ⊤
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the forward direction of `isMaxFilter_dual_iff`. -/
IsMaxFilter.undual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter (⇑OrderDual.toDual ∘ f) l a → IsMinFilter f l a
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_one_right : ∀ (p : ℕ), p.maxPowDvdDiv 1 = (0, 1)
-- Init.Data.List.MinMaxOn
List.maxOn_eq_max : ∀ {α : Type u_1} {β : Type u_2} [inst : Max α] [inst_1 : LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α]
  [inst_4 : LE β] [inst_5 : DecidableLE β] {f : α → β} {l : List α} {h : l ≠ []},
  (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → List.maxOn f l h = l.max h
-- Init.Data.List.Sublist
List.prefix_cons_inj : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTraceAux_def : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] (a : K),
  Algebra.normalizedTraceAux✝ F K a =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (Algebra.trace F ↥F⟮a⟯) (IntermediateField.AdjoinSimple.gen F a)
-- Mathlib.Geometry.Manifold.ChartedSpace
modelProdInhabited : {H : Type u} → {H' : Type u_1} → [Inhabited H] → [Inhabited H'] → Inhabited (ModelProd H H')
-- Mathlib.Algebra.Quandle
ShelfHom.mk.injEq : ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (toFun : S₁ → S₂)
  (map_act' : ∀ {x y : S₁}, toFun (Shelf.act x y) = Shelf.act (toFun x) (toFun y)) (toFun_1 : S₁ → S₂)
  (map_act'_1 : ∀ {x y : S₁}, toFun_1 (Shelf.act x y) = Shelf.act (toFun_1 x) (toFun_1 y)),
  ({ toFun := toFun, map_act' := map_act' } = { toFun := toFun_1, map_act' := map_act'_1 }) = (toFun = toFun_1)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Construct an augmented cosimplicial object in the opposite
category from an augmented simplicial object.  -/
CategoryTheory.SimplicialObject.Augmented.rightOp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.SimplicialObject.Augmented C → CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.coe_toBipointed : ∀ (X : TwoP), X.toBipointed.X = X.X
-- Mathlib.CategoryTheory.Sites.Over
/-- The composition of two `overMapPullback` functors identifies to
`overMapPullback` for the composition.  -/
CategoryTheory.GrothendieckTopology.overMapPullbackComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {X Y Z : C} →
            (f : X ⟶ Y) →
              (g : Y ⟶ Z) →
                (J.overMapPullback A g).comp (J.overMapPullback A f) ≅
                  J.overMapPullback A (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.zero : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : Zero β], HasCompactSupport 0
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.strictMono : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne], StrictMono ⇑(Valuation.RankOne.hom v)
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- Notation for composition of reflexive prefunctors.  -/
CategoryTheory.ReflPrefunctor.«term_⋙rq_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_singleton : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (f : (i : ι) → α i),
  (MeasureTheory.Measure.pi μ) {f} = ∏ i, (μ i) {f i}
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
/-- The torsion tensor of a covariant derivative on the tangent bundle of a manifold.  -/
CovariantDerivative.torsion : {𝕜 : 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] →
                      [CompleteSpace 𝕜] →
                        [CompleteSpace E] →
                          [FiniteDimensional 𝕜 E] →
                            [inst_9 : IsManifold I 2 M] →
                              CovariantDerivative I E (TangentSpace I) →
                                (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x
-- Lean.CoreM
Lean.getDiag : Lean.Options → Bool
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The pi-type of profinite additive groups is a
profinite additive group.  -/
ProfiniteAddGrp.pi : {α : Type u} → (α → ProfiniteAddGrp.{u_1}) → ProfiniteAddGrp.{max u u_1}
-- Lean.Elab.InfoTree.Types
Lean.Elab.CustomInfo.mk.inj : ∀ {stx : Lean.Syntax} {value : Dynamic} {stx_1 : Lean.Syntax} {value_1 : Dynamic},
  { stx := stx, value := value } = { stx := stx_1, value := value_1 } → stx = stx_1 ∧ value = value_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Whiskering left of a `CatCospanTransformMorphism` by a `CatCospanTransform`.  -/
CategoryTheory.Limits.CatCospanTransform.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Lie.DirectSum
/-- The inclusion of each component into the direct sum as morphism of Lie algebras.  -/
DirectSum.lieAlgebraOf : (R : Type u) →
  (ι : Type v) →
    [inst : CommRing R] →
      (L : ι → Type w) →
        [inst_1 : (i : ι) → LieRing (L i)] →
          [inst_2 : (i : ι) → LieAlgebra R (L i)] → [DecidableEq ι] → (j : ι) → L j →ₗ⁅R⁆ DirectSum ι fun i => L i
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.ofList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {k : α} {v : β},
  Std.DHashMap.Const.ofList [(k, v)] = ∅.insert k v
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstMulInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
_private.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card.0.Matrix.termQ : Lean.ParserDescr
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_eq_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ},
  List.maxIdxOn f xs h = i ↔
    ∃ (h : i < xs.length), (∀ (j : ℕ) (x : j < xs.length), f xs[j] ≤ f xs[i]) ∧ ∀ (j : ℕ) (x : j < i), f xs[j] < f xs[i]
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- `tensorLeft X` is a left adjoint  -/
CategoryTheory.Closed.adj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} →
        [self : CategoryTheory.Closed X] →
          CategoryTheory.MonoidalCategory.tensorLeft X ⊣ CategoryTheory.Closed.rightAdj X
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology],
  (S.map F).Exact ↔ CategoryTheory.Limits.IsZero (F.obj h.H)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) '' Set.Iic b = Set.Iic (b / a)
-- Mathlib.Order.BourbakiWitt
/-- The supremum of a nonempty chain  -/
ChainCompletePartialOrder.cSup : {α : Type u_4} → [self : ChainCompletePartialOrder α] → NonemptyChain α → α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_sub_one : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      m.contains k = true →
        (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isNone = true →
          (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size = (↑m).size - 1
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.go.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (p p_1 : ℕ) (e_p : p = p_1) (hp : 1 < p ∧ n ≠ 0),
  Nat.maxPowDvdDiv.go n p hp = Nat.maxPowDvdDiv.go n_1 p_1 ⋯
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The simple reflection of `W` at the index `i`.  -/
CoxeterSystem.simple : {B : Type u_1} → {W : Type u_3} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → B → W
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections of the constructed basis correspond to the input data `D.P`.  -/
SchauderBasis.RankOneDecomposition.basis_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (D : SchauderBasis.RankOneDecomposition 𝕜 X), D.basis.proj = D.P
-- Init.Data.ByteArray.Bootstrap
_private.Init.Data.ByteArray.Bootstrap.0.List.toByteArray_append'.ext : ∀ {x y : Array UInt8}, x.toList = y.toList → x = y
-- Mathlib.Data.Int.ModEq
Int.ModEq.refl : ∀ {n : ℤ} (a : ℤ), a ≡ a [ZMOD n]
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.ext : ∀ {𝕜 : 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 : ∀ (x : M), IsTopologicalAddGroup (V x)}
  {inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)} {inst_14 : FiberBundle F V} {x y : CovariantDerivative I F V},
  ↑x = ↑y → x = y
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.aeval_eq_sum : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a : S} [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a)
  (f : PowerSeries R), (PowerSeries.aeval ha) f = ∑' (d : ℕ), (PowerSeries.coeff d) f • a ^ d
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.isCyclicallyReduced_iff : ∀ {α : Type u} {L : List (α × Bool)},
  FreeAddGroup.IsCyclicallyReduced L ↔ FreeAddGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_smul_iff : ∀ {α : Type u_1} {n : Type u_4} {R : Type u_5} [inst : Monoid R] [inst_1 : Star R] [inst_2 : Star α]
  [inst_3 : MulAction R α] [StarModule R α] {A : Matrix n n α} {k : R} [Invertible k],
  IsSelfAdjoint k → ((k • A).IsHermitian ↔ A.IsHermitian)
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.comp_homeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X},
  IsCoveringMapOn f s → ∀ {E' : Type u_3} [inst_2 : TopologicalSpace E'] (g : E' ≃ₜ E), IsCoveringMapOn (f ∘ ⇑g) s
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.fixedPoint_unique' : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ {x y : α}, Function.IsFixedPt f x → Function.IsFixedPt f y → x = y
-- Mathlib.Probability.Independence.Basic
/-- The probability of an intersection of preimages conditioning on another intersection factors
into a product.  -/
ProbabilityTheory.cond_iInter : ∀ {ι : Type u_6} {Ω : Type u_7} {α : Type u_8} {β : Type u_9} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {Y : ι → Ω → β} {f : ι → Set Ω} {t : ι → Set β}
  {s : Finset ι} [Finite ι],
  (∀ (i : ι), Measurable (Y i)) →
    ProbabilityTheory.iIndepFun (fun i ω => (X i ω, Y i ω)) μ →
      (∀ i ∈ s, MeasurableSet (f i)) →
        (∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0) →
          (∀ (i : ι), MeasurableSet (t i)) → μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.isSameEMatchTheoremPtr : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatchTheorem → Bool
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₃₂_comp_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G × G × G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom
        (ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A))
          (fun n => groupHomology.inhomogeneousChains.d A n) 3 2))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₃ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) x)
-- Init.Data.UInt.Bitwise
UInt16.xor_eq_zero_iff : ∀ {a b : UInt16}, a ^^^ b = 0 ↔ a = b
-- Std.Http.Protocol.H1.Writer
/-- The state of the writer machine.
 -/
Std.Http.Protocol.H1.Writer.state : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer.State
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divLeft_symm_apply : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (c b : G), (IsometryEquiv.divLeft c).symm b = b⁻¹ * c
-- Mathlib.Data.Set.Basic
Set.nontrivial_of_nonempty : ∀ {α : Type u} [Nonempty α], Nontrivial (Set α)
-- Mathlib.Analysis.Convex.Strong
strongConvexOn_iff_convex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {s : Set E} {m : ℝ} {f : E → ℝ},
  StrongConvexOn s m f ↔ ConvexOn ℝ s fun x => f x - m / 2 * ‖x‖ ^ 2
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality for applications without `ProofInstInfo`.
Recursively checks function and argument equality.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqAppDefault : Lean.Expr → Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Init.Data.List.Basic
List.intersperse_nil : ∀ {α : Type u} {sep : α}, List.intersperse sep [] = []
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧),
  P 2 = 0 → { point := ⟦P⟧, nonsingular := hP }.toAffineLift = 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The obvious map from a type to its 1-combinations, as an equivariant map.  -/
Set.powersetCard.mulActionHom_singleton : (G : Type u_1) →
  [inst : Group G] →
    (α : Type u_2) → [inst_1 : MulAction G α] → [inst_2 : DecidableEq α] → α →ₑ[id] ↑(Set.powersetCard α 1)
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeq1Indented.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.Clean
/-- `clean% t` fully elaborates `t` and then eliminates all identity functions from it.

Identity functions are normally generated with terms like `show t from p`,
which translate to some variant on `@id t p` in order to retain the type.
These are also generated by tactics such as `dsimp` to insert type hints.

Example:
```lean
def x : Id Nat := by dsimp [Id]; exact 1
#print x
-- def x : Id Nat := id 1

def x' : Id Nat := clean% by dsimp [Id]; exact 1
#print x'
-- def x' : Id Nat := 1
```
 -/
Mathlib.Tactic.cleanStx : Lean.ParserDescr
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.whiskerLeft_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X x x_1 : CategoryTheory.Dial C) (f : x ⟶ x_1),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) f.F)
-- Mathlib.RingTheory.RingHom.Unramified
/-- A ring homomorphism `R →+* A` is formally unramified if `Ω[A⁄R]` is trivial.
See `Algebra.FormallyUnramified`.
 -/
RingHom.FormallyUnramified : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The integrand in the definition of `I` is nonnegative and takes a positive value at least one point,
so the integral is positive.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.I_pos : ∀ {n : ℕ}, 0 < I✝ n (Real.pi / 2)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_zero_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a : K}, a ≤ᵥ 0 ↔ a = 0
-- Mathlib.RingTheory.Spectrum.Prime.LTSeries
/-- Let $R$ be a Noetherian ring, $\mathfrak{p}_0 < \dots < \mathfrak{p}_n$ be a
chain of primes, $x \in \mathfrak{p}_n$. Then we can find another chain of primes
$\mathfrak{q}_0 < \dots < \mathfrak{q}_n$ such that $x \in \mathfrak{q}_1$,
$\mathfrak{p}_0 = \mathfrak{q}_0$ and $\mathfrak{p}_n = \mathfrak{q}_n$.  -/
PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : LTSeries (PrimeSpectrum R)) {x : R},
  x ∈ (RelSeries.last p).asIdeal →
    ∃ q,
      x ∈ (q.toFun 1).asIdeal ∧
        p.length = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_univ₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {s : Set α},
  ¬s ⊆ 0 → s • Set.univ = Set.univ
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.ext_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {ps : DiscreteTiling.Protoset G X ιₚ} {x y : DiscreteTiling.PlacedTile ps},
  x = y ↔ x.index = y.index ∧ x.groupElts ≍ y.groupElts
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_mul_right_eball`. -/
EMetric.preimage_mul_right_ball : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x * a) ⁻¹' Metric.eball b r = Metric.eball (b / a) r
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIcc_filter : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  (SummationFilter.symmetricIcc G).filter = Filter.map (fun g => Finset.Icc (-g) g) Filter.atTop
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_leadingTerm_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  (p q : MvPolynomial σ R), m.degree (m.leadingTerm p * q) = m.degree (p * q)
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- The `n`-th iterated derivative of an analytic function is symmetric.  -/
AnalyticOn.iteratedFDeriv_comp_perm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E},
  AnalyticOn 𝕜 f Set.univ →
    ∀ {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)), (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spineInjective : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : autoParam (m ≤ n + 1) _auto_38✝),
  Function.Injective ⇑(sx.spineEquiv m h)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic.0.CategoryTheory.Abelian.Ext.neg_hom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n), (-α).hom' = -α.hom'
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B),
  (CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso.inv.app X).1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sum.swapCompInl A' A).inv X)
      ((CategoryTheory.Sum.inl_ A' A).associator (CategoryTheory.Sum.swap A' A) X).hom
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure.congr_simp : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1)
  [hμ : MeasureTheory.IsFiniteMeasure μ], μ.toSignedMeasure = μ_1.toSignedMeasure
-- Mathlib.Analysis.Complex.OpenMapping
AnalyticOnNhd.is_constant_or_isOpenMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {g : E → ℂ},
  AnalyticOnNhd ℂ g Set.univ → (∃ w, ∀ (z : E), g z = w) ∨ IsOpenMap g
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- Given a graph in which the universal vertices do not violate Tutte's condition,
if the graph decomposes into cliques, there exists a matching that covers
everything except some universal vertices.

This lemma is marked private, because
it is strictly weaker than `IsPerfectMatching.exists_of_isClique_supp`.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Tutte.0.SimpleGraph.Subgraph.IsMatching.exists_verts_compl_subset_universalVerts : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  ¬G.IsTutteViolator G.universalVerts →
    (∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) →
      ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.rightTriple_adj₂ : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.rightTriple.adj₂ = q.adj₃
-- Mathlib.Topology.Algebra.Support
mulTSupport_mul : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass α] (f g : X → α),
  (mulTSupport fun x => f x * g x) ⊆ mulTSupport f ∪ mulTSupport g
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_utf8EncodeChar_eq_done : ∀ {c : Char},
  c.utf8Size = 1 →
    ByteArray.utf8DecodeChar?.parseFirstByte (String.utf8EncodeChar c)[0] = ByteArray.utf8DecodeChar?.FirstByte.done