mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Fintype.piFinset_neg : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Neg (α i)] (s : (i : ι) → Finset (α i)), (Fintype.piFinset fun i => -s i) = -Fintype.piFinset s
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.singleton : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : M), IsSemilinearSet {a}
-- Init.CbvSimproc
Lean.Parser.Attr.cbvSimprocAttr : Lean.ParserDescr
-- Init.Data.String.OrderInstances
String.Pos.Raw.toInt_eq : ∀ {p : String.Pos.Raw}, ↑p = ↑p.byteIdx
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_ne_zero_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x ≠ 0 ↔
    ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x ≠ 0
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_1.eq_1 : ∀ (motive : Option Bool → Option Bool → Sort u_1) (x : Option Bool) (h_1 : (x : Option Bool) → motive (some false) x)
  (h_2 : (x : Option Bool) → motive x (some false)) (h_3 : (x : Option Bool) → motive (some true) x)
  (h_4 : (x : Option Bool) → motive x (some true)) (h_5 : (x x_1 : Option Bool) → motive x x_1),
  (match some false, x with
    | some false, x => h_1 x
    | x, some false => h_2 x
    | some true, x => h_3 x
    | x, some true => h_4 x
    | x, x_1 => h_5 x x_1) =
    h_1 x
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
IsTopologicallyNilpotent.exists_pow_mem_of_mem_nhds : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : MonoidWithZero R] {a : R},
  IsTopologicallyNilpotent a → ∀ {v : Set R}, v ∈ nhds 0 → ∃ n, a ^ n ∈ v
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_union : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (s s' : Set A),
  ProjectiveSpectrum.zeroLocus 𝒜 (s ∪ s') = ProjectiveSpectrum.zeroLocus 𝒜 s ∩ ProjectiveSpectrum.zeroLocus 𝒜 s'
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} (f g : A ⟶ B),
  f.hom.hom = g.hom.hom → f = g
-- Mathlib.Data.Num.Basic
instInhabitedZNum : Inhabited ZNum
-- Init.Meta.Defs
/-- Decodes a string literal, removing quotation marks and unescaping escaped characters.

Returns `""` if the syntax is malformed.
 -/
Lean.TSyntax.getString : Lean.StrLit → String
-- Mathlib.Condensed.Discrete.Colimit
/-- The functor `locallyConstantPresheaf` takes cofiltered limits of finite sets with surjective
projection maps to colimits.
 -/
Condensed.isColimitLocallyConstantPresheaf : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    [CategoryTheory.IsCofiltered I] →
      {F : CategoryTheory.Functor I FintypeCat} →
        (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
          (X : Type (u + 1)) →
            CategoryTheory.Limits.IsLimit c →
              [∀ (i : I), CategoryTheory.Epi (c.π.app i)] →
                CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone c.op)
-- Mathlib.Algebra.MvPolynomial.Eval
Algebra.adjoin_range_eq_range_aeval : ∀ (R : Type u) {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁), Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_foldM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.drain = Std.IterM.foldM (fun x x_1 => pure PUnit.unit) PUnit.unit it
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Preregular C] [inst_3 : CategoryTheory.FinitaryExtensive C]
  [∀ (X : C), CategoryTheory.Projective X],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Limits.PreservesFiniteProducts F
-- Mathlib.Data.Matrix.Mul
Matrix.neg_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype m] (v : m → α)
  (A : Matrix m n α), Matrix.vecMul (-v) A = -Matrix.vecMul v A
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trCfg_init : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] [inst_1 : Inhabited Λ]
  [inst_2 : Inhabited σ] (k : K) (L : List (Γ k)),
  Turing.TM2to1.TrCfg (Turing.TM2.init k L) (Turing.TM1.init (Turing.TM2to1.trInit k L))
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instIsRightCancelAdd : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Add (f i)] [∀ (i : I), IsRightCancelAdd (f i)],
  IsRightCancelAdd ((i : I) → f i)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instOne : {R : Type u} → [inst : Semiring R] → One (Polynomial R)
-- Mathlib.FieldTheory.PrimitiveElement
Field.primitive_element_iff_minpoly_natDegree_eq : ∀ (F : Type u_3) {E : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  (α : E), F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = Module.finrank F E
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {toSubsemiring : Subsemiring R}
  {mem_of_isSquare' :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) RingPreordering.mem_of_isSquare'._autoParam}
  {neg_one_notMem' : autoParam (-1 ∉ toSubsemiring.carrier) RingPreordering.neg_one_notMem'._autoParam}
  {toSubsemiring_1 : Subsemiring R}
  {mem_of_isSquare'_1 :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring_1.carrier) RingPreordering.mem_of_isSquare'._autoParam}
  {neg_one_notMem'_1 : autoParam (-1 ∉ toSubsemiring_1.carrier) RingPreordering.neg_one_notMem'._autoParam},
  { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare', neg_one_notMem' := neg_one_notMem' } =
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 } →
    toSubsemiring = toSubsemiring_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.subsemigroupMap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M) (x : ↥M'),
  ↑((f.subsemigroupMap M') x) = f ↑x
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The type of morphisms in the category `Arrow T`.  -/
CategoryTheory.Arrow.Hom : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Arrow T → CategoryTheory.Arrow T → Type v
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.exists_nonzero_dvd : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {s : S},
  IsAlgebraic R s → s ∈ nonZeroDivisors S → ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq : κ) (i₀ i₁ i₂ i₃ : ι) (h₀ : i₀ = data.i₀ r pq ⋯)
  (h₁ : i₁ = data.i₁ pq) (h₂ : i₂ = data.i₂ pq) (h₃ : i₃ = data.i₃ r pq ⋯) (n₀ n₁ n₂ : ℤ) (h : n₁ = data.deg pq)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h ⋯
      ⋯
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- To prove something for an arbitrary simple function, it suffices to show
that the property holds for constant functions and that it is closed under piecewise combinations
of functions.

To use in an induction proof, the syntax is `induction f with`.  -/
MeasureTheory.SimpleFunc.induction' : ∀ {α : Type u_5} {γ : Type u_6} [inst : MeasurableSpace α] [Nonempty γ] {P : MeasureTheory.SimpleFunc α γ → Prop},
  (∀ (c : γ), P (MeasureTheory.SimpleFunc.const α c)) →
    (∀ ⦃f g : MeasureTheory.SimpleFunc α γ⦄ {s : Set α} (hs : MeasurableSet s),
        P f → P g → P (MeasureTheory.SimpleFunc.piecewise s hs f g)) →
      ∀ (f : MeasureTheory.SimpleFunc α γ), P f
-- Mathlib.GroupTheory.Congruence.Defs
Con.toQuotient.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {c : Con M}, Con.toQuotient = Quotient.mk''
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mkCollisionNode : {α : Type u_1} → {β : Type u_2} → α → β → α → β → Lean.PersistentHashMap.Node α β
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whiskering_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x)
  (t : CategoryTheory.Bicategory.LeftExtension f g),
  (CategoryTheory.Bicategory.LeftExtension.whiskering h).obj t = t.whisker h
-- Mathlib.Topology.Separation.Basic
Topology.IsInducing.r0Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R0Space X] [inst_2 : TopologicalSpace Y] {f : Y → X},
  Topology.IsInducing f → R0Space Y
-- Mathlib.Data.NNReal.Defs
/-- **Alias** of the reverse direction of `NNReal.coe_pos`. -/
_private.Mathlib.Data.NNReal.Defs.0.NNReal.Bound.coe_pos_of_pos : ∀ {r : NNReal}, 0 < r → 0 < ↑r
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.coe_eq_coe' : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
  ConnectedComponents.mk x = ConnectedComponents.mk y ↔ x ∈ connectedComponent y
-- Mathlib.Algebra.Group.Units.Hom
/-- If a homomorphism `f : M →* N` sends each element to an `IsUnit`, then it can be lifted
to `f : M →* Nˣ`. See also `Units.liftRight` for a computable version.  -/
IsUnit.liftRight : {M : Type u_3} →
  {N : Type u_4} → [inst : Monoid M] → [inst_1 : Monoid N] → (f : M →* N) → (∀ (x : M), IsUnit (f x)) → M →* Nˣ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Since a convolution unit is a pointwise left Kan extension, maps out of it at
any object are uniquely characterized.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U] {c : C} {v : V}
  {g h : U.obj c ⟶ v},
  (∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ c),
      CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategory.DayConvolutionUnit.can
          (CategoryTheory.CategoryStruct.comp (U.map f) g) =
        CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategory.DayConvolutionUnit.can
          (CategoryTheory.CategoryStruct.comp (U.map f) h)) →
    g = h
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.replaceTopology_eq : ∀ {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ)
  (H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace), m.replaceTopology H = m
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).minKey ⋯ = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.refl : ∀ {X : Type u_1} (U : SetRel X X) [U.IsRefl] (s : Set X), U.IsCover s s
-- Mathlib.Tactic.Ring.RingNF
/-- `ring_nf` simplifies expressions in the language of commutative (semi)rings,
which rewrites all ring expressions into a normal form, allowing variables in the exponents.

`ring_nf` works as both a tactic and a conv tactic.

See also the `ring` tactic for solving a goal which is an equation in the language
of commutative (semi)rings.

* `ring_nf!` will use a more aggressive reducibility setting to identify atoms.
* `ring_nf (config := cfg)` allows for additional configuration (see `RingNF.Config`):
  * `red`: the reducibility setting (overridden by `!`)
  * `zetaDelta`: if true, local let variables can be unfolded (overridden by `!`)
  * `recursive`: if true, `ring_nf` will also recurse into atoms
* `ring_nf at l1 l2 ...` can be used to rewrite at the given locations.

Examples:
This can be used non-terminally to normalize ring expressions in the goal such as
`⊢ P (x + x + x)` ~> `⊢ P (x * 3)`, as well as being able to prove some equations that
`ring` cannot because they involve ring reasoning inside a subterm, such as
`sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
 -/
Mathlib.Tactic.RingNF.tacticRing_nf!__ : Lean.ParserDescr
-- Init.Data.FloatArray.Basic
_private.Init.Data.FloatArray.Basic.0.FloatArray.foldlM.loop : {β : Type v} →
  {m : Type v → Type w} →
    [Monad m] → (β → Float → m β) → (as : FloatArray) → (stop : ℕ) → stop ≤ as.size → ℕ → ℕ → β → m β
-- Init.Grind.Attr
/-- Gadget for representing generalization steps `h : x = val` in patterns
This gadget is used to represent patterns in theorems that have been generalized to reduce the
number of casts introduced during E-matching based instantiation.

For example, consider the theorem
```
Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
    {f : (a_1 : α1) → some a = some a_1 → Option α2}
    : (some a).pbind f = f a rfl
```
Now, suppose we have a goal containing the term `c.pbind g` and the equivalence class
`{c, some b}`. The E-matching module generates the instance
```
(some b).pbind (cast ⋯ g)
```
The `cast` is necessary because `g`'s type contains `c` instead of `some b.
This `cast` problematic because we don't have a systematic way of pushing casts over functions
to its arguments. Moreover, heterogeneous equality is not effective because the following theorem
is not provable in DTT:
```
theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...
```
The standard solution is to generalize the theorem above and write it as
```
theorem Option.pbind_some'
        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
        {x : Option α1}
        {f : (a_1 : α1) → x = some a_1 → Option α2}
        (h : x = some a)
        : x.pbind f = f a h := by
  subst h
  apply Option.pbind_some
```
Internally, we use this gadget to mark the E-matching pattern as
```
(genPattern h x (some a)).pbind f
```
This pattern is matched in the same way we match `(some a).pbind f`, but it saves the proof
for the actual term to the `some`-application in `f`, and the actual term in `x`.

In the example above, `c.pbind g` also matches the pattern `(genPattern h x (some a)).pbind f`,
and stores `c` in `x`, `b` in `a`, and the proof that `c = some b` in `h`.
 -/
Lean.Grind.genPattern : {α : Sort u} → Prop → α → α → α
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The iterated derivative of a function multiplied by `(L v ⬝) ^ n` can be controlled in terms
of the iterated derivatives of the initial function.  -/
VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {K : WithTop ℕ∞} {C : ℝ},
  ContDiff ℝ K f →
    ∀ {n k : ℕ},
      ↑k ≤ K →
        ∀ {v : V},
          (∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C) →
            ‖iteratedFDeriv ℝ k (fun v => VectorFourier.fourierPowSMulRight L f v n) v‖ ≤
              (2 * Real.pi) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instSubsingleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Subsingleton α], Subsingleton (TopologicalSpace.NonemptyCompacts α)
-- Lean.Declaration
Lean.DefinitionVal.hints : Lean.DefinitionVal → Lean.ReducibilityHints
-- Init.Grind.Config
Lean.Grind.CutsatConfig.mk.inj : ∀ {toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig},
  { toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 } → toNoopConfig = toNoopConfig_1
-- Mathlib.Algebra.Group.Action.Defs
/-- Like `Mul.toSMul`, but multiplies on the right.

See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`.  -/
Mul.toSMulMulOpposite : (α : Type u_9) → [Mul α] → SMul αᵐᵒᵖ α
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_add_measure_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ ν : MeasureTheory.Measure α}, AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_sub : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂]
  (f g : M →SL[σ₁₂] M₂), ↑(f - g) = ↑f - ↑g
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.trans_refl : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  e.trans (AddConstEquiv.refl b) = e
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_eq_iff_values_eq_on : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F),
  Set.InjOn v ↑s → ((Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r' ↔ ∀ i ∈ s, r i = r' i)
-- Mathlib.Data.Sym.Basic
Sym.coe_fill : ∀ {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {m : Sym α (n - ↑i)},
  ↑(Sym.fill a i m) = ↑m + ↑(Sym.replicate (↑i) a)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_biUnion_congr : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set ι} {t : ι → Set α},
  s.Countable → (μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i))
-- Mathlib.GroupTheory.Perm.ConjAct
Equiv.Perm.support_toConjAct_eq_smul_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (k g : Equiv.Perm α),
  (ConjAct.toConjAct k • g).support = k • g.support
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f] {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.inv f))
        h) =
    h
-- Init.Data.Nat.Lcm
Nat.gcd_dvd_mul : ∀ (m n : ℕ), m.gcd n ∣ m * n
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_comp' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (φ : S →+* T) (ψ : R →+* S),
  PrimeSpectrum.BasicConstructibleSetData.map (φ.comp ψ) =
    PrimeSpectrum.BasicConstructibleSetData.map φ ∘ PrimeSpectrum.BasicConstructibleSetData.map ψ
-- Mathlib.Topology.Algebra.Ring.Real
NNReal.instContinuousSub : ContinuousSub NNReal
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.singletonSubgraph_verts : ∀ {V : Type u} (G : SimpleGraph V) (v : V), (G.singletonSubgraph v).verts = {v}
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffAt_prod_iff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {x : M} {n : WithTop ℕ∞} (f : M → M' × N'),
  ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x
-- Mathlib.Order.Interval.Set.Image
StrictMono.image_Iio_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictMono f → f '' Set.Iio b ⊆ Set.Iio (f b)
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMax : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms], (P ⊔ Q).IsClosedUnderIsomorphisms
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- This allows us to get `NormedAddCommGroup` and `NormedSpace` instances on `E` via
`NormedAddCommGroup.ofCore` and `NormedSpace.ofCore`.  -/
CStarModule.normedSpaceCore : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [CStarModule A E] [StarOrderedRing A],
  NormedSpace.Core ℂ E
-- Lean.Meta.InferType
Lean.Meta.throwUnknownMVar : {α : Type} → Lean.MVarId → Lean.MetaM α
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.isTable_empty : String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ ByteArray.empty #[]
-- Mathlib.Order.Lex
instInhabitedLex : (α : Type u_2) → [Inhabited α] → Inhabited (Lex α)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.other.injEq : ∀ (name name_1 : Lean.Name), (Lean.Meta.Origin.other name = Lean.Meta.Origin.other name_1) = (name = name_1)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.uniq_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation)
  (g : relations.G), (h.uniq h') (solution.var g) = solution'.var g
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.isoMk_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (h : A₀.a ≅ A₁.a)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom)
      CategoryTheory.Endofunctor.Algebra.isoMk._auto_1),
  (CategoryTheory.Endofunctor.Algebra.isoMk h w).inv.f = h.inv
-- Mathlib.Topology.Homotopy.Basic
/-- Given `HomotopyWith f₀ f₁ P` and `HomotopyWith f₁ f₂ P`, we can define a `HomotopyWith f₀ f₂ P`
by putting the first homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
 -/
ContinuousMap.HomotopyWith.trans : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {P : C(X, Y) → Prop} → {f₀ f₁ f₂ : C(X, Y)} → f₀.HomotopyWith f₁ P → f₁.HomotopyWith f₂ P → f₀.HomotopyWith f₂ P