mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightHom_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (e : P.Equiv P),
  (RootPairing.Equiv.weightHom P) e = RootPairing.Equiv.weightEquiv P P e
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃),
  (g ∘ₛₗ f).ker = Submodule.comap f g.ker
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_smul_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (p : Polynomial R),
  matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (I J : CategoryTheory.InjectiveResolution X), CategoryTheory.CategoryStruct.comp I.ι (I.homotopyEquiv J).hom = J.ι
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.logOf_one_add_X : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Algebra ℚ A], (1 + PowerSeries.X).logOf = PowerSeries.log A
-- Mathlib.FieldTheory.Isaacs
/-- **Alias** of `IsAlgClosure.of_exists_root`. -/
IsAlgClosure.of_exist_roots : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [alg : Algebra.IsAlgebraic F E],
  (∀ (p : Polynomial F), p.Monic → Irreducible p → ∃ x, (Polynomial.aeval x) p = 0) → IsAlgClosure F E
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isInt_pow : ∀ {α : Type u_1} [inst : Ring α] {f : α → ℕ → α} {a : α} {b : ℕ} {a' : ℤ} {b' : ℕ} {c : ℤ},
  f = HPow.hPow →
    Mathlib.Meta.NormNum.IsInt a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.pow b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
NNReal.concaveOn_rpow : ∀ {p : ℝ}, 0 ≤ p → p ≤ 1 → ConcaveOn NNReal Set.univ fun x => x ^ p
-- Mathlib.Order.SetIsMax
Set.not_isMax_coe : ∀ {J : Type u} [inst : Preorder J] {S : Set J} (m : ↑S), ¬IsMax m → ¬IsMax ↑m
-- Mathlib.Data.Set.Basic
Set.mem_of_mem_inter_right : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∩ b → x ∈ b
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSemigroupOfMulOpposite : {M : Type u_1} → [Semigroup Mᵐᵒᵖ] → Semigroup Mᵈᵐᵃ
-- Mathlib.Analysis.Convolution
/-- The convolution `f * g` is continuous if `f` is locally integrable and `g` is continuous and
compactly supported. Version where `g` depends on an additional parameter in a subset `s` of
a parameter space `P` (and the compact support `k` is independent of the parameter in `s`).  -/
MeasureTheory.continuousOn_convolution_right_with_param : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F)
  [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G]
  [inst_10 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [inst_13 : TopologicalSpace P]
  {g : P → G → E'} {s : Set P} {k : Set G},
  IsCompact k →
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      MeasureTheory.LocallyIntegrable f μ →
        ContinuousOn (↿g) (s ×ˢ Set.univ) →
          ContinuousOn (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.toList : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → List α
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.bilinearComp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X Y Z : C) (a b c : ℕ) (h : a + b = c),
  CategoryTheory.Abelian.Ext.bilinearComp X Y Z a b c h = CategoryTheory.Abelian.Ext.bilinearComp X Y Z a b c h
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.State.mk.inj : ∀ {vars : Lean.PArray Lean.Expr} {varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var}
  {vars' : Lean.PArray Lean.Expr} {varMap' : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var}
  {natToIntMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)}
  {natDef : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var}
  {dvds : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)}
  {lowers uppers : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr)}
  {diseqs : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)}
  {elimEqs : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} {elimStack : List Int.Internal.Linear.Var}
  {occurs : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet} {assignment : Lean.PArray ℚ} {nextCnstrId : ℕ}
  {caseSplits : Bool} {steps : ℕ} {conflict? : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof}
  {diseqSplits : Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId} {divMod : Lean.PHashSet (Lean.Expr × ℤ)}
  {toIntIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {toIntInfos : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo}
  {toIntTermMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo}
  {toIntVarMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {usedCommRing : Bool}
  {nonlinearOccs : Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var)}
  {vars_1 : Lean.PArray Lean.Expr} {varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var}
  {vars'_1 : Lean.PArray Lean.Expr} {varMap'_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var}
  {natToIntMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)}
  {natDef_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var}
  {dvds_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)}
  {lowers_1 uppers_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr)}
  {diseqs_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)}
  {elimEqs_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} {elimStack_1 : List Int.Internal.Linear.Var}
  {occurs_1 : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet} {assignment_1 : Lean.PArray ℚ} {nextCnstrId_1 : ℕ}
  {caseSplits_1 : Bool} {steps_1 : ℕ} {conflict?_1 : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof}
  {diseqSplits_1 : Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId} {divMod_1 : Lean.PHashSet (Lean.Expr × ℤ)}
  {toIntIds_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {toIntInfos_1 : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo}
  {toIntTermMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo}
  {toIntVarMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {usedCommRing_1 : Bool}
  {nonlinearOccs_1 : Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var)}, ⋯ → ⋯
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when
`H` is a subgroup of the normalizer of `N` in `G`.  -/
Subgroup.coe_mul_of_right_le_normalizer_left : ∀ {G : Type u_2} [inst : Group G] (N H : Subgroup G), H ≤ Subgroup.normalizer ↑N → ↑(N ⊔ H) = ↑N * ↑H
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_singleton_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (s : Finset β) (f : β → α),
  (s.sup fun b => {f b}) = Finset.image f s
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNat : ∀ {n : ℕ}, n < 4294967296 → (OfNat.ofNat n).toUInt64 = OfNat.ofNat n
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copyIndep_Indep : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E)
  (h : ∀ (I : Set α), Indep I ↔ M.Indep I) (a : Set α), (M.copyIndep E Indep hE h).Indep a = Indep a
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instLinearMapClass : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂], LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Construct a strong natural transformation from an oplax natural transformation whose
naturality 2-morphism is an isomorphism.  -/
CategoryTheory.Oplax.StrongTrans.mkOfOplax' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (η : CategoryTheory.Oplax.OplaxTrans F G) →
            [∀ (a b : B) (f : a ⟶ b), CategoryTheory.IsIso (η.naturality f)] → CategoryTheory.Oplax.StrongTrans F G
-- Mathlib.Probability.Kernel.CompProdEqIff
ProbabilityTheory.Kernel.ae_eq_of_compProd_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β]
  [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  μ.compProd κ = μ.compProd η → ⇑κ =ᵐ[μ] ⇑η
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.copy_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {K' H' : C} (eK : K' ≅ h.K) (eH : H' ≅ h.H),
  (h.copy eK eH).π = CategoryTheory.CategoryStruct.comp eK.hom (CategoryTheory.CategoryStruct.comp h.π eH.inv)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).hom f =
    (CategoryTheory.Subobject.mk f).arrow
-- Mathlib.Data.Multiset.Fintype
Multiset.cast.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} (h : s = t), Multiset.cast h = Multiset.cast h
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forget
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.eq_top_iff' : ∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), S = ⊤ ↔ ∀ (x : M), x ∈ S
-- Mathlib.Topology.Connected.TotallyDisconnected
TotallySeparatedSpace.totallyDisconnectedSpace : ∀ (α : Type u) [inst : TopologicalSpace α] [TotallySeparatedSpace α], TotallyDisconnectedSpace α
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.Topology.Order.LeftRightLim
Antitone.tendsto_leftLim_within : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhdsWithin (Function.leftLim f x) (Set.Ici (Function.leftLim f x)))
-- Std.Tactic.Do.Syntax
/-- `mrename_i` is like `rename_i`, but names inaccessible stateful hypotheses in a `Std.Do.SPred` goal.
 -/
Lean.Parser.Tactic.mrenameI : Lean.ParserDescr
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Linear_CC'.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.Linear_CC' C hsC ho =
    Profinite.NobelingProof.Linear_CC'₁ C hsC ho - Profinite.NobelingProof.Linear_CC'₀ C ho
-- Lean.Data.NameTrie
Lean.NamePart.num.injEq : ∀ (n n_1 : ℕ), (Lean.NamePart.num n = Lean.NamePart.num n_1) = (n = n_1)
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.prodMap : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} {δ : Type u_2} [inst : UniformSpace β]
  [inst_1 : Preorder γ] [inst_2 : Preorder δ] {u : γ → α} {v : δ → β},
  CauchySeq u → CauchySeq v → CauchySeq (Prod.map u v)
-- Mathlib.Data.Vector.Basic
List.Vector.comp_traverse : ∀ {n : ℕ} {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G] {α β γ : Type u}
  (f : β → F γ) (g : α → G β) (x : List.Vector α n),
  List.Vector.traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x =
    Functor.Comp.mk (List.Vector.traverse f <$> List.Vector.traverse g x)
-- Mathlib.Order.WithBot
WithBot.unbot_le_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α} (hx : x ≠ ⊥), x.unbot hx ≤ a ↔ x ≤ ↑a
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages do not change when replacing the radius by its absolute value.  -/
Real.circleAverage_abs_radius : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  Real.circleAverage f c |R| = Real.circleAverage f c R
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
AbsoluteValue.IsEuclidean.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {abv : AbsoluteValue R S}, (∀ {x y : R}, abv x < abv y ↔ EuclideanDomain.r x y) → abv.IsEuclidean
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_constants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {c : L.Constants} {v : α → M},
  FirstOrder.Language.Term.realize v c.term = ↑c
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.self_le_rpow_of_le_one : ∀ {x y : ℝ}, 0 ≤ x → x ≤ 1 → y ≤ 1 → x ≤ x ^ y
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_symm_apply_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (f : X ⟶ Y) (x : P.obj (Opposite.op X)), (CategoryTheory.Presieve.FamilyOfElements.singletonEquiv P f).symm x f ⋯ = x
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.edge_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.Inc e x → e ∈ G.edgeSet
-- Mathlib.Algebra.Group.Defs
AddZeroClass.ext : ∀ {M : Type u} ⦃m₁ m₂ : AddZeroClass M⦄, Add.add = Add.add → m₁ = m₂
-- Lean.Data.PrefixTree
_private.Lean.Data.PrefixTree.0.Lean.PrefixTreeNode.foldMatchingM.find : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} →
      {σ : Type u_1} →
        [Monad m] → (cmp : α → α → Ordering) → σ → (β → σ → m σ) → List α → Lean.PrefixTreeNode α β cmp → σ → m σ
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction₀.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ),
  ZMod.completedLFunction₀ Φ s =
    ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.completedHurwitzZetaEven₀ (ZMod.toAddCircle j) s +
      ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.completedHurwitzZetaOdd (ZMod.toAddCircle j) s
-- Mathlib.Logic.Basic
not_xor : ∀ (P Q : Prop), ¬Xor P Q ↔ (P ↔ Q)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineEquiv.coe_ofEq_apply : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [inst_4 : Nonempty ↥S₁] [inst_5 : Nonempty ↥S₂] (h : S₁ = S₂)
  (x : ↥S₁), ↑((AffineEquiv.ofEq S₁ S₂ h) x) = ↑x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] [inst_2 : Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).get!
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_eq_zero_iff_of_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] {s : Finset ι} {f : ι → α},
  (∀ i ∈ s, 0 ≤ f i) → ((s.expect fun i => f i) = 0 ↔ ∀ i ∈ s, f i = 0)
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.eq_zero_iff_forall_finiteIndexNormalSubroup : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.ResiduallyFinite G] (g : G),
  (∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) → g = 0
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.zero_eventuallyLE_add_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M}, 0 ≤ᶠ[l] f → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Scalar multiplication by `ℝ`, valid without restrictions on the determinant.  -/
SlashInvariantForm.instSMulℝ : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {α : Type u_2} → [inst : SMul α ℂ] → [inst_1 : SMul α ℝ] → [IsScalarTower α ℝ ℂ] → SMul α (SlashInvariantForm Γ k)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCoreAux_maximal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, t ⊆ s → Balanced 𝕜 t → t ⊆ balancedCoreAux 𝕜 s
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_map : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (s : Subring R),
  ↑(Subring.map f s) = ⇑f '' ↑s
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α (β × γ)} [h : ProbabilityTheory.IsFiniteKernel κ.fst],
  ProbabilityTheory.IsFiniteKernel κ
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Addition in the colimit is well-defined in the right argument.  -/
AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {x y y' : (j : J) × ↑(F.obj j)},
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) y y' →
    AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x y'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minKey?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKey? = t₂.minKey?
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mulOneClass.eq_1 : ∀ {α : Type u_2} [inst : MulOneClass α],
  Set.mulOneClass = { toOne := Set.one, toMul := Set.mul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative equal to the
Fréchet derivative of `l` applied to the derivative of `f`.  -/
HasFDerivAt.comp_hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E},
  HasFDerivAt l l' (f x) → HasDerivAt f f' x → HasDerivAt (l ∘ f) (l' f') x
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.trans_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasPushout P.i₁ P'.i₀],
  (P.trans P').i₀ = CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.Limits.pushout.inl P.i₁ P'.i₀)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.sum_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β] {ι : Type u_5} (s : Finset ι) (f : ι → CompactlySupportedContinuousMap α β) (a : α),
  (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.ae_eq_compProd_of_ae_eq_fst : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {γ : Type u_3} {mγ : MeasurableSpace γ} [MeasurableEq γ] (κ : ProbabilityTheory.Kernel α β) {f g : α → γ},
  Measurable f → Measurable g → f =ᵐ[μ] g → (fun p => f p.1) =ᵐ[μ.compProd κ] fun p => g p.1
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_homMap : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7}
  [inst : CategoryTheory.Category.{v_2, u_2} C₁] [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂]
  [inst_2 : CategoryTheory.Category.{v_4, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} D₂] [inst_5 : CategoryTheory.Category.{v_7, u_7} D₃]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₃ : CategoryTheory.MorphismProperty C₃} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₃) (L₁ : CategoryTheory.Functor C₁ D₁) [inst_6 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_7 : L₂.IsLocalization W₂] (L₃ : CategoryTheory.Functor C₃ D₃)
  [inst_8 : L₃.IsLocalization W₃] {X Y : C₁} (f : L₁.obj X ⟶ L₁.obj Y),
  Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f
-- Init.PropLemmas
Bool.ite_else_false : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then x else false) = true ↔ p ∧ x = true
-- Mathlib.RingTheory.Ideal.NatInt
ringKrullDim_nat : ringKrullDim ℕ = 2
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_eq_none_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  Std.Internal.List.minEntry? l = none ↔ l.isEmpty = true
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm_comp_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) (f : α → α) (g : α → β), ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.instCompleteLattice : {α : Type u_1} → CompleteLattice (MeasurableSpace α)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensFunctor.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.opensFunctor f = AlgebraicGeometry.Scheme.Hom.opensFunctor f_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_log_of_zpow_le : ∀ {x y : ℝ} {n : ℤ}, 0 < x → x ^ n ≤ y → ↑n * Real.log x ≤ Real.log y
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.beq_of_beq_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, (#[a] == #[b]) = true → (a == b) = true
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split.eq_2 : ∀ (e : ONote) (n : ℕ+) (a : ONote),
  (e.oadd n a).split =
    if e = 0 then (0, ↑n)
    else
      match a.split with
      | (a', m) => (e.oadd n a', m)