mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Calculus
fderiv_inner_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {x : G},
  DifferentiableAt ℝ f x →
    DifferentiableAt ℝ g x →
      ∀ (y : G),
        (fderiv ℝ (fun t => inner 𝕜 (f t) (g t)) x) y =
          inner 𝕜 (f x) ((fderiv ℝ g x) y) + inner 𝕜 ((fderiv ℝ f x) y) (g x)
-- Init.Data.List.Lemmas
List.self_eq_append_right : ∀ {α : Type u_1} {xs ys : List α}, xs = xs ++ ys ↔ ys = []
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.pointReflection_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x y : P₁), (AffineEquiv.pointReflection k x) y = (x -ᵥ y) +ᵥ x
-- Lean.Elab.Tactic.RCases
/-- This function is used for producing rcases patterns based on a case tree. This is like
`alts₁Core`, but it produces a cases pattern directly instead of a list of alternatives. We
specially translate the empty alternation to `⟨⟩`, and translate `|(a | b)` to `⟨a | b⟩` (because we
don't have any syntax for unary alternation). Otherwise we can use the regular merging of
alternations at the last argument so that `a | b | (c | d)` becomes `a | b | c | d`.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.alts₁ : Lean.Syntax → List (List Lean.Elab.Tactic.RCases.RCasesPatt) → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.eq_1 : ∀ (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ)
  [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid P] [inst_15 : Module A P]
  [inst_16 : AddCommMonoid Q] [inst_17 : Module R Q] [inst_18 : Module R P] [inst_19 : IsScalarTower R A P]
  [inst_20 : Algebra A B] [inst_21 : IsScalarTower A B M] [inst_22 : CommSemiring S] [inst_23 : Algebra R S]
  [inst_24 : Algebra S B] [inst_25 : Module S M] [inst_26 : Module S N] [inst_27 : IsScalarTower R S M]
  [inst_28 : SMulCommClass A S M] [inst_29 : SMulCommClass S A M] [inst_30 : IsScalarTower S B M]
  [inst_31 : IsScalarTower R S N],
  TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q =
    (TensorProduct.AlgebraTensorModule.assoc R A B (TensorProduct S M N) P Q).symm ≪≫ₗ
        TensorProduct.AlgebraTensorModule.congr (TensorProduct.AlgebraTensorModule.rightComm A S B M N P)
          (LinearEquiv.refl R Q) ≪≫ₗ
      TensorProduct.AlgebraTensorModule.assoc R S B (TensorProduct A M P) N Q
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.isAffineMap_toFun : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (self : Convexity.ConvexSpace.AffineMap R X Y), Convexity.IsAffineMap R self.toFun
-- Mathlib.Data.PNat.Basic
PNat.natPred_le_natPred : ∀ {m n : ℕ+}, m.natPred ≤ n.natPred ↔ m ≤ n
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.disjoint_interior_base_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D] {n : ℕ}
  {j : Topology.RelCWComplex.cell C n}, Disjoint (interior D) (Topology.RelCWComplex.closedCell n j)
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_le_one : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0}, ↑p ≤ 1 ↔ p ≤ 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.instFinite : ∀ {V : Type u} {G : SimpleGraph V} [Finite V], Finite G.ConnectedComponent
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.CSLiftVal.mk : ∀ {α : Type u} {β : outParam (Type u)} [inst : Mathlib.Tactic.Ring.CSLift α β] {a : α} {b : outParam β},
  b = Mathlib.Tactic.Ring.CSLift.lift a → Mathlib.Tactic.Ring.CSLiftVal a b
-- Mathlib.Analysis.Matrix.Normed
/-- Seminormed group instance (using the Frobenius norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.frobeniusSeminormedAddCommGroup : {m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [SeminormedAddCommGroup α] → SeminormedAddCommGroup (Matrix m n α)
-- Mathlib.Order.Hom.BoundedLattice
/-- Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual
lattices.  -/
InfTopHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] → [inst_1 : Top α] → [inst_2 : Min β] → [inst_3 : Top β] → InfTopHom α β ≃ SupBotHom αᵒᵈ βᵒᵈ
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCommSemigroup : {α : Type u_1} → [AddCommSemigroup α] → AddCommSemigroup αᵒᵈ
-- Mathlib.Data.Finset.NoncommProd
Multiset.mul_noncommProd_erase : ∀ {α : Type u_3} [inst : Monoid α] [inst_1 : DecidableEq α] (s : Multiset α) {a : α},
  a ∈ s →
    ∀ (comm : {x | x ∈ s}.Pairwise Commute)
      (comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1) ⋯),
      a * (s.erase a).noncommProd comm' = s.noncommProd comm
-- Mathlib.Algebra.Star.StarRingHom
/-- By definition, a ⋆-ring equivalence preserves the `star` operation.  -/
StarRingEquivClass.map_star : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {inst : Add A} {inst_1 : Mul A} {inst_2 : Star A}
  {inst_3 : Add B} {inst_4 : Mul B} {inst_5 : Star B} {inst_6 : EquivLike F A B} [self : StarRingEquivClass F A B]
  (f : F) (a : A), f (star a) = star (f a)
-- Lean.Compiler.LCNF.Basic
/-- The signature of a declaration being processed by the Lean to Lean compiler passes.
 -/
Lean.Compiler.LCNF.Signature : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.Topology.Algebra.Group.Basic
Inseparable.zpow : ∀ {G : Type u_1} [inst : DivInvMonoid G] [inst_1 : TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G},
  Inseparable x y → ∀ (m : ℤ), Inseparable (x ^ m) (y ^ m)
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- Continuity within a set at a point can be read under right composition with a local
homeomorphism, if the point is in its target  -/
OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y} {x : Y},
  x ∈ e.target → (ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x))
-- Mathlib.Algebra.BigOperators.Finprod
finprod_cond_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (a : α) [inst_1 : DecidableEq α]
  (hf : Function.HasFiniteMulSupport f), ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ (Set.Finite.toFinset hf).erase a, f i
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.map_one : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N), f 1 = 1
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.mk.inj : ∀ {decl : Lean.Declaration} {indFvars : Array Lean.Expr} {numParams : ℤ}
  {rs : Array Lean.Elab.Command.PreElabHeaderResult} {decl_1 : Lean.Declaration} {indFvars_1 : Array Lean.Expr}
  {numParams_1 : ℤ} {rs_1 : Array Lean.Elab.Command.PreElabHeaderResult},
  { decl := decl, indFvars := indFvars, numParams := numParams, rs := rs } =
      { decl := decl_1, indFvars := indFvars_1, numParams := numParams_1, rs := rs_1 } →
    decl = decl_1 ∧ indFvars = indFvars_1 ∧ numParams = numParams_1 ∧ rs = rs_1
-- Mathlib.RingTheory.Ideal.Operations
/-- **Alias** of `Ideal.radical_bot_of_isReduced`. -/
Ideal.radical_bot_of_noZeroDivisors : ∀ {R : Type u} [inst : CommSemiring R] [IsReduced R], ⊥.radical = ⊥
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_mod_of_dvd : ∀ (a b : UInt32), b.toNat ∣ 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_log : Measurable Real.log
-- Mathlib.Order.Heyting.Hom
/-- `id` as a `HeytingHom`.  -/
HeytingHom.id : (α : Type u_2) → [inst : HeytingAlgebra α] → HeytingHom α α
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Predicate for the empty walk.

Solves the dependent type problem where `p = G.Walk.nil` typechecks
only if `p` has defeq endpoints.  -/
SimpleGraph.Walk.Nil : {V : Type u} → {G : SimpleGraph V} → {v w : V} → G.Walk v w → Prop
-- Mathlib.CategoryTheory.Category.Quiv
/-- Category structure on `Quiv`  -/
CategoryTheory.Quiv.category : CategoryTheory.LargeCategory CategoryTheory.Quiv
-- Mathlib.Order.Lattice
lt_sup_of_lt_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c < a → c < a ⊔ b
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂) (r : X ⟶ R)
  (reflexivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp r p₁ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₁._autoParam)
  (reflexivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp r p₂ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₂._autoParam)
  (toJointlyMono₂_1 : CategoryTheory.JointlyMono₂ p₁ p₂) (r_1 : X ⟶ R)
  (reflexivity₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp r_1 p₁ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₁._autoParam)
  (reflexivity₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp r_1 p₂ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₂._autoParam),
  ({ toJointlyMono₂ := toJointlyMono₂, r := r, reflexivity₁ := reflexivity₁, reflexivity₂ := reflexivity₂ } =
      { toJointlyMono₂ := toJointlyMono₂_1, r := r_1, reflexivity₁ := reflexivity₁_1,
        reflexivity₂ := reflexivity₂_1 }) =
    (r = r_1)
-- Mathlib.Data.List.Destutter
List.destutter'_sublist : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α),
  (List.destutter' R a l).Sublist (a :: l)
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.toCommRing : {R : Type u} → [self : EuclideanDomain R] → CommRing R
-- Mathlib.Tactic.Measurability
/-- The tactic `measurability` solves goals of the form `Measurable f`, `AEMeasurable f`,
`StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
with the `measurability` user attribute.

Note that `measurability` uses `fun_prop` for solving measurability of functions, so statements
about `Measurable`, `AEMeasurable`, `StronglyMeasurable` and `AEStronglyMeasurable` should be tagged
with `fun_prop` rather that `measurability`. The `measurability` attribute is equivalent to
`fun_prop` in these cases for backward compatibility with the earlier implementation.
 -/
Mathlib.Tactic.measurability : Lean.ParserDescr
-- Mathlib.Order.Category.Semilat
SemilatInfCat.dual_obj_isOrderBot : ∀ (X : SemilatInfCat), (SemilatInfCat.dual.obj X).isOrderBot = OrderDual.instOrderBotOfOrderTop X.X
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The first arrow.  -/
CategoryTheory.GrothendieckTopology.Cover.Relation.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → S.Relation → S.Arrow
-- Std.Data.ExtTreeMap.Basic
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.ExtTreeMap.diff : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.mem_support_notMem_vars_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : MvPolynomial σ R} {x : σ →₀ ℕ},
  x ∈ f.support → ∀ {v : σ}, v ∉ f.vars → x v = 0
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.forget_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y), (CategoryTheory.Grothendieck.forget F).map f = f.base
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `x : α` is in some `S ∈ 𝔖`, then evaluation at `x` is uniformly continuous on
`α →ᵤ[𝔖] β`.  -/
UniformOnFun.uniformContinuous_eval_of_mem : ∀ {α : Type u_1} (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)) {x : α},
  x ∈ s → s ∈ 𝔖 → UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_add_adjacent_intervals_cancel : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable f μ b c → ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.eq_1 : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  (D : A → B) [inst_3 : Nonempty A] (f : AddMonoidAlgebra R A),
  AddMonoidAlgebra.Monic D f = (AddMonoidAlgebra.leadingCoeff D f = 1)
-- Mathlib.RingTheory.Algebraic.Pi
polynomial_smul_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Semiring R] [inst_1 : SMul R S] (p : Polynomial R) (f : R → S) (x : R),
  (p • f) x = Polynomial.eval x p • f x
-- Mathlib.Algebra.Order.Group.End
RelHom.one_apply : ∀ {α : Type u_1} {r : α → α → Prop} (a : α), 1 a = a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {x : G} {n : WithTop ℕ∞}, ContDiffAt ℝ n f x → ContDiffAt ℝ n g x → ContDiffAt ℝ n (fun x => inner 𝕜 (f x) (g x)) x
-- Mathlib.Order.Concept
Concept.intent_sInf : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)),
  (sInf S).intent = upperPolar r (⋂ i ∈ S, i.extent)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsBoundedSMul : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] {𝕜' : Type u_1}
  [inst_6 : SeminormedRing 𝕜'] [inst_7 : Module 𝕜' G] [inst_8 : IsBoundedSMul 𝕜' G] [inst_9 : SMulCommClass 𝕜 𝕜' G],
  IsBoundedSMul 𝕜' (ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.Combinatorics.Additive.Corner.Roth
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.farFromTriangleFree_graph : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Finset (G × G)} {ε : ℝ} [inst_1 : Fintype G] [inst_2 : DecidableEq G],
  ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card →
    (SimpleGraph.TripartiteFromTriangles.graph (Corners.triangleIndices✝ A)).FarFromTriangleFree (ε / 9)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], AddMonoidAlgebra.ofCoeff 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.ι_comp_sigmaComparison_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasCoproduct f] [inst_3 : CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)]
  (b : β) {Z : D} (h : G.obj (∐ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun b => G.obj (f b)) b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.ι f b)) h
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Any linear isometric equivalence in `V` with positive determinant is `rotation`.  -/
Orientation.exists_linearIsometryEquiv_eq_of_det_pos : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {f : V ≃ₗᵢ[ℝ] V}, 0 < LinearMap.det ↑f.toLinearEquiv → ∃ θ, f = o.rotation θ
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.div_div_cancel'` for a stronger version.  -/
ENNReal.div_div_cancel : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → a / (a / b) = b
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.rightFunc.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Arrow.rightFunc = CategoryTheory.Comma.snd (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- **Alias** of `Ideal.ramificationIdxIn_mul_ramificationIdxIn`. -/
Ideal.ramificationIdxIn_mul_ramificationIdxIn' : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (G : Type u_3) [inst_3 : Group G] [Finite G]
  [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B] (C : Type u_4) [inst_7 : CommRing C] [inst_8 : Algebra A C]
  [inst_9 : Algebra B C] [Nonempty ↑(P.primesOver C)] [IsScalarTower A B C] (GAC : Type u_5) [inst_12 : Group GAC]
  [Finite GAC] [inst_14 : MulSemiringAction GAC C] [IsGaloisGroup GAC A C] (GBC : Type u_6) [inst_16 : Group GBC]
  [Finite GBC] [inst_18 : MulSemiringAction GBC C] [IsGaloisGroup GBC B C] [Module.Flat B C],
  p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
-- Init.Data.UInt.Bitwise
UInt16.xor_assoc : ∀ (a b c : UInt16), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.CategoryTheory.Localization.Composition
/-- Under some conditions on the `MorphismProperty`, functors satisfying the strict
universal property of the localization are stable under composition  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.comp : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {E : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E] →
                {L₁ : CategoryTheory.Functor C₁ C₂} →
                  {L₂ : CategoryTheory.Functor C₂ C₃} →
                    {W₁ : CategoryTheory.MorphismProperty C₁} →
                      {W₂ : CategoryTheory.MorphismProperty C₂} →
                        CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L₁ W₁ E →
                          CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L₂ W₂ E →
                            (W₃ : CategoryTheory.MorphismProperty C₁) →
                              W₃.IsInvertedBy (L₁.comp L₂) →
                                W₁ ≤ W₃ →
                                  W₂ ≤ W₃.map L₁ →
                                    CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (L₁.comp L₂) W₃ E
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCancelMonoid : {α : Type u_1} → [CancelMonoid α] → CancelMonoid αᵒᵈ
-- Std.Data.ExtTreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.ExtTreeMap.insertMany : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → {ρ : Type u_1} → [ForIn Id ρ (α × β)] → Std.ExtTreeMap α β cmp → ρ → Std.ExtTreeMap α β cmp
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- `U.starProjection` is a symmetric projection.  -/
Submodule.isSymmetricProjection_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection], (↑U.starProjection).IsSymmetricProjection