mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α →CO β},
  f = g ↔ ∀ (a : α), f a = g a
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_mod : ∀ {a b : ℕ} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64), UInt64.ofNatLT (a % b) ⋯ = UInt64.ofNatLT a ha % UInt64.ofNatLT b hb
-- Mathlib.FieldTheory.NormalizedTrace
/-- The normalized trace map from an algebraic extension `K` to the base field `F`.  -/
Algebra.normalizedTrace : (F : Type u_1) →
  (K : Type u_2) →
    [inst : Field F] → [inst_1 : Field K] → [inst_2 : Algebra F K] → [CharZero F] → [Algebra.IsIntegral F K] → K →ₗ[F] F
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F L],
      Cardinal.lift.{v, w} (Module.rank F L) * Cardinal.lift.{w, v} (Module.rank (↥(IntermediateField.adjoin L ↑A)) E) =
        Cardinal.lift.{w, v} (Module.rank (↥A) E)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- A base angle of an isosceles triangle with apex at the center of a circle is acute.  -/
EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two : ∀ {V : Type u_3} {P : Type u_4} [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)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → |(EuclideanGeometry.oangle p₂ p₁ s.center).toReal| < Real.pi / 2
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given closed range as an array in ascending order.
 -/
Std.Ric.toArray : {α : Type u} →
  [Std.PRange.Least? α] →
    [inst : LE α] →
      [DecidableLE α] →
        [inst_2 : Std.PRange.UpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxc.IsAlwaysFinite α] → Std.Ric α → Array α
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.isRadical : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.IsPrime → I.IsRadical
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_prod : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (s : Finset ι) (x y : R) (p : ι → Polynomial (Polynomial R)),
  Polynomial.evalEval x y (∏ j ∈ s, p j) = ∏ j ∈ s, Polynomial.evalEval x y (p j)
-- Mathlib.Data.List.Rotate
List.IsRotated.forall : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate n ~r l
-- Lean.Message
Lean.stringToMessageData : String → Lean.MessageData
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.keyAtIdx!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {i : ℕ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keyAtIdx! i = t₂.keyAtIdx! i
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfRightInverse_comp_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g // RingHom.ker f ≤ RingHom.ker g }) (x : A),
  ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.deriv_inv_log_apply : ∀ {x : ℝ}, deriv (fun x => (Real.log x)⁻¹) x = -x⁻¹ / Real.log x ^ 2
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE Int32
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
/-- The inclusion of the Moore complex in the alternating face map complex
is a homotopy equivalence  -/
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex : {A : Type u_2} →
  [inst : CategoryTheory.Category.{v_2, u_2} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      {Y : CategoryTheory.SimplicialObject A} →
        HomotopyEquiv ((AlgebraicTopology.normalizedMooreComplex A).obj Y)
          ((AlgebraicTopology.alternatingFaceMapComplex A).obj Y)
-- Init.Data.UInt.Bitwise
USize.xor_comm : ∀ (a b : USize), a ^^^ b = b ^^^ a
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_sub_ne : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] {x y : HahnSeries Γ R} {g : Γ},
  x.orderTop = ↑g → y.orderTop = ↑g → x.leadingCoeff = y.leadingCoeff → (x - y).orderTop ≠ ↑g
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd : ∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X)
  (x : ↑(F.obj.obj (Opposite.op (U ⊔ V)))),
  (↑((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).hom) x)).2 =
    (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) x
-- Mathlib.Logic.Equiv.Basic
/-- Given `φ : α → β → Sort*`, we have an equivalence between `∀ a b, φ a b` and `∀ b a, φ a b`.
This is `Function.swap` as an `Equiv`.  -/
Equiv.piComm : {α : Sort u_1} → {β : Sort u_4} → (φ : α → β → Sort u_9) → ((a : α) → (b : β) → φ a b) ≃ ((b : β) → (a : α) → φ a b)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stk_nth_val : ∀ {K : Type u_1} {Γ : K → Type u_2} {L : Turing.ListBlank ((k : K) → Option (Γ k))} {k : K} {S : List (Γ k)} (n : ℕ),
  Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse → L.nth n k = S.reverse[n]?
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- We say that `μ` is absolutely continuous with respect to `ν`, or that `μ` is dominated by `ν`,
if `ν(A) = 0` implies that `μ(A) = 0`.  -/
MeasureTheory.Measure.AbsolutelyContinuous : {α : Type u_1} → {_m0 : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Prop
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the day of the month to the given `days` value, with any
out-of-range days clipped to the nearest valid date.
 -/
Std.Time.PlainDateTime.withDaysClip : Std.Time.PlainDateTime → Std.Time.Day.Ordinal → Std.Time.PlainDateTime
-- Lean.Elab.DefView
Lean.Elab.instInhabitedDefKind.default : Lean.Elab.DefKind
-- Mathlib.Combinatorics.SimpleGraph.Cayley
/-- See `mulCayley_adj` for the more convenient form in a `Group`.  -/
SimpleGraph.mulCayley_adj' : ∀ {M : Type u_1} (s : Set M) [inst : Mul M] (u v : M),
  (SimpleGraph.mulCayley s).Adj u v ↔ u ≠ v ∧ ∃ g ∈ s, u * g = v ∨ u = v * g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.get?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.get? k = t₂.get? k
-- Mathlib.Order.TypeTags
WithTop.recTopCoe.eq_1 : ∀ {α : Type u_1} {C : WithTop α → Sort u_2} (bot : C ⊤) (coe : (a : α) → C ↑a), WithTop.recTopCoe bot coe none = bot
-- Mathlib.Analysis.Normed.Module.Basic
/-- A normed space over a normed field is a vector space endowed with a norm which satisfies the
equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove
`‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`.

Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this
typeclass can be used for "seminormed spaces" too, just as `Module` can be used for
"semimodules".  -/
NormedSpace.norm_smul_le : ∀ {𝕜 : Type u_6} {E : Type u_7} {inst : NormedField 𝕜} {inst_1 : SeminormedAddCommGroup E} [self : NormedSpace 𝕜 E]
  (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.incremental.sizeOf_spec : sizeOf Lean.Lsp.TextDocumentSyncKind.incremental = 1
-- Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
/-- Construct a simplicial complex from a `PreAbstractSimplicialComplex` on a set of points in a space,
under the assumption that the union of the defining points is affinely independent.
 -/
Geometry.SimplicialComplex.ofAffineIndependent : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [DecidableEq E] →
            [inst_4 : AddCommGroup E] →
              [inst_5 : Module 𝕜 E] →
                (abstract : PreAbstractSimplicialComplex E) →
                  AffineIndependent 𝕜 Subtype.val → Geometry.SimplicialComplex 𝕜 E
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.instModule : {R : Type u_2} →
  {α : Type u_3} →
    [inst : UniformSpace α] →
      [inst_1 : AddCommGroup α] →
        [inst_2 : IsUniformAddGroup α] →
          [inst_3 : Semiring R] →
            [inst_4 : Module R α] → [UniformContinuousConstSMul R α] → Module R (UniformSpace.Completion α)
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf K A) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).obj X).obj.map f = X.obj.map (e.functor.map f.unop).op
-- Mathlib.Order.OrderDual
OrderDual.instDecidableLT : (α : Type u_2) → [inst : LT α] → [h : DecidableLT α] → DecidableLT αᵒᵈ
-- Mathlib.Order.Interval.Finset.Basic
/-- A function from a locally finite preorder is strictly antitone if and only if it is strictly
antitone when restricted to pairs satisfying `a ⋖ b`.  -/
strictAnti_iff_forall_covBy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [LocallyFiniteOrder α] [inst_2 : Preorder β] (f : α → β),
  StrictAnti f ↔ ∀ (a b : α), a ⋖ b → f b < f a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.reify.mk : ∀ {v : Sat.Valuation} {l : Sat.Literal} {p : Prop}, (v.neg l → p) → Sat.Literal.reify v l p
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CommaMorphism.mk'.congr_simp : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma R L} (right right_1 : Y.right ⟶ X.right)
  (e_right : right = right_1) (left left_1 : Y.left ⟶ X.left) (e_left : left = left_1)
  (w : CategoryTheory.CategoryStruct.comp Y.hom (L.map right) = CategoryTheory.CategoryStruct.comp (R.map left) X.hom),
  CategoryTheory.CommaMorphism.mk' right left w = CategoryTheory.CommaMorphism.mk' right_1 left_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.mul_self_mul_conjTranspose_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {p : Type u_5}
  (A : Matrix m n R) (B : Matrix p m R), B * (A * A.conjTranspose) = 0 ↔ B * A = 0
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts.0.CategoryTheory.Limits.Fan.combPairHoms.match_1.eq_2 : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} (motive : ι₁ ⊕ ι₂ → Sort u_3) (a : ι₂) (h_1 : (a : ι₁) → motive (Sum.inl a))
  (h_2 : (a : ι₂) → motive (Sum.inr a)),
  (match Sum.inr a with
    | Sum.inl a => h_1 a
    | Sum.inr a => h_2 a) =
    h_2 a
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_vsub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β}, (f -ᵥ g).NeBot → f.NeBot
-- Mathlib.GroupTheory.ResiduallyFinite
Group.instResiduallyFiniteProd : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] [Group.ResiduallyFinite G]
  [Group.ResiduallyFinite G'], Group.ResiduallyFinite (G × G')
-- Mathlib.Data.Set.Semiring
instOrderBotSetSemiring : (α : Type u_1) → OrderBot (SetSemiring α)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.closedBallSubgroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (c : MulArchimedeanClass M),
  c.closedBallSubgroup = MulArchimedeanClass.subgroup (UpperSet.Ici c)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.counitIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instMulZeroClass : {α : Type u_1} → [MulZeroClass α] → MulZeroClass (Lex α)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.union m₂).get? k = m₂.get? k
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyEq.isLocalExtrOn_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  f =ᶠ[nhdsWithin a s] g → a ∈ s → (IsLocalExtrOn f s a ↔ IsLocalExtrOn g s a)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v l
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
              motive x
-- Mathlib.Order.SetNotation
Set.mem_sUnion : ∀ {α : Type u} {x : α} {S : Set (Set α)}, x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t
-- Mathlib.Data.List.Sigma
List.kextract.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : Sigma β) (l : List (Sigma β)),
  List.kextract a (s :: l) =
    if h : s.fst = a then (some (Eq.recOn h s.snd), l)
    else
      match List.kextract a l with
      | (b', l') => (b', s :: l')
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffOn_of_subsingleton : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {n : WithTop ℕ∞} [Subsingleton M'], ContMDiffOn I I' n f s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} {K : Type u}
  [inst_3 : Field K] [inst_4 : Algebra F K] (h : IsIntegral F α) (x : { x // x ∈ (minpoly F α).aroots K }),
  ((IntermediateField.algHomAdjoinIntegralEquiv F h).symm x) (IntermediateField.AdjoinSimple.gen F α) = ↑x
-- Mathlib.Algebra.Group.Prod
MulHom.fst_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), (MulHom.fst N P).comp (f.prod g) = f
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.insertEntry k v l).length =
    if Std.Internal.List.containsKey k l = true then l.length else l.length + 1
-- Mathlib.Algebra.Group.Hom.Defs
/-- `1` is the multiplicative homomorphism sending all elements to `1`.  -/
instOneMulHom : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : MulOneClass N] → One (M →ₙ* N)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.postcompLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} {F' : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace ℝ F']
  [inst_9 : NormedSpace 𝕜 F'] [inst_10 : SMulCommClass ℝ 𝕜 F'] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  [inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜] (T : F →L[𝕜] F') (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.postcompLM T) f) = ⇑T ∘ ⇑f
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumRight_symm_lof_tmul : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'] (x : M₁') (i : ι₂) (y : M₂ i),
  (TensorProduct.directSumRight R S M₁' M₂).symm
      ((DirectSum.lof S ι₂ (fun i => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) =
    x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y
-- Mathlib.Tactic.Linter.TextBased
/-- The existing exception also covers the new error:
we keep the existing exception.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ComparisonResult.Comparable : Mathlib.Linter.TextBased.ComparisonResult✝
-- Mathlib.GroupTheory.QuotientGroup.Defs
_private.Mathlib.GroupTheory.QuotientGroup.Defs.0.QuotientGroup.termQ : Lean.ParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.prop_iSup_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C)
  (X : C), (⨆ a, P a) X ↔ ∃ a, P a X
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Right unitality of the enriched structure  -/
CategoryTheory.MonoidalClosed.comp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (x ⟹ y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (x ⟹ y) (CategoryTheory.MonoidalClosed.id y))
        (CategoryTheory.MonoidalClosed.comp x y y)) =
    CategoryTheory.CategoryStruct.id (x ⟹ y)
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- An element `a` of a semigroup with a distributive negation divides the negation of an element
`b` iff `a` divides `b`.  -/
dvd_neg : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ -b ↔ a ∣ b
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁ comm h₁₂ h₂₃ h₁₃ h).hom₃ = u₂₃
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `G` is a finite Galois group for `B/A`, then `G` is isomorphic to `Gal(B/A)`.  -/
IsGaloisGroup.mulEquivAlgEquiv : (G : Type u_1) →
  [inst : Group G] →
    (A : Type u_2) →
      (B : Type u_3) →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [IsDomain B] →
              [inst_4 : Algebra A B] →
                [FaithfulSMul A B] →
                  [inst_6 : MulSemiringAction G B] → [IsGaloisGroup G A B] → [Finite G] → G ≃* B ≃ₐ[A] B
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_le_sum : ∀ {ι : Type u} (f : ι → Cardinal.{v}) (i : ι), Cardinal.lift.{u, v} (f i) ≤ Cardinal.sum f
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionValue.mk.injEq : ∀ (value : String)
  (isValidExtensionValue :
    autoParam (Std.Http.Chunk.IsValidExtensionValue value)
      Std.Http.Chunk.ExtensionValue.isValidExtensionValue._autoParam)
  (value_1 : String)
  (isValidExtensionValue_1 :
    autoParam (Std.Http.Chunk.IsValidExtensionValue value_1)
      Std.Http.Chunk.ExtensionValue.isValidExtensionValue._autoParam),
  ({ value := value, isValidExtensionValue := isValidExtensionValue } =
      { value := value_1, isValidExtensionValue := isValidExtensionValue_1 }) =
    (value = value_1)
-- Init.Data.Order.MinMaxOn
minOn_eq_or : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x y : α},
  minOn f x y = x ∨ minOn f x y = y
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {F' G' : HomologicalComplex C c} (φ' : F' ⟶ G')
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] (H : ∀ (j : ι), ∃ i, c.Rel i j)
  (α : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'),
  (HomologicalComplex.homotopyCofiber.mapArrowIso φ φ' H α).inv =
    HomologicalComplex.homotopyCofiber.mapArrowHom φ' φ H α.inv
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.alter_eq_empty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, t.alter k f = ∅ ↔ (t = ∅ ∨ t.size = 1 ∧ k ∈ t) ∧ f t[k]? = none
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.limitsOfShape J ≤ P → P.IsClosedUnderLimitsOfShape J