mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObjIsoOfRepresentableBy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X),
  CategoryTheory.yonedaMonObjIsoOfRepresentableBy X F α =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        (let __Equiv := α.homEquiv';
          { toEquiv := __Equiv, map_mul' := ⋯ }).toMonCatIso)
      ⋯
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.instNonemptySubtypeMemAffineSubspaceRealOrthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P), Nonempty ↥(s.orthRadius p)
-- Lean.LocalContext
Lean.LocalContext.auxDeclToFullName : Lean.LocalContext → Lean.FVarIdMap Lean.Name
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval : ∀ (i : ℕ) (v : Lean.Omega.Coeffs), (Lean.Omega.LinearCombo.coordinate i).eval v = v.get i
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_closure_eq_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G},
  AddSubgroup.normalClosure ↑(AddSubgroup.closure s) = AddSubgroup.normalClosure s
-- Mathlib.GroupTheory.Finiteness
Group.fg_of_mul_group_fg : ∀ {H : Type u_4} [inst : AddGroup H] [AddGroup.FG H], Group.FG (Multiplicative H)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forgetComp_hom_app : ∀ {W : Type v'} [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory W C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory W D]
  {E : Type u₃} [inst_4 : CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D)
  (G : CategoryTheory.EnrichedFunctor W D E) (X : CategoryTheory.ForgetEnrichment W C),
  (F.forgetComp G).hom.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of W (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to W X))))
-- Lean.Elab.DeclModifiers
/-- Adds attribute `attr` in `modifiers`, at the beginning  -/
Lean.Elab.Modifiers.addFirstAttr : Lean.Elab.Modifiers → Lean.Elab.Attribute → Lean.Elab.Modifiers
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp₂_contDiffOn : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂] [inst_7 : NormedSpace 𝕜 E₁]
  [inst_8 : NormedSpace 𝕜 E₂] {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : Set F},
  ContDiff 𝕜 n g → ContDiffOn 𝕜 n f₁ s → ContDiffOn 𝕜 n f₂ s → ContDiffOn 𝕜 n (fun x => g (f₁ x, f₂ x)) s
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The cocone over the proposed colimit ring.  -/
RingCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J RingCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_sub_lt_right : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  p.degree = q.degree → q ≠ 0 → p.leadingCoeff = q.leadingCoeff → (p - q).degree < q.degree
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The composition of two ContinuousMulEquiv.  -/
ContinuousMulEquiv.trans : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : Mul M] →
          [inst_3 : Mul N] →
            {L : Type u_3} → [inst_4 : Mul L] → [inst_5 : TopologicalSpace L] → M ≃ₜ* N → N ≃ₜ* L → M ≃ₜ* L
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.fst_exp : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [Algebra ℚ R] [Module ℚ M]
  [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : IsCentralScalar R M] [inst_7 : TopologicalSpace R]
  [inst_8 : TopologicalSpace M] [inst_9 : IsTopologicalRing R] [inst_10 : IsTopologicalAddGroup M]
  [inst_11 : ContinuousSMul R M] [inst_12 : ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M),
  (NormedSpace.exp x).fst = NormedSpace.exp x.fst
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.ae_map_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ {p : β → Prop} {μ : MeasureTheory.Measure α},
      (∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
-- Lean.Declaration
Lean.AxiomVal.isUnsafe : Lean.AxiomVal → Bool
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- If two triangles have two points the same, and twice the angle at the third point the same,
they have the same circumsphere.  -/
Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t₁ t₂ : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        t₁.points i₁ = t₂.points i₁ →
          t₁.points i₃ = t₂.points i₃ →
            2 • EuclideanGeometry.oangle (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) =
                2 • EuclideanGeometry.oangle (t₂.points i₁) (t₂.points i₂) (t₂.points i₃) →
              Affine.Simplex.circumsphere t₁ = Affine.Simplex.circumsphere t₂
-- Mathlib.Data.Multiset.Defs
Multiset.decidableMem : {α : Type u_1} → [DecidableEq α] → (a : α) → (s : Multiset α) → Decidable (a ∈ s)
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.parallelPair_pullback_initial : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X B : C} (π : X ⟶ B)
  (c : CategoryTheory.Limits.PullbackCone π π) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.parallelPair (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.fst ⋯)).op
      (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.snd ⋯)).op).Initial
-- Mathlib.Data.List.Basic
List.Forall.imp : ∀ {α : Type u} {p q : α → Prop}, (∀ (x : α), p x → q x) → ∀ {l : List α}, List.Forall p l → List.Forall q l
-- Mathlib.Logic.Function.Basic
cast_inj : ∀ {α β : Type u} (h : α = β) {x y : α}, cast h x = cast h y ↔ x = y
-- Init.Data.List.Lemmas
List.head?_concat_concat : ∀ {α : Type u_1} {l : List α} {a b : α}, (l ++ [a, b]).head? = (l ++ [a]).head?
-- Lean.Structure
/-- Returns true iff `constName` is a non-recursive inductive datatype that has only one constructor and no indices.

Such types have special kernel support (e.g. the eta rule). This must be in sync with `is_non_rec_structure()`.
 -/
Lean.isNonRecStructure : Lean.Environment → Lean.Name → Bool
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.instInhabitedCombinatorAttribute.default : Lean.ParserCompiler.CombinatorAttribute
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Map `WithInitial` with respect to a functor `F : C ⥤ D`.  -/
CategoryTheory.WithInitial.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (CategoryTheory.WithInitial C) (CategoryTheory.WithInitial D)
-- Init.Data.List.Lemmas
List.all_filter : ∀ {α : Type u_1} {l : List α} {p q : α → Bool}, (List.filter p l).all q = l.all fun a => !p a || q a
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Eta-expanded form of `Function.HasTemperateGrowth.mul`

---

The product of two functions of temperate growth is again of temperate growth.  -/
Function.HasTemperateGrowth.fun_mul : ∀ {R : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing R]
  [inst_3 : NormedAlgebra ℝ R] {f g : E → R},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth fun i => f i * g i
-- Init.Grind.ToInt
/-- The embedding function lands in the interval.  -/
Lean.Grind.ToInt.toInt_mem : ∀ {α : Type u} {range : outParam Lean.Grind.IntInterval} [self : Lean.Grind.ToInt α range] (x : α), ↑x ∈ range
-- Init.Data.Array.Lemmas
Array.instDecidableExistsAndMemOfDecidablePred : {α : Type u_1} → {xs : Array α} → {p : α → Prop} → [DecidablePred p] → Decidable (∃ x ∈ xs, p x)
-- Init.Data.Nat.Order
Nat.instLawfulOrderLT : Std.LawfulOrderLT ℕ
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.beckCofork_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  (CategoryTheory.Monad.beckCofork X).π = X.a
-- Init.Data.Array.Subarray
/-- A region of some underlying array.

A subarray contains an array together with the start and end indices of a region of interest.
Subarrays can be used to avoid copying or allocating space, while being more convenient than
tracking the bounds by hand. The region of interest consists of every index that is both greater
than or equal to `start` and strictly less than `stop`.
 -/
Subarray : Type u → Type u
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_sInf : ∀ {R : Type u} [inst : NonAssocRing R] {S : Set (Subring R)} {x : R}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.coe_unit_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] (u : (Associates M)ˣ), ↑u = 1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.realize_transitive : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
  M ⊨ r.transitive ↔ IsTrans M fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
-- Mathlib.Order.UpperLower.Hom
LowerSet.iicInfHom_apply : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a : α), LowerSet.iicInfHom a = LowerSet.Iic a
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorph.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → ∀ (x : X), Filter.map f (nhds x) = nhds (f x)
-- Lean.Syntax
Lean.Syntax.replaceM : {m : Type → Type} → [Monad m] → (Lean.Syntax → m (Option Lean.Syntax)) → Lean.Syntax → m Lean.Syntax
-- Mathlib.Data.NNRat.Defs
NNRat.lt_def : ∀ {p q : ℚ≥0}, p < q ↔ p.num * q.den < q.num * p.den
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lifts.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x : PiTensorProduct R fun i => s i), x.lifts = {p | ↑p = x}
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a coherence isomorphism.  -/
Mathlib.Tactic.BicategoryLike.CoherenceHom.tgt : Mathlib.Tactic.BicategoryLike.CoherenceHom → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.conjMap_comp : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g h k : G} {a b c : α} (hg : b = g • a)
  (hh : c = h • b) (hk : c = k • a) (H : k = h * g),
  (SubMulAction.ofStabilizer.conjMap hh).comp (SubMulAction.ofStabilizer.conjMap hg) =
    SubMulAction.ofStabilizer.conjMap hk
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_of_not_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  ¬LinearIndependent R ![P.root i, P.root j] → RootPairing.chainTopCoeff i j = 0
-- Mathlib.Analysis.Real.Sqrt
Real.le_sqrt_of_sq_le : ∀ {x y : ℝ}, x ^ 2 ≤ y → x ≤ √y
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.support_eq_bot : ∀ {F : Type u_2} [inst : Field F] (P : RingPreordering F), P.support = ⊥
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.eq_zero_of_mulVec_eq_zero : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R}
  [NoZeroDivisors R], M.det ≠ 0 → ∀ {v : m → R}, M.mulVec v = 0 → v = 0
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_singleton_univ : ∀ {α : Type u_1}, MeasurableSpace.generateFrom {Set.univ} = ⊥
-- Mathlib.Data.Fintype.EquivFin
Function.Embedding.nonempty_of_card_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β],
  Fintype.card α ≤ Fintype.card β → Nonempty (α ↪ β)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_addLeft : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  (MeasurableEquiv.addLeft g).symm = MeasurableEquiv.addLeft (-g)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.hasIntScalar : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → SMul ℤ (LeftInvariantDerivation I G)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_ofNat_lt_lift : ∀ {o : Ordinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Ordinal.omega (OfNat.ofNat n) < Ordinal.lift.{v, u} o ↔ Ordinal.omega (OfNat.ofNat n) < o
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenexImp.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 x_2 : L.BoundedFormula α x),
  x_1.toPrenexImp x_2 =
    match x, x_1, x_2 with
    | n, (φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum, ψ =>
      (φ.toPrenexImp (FirstOrder.Language.BoundedFormula.liftAt 1 n ψ)).all
    | n, φ.all, ψ => (φ.toPrenexImp (FirstOrder.Language.BoundedFormula.liftAt 1 n ψ)).ex
    | x, φ, ψ => φ.toPrenexImpRight ψ
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.instDecidableEqXWithInfinity : {A B : GrpCat} → (f : A ⟶ B) → DecidableEq (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [P.ContainsIdentities] [P.RespectsIso], P.precoverage.HasIsos
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.hexagon_reverse_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom
      (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).inv Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).inv) h))
-- Lean.Structure
/-- Gets the `StructureFieldInfo` for the given direct field of the structure.  -/
Lean.getFieldInfo? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.StructureFieldInfo
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_ofReal_mul_I : ∀ (x : ℝ), Complex.exp (↑x * Complex.I) = ↑(Real.cos x) + ↑(Real.sin x) * Complex.I
-- Init.Data.List.MapIdx
List.getElem?_mapIdx : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α} {i : ℕ}, (List.mapIdx f l)[i]? = Option.map (f i) l[i]?
-- Mathlib.Algebra.Order.ZeroLEOne
Prod.instZeroLEOneClass : ∀ {R : Type u_2} {S : Type u_3} [inst : Zero R] [inst_1 : One R] [inst_2 : LE R] [ZeroLEOneClass R] [inst_4 : Zero S]
  [inst_5 : One S] [inst_6 : LE S] [ZeroLEOneClass S], ZeroLEOneClass (R × S)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.symm_piecewise : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} [inst_2 : (x : X) → Decidable (x ∈ s)]
  [inst_3 : (y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
  (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)),
  (e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Finset.Lattice.Fold
Finset.lt_sup'_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α},
  a < s.sup' H f ↔ ∃ b ∈ s, a < f b
-- Init.Data.Iterators.Consumers.Total
/-- A wrapper around an iterator that provides strictly terminating consumers. See
`Iter.ensureTermination`.
 -/
Std.Iter.Total : {α : Type w} → Type w → Type w
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.mk.injEq : ∀ {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.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.equivApp_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (g : G) (X : FDRep k G),
  (TannakaDuality.FiniteGroup.equivApp g X).hom = CategoryTheory.InducedCategory.homMk (ModuleCat.ofHom (X.ρ g))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ},
  (Std.ExtTreeMap.filterMap f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), (f (t.getKey k h) t[k]).isSome = true
-- Mathlib.Analysis.Fourier.AddCircle
/-- Express Fourier coefficients of `f` on an interval in terms of those of its derivative.  -/
fourierCoeffOn_of_hasDerivAt : ∀ {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ},
  n ≠ 0 →
    (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
      IntervalIntegrable f' MeasureTheory.volume a b →
        fourierCoeffOn hab f n =
          1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
-- Init.Data.Vector.Find
Vector.findSomeRev?_push : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {a : α} {f : α → Option β},
  Vector.findSomeRev? f (xs.push a) = (f a).or (Vector.findSomeRev? f xs)
-- Init.Data.SInt.Lemmas
Int16.iSizeMinValue_le_toInt : ∀ (x : Int16), ISize.minValue.toInt ≤ x.toInt
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
act_rel_of_rel_of_act_rel : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [CovariantClass M N μ r] [IsTrans N r] (m : M)
  {a b c : N}, r a b → r (μ m b) c → r (μ m a) c
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsComonHom.hom_comul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.ComonObj M} {inst_3 : CategoryTheory.ComonObj N} (f : M ⟶ N)
  [self : CategoryTheory.IsComonHom f] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj N N ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) h)
-- Mathlib.Data.Fintype.Card
Fintype.subtype_card : ∀ {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x), Fintype.card { x // p x } = s.card
-- Aesop.Script.Step
Aesop.Script.Step.mk : Lean.Meta.SavedState →
  Lean.MVarId → Aesop.Script.Tactic → Lean.Meta.SavedState → Array Aesop.GoalWithMVars → Aesop.Script.Step
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex ℝ ι` is path connected.  -/
isPathConnected_stdSimplex : ∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι], IsPathConnected (stdSimplex ℝ ι)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.instAlgebra : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → Algebra K (IsDedekindDomain.FiniteAdeleRing R K)
-- Mathlib.Algebra.Group.Defs
AddRightCancelMonoid.toIsRightCancelAdd : ∀ {M : Type u} [self : AddRightCancelMonoid M], IsRightCancelAdd M
-- Init.Data.SInt.Lemmas
Int64.ofInt_eq_iff_bmod_eq_toInt : ∀ (a : ℤ) (b : Int64), Int64.ofInt a = b ↔ a.bmod (2 ^ 64) = b.toInt
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.toMul_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : Additive α}, Additive.toMul a ≤ Additive.toMul b ↔ a ≤ b
-- Mathlib.Topology.MetricSpace.IsometricSMul
Units.isIsometricSMul : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X] [inst_3 : Monoid M],
  IsIsometricSMul Mˣ X
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → FunLike (FrameHom α β) α β
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂)[k]? = none
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.scoped.inj : ∀ {α : Type} {a : Lean.Name} {a_1 : α} {a_2 : Lean.Name} {a_3 : α},
  Lean.ScopedEnvExtension.Entry.scoped a a_1 = Lean.ScopedEnvExtension.Entry.scoped a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.aux_size_modify : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] {k : α} {f : β k → β k}
  {t : Std.DTreeMap.Internal.Impl α β}, (Std.DTreeMap.Internal.Impl.modify k f t).size = t.size
-- Mathlib.GroupTheory.Torsion
AddCommGroup.torsion_sum : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H],
  AddCommGroup.torsion (G × H) = (AddCommGroup.torsion G).prod (AddCommGroup.torsion H)
-- Mathlib.Order.GaloisConnection.Basic
OrderIso.bddAbove_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
  BddAbove (⇑e '' s) ↔ BddAbove s
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.encode.match_1.splitter : (motive : Mathlib.Deriving.Encodable.S✝ → Sort u_1) →
  (x : Mathlib.Deriving.Encodable.S✝) →
    ((n : ℕ) → motive (Mathlib.Deriving.Encodable.S.nat✝ n)) →
      ((a b : Mathlib.Deriving.Encodable.S✝) → motive (Mathlib.Deriving.Encodable.S.cons✝ a b)) → motive x
-- Init.Data.BitVec.Lemmas
BitVec.ne_of_lt : ∀ {n : ℕ} {x y : BitVec n}, x < y → x ≠ y
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_eq_nil_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {p : Equiv.Perm α} {x : α}, p.toList x = [] ↔ x ∉ p.support