mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.forM_eq_forMUncurried : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.ExtDTreeMap.forM f t = Std.ExtDTreeMap.Const.forMUncurried (fun a => f a.1 a.2) t
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.collectFVars : Lean.Meta.Match.AltLHS → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Std.Time.DateTime
/-- Determines the quarter of the year for the given `DateTime`.
 -/
Std.Time.DateTime.quarter : Std.Time.DateTime → Std.Time.Internal.Bounded.LE 1 4
-- Aesop.RuleSet.Name
Aesop.localRuleSetName : Aesop.RuleSetName
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.mk.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (toLieModuleHom toLieModuleHom_1 : M →ₗ⁅R,L⁆ N)
  (e_toLieModuleHom : toLieModuleHom = toLieModuleHom_1) (invFun invFun_1 : N → M) (e_invFun : invFun = invFun_1)
  (left_inv : Function.LeftInverse invFun (↑toLieModuleHom).toFun)
  (right_inv : Function.RightInverse invFun (↑toLieModuleHom).toFun),
  { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_compLeft : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix b) (B.compLeft f) =
    ((LinearMap.toMatrix b b) f).transpose * (LinearMap.BilinForm.toMatrix b) B
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.Submartingale.predictablePart_nonneg : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E],
  MeasureTheory.Submartingale f ℱ μ → ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ MeasureTheory.predictablePart f ℱ μ n ω
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] {G : SimpleGraph α} {a : α} (p p_1 : G.Walk a a),
  p = p_1 → p.IsHamiltonianCycle = p_1.IsHamiltonianCycle
-- Mathlib.Order.FixedPoints
/-- Previous fixed point of a monotone map. If `f` is a monotone self-map of a complete lattice and
`x` is a point such that `f x ≤ x`, then `f.prevFixed x hx` is the greatest fixed point of `f`
that is less than or equal to `x`.  -/
OrderHom.prevFixed : {α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → (x : α) → f x ≤ x → ↑(Function.fixedPoints ⇑f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.get_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂),
  t₁.get k hk = t₂.get k ⋯
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_apply : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq α]
  [inst_3 : DecidableRel G.Adj] {a : α} {e : Sym2 α}, SimpleGraph.incMatrix R G a e = (G.incidenceSet a).indicator 1 e
-- Init.Data.List.Basic
List.modifyHead_cons : ∀ {α : Type u} {a : α} {l : List α} {f : α → α}, List.modifyHead f (a :: l) = f a :: l
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.noAccidental : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] {s : Finset α},
  ThreeAPFree ↑s → SimpleGraph.TripartiteFromTriangles.NoAccidental (triangleIndices✝ s)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_congr' : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {B : Set ℕ} [inst_1 : DecidablePred fun x => x ∈ B],
  (∀ n > 0, n ∈ A ↔ n ∈ B) → schnirelmannDensity A = schnirelmannDensity B
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_zero_of_add_nonpos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [AddLeftMono α] {a b : α},
  0 ≤ a → 0 ≤ b → a + b ≤ 0 → a = 0
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomRight : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (d : C) (x x_1 : CategoryTheory.Functor C C)
  (f : x ⟶ x_1), CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f = f.app d
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_succ : ∀ {n : ℕ} (i : Fin n) {M : Type u_1} [inst : Zero M] (y : M) (s : Fin n →₀ M), (Finsupp.cons y s) i.succ = s i
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_restrict_iff_comap_subtype : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {s : Set α},
  MeasurableSet s →
    ∀ {μ : MeasureTheory.Measure α} {f : α → β},
      AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ Subtype.val) (MeasureTheory.Measure.comap Subtype.val μ)
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_lt_iff_lt : ∀ {a b : ℤ} (ha₁ : ISize.minValue.toInt ≤ a) (ha₂ : a ≤ ISize.maxValue.toInt) (hb₁ : ISize.minValue.toInt ≤ b)
  (hb₂ : b ≤ ISize.maxValue.toInt), ISize.ofIntLE a ha₁ ha₂ < ISize.ofIntLE b hb₁ hb₂ ↔ a < b
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.sign.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n.succ)) (h_2 : Unit → motive (Int.ofNat 0))
  (h_3 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.ofNat n.succ with
    | Int.ofNat n.succ => h_1 n
    | Int.ofNat 0 => h_2 ()
    | Int.negSucc a => h_3 a) =
    h_1 n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is nonzero, the last two points are not
equal.  -/
EuclideanGeometry.right_ne_of_oangle_sign_ne_zero : ∀ {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)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0 → p₃ ≠ p₂
-- Mathlib.Data.Real.Basic
/-- A function `f : R → ℝ` is power-multiplicative if for all `r ∈ R` and all positive `n ∈ ℕ`,
`f (r ^ n) = (f r) ^ n`.  -/
IsPowMul : {R : Type u_1} → [Pow R ℕ] → (R → ℝ) → Prop
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_sym : ∀ {α : Type u_1} (a : α), SymAlg.unsym (SymAlg.sym a) = a
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_eq_one : ∀ {r : ℝ}, ENNReal.ofReal r = 1 ↔ r = 1
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.of_toReal : ∀ {p q : ENNReal}, p.toReal.HolderConjugate q.toReal → p.HolderConjugate q
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_iff : ∀ {x : ℝ*}, x.Infinite ↔ ArchimedeanClass.mk x < 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- This instance applies more often than `hasBiproduct_of_preserves`, but the discrimination
tree key matches a lot more (since it does not look through lambdas).  -/
CategoryTheory.Functor.hasBiproduct_of_preserves' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproduct f F],
  CategoryTheory.Limits.HasBiproduct fun i => F.obj (f i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Monotone.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [AddRightMono α],
  Monotone f → ∀ (a : α), Monotone fun x => f x + a
-- Mathlib.Algebra.Order.IsBotOne
instZeroLEOneClassOfIsBotZeroClass : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Zero α] [inst_2 : One α] [IsBotZeroClass α], ZeroLEOneClass α
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalAddGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  CompleteSpace G ↔ CompleteSpace G
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.ext : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F}
  (f g : c ⟶ c'), f.hom = g.hom → f = g
-- Mathlib.Order.Interval.Basic
Interval.coe_sSubset_coe : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Interval α}, ↑s ⊂ ↑t ↔ s < t
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_smul : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Module R S] (φ : PowerSeries S)
  (a : R), PowerSeries.constantCoeff (a • φ) = a • PowerSeries.constantCoeff φ
-- Mathlib.CategoryTheory.Localization.Composition
CategoryTheory.Localization.uniq.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5}
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂]
  (L₁ L₁_1 : CategoryTheory.Functor C D₁) (e_L₁ : L₁ = L₁_1) (L₂ L₂_1 : CategoryTheory.Functor C D₂) (e_L₂ : L₂ = L₂_1)
  (W' W'_1 : CategoryTheory.MorphismProperty C) (e_W' : W' = W'_1) [inst_3 : L₁.IsLocalization W']
  [inst_4 : L₂.IsLocalization W'],
  CategoryTheory.Localization.uniq L₁ L₂ W' = CategoryTheory.Localization.uniq L₁_1 L₂_1 W'_1
-- Init.Core
/-- A dependent recursion principle for `Quot` that takes the quotient first. It is analogous to the
[recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
 * `Quot.lift` is useful for defining non-dependent functions.
 * `Quot.ind` is useful for proving theorems about quotients.
 * `Quot.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quot.hrecOn` uses [heterogeneous equality](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=HEq) instead of rewriting with
   `Quot.sound`.

`Quot.rec` is a version of this recursor that takes the quotient parameter last.
 -/
Quot.recOn : {α : Sort u} →
  {r : α → α → Prop} →
    {motive : Quot r → Sort v} →
      (q : Quot r) → (f : (a : α) → motive (Quot.mk r a)) → (∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) → motive q
-- Init.Conv
/-- Reduces the target to Weak Head Normal Form. This reduces definitions
in "head position" until a constructor is exposed. For example, `List.map f [a, b, c]`
weak head normalizes to `f a :: List.map f [b, c]`.  -/
Lean.Parser.Tactic.Conv.whnf : Lean.ParserDescr
-- Mathlib.Logic.Relation
Relation.ReflTransGen.total_of_right_unique : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
  Relator.RightUnique r →
    Relation.ReflTransGen r a b →
      Relation.ReflTransGen r a c → Relation.ReflTransGen r b c ∨ Relation.ReflTransGen r c b
-- Mathlib.Order.Category.BddLat
BddLat.instLargeCategory : CategoryTheory.LargeCategory BddLat
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- Given a morphism property `W`, the `multiplicativeClosure W` is the smallest
multiplicative property greater than or equal to `W`.  -/
CategoryTheory.MorphismProperty.multiplicativeClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Init.Data.Int.Gcd
Int.gcd_ediv_gcd_ediv_gcd_of_ne_zero_right : ∀ {n m : ℤ}, m ≠ 0 → (n / ↑(n.gcd m)).gcd (m / ↑(n.gcd m)) = 1
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
Finset.lcm_eq_prod : ∀ {ι : Type u_1} {s : Finset ι} {f : ι → ℕ}, (↑s).Pairwise (Function.onFun Nat.Coprime f) → s.lcm f = s.prod f
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportState.mk.injEq : ∀ (moduleNameMap : Std.HashMap Lean.Name Lean.ImportedModule✝) (moduleNames : Array Lean.Name)
  (moduleNameMap_1 : Std.HashMap Lean.Name Lean.ImportedModule✝) (moduleNames_1 : Array Lean.Name),
  ({ moduleNameMap := moduleNameMap, moduleNames := moduleNames } =
      { moduleNameMap := moduleNameMap_1, moduleNames := moduleNames_1 }) =
    (moduleNameMap = moduleNameMap_1 ∧ moduleNames = moduleNames_1)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.subgroupOf_sup : ∀ {G : Type u_1} [inst : Group G] {A A' B : Subgroup G},
  A ≤ B → A' ≤ B → (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.withAutoBoundImplicit.loop : {α : Type} →
  Lean.Elab.TermElabM α → Lean.Elab.Term.SavedState → Lean.Elab.AutoBoundImplicitContext → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddGroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α],
  Lex.instAddGroup = { toSubNegMonoid := Lex.instSubNegAddMonoid, neg_add_cancel := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.mul_inv_cancel_of_le_one : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDedekindDomain A] {I : Ideal A},
  I ≠ ⊥ → (↑I * (↑I)⁻¹)⁻¹ ≤ 1 → ↑I * (↑I)⁻¹ = 1
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.coe_of : ∀ (X : Type u) [inst : MeasurableSpace X], { carrier := X, str := inst }.carrier = X
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.flatMap_mk : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (l : List Γ) (f : Γ → List Γ')
  (hf : ∃ n, f default = List.replicate n default),
  (Turing.ListBlank.mk l).flatMap f hf = Turing.ListBlank.mk (List.flatMap f l)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMonoidMorphism.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {H' : Type u_5} {inst_4 : TopologicalSpace H'}
  {E' : Type u_6} {inst_5 : NormedAddCommGroup E'} {inst_6 : NormedSpace 𝕜 E'} {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} {inst_7 : TopologicalSpace G}
  {inst_8 : ChartedSpace H G} {inst_9 : Monoid G} {G' : Type u_9} {inst_10 : TopologicalSpace G'}
  {inst_11 : ChartedSpace H' G'} {inst_12 : Monoid G'} {toMonoidHom : G →* G'}
  {contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom).toFun} {toMonoidHom_1 : G →* G'}
  {contMDiff_toFun_1 : ContMDiff I I' n (↑toMonoidHom_1).toFun},
  { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun } =
      { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.Order.Hom.CompleteLattice
FrameHomClass.mk : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [toInfTopHomClass : InfTopHomClass F α β],
  (∀ (f : F) (s : Set α), f (sSup s) = sSup (⇑f '' s)) → FrameHomClass F α β
-- Mathlib.Data.Int.ModEq
Dvd.dvd.zero_modEq_int : ∀ {n a : ℤ}, n ∣ a → 0 ≡ a [ZMOD n]
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- Variant of `single_v_eq_zero` where the assumption is `q' ≠ q` rather than `p' ≠ p`.  -/
CochainComplex.HomComplex.Cochain.single_v_eq_zero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n p' q' : ℤ) (hpq' : p' + n = q'),
  q' ≠ q → (CochainComplex.HomComplex.Cochain.single f n).v p' q' hpq' = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, t.size ≤ (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.size
-- Mathlib.Data.Matrix.DMatrix
/-- The transpose of a dmatrix.  -/
DMatrix.transpose : {m : Type u_1} → {n : Type u_2} → {α : m → n → Type v} → DMatrix m n α → DMatrix n m fun j i => α i j
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.gc : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
  GaloisConnection (NonUnitalAlgebra.adjoin R) SetLike.coe
-- Mathlib.Order.Lattice.Nat
Set.Infinite.Nat.sSup_eq_zero : ∀ {s : Set ℕ}, s.Infinite → sSup s = 0
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_zero : Real.sin 0 = 0
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.comp_C_mul_X_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {r : R},
  r ∈ nonZeroDivisors R → (p.comp (Polynomial.C r * Polynomial.X) = 0 ↔ p = 0)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.unique : {R : Type u} → [inst : Semiring R] → [Subsingleton R] → Unique (Polynomial R)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Propagator : Type
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instSetLike : (G : Type u) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → SetLike (ClosedAddSubgroup G) G
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.List.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseP_eq_erasePTR.go : ∀ (α : Type u_1) (p : α → Bool) (l : List α) (acc : Array α) (xs : List α),
  l = acc.toList ++ xs → List.erasePTR.go✝ p l xs acc = acc.toList ++ List.eraseP p xs
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_zero : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.scaleRoots 0 = p.leadingCoeff • Polynomial.X ^ p.natDegree
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_unop : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [T2Space α] {f : β → αᵐᵒᵖ}, ∑'[L] (x : β), MulOpposite.unop (f x) = MulOpposite.unop (∑'[L] (x : β), f x)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.of_mul_right_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime x (y * z) → IsRelPrime x z
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectOutput.brecOn : ∀ {α β : Type w} [inst : Std.Iterator α Id β]
  {motive : (a : Std.Iter β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} {a : Std.Iter β} {a_1 : β}
  (t : a.IsPlausibleIndirectOutput a_1),
  (∀ (a : Std.Iter β) (a_2 : β) (t : a.IsPlausibleIndirectOutput a_2),
      Std.Iter.IsPlausibleIndirectOutput.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
LinearIsometry.integral_comp_comm : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F]
  [CompleteSpace F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedSpace ℝ F] [CompleteSpace E] [inst_9 : NormedSpace ℝ E]
  (L : E →ₗᵢ[𝕜] F) (φ : X → E), ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
-- Lean.Data.Trie
Lean.Data.Trie.brecOn_1.go : {α : Type} →
  {motive_1 : Lean.Data.Trie α → Sort u} →
    {motive_2 : Array (Lean.Data.Trie α) → Sort u} →
      {motive_3 : List (Lean.Data.Trie α) → Sort u} →
        (t : Array (Lean.Data.Trie α)) →
          ((t : Lean.Data.Trie α) → t.below → motive_1 t) →
            ((t : Array (Lean.Data.Trie α)) → Lean.Data.Trie.below_1 t → motive_2 t) →
              ((t : List (Lean.Data.Trie α)) → Lean.Data.Trie.below_2 t → motive_3 t) →
                motive_2 t ×' Lean.Data.Trie.below_1 t
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongrAlg_apply : ∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e : G ≃* H}
  (he : ∀ (a : G) (x : A), a • x = e a • x) (f : SkewMonoidAlgebra A G) (h : H),
  ((SkewMonoidAlgebra.domCongrAlg k A he) f).coeff h = f.coeff (e.symm h)
-- Mathlib.Topology.DenseEmbedding
isClosed_property2 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β} {p : β → β → Prop},
  DenseRange e → IsClosed {q | p q.1 q.2} → (∀ (a₁ a₂ : α), p (e a₁) (e a₂)) → ∀ (b₁ b₂ : β), p b₁ b₂
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_castAdd_natAdd : ∀ {m n : ℕ} {α : Sort u_1} {f : Fin (m + n) → α},
  (Fin.append (fun i => f (Fin.castAdd n i)) fun i => f (Fin.natAdd m i)) = f
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivFunctorCompSndIso_hom_app_app : ∀ {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) (X_1 : A'),
  (CategoryTheory.Sum.functorEquivFunctorCompSndIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inr X_1))
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_6 : Std.Time.Weekday.saturday.toOrdinal = 6
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- Two linear maps from the graded tensor product agree if they agree on the underlying tensor
product.  -/
GradedTensorProduct.hom_ext : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {M : Type u_5}
  [inst_9 : AddCommMonoid M] [inst_10 : Module R M] ⦃f g : GradedTensorProduct R 𝒜 ℬ →ₗ[R] M⦄,
  f ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) = g ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) → f = g
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_sentence : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N) (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
-- Lean.Meta.Tactic.Simp.Types
/-- Helper function for `simpAppUsingCongr`  -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkCongrFun' : Lean.Expr → Lean.Meta.Simp.Result → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.coe_zpow : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) (n : ℤ), ↑(x ^ n) = ↑x ^ n
-- Init.Data.Fin.Lemmas
Fin.le_antisymm_iff : ∀ {n : ℕ} {x y : Fin n}, x = y ↔ x ≤ y ∧ y ≤ x
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.MakeEditLinkProps.mk.inj : ∀ {edit : Lean.Lsp.TextDocumentEdit} {newSelection? : Option Lean.Lsp.Range} {title? : Option String}
  {edit_1 : Lean.Lsp.TextDocumentEdit} {newSelection?_1 : Option Lean.Lsp.Range} {title?_1 : Option String},
  { edit := edit, newSelection? := newSelection?, title? := title? } =
      { edit := edit_1, newSelection? := newSelection?_1, title? := title?_1 } →
    edit = edit_1 ∧ newSelection? = newSelection?_1 ∧ title? = title?_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km fallback : α}, t.maxKey? = some km → t.getKeyD km fallback = km