mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associativity_functor : ∀ (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],
  (CategoryTheory.sum.associativity C D E).functor = CategoryTheory.sum.associator C D E
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- If `s` is a dense set in an additive monoid `M`, `AddSubmonoid.closure s = ⊤`, then in
order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for
`x ∈ s`, verify `p 0`, and verify that `p x` and `p y` imply `p (x + y)`.  -/
AddSubmonoid.dense_induction : ∀ {M : Type u_1} [inst : AddZeroClass M] {motive : M → Prop} (s : Set M),
  AddSubmonoid.closure s = ⊤ →
    (∀ x ∈ s, motive x) → motive 0 → (∀ (x y : M), motive x → motive y → motive (x + y)) → ∀ (x : M), motive x
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.isTopologicalBasis_cylinders : ∀ (E : ℕ → Type u_1) [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)],
  TopologicalSpace.IsTopologicalBasis {s | ∃ x n, s = PiNat.cylinder x n}
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_addConst_mul_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.addConst B) * ↑A.card = ↑(A + B).card
-- Init.Data.Array.Find
Array.back!_filter : ∀ {α : Type} [inst : Inhabited α] {p : α → Bool} {xs : Array α}, (Array.filter p xs).back! = (Array.findRev? p xs).get!
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol of `a^2` at `p` is 1 if `p ∤ a`.  -/
legendreSym.sq_one' : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ}, ↑a ≠ 0 → legendreSym p (a ^ 2) = 1
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.coe_sub : ∀ (m n : ℕ), ↑m - ↑n = ↑(m - n)
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] (S : ι →o L.PartialEquiv M N),
  DirectedSystem (fun i => ↥(S i).cod) fun x x_1 h => ⇑(FirstOrder.Language.Substructure.inclusion ⋯)
-- Init.Control.Lawful.MonadLift.Instances
Except.bind.eq_1 : ∀ {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → Except ε β) (err : ε),
  (Except.error err).bind f = Except.error err
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The pre-path object obtained by switching the two projections.  -/
HomotopicalAlgebra.PrepathObject.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} → HomotopicalAlgebra.PrepathObject A → HomotopicalAlgebra.PrepathObject A
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_le_re`. -/
Complex.frontier_setOf_le_re : ∀ (a : ℝ), frontier {z | a ≤ z.re} = {z | z.re = a}
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.comp.match_1.eq_3 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2)
  (_X : C) (x : CategoryTheory.WithTerminal C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithTerminal.of _X) (CategoryTheory.WithTerminal.of _Y)
        (CategoryTheory.WithTerminal.of _Z))
  (h_2 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive (CategoryTheory.WithTerminal.of _X) x CategoryTheory.WithTerminal.star)
  (h_3 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _X) x)
  (h_4 :
    (x : CategoryTheory.WithTerminal C) →
      (_Y : C) → motive x CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _Y))
  (h_5 :
    Unit → motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => h_2 _X x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => h_3 _X x
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => h_4 x _Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star => h_5 ()) =
    h_3 _X x
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_pred_lt_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0), (a.pred ha).castSucc < b ↔ a ≤ b
-- Mathlib.Control.EquivFunctor
EquivFunctor.mapEquiv_symm_apply : ∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β : Type u₀} (e : α ≃ β) (y : f β),
  (EquivFunctor.mapEquiv f e).symm y = EquivFunctor.map e.symm y
-- Lean.PrettyPrinter.Parenthesizer
/-- Wraps the term `stx` in parentheses and then moves its `SourceInfo` to the result.
The purpose of this is to move synthetic delaborator positions from the `stx` node to the parentheses node,
which causes the info view to view the node with parentheses as referring to the parenthesized expression.
If we did not move info, the info view would consider the parentheses to belong to the outer term.
Note: we do not do `withRef stx` because that causes the "(" and ")" tokens to have source info as well,
causing the info view to highlight each parenthesis as an independent expression.  -/
_private.Lean.PrettyPrinter.Parenthesizer.0.Lean.PrettyPrinter.Parenthesizer.term.parenthesizer.wrapParens : Lean.Syntax → Lean.Syntax
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_3.eq_2 : ∀ (motive : Std.HashSet Lean.Syntax.Range → Lean.Syntax → Sort u_1) (curr : Std.HashSet Lean.Syntax.Range)
  (info : Lean.SourceInfo)
  (h_1 :
    (curr : Std.HashSet Lean.Syntax.Range) →
      (s : Lean.Syntax) →
        (info : Lean.SourceInfo) →
          (kind : Lean.SyntaxNodeKind) →
            (args : Array Lean.Syntax) →
              s = Lean.Syntax.node info kind args → motive curr (Lean.Syntax.node info kind args))
  (h_2 :
    (curr : Std.HashSet Lean.Syntax.Range) → (info : Lean.SourceInfo) → motive curr (Lean.Syntax.atom info "where"))
  (h_3 : (curr : Std.HashSet Lean.Syntax.Range) → (x : Lean.Syntax) → motive curr x),
  (match curr, Lean.Syntax.atom info "where" with
    | curr, s@h:(Lean.Syntax.node info kind args) => h_1 curr s info kind args h
    | curr, Lean.Syntax.atom info "where" => h_2 curr info
    | curr, x => h_3 curr x) =
    h_2 curr info
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.ediv.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (a : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (a : ℕ) → motive (Int.negSucc a) 0)
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc a, 0 with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc a, 0 => h_3 a
    | Int.negSucc m, Int.ofNat n.succ => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_3 a
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₁ =
    (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₁
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.functorH_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (n : ℕ)
  {X Y : CategoryTheory.Sheaf J AddCommGrpCat} (f : X ⟶ Y),
  (CategoryTheory.Sheaf.functorH J n).map f = AddCommGrpCat.ofHom (CategoryTheory.Sheaf.H.map f n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_union!_of_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₁ = true → Std.DTreeMap.Internal.Impl.contains a m₂ = false) →
        (m₁.union! m₂).size = m₁.size + m₂.size
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ X₃ ⊗ (X₁ ⊗ X₂)`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Lean.Data.LOption
Lean.instBEqLOption.beq : {α : Type u_1} → [BEq α] → Lean.LOption α → Lean.LOption α → Bool
-- Mathlib.FieldTheory.Finite.Basic
/-- The cardinality `q` is a power of the characteristic of `K`.  -/
FiniteField.card : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (p : ℕ) [CharP K p], ∃ n, Nat.Prime p ∧ Fintype.card K = p ^ ↑n
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.prod_range_succ_factorial : ∀ (n : ℕ), ∏ x ∈ Finset.range (n + 1), x.factorial = n.superFactorial
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mk_eq_iff : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) {x y : V},
  (Representation.Coinvariants.mk ρ) x = (Representation.Coinvariants.mk ρ) y ↔
    x - y ∈ Representation.Coinvariants.ker ρ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_star : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_6} [inst : NormedAddCommGroup R]
  [inst_1 : StarAddMonoid R] [inst_2 : NormedStarGroup R] {p : ENNReal} (f : ↥(MeasureTheory.Lp R p μ)),
  ↑↑(star f) =ᵐ[μ] star ↑↑f
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometryEquiv.norm_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂] (e : E ≃ₛₗᵢ[σ₁₂] F),
  ‖↑↑e‖ = 1
-- Mathlib.Algebra.GradedMonoid
/-- A graded version of `Monoid`

Like `Monoid.npow`, this has an optional `GMonoid.gnpow` field to allow definitional control of
natural powers of a graded monoid.  -/
GradedMonoid.GMonoid : {ι : Type u_1} → (ι → Type u_2) → [AddMonoid ι] → Type (max u_1 u_2)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.yonedaEquiv_toOfSimplex : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })), SSet.yonedaEquiv (SSet.Subcomplex.toOfSimplex x) = ⟨x, ⋯⟩
-- Lean.Util.ForEachExpr
Lean.ForEachExpr.visit : {ω : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [MonadLiftT (ST ω) m] → [Monad m] → (Lean.Expr → m Bool) → Lean.Expr → Lean.MonadCacheT Lean.Expr Unit m Unit
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.add_scaleRoots_of_natDegree_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
  p.natDegree = q.natDegree →
    r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittNSMul.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (n n_1 : ℕ),
  n = n_1 → ∀ (a a_1 : ℕ), a = a_1 → WittVector.wittNSMul p n a = WittVector.wittNSMul p_1 n_1 a_1
-- Init.Grind.Module.Basic
/-- Scalar multiplication by integers.  -/
Lean.Grind.IntModule.zsmul : {M : Type u} → [self : Lean.Grind.IntModule M] → SMul ℤ M
-- Mathlib.Algebra.Order.Module.Field
OrderIso.smulRightDual_symm_apply : ∀ {𝕜 : Type u_1} (G : Type u_2) [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [inst_5 : IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜}
  [inst_7 : PosSMulMono 𝕜 G] (ha : a < 0) (a_1 : Gᵒᵈ),
  (RelIso.symm (OrderIso.smulRightDual G ha)) a_1 = a⁻¹ • OrderDual.ofDual a_1
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremWith'_iff_fermatLastTheoremWith : ∀ {R : Type u_2} [inst : CommSemiring R] [IsDomain R] {n : ℕ},
  (∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) →
    (FermatLastTheoremWith' R n ↔ FermatLastTheoremWith R n)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.instHasPushoutUnopOfHasPullbackOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasPullback f g], CategoryTheory.Limits.HasPushout f.unop g.unop
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_submatrix_equiv : ∀ {m : Type u} {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] [inst_4 : CommRing α] (A : Matrix m m α) (e : n ≃ m) (b : n → α),
  (A.submatrix ⇑e ⇑e).cramer b = A.cramer (b ∘ ⇑e.symm) ∘ ⇑e
-- Lean.Data.Format
Lean.instToFormatDataValue : Std.ToFormat Lean.DataValue
-- Mathlib.Topology.Algebra.InfiniteSum.Order
le_hasProd : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop],
  HasProd f a L → ∀ (i : ι), (∀ (j : ι), j ≠ i → 1 ≤ f j) → f i ≤ a
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.map_comp : ∀ {M : Type u_5} [inst : AddCommMonoid M] {X : Type u_6} {Y : Type u_7} {Z : Type u_8} [inst_1 : Finite X]
  [inst_2 : Finite Y] [inst_3 : Finite Z] (g : Y → Z) (f : X → Y),
  FunOnFinite.map (g ∘ f) = FunOnFinite.map g ∘ FunOnFinite.map f
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.IsGaussian.hasGaussianLaw : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : TopologicalSpace E]
  [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X : Ω → E}
  [ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map X P)], ProbabilityTheory.HasGaussianLaw X P
-- Mathlib.Data.Set.Card
Set.finite_of_encard_le_coe : ∀ {α : Type u_1} {s : Set α} {k : ℕ}, s.encard ≤ ↑k → s.Finite
-- Mathlib.Algebra.Ring.Prod
/-- A ring `R` is isomorphic to `S × R` when `S` is the zero ring  -/
RingEquiv.zeroRingProd : (R : Type u_1) →
  (S : Type u_3) → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → [Subsingleton S] → R ≃+* S × R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_X_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 →
            W.add P Q =
              WeierstrassCurve.Jacobian.addZ P Q •
                ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  1]
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.forall.sizeOf_spec : sizeOf Lean.Meta.RefinedDiscrTree.Key.forall = 1
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.imported.sizeOf_spec : sizeOf Mathlib.Tactic.ClickSuggestions.SectionKind.imported = 1
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.eq_inf : @AlgebraicGeometry.IsClosedImmersion =
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding) ⊓
    @AlgebraicGeometry.SurjectiveOnStalks
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_casesOn' : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} {g : α → ℕ → β},
  Primrec f → Primrec₂ g → Primrec₂ fun a n => Nat.casesOn n (f a) (g a)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_pow_comm : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ) (n : ℕ), (x ^ y) ^ n = (x ^ n) ^ y
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.functorCategoryHasLimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C],
  CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, max u₂ v, max (max (max u u₂) v) v₂} (CategoryTheory.Functor K C)
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instPreservesInjectiveObjectsUliftFunctorOfSmall : ∀ (R : Type u) [inst : Ring R] [Small.{v, u} R], (ModuleCat.uliftFunctor.{v', v, u} R).PreservesInjectiveObjects
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (self : P.LeftHomotopy f g), CategoryTheory.CategoryStruct.comp P.i₁ self.h = g
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.asEquivalence_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence] (X : C),
  F.asEquivalence.unitIso.hom.app X = F.preimage (F.objObjPreimageIso (F.obj X)).inv
-- Mathlib.CategoryTheory.Action.Concrete
Action.ρ_self_inv_apply : ∀ {G : Type u} [inst : Group G] {A : Action (Type u) G} (g : G) (x : A.V),
  (CategoryTheory.ConcreteCategory.hom (A.ρ g)) ((CategoryTheory.ConcreteCategory.hom (A.ρ g⁻¹)) x) = x
-- Mathlib.Data.Nat.Pairing
Nat.unpair_right_le : ∀ (n : ℕ), (Nat.unpair n).2 ≤ n
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.trans : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e →
    ∀ {e' : OpenPartialHomeomorph M' M''},
      OpenPartialHomeomorph.MDifferentiable I' I'' e' → OpenPartialHomeomorph.MDifferentiable I I'' (e.trans e')
-- Mathlib.Topology.MetricSpace.Lipschitz
lipschitzWith_max : LipschitzWith 1 fun p => max p.1 p.2
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- **Cartan's formula** with the additive constant written explicitly as a circle average of the
logarithm of the first nonzero Laurent coefficient of `f - a` at the origin.

See `circleIntegrable_logCounting` and `circleIntegrable_log_meromorphicTrailingCoeffAt` for the
facts that the summands are actually circle integrable.
 -/
ValueDistribution.characteristic_top_eq_circleAverage_add_circleAverage : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    R ≠ 0 →
      ValueDistribution.characteristic f ⊤ R =
        Real.circleAverage (fun x => ValueDistribution.logCounting f (↑x) R) 0 1 +
          Real.circleAverage (fun a => Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖) 0 1
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- Given a nondegenerate bilinear form `B` on a finite-dimensional vector space, `B.toDual` is
the linear equivalence between a vector space and its dual.  -/
LinearMap.BilinForm.toDual : {V : Type u_5} →
  {K : Type u_6} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] → (B : LinearMap.BilinForm K V) → B.Nondegenerate → V ≃ₗ[K] Module.Dual K V
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_hsum : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α} {g : Γ}, s.hsum.coeff g = ∑ᶠ (i : α), (s i).coeff g
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Returns true if the given predicate is true for any item in the RBSet.  -/
RBTree.RBSet.any : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Bool) → Bool
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_equivOfInverse : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h₁ : Function.LeftInverse ⇑f₂ ⇑f₁) (h₂ : Function.RightInverse ⇑f₂ ⇑f₁),
  (ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂).symm = ContinuousLinearEquiv.equivOfInverse f₂ f₁ h₂ h₁
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImpRight.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 x_2 : L.BoundedFormula α x) →
          ((n : ℕ) →
              (φ : L.BoundedFormula α n) →
                (ψ : L.BoundedFormula α (n + 1)) →
                  motive n φ
                    ((ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp
                      FirstOrder.Language.BoundedFormula.falsum)) →
            ((n : ℕ) → (φ : L.BoundedFormula α n) → (ψ : L.BoundedFormula α (n + 1)) → motive n φ ψ.all) →
              ((_n : ℕ) →
                  (φ ψ : L.BoundedFormula α _n) →
                    (∀ (ψ_1 : L.BoundedFormula α (_n + 1)),
                        ψ =
                            (ψ_1.imp FirstOrder.Language.BoundedFormula.falsum).all.imp
                              FirstOrder.Language.BoundedFormula.falsum →
                          False) →
                      (∀ (ψ_1 : L.BoundedFormula α (_n + 1)), ψ = ψ_1.all → False) → motive _n φ ψ) →
                motive x x_1 x_2
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.op_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F), c.op.pt = Opposite.op c.pt
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The bundled commutative ring giving the filtered colimit of a diagram.  -/
CommRingCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommRingCat → CommRingCat
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr_symm : ∀ {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
  (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm