mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.splitter : (motive : Lean.Grind.Linarith.Expr → Sort u_1) →
  (x : Lean.Grind.Linarith.Expr) →
    (Unit → motive Lean.Grind.Linarith.Expr.zero) →
      ((v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v)) →
        ((a b : Lean.Grind.Linarith.Expr) → motive (a.add b)) →
          ((a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) →
            ((k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)) →
              ((k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a)) →
                ((a : Lean.Grind.Linarith.Expr) → motive a.neg) → motive x
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_add_self : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), ↑(AddAction.stabilizer G s) + s = s
-- Mathlib.Data.NNReal.Defs
NNReal.instNontrivial : Nontrivial NNReal
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_add_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a + x) '' Set.Iio b = Set.Iio (a + b)
-- Lean.Parser.Extension
Lean.Parser.getConstAlias : {α : Type} → IO.Ref (Lean.Parser.AliasTable α) → Lean.Name → IO α
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.withReader : ∀ {m n : Type u → Type v} {ρ α : Type u} [inst : MonadFunctor m n] [inst_1 : MonadWithReaderOf ρ m] (f : ρ → ρ),
  MonadWithReaderOf.withReader f = monadMap fun {β} => MonadWithReaderOf.withReader f
-- Mathlib.Computability.Primrec.Basic
Primrec.option_casesOn : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {o : α → Option β} {f : α → σ} {g : α → β → σ},
  Primrec o → Primrec f → Primrec₂ g → Primrec fun a => Option.casesOn (o a) (f a) (g a)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.subtype_injective : ∀ {M : Type u_4} [inst : MulOneClass M] (s : Submonoid M), Function.Injective ⇑s.subtype
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.inclusionObj.eq_def : ∀ {C : Type u} (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.inclusionObj x =
    match x with
    | CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit => CategoryTheory.FreeMonoidalCategory.unit
    | n.tensor a =>
      (CategoryTheory.FreeMonoidalCategory.inclusionObj n).tensor (CategoryTheory.FreeMonoidalCategory.of a)
-- Mathlib.Dynamics.Newton
Polynomial.isNilpotent_iterate_newtonMap_sub_of_isNilpotent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S}, IsNilpotent ((Polynomial.aeval x) P) → ∀ (n : ℕ), IsNilpotent (P.newtonMap^[n] x - x)
-- Lean.Structure
/-- Sets parent projection info for a structure defined in the current module.
Throws an error if the structure has not already been registered with `Lean.registerStructure`.
 -/
Lean.setStructureParents : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → Array Lean.StructureParentInfo → m Unit
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.integral_norm_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F},
  AEMeasurable X μ →
    AEMeasurable Y μ →
      MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        MeasureTheory.Integrable (fun a => ∫ (y : Ω), ‖f (X a, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
-- Batteries.Data.List.Basic
List.takeWhile₂.eq_def : ∀ {α : Type u_1} {β : Type u_2} (R : α → β → Bool) (x : List α) (x_1 : List β),
  List.takeWhile₂ R x x_1 =
    match x, x_1 with
    | a :: as, b :: bs =>
      if R a b = true then
        match List.takeWhile₂ R as bs with
        | (as', bs') => (a :: as', b :: bs')
      else ([], [])
    | x, x_2 => ([], [])
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_hom_inv_id_eval_assoc : ∀ {C : Type u_1} {D : Type u_2} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C D) (j : J) {Z : D} (h : F.obj (X j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (e.hom j)) (CategoryTheory.CategoryStruct.comp (F.map (e.inv j)) h) = h
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filterMap_eq_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : (a : α) → β a → Bool},
  Std.ExtDHashMap.filterMap (fun k => Option.guard fun v => f k v) m = Std.ExtDHashMap.filter f m
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f : ℕ → M` is multipliable, then the partial products `∏ i ∈ range n, f i` converge
to `∏' i, f i`.  -/
Multipliable.tendsto_prod_tprod_nat : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  Multipliable f → Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, f i) Filter.atTop (nhds (∏' (i : ℕ), f i))
-- Mathlib.Order.Monotone.Monovary
StrictMonoOn.trans_monovaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : PartialOrder ι], StrictMonoOn f s → MonovaryOn g f s → MonotoneOn g s
-- Init.Data.SInt.Lemmas
Int64.zero_le_ofNat_of_lt : ∀ {a : ℕ}, a < 2 ^ 63 → 0 ≤ Int64.ofNat a
-- Init.Data.List.Lemmas
List.filter_filter : ∀ {α : Type u_1} {p q : α → Bool} {l : List α}, List.filter p (List.filter q l) = List.filter (fun a => p a && q a) l
-- Mathlib.Algebra.Group.Defs
/-- Any `AddCommMagma G` that
satisfies `IsLeftCancelAdd G` also satisfies `IsRightCancelAdd G`.  -/
AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd : ∀ (G : Type u) [inst : AddCommMagma G] [IsLeftCancelAdd G], IsRightCancelAdd G
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.ext : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.NonemptyCompacts α}, ↑s = ↑t → s = t
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationsParams.expr : ProofWidgets.GetExprPresentationsParams → Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.mk.inj : ∀ {E : Type u_1} {inst : NormedAddCommGroup E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  {toFun : ↑(Set.Icc tmin tmax) → E} {lipschitzWith : LipschitzWith L toFun}
  {mem_closedBall₀ : toFun t₀ ∈ Metric.closedBall x₀ ↑r} {toFun_1 : ↑(Set.Icc tmin tmax) → E}
  {lipschitzWith_1 : LipschitzWith L toFun_1} {mem_closedBall₀_1 : toFun_1 t₀ ∈ Metric.closedBall x₀ ↑r},
  { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ } =
      { toFun := toFun_1, lipschitzWith := lipschitzWith_1, mem_closedBall₀ := mem_closedBall₀_1 } →
    toFun = toFun_1
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.instIsLeftAdjointCostar : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  (CategoryTheory.Under.costar X).IsLeftAdjoint
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Mathlib.Topology.Sober
IsIrreducible.isGenericPoint_genericPoint : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] {S : Set α} (hS : IsIrreducible S),
  IsClosed S → IsGenericPoint hS.genericPoint S
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `α ◫ (β ≫ η ≫ ηs)`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompNilCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural →
      Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The morphism from the colimit object to the cone point of any other cocone.  -/
CategoryTheory.Limits.colimit.desc : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            (c : CategoryTheory.Limits.Cocone F) → CategoryTheory.Limits.colimit F ⟶ c.pt
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- Precomposition by a fixed continuous linear map, as a continuous linear map when all spaces
of continuous linear maps are equipped with the weak operator topology.  -/
ContinuousLinearMapWOT.precompCLM : {𝕜₁ : Type u_5} →
  {𝕜₂ : Type u_6} →
    {𝕜₃ : Type u_7} →
      {E : Type u_9} →
        {F : Type u_10} →
          {G : Type u_11} →
            [inst : NormedField 𝕜₁] →
              [inst_1 : NormedField 𝕜₂] →
                [inst_2 : NormedField 𝕜₃] →
                  {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
                    {σ₁₃ : 𝕜₁ →+* 𝕜₃} →
                      {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : TopologicalSpace E] →
                              [inst_6 : Module 𝕜₁ E] →
                                [inst_7 : AddCommGroup F] →
                                  [inst_8 : TopologicalSpace F] →
                                    [inst_9 : Module 𝕜₂ F] →
                                      [inst_10 : AddCommGroup G] →
                                        [inst_11 : TopologicalSpace G] →
                                          [inst_12 : Module 𝕜₃ G] →
                                            [inst_13 : IsTopologicalAddGroup G] →
                                              [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                (E →SWOT[σ₁₂] F) → (F →SWOT[σ₂₃] G) →L[𝕜₃] E →SWOT[σ₁₃] G
-- Mathlib.AlgebraicTopology.MooreComplex
CategoryTheory.SimplicialObject.δ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)), X.δ i = X.map (SimplexCategory.δ i).op
-- Mathlib.CategoryTheory.Monad.Limits
/-- `D ⋙ forget T` has a limit, then `D` has a limit.  -/
CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  [CategoryTheory.Limits.HasLimit (D.comp T.forget)], CategoryTheory.Limits.HasLimit D
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_constVSub : ∀ (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₁] (p : P₁), ⇑(AffineEquiv.constVSub k p) = fun x => p -ᵥ x
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{w, v, u} Q], CategoryTheory.ObjectProperty.Small.{w, v, u} (P ⊓ Q)
-- Mathlib.FieldTheory.Relrank
IntermediateField.finrank_comap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E),
  Module.finrank (↥(IntermediateField.comap f A)) L = A.relfinrank f.fieldRange
-- Mathlib.Order.Filter.Bases.Basic
Filter.disjoint_pure_pure : ∀ {α : Type u_1} {x y : α}, Disjoint (pure x) (pure y) ↔ x ≠ y
-- Mathlib.GroupTheory.Torsion
/-- A nontrivial torsion abelian group is not torsion-free.  -/
not_isMulTorsionFree_of_isMulTorsion : ∀ {G : Type u_1} [inst : CommGroup G] [Nontrivial G], IsMulTorsion G → ¬IsMulTorsionFree G
-- Mathlib.Topology.Constructions
closure_subtype : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {x : { a // p a }} {s : Set { a // p a }},
  x ∈ closure s ↔ ↑x ∈ closure (Subtype.val '' s)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.realize_zero : ∀ {α : Type u_1} {M : Type u_2} {v : α → M} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M],
  FirstOrder.Language.Term.realize v 0 = 0
-- Mathlib.Data.Finsupp.Ext
Finsupp.addHom_ext'_iff : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : (α →₀ M) →+ N},
  f = g ↔ ∀ (x : α), f.comp (Finsupp.singleAddHom x) = g.comp (Finsupp.singleAddHom x)
-- Init.Data.List.Basic
List.range'TR.go.eq_1 : ∀ (step a : ℕ) (a_1 : List ℕ), List.range'TR.go step 0 a a_1 = a_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t ≠ ∅ → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Lean.Compiler.InitAttr
Lean.getBuiltinInitFnNameFor? : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.Algebra.Colimit.Ring
Ring.instDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → Ring (Ring.DirectLimit G f)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X Y : CategoryTheory.Limits.Cocone F.op} (f : X ⟶ Y),
  CategoryTheory.Limits.coneOpEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.Raw.ofList l).getKey? k = none
-- Mathlib.Analysis.PSeries
NNReal.summable_condensed_iff : ∀ {f : ℕ → NNReal}, (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) → ((Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.Sheaf.cohomologyPresheaf.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)]
  (F F_1 : CategoryTheory.Sheaf J AddCommGrpCat),
  F = F_1 → ∀ (n n_1 : ℕ), n = n_1 → F.cohomologyPresheaf n = F_1.cohomologyPresheaf n_1
-- Mathlib.Algebra.Notation.Support
Function.support_disjoint_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set ι},
  Disjoint (Function.support f) s ↔ Set.EqOn f 0 s
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The red and the blue arrows in ![this diagram](https://i.imgur.com/q6X1GJ9.png) commute.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))) {Z : C}
  (h :
    ((TopCat.Presheaf.pushforward C (D.t k i).base).obj (D.V (k, i)).presheaf).obj
        (Opposite.op
          ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
                (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj
            U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))
        U)
      (CategoryTheory.CategoryStruct.comp
        ((D.t k i).c.app
          (Opposite.op
            ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
                  (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj
              U)))
        h) =
    CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j)) ((TopologicalSpace.Opens.map (D.t' k i j).base).1 U))
        (CategoryTheory.CategoryStruct.comp ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))
-- Lean.SubExpr
/-- A subexpression of the value of one of the let-bound hypotheses.  -/
Lean.SubExpr.GoalLocation.hypValue : Lean.FVarId → Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
-- Init.Data.String.Basic
String.ofList_inj : ∀ {l₁ l₂ : List Char}, String.ofList l₁ = String.ofList l₂ ↔ l₁ = l₂
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.sty : ProofWidgets.Penrose.DiagramProps → String
-- Mathlib.Order.RelIso.Basic
RelHomClass.asymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) [Std.Asymm s], Std.Asymm r
-- Mathlib.Data.List.Nodup
List.nodup_map_iff_inj_on : ∀ {α : Type u} {β : Type v} {f : α → β} {l : List α},
  l.Nodup → ((List.map f l).Nodup ↔ ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y)
-- Mathlib.Topology.Algebra.GroupWithZero
Continuous.zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀]
  {X : Type u_4} [inst_4 : TopologicalSpace X] {f : X → G₀},
  Continuous f → ∀ (m : ℤ), (∀ (a : X), f a ≠ 0 ∨ 0 ≤ m) → Continuous fun x => f x ^ m
-- Init.Data.Option.Lemmas
Option.isSome_left_of_isSome_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, (o ⊓ o').isSome = true → o.isSome = true
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.order_neg : ∀ {σ : Type u_1} {R : Type u_3} [inst : Ring R] (f : MvPowerSeries σ R), (-f).order = f.order
-- Mathlib.Algebra.Group.Nat.Hom
/-- Monoid homomorphisms from `Multiplicative ℕ` are defined by the image
of `Multiplicative.ofAdd 1`.  -/
powersHom : (M : Type u_1) → [inst : Monoid M] → M ≃ (Multiplicative ℕ →* M)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_l_u_eq_u' : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → u ∘ l ∘ u = u
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instFintype : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [IsDomain R] → [Module.IsTorsionFree R M] → [IsNoetherian R M] → Fintype (LieModule.Weight R L M)
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_apply_of_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β}
  {g : C(↑s, β)} {x : ↑s}, ContinuousOn f s → (ContinuousMap.mkD (s.domRestrict f) g) x = f ↑x
-- Init.Data.Vector.Lex
Vector.le_iff_exists : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs ys : Vector α n}, xs ≤ ys ↔ xs = ys ∨ ∃ i, ∃ (h : i < n), (∀ (j : ℕ) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]
-- Mathlib.Analysis.Calculus.FDeriv.Star
Differentiable.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} [TrivialStar 𝕜],
  Differentiable 𝕜 f → Differentiable 𝕜 fun y => star (f y)
-- Init.Data.Vector.Nat
Vector.prod_pos_iff_forall_pos_nat : ∀ {n : ℕ} {xs : Vector ℕ n}, 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instLE : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [LE β] → LE (l.Germ β)
-- Mathlib.RingTheory.MvPowerSeries.Inverse
/-- Multivariate formal power series over a local ring form a local ring.  -/
MvPowerSeries.instIsLocalRing : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [IsLocalRing R], IsLocalRing (MvPowerSeries σ R)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, t.isEmpty = true → t.getKey! a = default
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight_assoc : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (y : D) (z : C) {x x' : C} (f : x ⟶ x') {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z) x' ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z) f)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso y z x).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight y
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft z f))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso y z x').hom h))
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.setIntegral_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α → ℝ) (g : α → E) (s : Set α),
  ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) • g x ∂μ
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
antitone_mul_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R]
  [AddRightReflectLE R] {a : R}, a ≤ 0 → Antitone fun x => a * x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_sub : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] (f g : P →ᴬ[R] W),
  ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_ne_zero_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.neg_add_cancel : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.add (Lean.Grind.Ring.OfSemiring.neg a) a = Lean.Grind.Ring.OfSemiring.natCast 0