mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.Sum
/-- `sigmaFiberEquiv f` for `f : α → β` is the natural equivalence between
the type of all fibres of `f` and the total space `α`.  -/
Equiv.sigmaFiberEquiv : {α : Type u_9} → {β : Type u_10} → (f : α → β) → (y : β) × { x // f x = y } ≃ α
-- Init.Prelude
/-- Optional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
 -/
Option : Type u → Type u
-- Lean.Elab.Tactic.Grind.Basic
/-- Throws an error unless the tactic is being executed in `sym =>` mode.  -/
Lean.Elab.Tactic.Grind.ensureSym : Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.iff_of_equiv : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B), Algebra.FormallySmooth R A ↔ Algebra.FormallySmooth R B
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.codeBlock.sizeOf_spec : sizeOf Lean.Elab.DocElabKind.codeBlock = 1
-- Mathlib.Data.Set.Basic
SetCoe.exists' : ∀ {α : Type u} {s : Set α} {p : (x : α) → x ∈ s → Prop}, (∃ x, ∃ (h : x ∈ s), p x h) ↔ ∃ x, p ↑x ⋯
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure.congr_simp : ∀ {R : Type u_2} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f f_1 : StieltjesFunction R),
  f = f_1 →
    ∀ [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
      [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R], f.measure = f_1.measure
-- Mathlib.NumberTheory.Dioph
IsPoly.neg : ∀ {α : Type u_1} {f : (α → ℕ) → ℤ}, IsPoly f → IsPoly (-f)
-- Mathlib.GroupTheory.Commutator.Finite
card_commutatorSet_closureCommutatorRepresentatives : ∀ {G : Type u_1} [inst : Group G],
  Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(commutatorSet G)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.hp : ∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (self : Algebra.Smooth.DescentAux✝ A B) (j : Algebra.Smooth.DescentAux.rels✝ self),
  (MvPolynomial.eval (Algebra.Smooth.DescentAux.P✝ self).relation) (Algebra.Smooth.DescentAux.p✝ self j) =
    (MvPolynomial.aeval (Algebra.Smooth.DescentAux.h✝ self)) ((Algebra.Smooth.DescentAux.P✝ self).relation j)
-- Mathlib.Data.Matrix.Basic
Matrix.map_algebraMap : ∀ {n : Type u_3} {R : Type u_7} {α : Type u_11} {β : Type u_12} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Algebra R α] [inst_6 : Algebra R β]
  (r : R) (f : α → β),
  f 0 = 0 →
    f ((algebraMap R α) r) = (algebraMap R β) r →
      ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_eq_elim' : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M) (a : Option α),
  (Finsupp.optionElim y f) a = Option.elim' y (⇑f) a
-- Mathlib.Topology.Constructions
Pi.continuous_domRestrict₂ : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {s t : Set ι} (hst : s ⊆ t),
  Continuous (Set.domRestrict₂ hst)
-- Lean.Structure
/-- The binder info for the field from the `structure` definition.  -/
Lean.StructureFieldInfo.binderInfo : Lean.StructureFieldInfo → Lean.BinderInfo
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_toLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑e.toLinearEquiv = ⇑e
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.match_16.eq_1 : ∀ (aig : Std.Sat.AIG ℕ) (upper : ℕ) (h : upper < aig.decls.size) (rstate : Std.Sat.AIG.toCNF.State✝ aig)
  (motive : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ rstate out upper h } → Sort u_1)
  (ret : Std.Sat.AIG.toCNF.State✝ aig) (hretstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ rstate ret upper h)
  (h_1 :
    (ret : Std.Sat.AIG.toCNF.State✝ aig) →
      (hretstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ rstate ret upper h) → motive ⟨ret, hretstate⟩),
  (match ⟨ret, hretstate⟩ with
    | ⟨ret, hretstate⟩ => h_1 ret hretstate) =
    h_1 ret hretstate
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y : CategoryTheory.Dial C} →
          (f : X.src ⟶ Y.src) →
            (F : X.src ⨯ Y.tgt ⟶ X.tgt) →
              (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj
                    X.rel ≤
                  (CategoryTheory.Subobject.pullback
                        (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
                    Y.rel →
                X.Hom Y
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_const_sub_iff`. -/
Sbtw.const_sub : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R x y z → Sbtw R (v - x) (v - y) (v - z)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.revMatchesAt_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt c pos ↔ ∃ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ = c
-- Mathlib.Algebra.Order.Floor.Defs
/-- A version of `Nat.strictMono_cast` for floor semirings, whose addition is not necessarily
monotone.  -/
FloorSemiring.natCast_strictMono : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [FloorSemiring α], StrictMono Nat.cast
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_order_eq_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R},
  x.coeff x.order = 0 ↔ x = 0
-- Mathlib.Topology.Compactness.SigmaCompact
compactCovering_subset : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] ⦃m n : ℕ⦄,
  m ≤ n → compactCovering X m ⊆ compactCovering X n
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightHom_toLinearMap : ∀ {ι : 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} (g : P.Aut),
  ↑((RootPairing.Equiv.weightHom P) g) = (RootPairing.Hom.weightHom P) ↑g
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddAssocClass'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddAssocClass α β γ], VAddAssocClass (Set α) (Set β) (Set γ)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure.eq_1 : ∀ {A : Type u_1} [inst : Semiring A] (p : Polynomial A) (v : A →+* ℂ),
  p.mapMahlerMeasure v = (Polynomial.map v p).mahlerMeasure
-- Mathlib.Algebra.Quaternion
Quaternion.imK_sub : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a - b).imK = a.imK - b.imK
-- Mathlib.Data.Set.NAry
Set.forall_mem_image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop},
  (∀ z ∈ Set.image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.HasNoLoop.not_rel_self : ∀ {ι : Type u_1} {c : ComplexShape ι} [self : c.HasNoLoop] (i : ι), ¬c.Rel i i
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` is a nontrivial multiplicative character on a finite field `F`,
then `J(χ,χ⁻¹) = -χ(-1)`.  -/
jacobiSum_nontrivial_inv : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : Fintype F] [inst_2 : CommRing R] [IsDomain R]
  {χ : MulChar F R}, χ ≠ 1 → jacobiSum χ χ⁻¹ = -χ (-1)
-- Mathlib.Analysis.Analytic.Basic
AnalyticAt.comp_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  AnalyticAt 𝕜 f x → ∀ (y : E), AnalyticAt 𝕜 (fun z => f (z - y)) (x + y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  m.WF → ((Std.DHashMap.Raw.filterMap f m).size = m.size ↔ ∀ (a : α) (h : a ∈ m), (f a (m.get a h)).isSome = true)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLEι_app : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  t.IsLE X n ↔ CategoryTheory.IsIso ((t.truncLEι n).app X)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Data.Set.Basic
Set.mem_dite_univ_right : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : p → Set α) (x : α),
  (x ∈ if h : p then t h else Set.univ) ↔ ∀ (h : p), x ∈ t h
-- Mathlib.Data.Fintype.Sigma
Sigma.instFintype : {ι : Type u_1} → {κ : ι → Type u_3} → [(i : ι) → Fintype (κ i)] → [Fintype ι] → Fintype ((i : ι) × κ i)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_bool : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : Bool → α),
  ∑' (i : Bool), f i = f false + f true
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ]
  (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) (l : Γ → σ → Λ) (v : σ) (T : Turing.Tape Γ)
  (h_1 :
    (d : Turing.Dir) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T)
  (h_2 :
    (a : Γ → σ → Γ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T)
  (h_3 :
    (s : Γ → σ → σ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T)
  (h_4 :
    (p : Γ → σ → Bool) →
      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T)
  (h_6 : (v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T),
  (match Turing.TM1.Stmt.goto l, v, T with
    | Turing.TM1.Stmt.move d q, v, T => h_1 d q v T
    | Turing.TM1.Stmt.write a q, v, T => h_2 a q v T
    | Turing.TM1.Stmt.load s q, v, T => h_3 s q v T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T => h_4 p q₁ q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => h_5 l v T
    | Turing.TM1.Stmt.halt, v, T => h_6 v T) =
    h_5 l v T
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_apply_le_of_forall_enorm_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {s : Set X} {m : MeasureTheory.Measure X},
  MeasurableSet s → (∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E) → μ.variation s ≤ m s
-- Qq.MatchImpl
Qq.Impl.mkLet' : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_neg : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ) (a : R), (SkewPolynomial.monomial n) (-a) = -(SkewPolynomial.monomial n) a
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coeAddHom.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : AddMonoid M] (l : Filter α),
  Filter.Germ.coeAddHom l = { toFun := Filter.Germ.ofFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.lintegral_strict_mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  μ ≠ 0 →
    AEMeasurable g μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → (∀ᵐ (x : α) ∂μ, f x < g x) → ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M) (x : C), S.ι.app x = MonCat.ofHom (S.obj x).subtype
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_induction : ∀ {α : Type u_3} [inst : AddMonoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise AddCommute) (p : α → Prop),
  (∀ (a b : α), p a → p b → p (a + b)) → p 0 → (∀ x ∈ s, p x) → p (s.noncommSum comm)
-- Mathlib.Algebra.Group.Basic
eq_neg_add_of_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, b + a = c → a = -b + c
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f f_1 : R.complex.X n ⟶ Y) (e_f : f = f_1) (m m_1 : ℕ) (e_m : m = m_1) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0), R.extMk f m hm hf = R.extMk f_1 m_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Commute.Defs
Commute.mul_inv_cancel : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a * b * a⁻¹ = b
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.mk : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α Unit → Lean.PersistentHashSet α
-- Mathlib.Computability.Partrec
Nat.Partrec.of_eq : ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → (∀ (n : ℕ), f n = g n) → Nat.Partrec g
-- Aesop.Forward.State
/-- Inserts a match associated with slot `slot` and instantiation `inst`.
The match's level must be `slot`. Returns `true` if the match was not previously
associated with `slot` and `inst`.  -/
Aesop.InstMap.insertMatchCore : Aesop.InstMap → Aesop.SlotIndex → Lean.Expr → Aesop.Match → Lean.MetaM (Aesop.InstMap × Bool)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂)[k] = t₁[k]
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd T.hom R.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom R.hom) h
-- Init.Grind.ToInt
Lean.Grind.toIntUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Category.Basic
/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
`Mono g` as explicit arguments. For a version taking them as typeclass arguments, see `mono_comp`.
 -/
CategoryTheory.mono_comp' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y},
  CategoryTheory.Mono g → CategoryTheory.Mono f → CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (app a) (G.map f) ≅
                      CategoryTheory.CategoryStruct.comp (F.map f) (app b)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (naturality f).hom
                        (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η))
                        (naturality g).hom)
                  CategoryTheory.Lax.StrongTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
                          (naturality (CategoryTheory.CategoryStruct.id a)).hom =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).inv
                            (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))))
                    CategoryTheory.Lax.StrongTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
                            (naturality (CategoryTheory.CategoryStruct.comp f g)).hom =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv
                                    (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)))))))
                      CategoryTheory.Lax.StrongTrans.naturality_comp._autoParam →
                    CategoryTheory.Lax.StrongTrans F G
-- Mathlib.Logic.Equiv.Defs
Equiv.cast.congr_simp : ∀ {α β : Sort u_1} (h : α = β), Equiv.cast h = Equiv.cast h
-- Mathlib.Algebra.Group.ULift
ULift.pow_down : ∀ {α : Type u} {β : Type v} [inst : Pow α β] (a : ULift.{w, u} α) (b : β), (a ^ b).down = a.down ^ b
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.isoMk_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (f : F X ≅ F Y),
  (CategoryTheory.InducedCategory.isoMk f).hom = CategoryTheory.InducedCategory.homMk f.hom
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The application of continuous functions as a continuous function.  -/
OmegaCompletePartialOrder.ContinuousHom.Prod.apply : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → (α →𝒄 β) × α →𝒄 β
-- Mathlib.Data.List.Map2
List.zipRight'_nil_right : ∀ {α : Type u} {β : Type v} (as : List α), as.zipRight' [] = ([], as)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- Coercion to a function as a `LinearMap`.  -/
ContMDiffMap.coeFnLinearMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {V : Type u_10} →
                          [inst_6 : NormedAddCommGroup V] →
                            [inst_7 : NormedSpace 𝕜 V] → ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n →ₗ[𝕜] N → V
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.comulAlgHom_def : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A] [inst_5 : Bialgebra R B] [inst_6 : Algebra R A]
  [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A],
  Bialgebra.comulAlgHom S (TensorProduct R A B) =
    (↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
      (Algebra.TensorProduct.map (Bialgebra.comulAlgHom S A) (Bialgebra.comulAlgHom R B))
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourier_add : ∀ {d : Type u_1} [inst : Fintype d] {n : d → ℤ} {x : UnitAddTorus d} {m : d → ℤ},
  (UnitAddTorus.mFourier (m + n)) x = (UnitAddTorus.mFourier m) x * (UnitAddTorus.mFourier n) x
-- Init.Data.Rat.Lemmas
Rat.natCast_ofNat : ∀ {a : ℕ}, ↑(OfNat.ofNat a) = OfNat.ofNat a
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_eq_toMatrix_constr : ∀ {ι : Type u_1} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : Module.Basis ι R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (v : ι → M),
  e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ℕ) v)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Y' Z : C)
  [inst_2 : CategoryTheory.ExactPairing Y Y'],
  CategoryTheory.tensorRightHomEquiv X Y Y' Z =
    {
      toFun := fun f =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (η_ Y Y'))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Y').inv
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y'))),
      invFun := fun f =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z Y' Y).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (ε_ Y Y'))
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom)),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The identity homomorphism for an Eilenberg–Moore coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.Hom.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {G : CategoryTheory.Comonad C} → (A : G.Coalgebra) → A.Hom A
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.synthPendingImp : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Polynomial.cardPowDegree.eq_1 : ∀ {Fq : Type u_1} [inst : Field Fq] [inst_1 : Fintype Fq],
  Polynomial.cardPowDegree =
    { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree, map_mul' := ⋯, nonneg' := ⋯,
      eq_zero' := ⋯, add_le' := ⋯ }