mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.BuiltinSimprocs.mk.inj : ∀ {keys : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)}
  {procs : Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)}
  {keys_1 : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)}
  {procs_1 : Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)},
  { keys := keys, procs := procs } = { keys := keys_1, procs := procs_1 } → keys = keys_1 ∧ procs = procs_1
-- Mathlib.NumberTheory.Divisors
Int.image_fst_divisorsAntidiag : ∀ {z : ℤ}, Finset.image Prod.fst z.divisorsAntidiag = z.divisors
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_ofNat_iff : ∀ {n : ℕ} [inst : n.AtLeastTwo], Irrational √(OfNat.ofNat n) ↔ ¬IsSquare (OfNat.ofNat n)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J] {i j : Shrink.{u, w} J} (f : (equivShrink J).symm i ⟶ (equivShrink J).symm j),
  CategoryTheory.CategoryStruct.comp (F.map f) ((AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).ι j) =
    (AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).ι i
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.isClopen : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (U : OpenAddSubgroup G),
  IsClopen ↑U
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_inter_Icc_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {x y : α},
  x ∈ s → y ∈ s → ((s ∩ Set.Icc x y).OrdConnected ↔ Set.Ioo x y ⊆ s)
-- Mathlib.Topology.WithTopology
WithTopology.isOpen_iff : ∀ {X : Type u_1} (t : TopologicalSpace X) {s : Set (WithTopology X t)},
  IsOpen s ↔ IsOpen (WithTopology.toTopology t ⁻¹' s)
-- Init.Data.List.SplitOn.Lemmas
/-- The original list `L` can be recovered by flattening the lists produced by `splitOnP p L`,
interspersed with the elements `L.filter p`.  -/
List.splitOnP_spec : ∀ {α : Type u_1} {p : α → Bool} (as : List α),
  (List.zipWith (fun x1 x2 => x1 ++ x2) (List.splitOnP p as)
        (List.map (fun x => [x]) (List.filter p as) ++ [[]])).flatten =
    as
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G)
  [CompleteSpace E],
  m ≤ mΩ →
    ∀ [MeasureTheory.IsFiniteMeasure μ] {f : Ω → F} {g : Ω → E},
      MeasureTheory.AEStronglyMeasurable f μ →
        MeasureTheory.Integrable g μ →
          ∀ (c : ℝ), (∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)
-- Init.Data.List.Count
_private.Init.Data.List.Count.0.List.findIdx.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (l : List α) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match a :: l, n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_2 a l n
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_union_of_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Init.Data.BitVec.Bitblast
BitVec.ule_eq_carry : ∀ {w : ℕ} (x y : BitVec w), x.ule y = BitVec.carry w y (~~~x) true
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_smul_measure : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {R : Type u_7}
  [inst_1 : Semiring R] [IsDomain R] [inst_3 : Module R ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal]
  [Module.IsTorsionFree R ENNReal] {c : R},
  c ≠ 0 → ∀ (f : α → ε), MeasureTheory.eLpNormEssSup f (c • μ) = MeasureTheory.eLpNormEssSup f μ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Given `NonUnitalSubsemiring`s `s`, `t` of semirings `R`, `S` respectively, `s.prod t` is
`s × t` as a non-unital subsemiring of `R × S`.  -/
NonUnitalSubsemiring.prod : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        NonUnitalSubsemiring R → NonUnitalSubsemiring S → NonUnitalSubsemiring (R × S)
-- Std.Time.Format.DateFormat
/-- The minimum number of days that a week must have in the new year to count as week 1.
ISO 8601 uses 4 (week 1 must contain the first Thursday); US locale uses 1 (any week
containing Jan 1 is week 1).
 -/
Std.Time.DateFormat.minimalDaysInFirstWeek : Std.Time.DateFormat → Std.Time.Internal.Bounded.LE 0 6
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.coe_toAddSubsemigroup_symm_apply : ∀ {M : Type u_1} [inst : Mul M] (S : AddSubsemigroup (Additive M)),
  ↑((RelIso.symm Subsemigroup.toAddSubsemigroup) S) = ⇑Additive.ofMul ⁻¹' ↑S
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input.inj : ∀ {p p_1 : Lean.Grind.CommRing.Poly},
  Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p = Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p_1 →
    p = p_1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂),
  CategoryTheory.Comma.mapRightIso R i =
    CategoryTheory.Equivalence.mk'' (CategoryTheory.Comma.mapRight R i.hom) (CategoryTheory.Comma.mapRight R i.inv)
      ((CategoryTheory.Comma.mapRightId L₁ R).symm ≪≫
        CategoryTheory.Comma.mapRightEq R (CategoryTheory.CategoryStruct.id L₁)
            (CategoryTheory.CategoryStruct.comp i.hom i.inv) ⋯ ≪≫
          CategoryTheory.Comma.mapRightComp R i.inv i.hom)
      ((CategoryTheory.Comma.mapRightComp R i.hom i.inv).symm ≪≫
        CategoryTheory.Comma.mapRightEq R (CategoryTheory.CategoryStruct.comp i.inv i.hom)
            (CategoryTheory.CategoryStruct.id L₂) ⋯ ≪≫
          CategoryTheory.Comma.mapRightId L₂ R)
      ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
/-- Given a vector of references `oldLayer`, add the `iterNum`-th couple of elements and
append the result of the addition to `newLayer`  -/
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {outWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth → Std.Sat.AIG.RefVecEntry α outWidth
-- Init.Prelude
List.brecOn.eq : ∀ {α : Type u} {motive : List α → Sort u_1} (t : List α) (F_1 : (t : List α) → List.below t → motive t),
  List.brecOn t F_1 = F_1 t (List.brecOn.go t F_1).2
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.of_leftInverse : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {g : Y → X},
  Function.LeftInverse f g → Continuous f → Continuous g → Topology.IsEmbedding g
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.eventuallyLT_norm_of_eventually_pos : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g → (∀ᶠ (x : α) in l, 0 < ‖g x‖) → ∀ᶠ (x : α) in l, ‖f x‖ < ‖g x‖
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.discreteHomFintype : {α : Type u_1} → (X Y : CategoryTheory.Discrete α) → Fintype (X ⟶ Y)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epimorphism is a morphism which is the cokernel of some morphism.  -/
CategoryTheory.NormalEpi.W : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X Y : C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} → (f : X ⟶ Y) → [self : CategoryTheory.NormalEpi f] → C
-- Init.Data.Sum.Basic
Sum.elim_inl : ∀ {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ) (x : α), Sum.elim f g (Sum.inl x) = f x
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- The type of strongly connected components (bidirectional reachability classes).  -/
Quiver.StronglyConnectedComponent : (V : Type u_2) → [Quiver V] → Type u_2
-- Mathlib.Computability.Primrec.Basic
Primrec₂.natPair : Primrec₂ Nat.pair
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_σ_of_gt' : ∀ {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.σ j) =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (j.castLT ⋯)) (SimplexCategory.δ (i.pred ⋯))
-- Mathlib.Algebra.Lie.Basic
Module.Dual.lie_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [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] (x : L)
  (m : M) (f : M →ₗ[R] R), ⁅x, f⁆ m = -f ⁅x, m⁆
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive
call site.
 -/
Lean.Elab.WF.GuessLex.collectRecCalls : Lean.Elab.PreDefinition →
  Lean.Elab.FixedParamPerms → Lean.Meta.ArgsPacker → Lean.MetaM (Array Lean.Elab.WF.GuessLex.RecCallWithContext)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_insert_zero : ∀ {α : Type u} [inst : Semiring α] {s : Set α}, Ideal.span (insert 0 s) = Ideal.span s
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.ByteArray.push.match_1.splitter : (motive : ByteArray → UInt8 → Sort u_1) →
  (x : ByteArray) → (x_1 : UInt8) → ((bs : Array UInt8) → (b : UInt8) → motive { data := bs } b) → motive x x_1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_zero_eq_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, iteratedFDerivWithin 𝕜 0 f s = ⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
-- Mathlib.Algebra.Order.Monoid.NatCast
ZeroLEOneClass.neZero.four : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  NeZero 4
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.forgetReflectIsos : (CategoryTheory.forget CommSemiRingCat).ReflectsIsomorphisms
-- Aesop.Tree.Data
Aesop.GoalState.isIrrelevant : Aesop.GoalState → Bool
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_addSubgroup_op : ∀ {G : Type u_1} [inst : AddGroup G] (s : AddSubgroup Gᵃᵒᵖ), AddAction.stabilizer G ↑s = s.unop
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `Function.const` is a continuous function.  -/
OmegaCompletePartialOrder.ContinuousHom.const : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → β → α →𝒄 β
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.next_apply₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (α : ODE.FunSpace t₀ x₀ r L), (ODE.FunSpace.next hf hx α).toFun t₀ = x
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.ind_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  P ≤ CategoryTheory.MorphismProperty.isFinitelyPresentable C →
    ∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsFinitelyAccessibleCategory (CategoryTheory.Under X)],
      P.ind f ↔
        ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
          CategoryTheory.MorphismProperty.isFinitelyPresentable C p →
            CategoryTheory.CategoryStruct.comp p g = f →
              ∃ W u v, CategoryTheory.CategoryStruct.comp u v = g ∧ P (CategoryTheory.CategoryStruct.comp p u)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertMany_append : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {l₁ l₂ : List (α × β)},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.instNormalCenter : ∀ {G : Type u_1} [inst : Group G], (Subgroup.center G).Normal
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (A A_1 : Finset G),
  A = A_1 → ∀ (B B_1 : Finset G), B = B_1 → A.mulConst B = A_1.mulConst B_1
-- Mathlib.Algebra.Module.Torsion.Free
IsSMulRegular.of_ne_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → IsSMulRegular M r
-- Mathlib.Data.ZMod.Basic
/-- So-named because the coercion is `Nat.cast` into `ZMod`. For `Nat.cast` into an arbitrary ring,
see `ZMod.natCast_val`.  -/
ZMod.natCast_zmod_val : ∀ {n : ℕ} [NeZero n] (a : ZMod n), ↑a.val = a
-- Mathlib.Data.Vector.Basic
List.Vector.nil.eq_1 : ∀ {α : Type u_1}, List.Vector.nil = ⟨[], ⋯⟩
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.toFormula.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (f : L.BoundedFormula α (x + 1)),
  f.all.toFormula =
    (FirstOrder.Language.BoundedFormula.relabel
        (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f.toFormula).all
-- Mathlib.Analysis.Normed.Module.RCLike.Real
exists_norm_eq : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] {c : ℝ},
  0 ≤ c → ∃ x, ‖x‖ = c
-- Lean.Parser.Extra
Lean.Parser.many1Indent.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α}
  [inst_3 : Inhabited (β a)] {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).get! a = default
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.im_coe : ∀ (z : Complex.UnitDisc), (↑z).im = z.im
-- Mathlib.GroupTheory.Transfer
Subgroup.coe_transferFunction : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G) (q : G ⧸ H), ↑(H.transferFunction g q) = q
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.instNatCast : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommMonoid (A i)] →
        [inst_1 : AddMonoid ι] → [DirectSum.GSemiring A] → NatCast (DirectSum ι fun i => A i)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is an open partial homeomorph.
This gives us an `e` that is defined on a subset of `f.source`.  -/
OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  (f : OpenPartialHomeomorph H H) {s : Set H} {x : H},
  x ∈ f.source ∪ sᶜ →
    (G.IsLocalStructomorphWithinAt (↑f) s x ↔
      x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source)
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_rii : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_rii._auto_1) {t : Std.TreeSet α cmp},
  Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.mk_eq_of_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g f' : a ⟶ b} {η θ : f ⟶ g} {η' θ' : f ≅ g}
  (η_f : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f')
  (η_g : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ≅ f'),
  η'.hom = η →
    θ'.hom = θ →
      CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) η' ≪≫ η_g = η_f →
        CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) θ' ≪≫ η_g = η_f → η = θ
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoal.goal : Lean.Lsp.PlainTermGoal → String