mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `G` preserves products and `C` has them, then the fan constructed of the mapped projection of a
product is a limit.
 -/
CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [inst_2 : CategoryTheory.Limits.HasProduct f] →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.Fan.mk (G.obj (∏ᶜ f)) fun j => G.map (CategoryTheory.Limits.Pi.π f j))
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_lt_zero : ∀ {q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], ↑q < 0 ↔ q < 0
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (e : σ ≃ τ)
  (a : ↥(MvPolynomial.symmetricSubalgebra τ R)),
  ↑((MvPolynomial.renameSymmetricSubalgebra e).symm a) = (MvPolynomial.rename ⇑e.symm) ↑a
-- Mathlib.Algebra.Lie.IdealOperations
LieIdeal.comap_bracket_le : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') {J₁ J₂ : LieIdeal R L'},
  ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ≤ LieIdeal.comap f ⁅J₁, J₂⁆
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatInt8SintOfNatNat : Lean.Grind.ToInt.OfNat Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
/-- Any flat morphism is generalizing.  -/
AlgebraicGeometry.Flat.generalizingMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f], GeneralizingMap ⇑f
-- Lean.Elab.Term.TermElabM
/-- State saved for reuse, if no fatal exception occurred.  -/
Lean.Elab.Tactic.TacticFinishedSnapshot.state? : Lean.Elab.Tactic.TacticFinishedSnapshot → Option Lean.Elab.Tactic.SavedState
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_leftUnitor : ∀ {G : Type v} [inst : Monoid G] (X : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  ↑(Representation.TensorProduct.lid k (Representation.linearize k G X)) =
    ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom).comp
          (Representation.LinearizeMonoidal.μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G))
            X)).comp
      (Representation.IntertwiningMap.rTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.ε k G))
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.Basis.toBasis_toOrthonormalBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v : Module.Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v),
  (v.toOrthonormalBasis hv).toBasis = v
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- `WeakBilin B` is a `IsTopologicalAddGroup`, meaning that addition and negation are
continuous.  -/
WeakBilin.instIsTopologicalAddGroup : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommRing 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜], IsTopologicalAddGroup (WeakBilin B)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreWhiskerRight : ∀ {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 G : CategoryTheory.Functor C D} (η : F ≅ G)
  (H : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.isoWhiskerRight η H).core =
    F.coreComp H ≪≫ CategoryTheory.Functor.isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instAddCancelCommMonoidLocalization.eq_1 : ∀ {M : Type u_3} [inst : AddCancelCommMonoid M] (S : AddSubmonoid M),
  AddSubmonoid.LocalizationMap.instAddCancelCommMonoidLocalization S =
    (AddLocalization.addMonoidOf S).addCancelCommMonoid
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfRoot_gen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0),
  (pb.equivOfRoot pb' h₁ h₂) pb.gen = pb'.gen
-- Std.Net.Addr
Std.Net.SocketAddressV6.mk.injEq : ∀ (addr : Std.Net.IPv6Addr) (port : UInt16) (addr_1 : Std.Net.IPv6Addr) (port_1 : UInt16),
  ({ addr := addr, port := port } = { addr := addr_1, port := port_1 }) = (addr = addr_1 ∧ port = port_1)
-- Mathlib.Order.Heyting.Hom
CoheytingHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  [inst_2 : CoheytingAlgebra γ] {f₁ f₂ : CoheytingHom α β} {g : CoheytingHom β γ},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, (m.modify k f).contains k' = m.contains k'
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_filter_atomise_le_two_pow : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {F : Finset (Finset α)},
  t ∈ F → {u ∈ (Finpartition.atomise s F).parts | u ⊆ t ∧ u.Nonempty}.card ≤ 2 ^ (F.card - 1)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.involutiveNeg.eq_1 : ∀ {α : Type u_2} [inst : InvolutiveNeg α], Set.involutiveNeg = { toNeg := Set.neg, neg_neg := ⋯ }
-- Mathlib.Order.Hom.Bounded
/-- Turn an element of a type `F` satisfying `TopHomClass F α β` into an actual
`TopHom`. This is declared as the default coercion from `F` to `TopHom α β`.  -/
TopHomClass.toTopHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : FunLike F α β] → [inst_1 : Top α] → [inst_2 : Top β] → [TopHomClass F α β] → F → TopHom α β
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp.congr_simp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommSemiring R] (s s_1 : ℤˣ),
  s = s_1 →
    ∀ (A A_1 : Matrix n n R),
      A = A_1 →
        ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → Matrix.adjp s A a a_2 = Matrix.adjp s_1 A_1 a_1 a_3
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_map_sectL : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a b : α) (c : β),
  Finset.map (Function.Embedding.sectL α c) (Finset.Ioc a b) = Finset.Ioc (a, c) (b, c)
-- Init.Data.Nat.Basic
Nat.instTransLeLt : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.size_expandIfNecessary : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β},
  (↑m.expandIfNecessary).size = (↑m).size
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lmk_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (s : Finset ι) (x : (i : ↑↑s) → M ↑i),
  (DFinsupp.lmk s) x = DFinsupp.mk s x
-- Mathlib.Tactic.ReduceModChar
/-- Given an integral expression `e : t` such that `t` is a ring of characteristic `n`,
reduce `e` modulo `n`.  -/
Tactic.ReduceModChar.normIntNumeral : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n : Q(ℕ)) → (e : Q(«$α»)) → (x : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Order.Category.LinOrd
LinOrd.ofHom_hom : ∀ {X Y : LinOrd} (f : X ⟶ Y), LinOrd.ofHom (LinOrd.Hom.hom f) = f
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.exists_measurable_superset_of_null : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  μ s = 0 → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- A `Cofan` gives a `Fan` in the opposite category.  -/
CategoryTheory.Limits.Cofan.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} → {Z : α → C} → CategoryTheory.Limits.Cofan Z → CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.crossing_eq_crossing_of_upperCrossingTime_lt : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω} {M : ℕ},
  N ≤ M →
    MeasureTheory.upperCrossingTime a b f N (n + 1) ω < N →
      MeasureTheory.upperCrossingTime a b f M (n + 1) ω = MeasureTheory.upperCrossingTime a b f N (n + 1) ω ∧
        MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω
-- Mathlib.Algebra.Order.Group.Basic
zpow_lt_zpow_iff_left : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α},
  0 < n → (a ^ n < b ^ n ↔ a < b)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- `trim` respects scalar multiplication.  -/
MeasureTheory.OuterMeasure.trim_smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {R : Type u_2} [inst_1 : SMul R ENNReal]
  [inst_2 : IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.OuterMeasure α), (c • m).trim = c • m.trim
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.image_closure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  (∀ x ∈ closure s, ContinuousWithinAt f s x) → f '' closure s ⊆ closure (f '' s)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mul_mem_cancel_right : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d e : C} {f : c ⟶ d}
  {g : d ⟶ e}, g ∈ S.arrows d e → (CategoryTheory.CategoryStruct.comp f g ∈ S.arrows c e ↔ f ∈ S.arrows c d)
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.isOpen_iff_of_isColimit_cofork : ∀ {X Y : TopCat} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) (hc : CategoryTheory.Limits.IsColimit c)
  (U : Set ↑c.pt), IsOpen U ↔ IsOpen (⇑(CategoryTheory.ConcreteCategory.hom c.π) ⁻¹' U)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofIsBaseOfFinite_E : ∀ {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ B, IsBase B)
  (isBase_exchange : Matroid.ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).E = E
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.pointwise_smul_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {R' : Type u_3}
  [inst_3 : Semiring R'] [inst_4 : MulSemiringAction R' A] [inst_5 : SMulCommClass R' R A] (m : R')
  (S : Subalgebra R A), Subalgebra.toSubmodule (m • S) = m • Subalgebra.toSubmodule S
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.isKan.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x)
  [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h = CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_const : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.IsProbabilityMeasure μ] (π : MeasureTheory.Measure Θ)
      [MeasureTheory.SFinite π],
      ProbabilityTheory.bayesRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_asc_factorial_div_factorial : ∀ (n k : ℕ), (n + k).choose k = (n + 1).ascFactorial k / k.factorial
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.ext_iff : ∀ {α : Type u_3} {d₁ d₂ : MeasurableSpace.DynkinSystem α}, d₁ = d₂ ↔ ∀ (s : Set α), d₁.Has s ↔ d₂.Has s
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Recursor for `W`  -/
MvPFunctor.wRec : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {C : Sort u_1} → ((a : P.A) → (P.drop.B a).Arrow α → (P.last.B a → P.W α) → (P.last.B a → C) → C) → P.W α → C
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_forall_get?_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α],
  (∀ (k : α), m₁.get? k = m₂.get? k) → m₁.Equiv m₂
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
/-- **Hausdorff–Alexandroff theorem**: every nonempty compact metric space is a continuous image
of the Cantor set.  -/
exists_nat_bool_continuous_surjective_of_compact : ∀ (X : Type u_1) [Nonempty X] [inst : MetricSpace X] [CompactSpace X], ∃ f, Continuous f ∧ Function.Surjective f
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_mul : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), ⇑(f * g) = ⇑f ∘ ⇑g
-- Batteries.Lean.Except
instDecidableEqExcept_batteries.decEq : {ε : Type u_1} → {α : Type u_2} → [DecidableEq ε] → [DecidableEq α] → (x x_1 : Except ε α) → Decidable (x = x_1)
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.hyperplane_separation_of_notMem : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : CompleteSpace E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℝ F] [inst_5 : CompleteSpace F]
  (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F},
  b ∉ ProperCone.map f K → ∃ y, (ContinuousLinearMap.adjoint f) y ∈ ProperCone.innerDual ↑K ∧ inner ℝ b y < 0
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_carrier : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.isBigO_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)}, HasFDerivAtFilter f f' L → (fun p => f p.1 - f p.2) =O[L] fun p => p.1 - p.2
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.ne_zero : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [Nontrivial R] (i : ι), b i ≠ 0
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)} {ι' : Type u_5} {g : ι' → ι},
  Function.Injective g → ProbabilityTheory.Kernel.iIndepSets π κ μ → ProbabilityTheory.Kernel.iIndepSets (π ∘ g) κ μ
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_isSelfAdjoint_and_spectrum_pos : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A}, IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instCoeOutAlgHom : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → CoeOut (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq : ∀ (x : ℂ), Complex.tan x = 2 * Complex.tan (x / 2) / (1 - Complex.tan (x / 2) ^ 2)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D'),
  (CategoryTheory.StructuredArrow.prodEquivalence S S' T T').inverse =
    CategoryTheory.StructuredArrow.prodInverse S S' T T'
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.Equiv.forIn_eq : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] [inst_4 : Monad m]
  [inst_5 : LawfulMonad m] [inst_6 : Monad n] [LawfulMonad n] [inst_8 : Std.IteratorLoop α₁ m n]
  [Std.LawfulIteratorLoop α₁ m n] [inst_10 : Std.IteratorLoop α₂ m n] [Std.LawfulIteratorLoop α₂ m n]
  [inst_12 : MonadLiftT m n] [LawfulMonadLiftT m n] {init : γ} {f : β → γ → n (ForInStep γ)} {ita : Std.IterM m β}
  {itb : Std.IterM m β}, ita.Equiv itb → forIn ita init f = forIn itb init f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_clearUnit : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments l).size = assignments.size
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap (-φ) = -CategoryTheory.ShortComplex.homologyMap φ
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft.mk : {m : Type → Type} →
  [toMonadHorizontalComp : Mathlib.Tactic.BicategoryLike.MonadHorizontalComp m] →
    (Mathlib.Tactic.BicategoryLike.Atom₁ →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
      Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft m
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_one : ∀ {R : Type u_1} {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → Submodule R A} [inst_5 : GradedAlgebra 𝒜], ⇑1 = id
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_closure_pair : ∀ {C : Type u_2} [inst : AddCommGroup C] {x y z : C}, z ∈ AddSubgroup.closure {x, y} ↔ ∃ m n, m • x + n • y = z
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- the second "inclusion" in the (pre)cylinder  -/
HomotopicalAlgebra.Precylinder.i₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A : C} → (self : HomotopicalAlgebra.Precylinder A) → A ⟶ self.I
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.saturate_p₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (x x_1 : E.I₀) (r : E.Relation x x_1), E.saturate.p₁ r = r.fst
-- Std.Sync.Channel
/-- The capacity of the buffer space.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.capacity : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → ℕ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [Inhabited α] {k : α} {f : β → β} {hc : k ∈ Std.DTreeMap.Const.modify t k f},
  (Std.DTreeMap.Const.modify t k f).getKey k hc = k
-- Mathlib.Control.ULift
ULift.instLawfulApplicative_mathlib : LawfulApplicative ULift.{u_2, u_1}
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toShortNFOfCharThree_a₂ : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : CharP R 3],
  (W.toShortNFOfCharThree • W).a₂ = W.b₂
-- Init.Data.Nat.Lemmas
Nat.shiftLeft_zero : ∀ {n : ℕ}, n <<< 0 = n
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_apply_eq_zero_iff : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) {x : M}, (p.projectionL q h) x = 0 ↔ x ∈ q
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.instNonemptyUnbounded : ∀ {α : Type}, Nonempty (Std.CloseableChannel.Unbounded✝ α)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsNontrivial_iff_exists_one_lt : ∀ {K : Type u_7} [inst : DivisionRing K] {Γ₀ : Type u_8} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  {v : Valuation K Γ₀}, v.IsNontrivial ↔ ∃ x, 1 < v x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF) (h' : k ∈ Std.TreeMap.Raw.filterMap f t),
  (f (t.getKey k ⋯) t[k]).isSome = true
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_inv : ∀ {ι : 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) (i : ι),
  (P.reflection i)⁻¹ = P.reflection i
-- Mathlib.Data.Finite.Prod
MulEquiv.finite_left : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β] [Finite α], Finite (α ≃* β)
-- Init.Data.Vector.Lemmas
Vector.toList_insertIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (h : i ≤ n),
  (xs.insertIdx i x h).toList = xs.toList.insertIdx i x
-- Mathlib.Probability.Process.Filtration
/-- A filtration `𝓕` is right continuous if it is equal to its right continuation `𝓕₊`.  -/
MeasureTheory.Filtration.IsRightContinuous : {Ω : Type u_1} →
  {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : PartialOrder ι] → MeasureTheory.Filtration ι m → Prop
-- Aesop.Rule.Forward
Aesop.instInhabitedForwardRulePriority.default : Aesop.ForwardRulePriority
-- Mathlib.Data.Set.Image
Set.image_sdiff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s t : Set α), f '' (s \ t) = f '' s \ f '' t
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.mk.injEq : ∀ {m : Type w → Type w'} {β : Type w} (α : Type w) (inst : Std.Iterator α m β) (iterator : Std.IterM m β) (α_1 : Type w)
  (inst_1 : Std.Iterator α_1 m β) (iterator_1 : Std.IterM m β),
  ({ α := α, inst := inst, iterator := iterator } = { α := α_1, inst := inst_1, iterator := iterator_1 }) =
    (α = α_1 ∧ inst ≍ inst_1 ∧ iterator ≍ iterator_1)
-- Mathlib.Algebra.Ring.Action.Invariant
IsInvariantSubring.coe_subtypeHom : ∀ (M : Type u_1) [inst : Monoid M] {R' : Type u_2} [inst_1 : Ring R'] [inst_2 : MulSemiringAction M R'] (U : Subring R')
  [inst_3 : IsInvariantSubring M U], ⇑(IsInvariantSubring.subtypeHom M U) = Subtype.val
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.pair_succ : ∀ {α : Type u_2} [inst : Preorder α] (a b : α) (hab : a ≤ b) (n : ℕ),
  (OmegaCompletePartialOrder.Chain.pair a b hab) (n + 1) = b
-- Init.Data.Fin.Fold
Fin.foldr_eq_foldrM : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α → α) (x : α),
  Fin.foldr n f x = (Fin.foldrM n (fun x1 x2 => pure (f x1 x2)) x).run