mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h)
      (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h))
          (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv))
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup.mk.congr_simp : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) (r r_1 : A)
  (e_r : r = r_1) (s s_1 : A) (e_s : s = s_1) (hr : f r ≠ 0) (hs : f s ≠ 0),
  MonoidWithZeroHom.valueGroup.mk f r s hr hs = MonoidWithZeroHom.valueGroup.mk f r_1 s_1 ⋯ ⋯
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
_private.Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord.0.NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral_aux : ∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)},
  NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹' NumberField.mixedEmbedding.normAtComplexPlaces '' A = A →
    NumberField.mixedEmbedding.normAtComplexPlaces '' A =
      ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹' A ∩
        Set.univ.pi fun w => if w.IsReal then Set.univ else Set.Ici 0
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The modification between strong transformations of pseudofunctors associated to a modification
between the underlying strong transformations of oplax functors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            (CategoryTheory.Pseudofunctor.StrongTrans.toOplax η).Modification
                (CategoryTheory.Pseudofunctor.StrongTrans.toOplax θ) →
              CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ
-- Mathlib.Tactic.NormNum.IsCoprime
/-- Evaluates the `IsCoprime` predicate over `ℤ`.  -/
Mathlib.Meta.NormNum.evalIntIsCoprime : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An independent set in a graph `G` that cannot be extended by adding more vertices.  -/
SimpleGraph.isMaximalIndepSet_iff : ∀ {α : Type u_3} {G : SimpleGraph α} {s : Set α},
  Maximal G.IsIndepSet s ↔ G.IsIndepSet s ∧ ∀ (t : Set α), G.IsIndepSet t → s ⊆ t → t ⊆ s
-- Mathlib.Data.Prod.Lex
Prod.Lex.noMinOrder_of_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMinOrder β], NoMinOrder (Lex (α × β))
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar? : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice s p ↔
    p = s.rawEndPos ∨
      p < s.rawEndPos ∧ (s.str.toByteArray.utf8DecodeChar? (s.startInclusive.offset.byteIdx + p.byteIdx)).isSome = true
-- Mathlib.Order.BooleanAlgebra.Basic
OrderDual.instBooleanAlgebra : {α : Type u} → [BooleanAlgebra α] → BooleanAlgebra αᵒᵈ
-- Mathlib.Order.RelClasses
InvImage.trichotomous : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Trichotomous r] {f : β → α},
  Function.Injective f → Std.Trichotomous (InvImage r f)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Alt.mk.injEq : ∀ (name : Lean.Name) (info : Lean.Meta.ElimAltInfo) (mvarId : Lean.MVarId) (name_1 : Lean.Name)
  (info_1 : Lean.Meta.ElimAltInfo) (mvarId_1 : Lean.MVarId),
  ({ name := name, info := info, mvarId := mvarId } = { name := name_1, info := info_1, mvarId := mvarId_1 }) =
    (name = name_1 ∧ info = info_1 ∧ mvarId = mvarId_1)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `y` is a conjugate root of an integral element `x` over `R`, then `y` is also integral
over `R`.
 -/
IsConjRoot.isIntegral : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsIntegral R x → IsConjRoot R x y → IsIntegral R y
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.eq_toGHSpace : ∀ {p : TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)}, ⟦p⟧ = GromovHausdorff.toGHSpace ↥p
-- Mathlib.Algebra.GroupWithZero.ProdHom
/-- The trivial group-with-zero hom is absorbing for composition.  -/
MonoidWithZeroHom.one_apply_apply_eq : ∀ {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : Nontrivial N₀] [inst_3 : NoZeroDivisors N₀] [inst_4 : MulZeroOneClass G₀]
  [inst_5 : DecidablePred fun x => x = 0] [inst_6 : DecidablePred fun x => x = 0] (f : M₀ →*₀ N₀) (x : M₀),
  1 (f x) = 1 x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The inclusion map from Schwartz functions to continuous functions vanishing at infinity as a
continuous linear map.  -/
SchwartzMap.toZeroAtInftyCLM : (𝕜 : Type u_2) →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [ProperSpace E] →
                [inst_5 : RCLike 𝕜] →
                  [inst_6 : NormedSpace 𝕜 F] →
                    [inst_7 : SMulCommClass ℝ 𝕜 F] → SchwartzMap E F →L[𝕜] ZeroAtInftyContinuousMap E F
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizer : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] [T2Space A] (s : Set A),
  (Algebra.adjoin R s).topologicalClosure ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R s)
-- Mathlib.Algebra.Algebra.Basic
Module.IsTorsionFree.to_faithfulSMul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [IsCancelMulZero R]
  [Nontrivial A] [Module.IsTorsionFree R A], FaithfulSMul R A
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_of_apply : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddCommMonoid ι] [inst_5 : PartialOrder ι]
  [CanonicallyOrderedAdd ι] [inst_7 : SetLike.GradedMonoid A] [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι]
  (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι) [inst_11 : Decidable (i ≤ n)],
  ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.writingBodyChunked.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.writingBodyChunked = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {f : α → β → γ} {k : α} {fallback : γ},
  Std.DHashMap.Const.getD (Std.DHashMap.map f m) k fallback =
    (Option.map (f k) (Std.DHashMap.Const.get? m k)).getD fallback
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.union : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y},
  e.IsImage s t → e.IsImage s' t' → e.IsImage (s ∪ s') (t ∪ t')
-- Lean.Server.AsyncList
Lean.AsyncList.ofList : {α : Type u_1} → {ε : Type u_2} → List α → Lean.AsyncList ε α
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_iff_image_closedBall_subset_compact : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  (f : M₁ →ₛₗ[σ₁₂] M₂) {r : ℝ}, 0 < r → (IsCompactOperator ⇑f ↔ ∃ K, IsCompact K ∧ ⇑f '' Metric.closedBall 0 r ⊆ K)
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalAddGroup : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [IsTopologicalAddGroup M] (S : Submodule R M), IsTopologicalAddGroup ↥S
-- Aesop.Rule
Aesop.LocalNormSimpRule.instBEq : BEq Aesop.LocalNormSimpRule
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_one : UInt8.toBitVec 1 = 1#8
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.mem_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N},
  y ∈ AddSubgroup.map f K ↔ ∃ x ∈ K, f x = y
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRevert : Lean.Elab.Tactic.Tactic
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.all.eq_def : ∀ {α : Type u_1} (p : α → Bool) (x : RBTree.RBNode α),
  RBTree.RBNode.all p x =
    match x with
    | RBTree.RBNode.nil => true
    | RBTree.RBNode.node c l v r => p v && RBTree.RBNode.all p l && RBTree.RBNode.all p r
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.comp_apply : ∀ {M N T : AddCommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDivOffset : Div Std.Time.Month.Offset
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.alter_eq_empty_iff_erase_eq_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, t.alter k f = ∅ ↔ t.erase k = ∅ ∧ f t[k]? = none
-- Mathlib.NumberTheory.Real.Irrational
irrational_ratCast_mul_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (↑q * x) ↔ q ≠ 0 ∧ Irrational x
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.shortComplexTruncLE_shortExact : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], (K.shortComplexTruncLE e).ShortExact
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_atBot_iff : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : Preorder α] [IsCodirectedOrder α] [Nonempty α],
  MeasureTheory.IntegrableAtFilter f Filter.atBot μ ↔ ∃ a, MeasureTheory.IntegrableOn f (Set.Iic a) μ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Submodule.toSubalgebra_mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Submodule R A)
  (h1 : 1 ∈ s) (hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s),
  s.toSubalgebra h1 hmul =
    { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
-- Mathlib.Order.Circular
sbtw_iff_btw_not_btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A choice of wide pushout.  -/
CategoryTheory.Limits.widePushout : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (objs : J → C) → (arrows : (j : J) → B ⟶ objs j) → [CategoryTheory.Limits.HasWidePushout B objs arrows] → C
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_neg_X : ∀ {R : Type u_1} [inst : Ring R] {f : Polynomial R}, f.Splits → (f.comp (-Polynomial.X)).Splits
-- Mathlib.Lean.Expr.Basic
/-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument.
An argument `n` may be provided which says how many arguments we are expecting `e` to have.  -/
Lean.Expr.modifyArgM : {M : Type → Type u} →
  [Monad M] → (Lean.Expr → M Lean.Expr) → (e : Lean.Expr) → ℕ → optParam ℕ e.getAppNumArgs → M Lean.Expr
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.instChartedSpaceComplex : ChartedSpace ℂ UpperHalfPlane
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommSemiring : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [CommSemiring Y] → CommSemiring (LocallyConstant X Y)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.smul_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (a : A) {S : Type u_5}
  [inst_6 : Monoid S] [inst_7 : DistribMulAction S M] [inst_8 : SMulCommClass R S M] [inst_9 : SMulCommClass S A M]
  (r : S) (D : Derivation R A M), (r • D) a = r • D a
-- Mathlib.Topology.Algebra.Support
image_eq_zero_of_notMem_tsupport : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] {f : X → α} {x : X},
  x ∉ tsupport f → f x = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k a : α} {v : β} {h₁ : a ∈ t.insert k v},
  Std.DTreeMap.Raw.Const.get (t.insert k v) a h₁ =
    if h₂ : cmp k a = Ordering.eq then v else Std.DTreeMap.Raw.Const.get t a ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {k a : α} [inst_3 : Inhabited (β a)], (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_comap_eq_self_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ {S : AddSubmonoid N}, AddSubmonoid.map f (AddSubmonoid.comap f S) = S
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `final_iff_final_comp` below.  -/
CategoryTheory.Functor.final_iff_equivalence_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence], G.Final ↔ (F.comp G).Final
-- Mathlib.Topology.ContinuousOn
Set.LeftInvOn.map_nhdsWithin_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {g : β → α}
  {x : β} {s : Set β},
  Set.LeftInvOn f g s →
    f (g x) = x →
      ContinuousWithinAt f (g '' s) (g x) →
        ContinuousWithinAt g s x → Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_equivIco_mk_apply : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)]
  [inst_3 : FloorRing 𝕜] (x : 𝕜), ↑((AddCircle.equivIco p 0) ↑x) = Int.fract (x / p) * p
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.apply_single₂ : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [inst : (i : ι) → Zero (M i)]
  [inst_1 : (i : ι) → Zero (N i)] [inst_2 : (i : ι) → Zero (O i)] [inst_3 : DecidableEq ι]
  (f' : (i : ι) → M i → N i → O i),
  (∀ (i : ι), f' i 0 0 = 0) →
    ∀ (i : ι) (x : M i) (y : N i) (j : ι), f' j (Pi.single i x j) (Pi.single i y j) = Pi.single i (f' i x y) j
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MkMor₁.mk : {m : Type → Type} → (Lean.Expr → m Mathlib.Tactic.BicategoryLike.Mor₁) → Mathlib.Tactic.BicategoryLike.MkMor₁ m
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection_subtype : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] (s' : AffineSubspace 𝕜 ↥s) [inst_6 : Nonempty ↥s']
  [inst_7 : s'.direction.HasOrthogonalProjection]
  [inst_8 : (AffineSubspace.map s.subtype s').direction.HasOrthogonalProjection] (p : ↥s),
  ↑((EuclideanGeometry.reflection s') p) = (EuclideanGeometry.reflection (AffineSubspace.map s.subtype s')) ↑p
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- If the topology is discrete, any sheaf is terminal.  -/
CategoryTheory.Sheaf.isTerminalOfEqTop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          J = ⊤ → (F : CategoryTheory.Sheaf J A) → CategoryTheory.Limits.IsTerminal F
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.mk.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (toEquiv toEquiv_1 : M ≃ N) (e_toEquiv : toEquiv = toEquiv_1)
  (map_fun' :
    ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
      toEquiv.toFun (FirstOrder.Language.Structure.funMap f x) =
        FirstOrder.Language.Structure.funMap f (toEquiv.toFun ∘ x))
  (map_rel' :
    ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
      FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x),
  { toEquiv := toEquiv, map_fun' := map_fun', map_rel' := map_rel' } =
    { toEquiv := toEquiv_1, map_fun' := ⋯, map_rel' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.C.eq_1 : ∀ (n : ℕ),
  CartanMatrix.C n =
    Matrix.of fun i j =>
      if i = j then 2 else if ↑i + 1 = ↑j then -1 else if ↑j + 1 = ↑i then if ↑i = n - 1 then -2 else -1 else 0
-- Mathlib.Analysis.Calculus.Deriv.ZPow
derivWithin_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {m : ℤ},
  UniqueDiffWithinAt 𝕜 s x → x ≠ 0 ∨ 0 ≤ m → derivWithin (fun x => x ^ m) s x = ↑m * x ^ (m - 1)
-- Mathlib.Topology.Closure
interior_empty : ∀ {X : Type u} [inst : TopologicalSpace X], interior ∅ = ∅
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_right_inj : ∀ {α : Type u_1} {a b : α} {n : ℕ}, n ≠ 0 → (Multiset.replicate n a = Multiset.replicate n b ↔ a = b)
-- Mathlib.Data.NNReal.Basic
NNReal.mul_iSup_le : ∀ {ι : Sort u_3} {a g : NNReal} {h : ι → NNReal}, (∀ (j : ι), g * h j ≤ a) → g * iSup h ≤ a
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_lt_aleph0_iff : ∀ {α : Type u} [inst : LinearOrder α], Order.cof α < Cardinal.aleph0 ↔ Order.cof α ≤ 1
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems.mk.injEq : ∀ (lemmas lemmas_1 : Lean.SMap Lean.Name (List Lean.Meta.SimpCongrTheorem)),
  ({ lemmas := lemmas } = { lemmas := lemmas_1 }) = (lemmas = lemmas_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- Conjugation induces an equivariant map between the `SubMulAction` of
the fixing subgroup of a subset and that of a translate.  -/
SubMulAction.conjMap_ofFixingSubgroup : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        {s t : Set α} →
          {g : M} →
            (hg : g • t = s) →
              ↥(SubMulAction.ofFixingSubgroup M t) →ₑ[⇑(SubMulAction.fixingSubgroupEquivFixingSubgroup hg)]
                ↥(SubMulAction.ofFixingSubgroup M s)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_nonneg : ∀ {p t x : ℝ}, 0 < p → 0 ≤ t → 0 ≤ x → 0 ≤ p.rpowIntegrand₀₁ t x
-- Mathlib.Data.Finset.Basic
Finset.erase_union_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Finset α} {a : α}, a ∈ t → ∀ (s : Finset α), s.erase a ∪ t = s ∪ t
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.map.instIsAddMonHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X Y : C) [inst_5 : CategoryTheory.AddMonObj X]
  [inst_6 : CategoryTheory.AddMonObj Y] (f : X ⟶ Y) [CategoryTheory.IsAddMonHom f], CategoryTheory.IsAddMonHom (F.map f)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ico_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ico a b)), Subtype.val '' Set.Iio c = Set.Ico a ↑c
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.tendsto_atBot_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν →
    ∀ (a : α), ∀ᵐ (b : β) ∂ν a, Filter.Tendsto (f (a, b)) Filter.atBot (nhds 0)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.leadCoeff : Lean.Grind.Linarith.Poly → ℤ
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.eq_liftPath_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {γ : C(↑unitInterval, X)} {e : E} (γ_0 : γ 0 = p e) {Γ : ↑unitInterval → E},
  Γ = ⇑(cov.liftPath γ e γ_0) ↔ Continuous Γ ∧ p ∘ Γ = ⇑γ ∧ Γ 0 = e
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.merge : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t₁.Equiv t₂ → t₃.Equiv t₄ → (t₁.merge t₃).Equiv (t₂.merge t₄)
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the forward direction of `dirSupClosedOn_compl`. -/
DirSupInaccOn.of_compl : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupClosedOn D sᶜ → DirSupInaccOn D s
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roo_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n - (m + 1)).toNat ≤ i → (m<...n).toArray[i]! = 0
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.le_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P ≤ P.isoClosure
-- Mathlib.Topology.Order
TopologicalSpace.nontrivial_iff_exists_not_inseparable : ∀ {α : Type u} {t : TopologicalSpace α}, NontrivialTopology α ↔ ∃ x y, ¬Inseparable x y
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_one_add : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (i : ℤ), A ^ (1 + i) = A * A ^ i
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The open sets of an open subscheme corresponds to the open sets containing in the image.  -/
AlgebraicGeometry.IsOpenImmersion.opensEquiv : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] → X.Opens ≃ { U // U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }
-- Lean.Expr
Lean.instInhabitedExprStructEq : Inhabited Lean.ExprStructEq
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- The additive group homomorphism `FreeAbelianGroup α →+ FreeAbelianGroup β` induced from a
map `α → β`.  -/
FreeAbelianGroup.map : {α : Type u} → {β : Type v} → (α → β) → FreeAbelianGroup α →+ FreeAbelianGroup β
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_pow : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x : R) (n : ℕ), v (x ^ n) = v x ^ n