mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)],
  HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjIso φ H =
    (HomologicalComplex.Hom.isoOfComponents
        (fun i => (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H i).symm) ⋯).symm
-- Lean.Parser.Extra
Lean.Parser.ppDedent.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularFormClass.qExpansion_coeff_eq_intervalIntegral : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [ModularFormClass F Γ k],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (n : ℕ) {t : ℝ} (ht : 0 < t),
        (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) =
          1 / ↑h *
            ∫ (u : ℝ) in 0..h,
              1 / Function.Periodic.qParam h (↑u + ↑t * Complex.I) ^ n *
                f { coe := ↑u + ↑t * Complex.I, coe_im_pos := ⋯ }
-- Lean.Util.Trace
Lean.instMonadAlwaysExceptEIO : {ε : Type} → Lean.MonadAlwaysExcept ε (EIO ε)
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.limsSup_eq_iInf_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
  f.HasBasis p s → f.limsSup = ⨅ i, ⨅ (_ : p i), sSup (s i)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.getElem_toList_eq : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.least?.bind (Std.PRange.succMany? i)).get ⋯
-- Mathlib.Algebra.Group.Units.Defs
isAddUnit_of_add_isAddUnit_left : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {x y : M}, IsAddUnit (x + y) → IsAddUnit x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getD_eq_getDₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : β),
  Std.DTreeMap.Internal.Impl.Const.getD l k fallback = Std.DTreeMap.Internal.Impl.Const.getDₘ l k fallback
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalence_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂),
  (HomologicalComplex₂.flipEquivalence C c₁ c₂).functor = HomologicalComplex₂.flipFunctor C c₁ c₂
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.submodule_linearEquiv_fun : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  {m : Submodule R M} [Module.Finite R ↥m] [Nontrivial ↥m],
  IsIsotypic R ↥m → ∃ n, ∃ (_ : NeZero n), ∃ S ≤ m, IsSimpleModule R ↥S ∧ Nonempty (↥m ≃ₗ[R] Fin n → ↥S)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instAddHom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → Add (A ⟶ B)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictDerivAt.cpow_const : ∀ {f : ℂ → ℂ} {f' x c : ℂ},
  HasStrictDerivAt f f' x → f x ∈ Complex.slitPlane → HasStrictDerivAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') x
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinderEvents_le_pi : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι},
  MeasureTheory.cylinderEvents Δ ≤ MeasurableSpace.pi
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_smul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {S : Type u_3}
  [inst_9 : SMul S R] [ContinuousConstSMul S R] [inst_11 : SMulZeroClass S A] [IsScalarTower S R A]
  [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_smul._auto_1 → cfc (fun x => s • f x) a = s • cfc f a
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.aemeasurable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasurableSpace E] (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  AEMeasurable (⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.ofIso`.

---

Being a subobject classifier is preserved under isomorphism.  -/
CategoryTheory.Classifier.ofIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒞 : CategoryTheory.Subobject.Classifier C) →
      {Ω₀ Ω : C} →
        (eΩ : 𝒞.Ω ≅ Ω) →
          (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) →
            ((C_1 : C) → C_1 ⟶ Ω₀) →
              (t : Ω₀ ⟶ Ω) →
                autoParam
                    (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
                    CategoryTheory.Subobject.Classifier.ofIso._auto_1 →
                  CategoryTheory.Subobject.Classifier C
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofSym.congr_simp : ∀ {n : ℕ} {σ : Type u_1} (s s_1 : Sym σ n),
  s = s_1 → ∀ {inst : DecidableEq σ} [inst_1 : DecidableEq σ], Nat.Partition.ofSym s = Nat.Partition.ofSym s_1
-- Init.Data.Array.Lemmas
Array.getElem_replace : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a b : α} {xs : Array α} {i : ℕ} (h : i < xs.size),
  (xs.replace a b)[i] = if (xs[i] == a) = true then if a ∈ xs.take i then a else b else xs[i]
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.unitOfList l cmp) k =
    if l.contains k = true then some () else none
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.sub : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x y : S},
  f.IsIntegralElem x → f.IsIntegralElem y → f.IsIntegralElem (x - y)
-- Lean.CoreM
Lean.catchInternalId : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] → [MonadExcept Lean.Exception m] → Lean.InternalExceptionId → m α → (Lean.Exception → m α) → m α
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecomposition_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α β : Type} [inst_3 : Finite α] [inst_4 : Finite β] {f : α → ι} {g : β → ι}
  (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι) (j : ↑(g ⁻¹' {i})) (k : ↑(f ⁻¹' {i})),
  o.matrixDecomposition z i j k =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j)
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.replaceHead.match_1.splitter : {ι : Type u_2} →
  {M : ι → Type u_1} →
    [inst : (i : ι) → Monoid (M i)] →
      (motive : (x x_1 : ι) → (x_2 : M x) → x_2 ≠ 1 → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) →
        (x x_1 : ι) →
          (x_2 : M x) →
            (x_3 : x_2 ≠ 1) →
              (x_4 : Monoid.CoprodI.NeWord M x x_1) →
                ((x : ι) →
                    (x_5 : M x) →
                      (h : x_5 ≠ 1) →
                        (x_6 : M x) → (a : x_6 ≠ 1) → motive x x x_5 h (Monoid.CoprodI.NeWord.singleton x_6 a)) →
                  ((x x_5 : ι) →
                      (x_6 : M x) →
                        (h : x_6 ≠ 1) →
                          (j k : ι) →
                            (w₁ : Monoid.CoprodI.NeWord M x j) →
                              (hne : j ≠ k) →
                                (w₂ : Monoid.CoprodI.NeWord M k x_5) → motive x x_5 x_6 h (w₁.append hne w₂)) →
                    motive x x_1 x_2 x_3 x_4
-- Mathlib.Data.ENNReal.Basic
/-- **Alias** of the reverse direction of `ENNReal.coe_lt_coe`. -/
ENNReal.coe_lt_coe_of_lt : ∀ {r q : NNReal}, r < q → ↑r < ↑q
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- **Alias** of `MeasureTheory.ae_tendsto_ofReal_norm`. -/
MeasureTheory.all_ae_tendsto_ofReal_norm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {f : α → β},
  (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
    ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => ENNReal.ofReal ‖F n a‖) Filter.atTop (nhds (ENNReal.ofReal ‖f a‖))
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.eval_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : C} (η : f ⟶ g),
  η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f).hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl g).hom)
-- Mathlib.Data.Sym.Sym2
Sym2.ball : ∀ {α : Type u_1} {p : α → Prop} {a b : α}, (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b
-- Init.Data.Float.Model.Float
/-- Converts an `Int16` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofInt16 : Int16 → Float.Model
-- Mathlib.Algebra.Group.Defs
AddRightCancelSemigroup.toAddSemigroup : {G : Type u} → [self : AddRightCancelSemigroup G] → AddSemigroup G
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_1.go : {motive_1 : Lean.Widget.MsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u} →
    {motive_3 :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
          (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) →
            ((t : Lean.Widget.MsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
                        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                    Lean.Widget.MsgEmbed.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                      Lean.Widget.MsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                        Lean.Widget.MsgEmbed.below_4 t → motive_5 t) →
                      motive_2 t ×' Lean.Widget.MsgEmbed.below_1 t
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioc_pred_left_eq_Icc_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Finset.Ioc (Order.pred a) b = Finset.Icc a b
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If `f` is `C^n` then its `m`-times iterated derivative is continuous for `m ≤ n`.  -/
ContDiff.continuous_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {m : ℕ}, ↑m ≤ n → ContDiff 𝕜 n f → Continuous fun x => iteratedFDeriv 𝕜 m f x
-- Mathlib.Computability.Primrec.Basic
Primrec.option_bind : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → Option β} {g : α → β → Option σ}, Primrec f → Primrec₂ g → Primrec fun a => (f a).bind (g a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.inter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (m₁ m₁_1 : Std.DTreeMap.Internal.Impl α β) (e_m₁ : m₁ = m₁_1)
  (m₂ m₂_1 : Std.DTreeMap.Internal.Impl α β), m₂ = m₂_1 → ∀ (h₁ : m₁.Balanced), m₁.inter m₂ h₁ = m₁_1.inter m₂_1 ⋯
-- Mathlib.Algebra.Module.Opposite
/-- `MulOpposite.distribMulAction` extends to a `Module`  -/
MulOpposite.instModule : (R : Type u) → {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Module R Mᵐᵒᵖ
-- Mathlib.Algebra.Opposites
AddOpposite.unop_div : ∀ {α : Type u_1} [inst : Div α] (a b : αᵃᵒᵖ), AddOpposite.unop (a / b) = AddOpposite.unop a / AddOpposite.unop b
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_gt_three : 3 < Real.pi
-- Lean.Parser.Types
Lean.Parser.FirstTokens.unknown.sizeOf_spec : sizeOf Lean.Parser.FirstTokens.unknown = 1
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.sdiff_of_isUpperSet : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsLowerSet s → IsUpperSet t → IsLowerSet (s \ t)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.mem_gt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o : WithTop α} {x : α},
  t.Bounded (↑x) o → Ordnode.All (fun x_1 => x_1 > x) t
-- Init.Grind.Config
/-- When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
 -/
Lean.Grind.Config.lia : Lean.Grind.Config → Bool
-- Init.Data.Repr
/-- Converts a natural number to the list of Unicode subscript digit characters that corresponds to
its decimal representation.

Examples:
 * `Nat.toSubDigits 0 = ['₀']`
 * `Nat.toSubDigits 35 = ['₃', '₅']`
 -/
Nat.toSubDigits : ℕ → List Char
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.logDeriv_eta_eq_E2 : ∀ (z : UpperHalfPlane), logDeriv ModularForm.eta ↑z = ↑Real.pi * Complex.I / 12 * EisensteinSeries.E2 z
-- Batteries.Lean.Meta.UnusedNames
Lean.Name.MatchUpToIndexSuffix.noMatch.sizeOf_spec : sizeOf Lean.Name.MatchUpToIndexSuffix.noMatch = 1
-- Init.Conv
/-- Focuses, converts the `conv` goal `⊢ lhs` into a regular goal `⊢ lhs = rhs`, and then executes the given tactic block.  -/
Lean.Parser.Tactic.Conv.nestedTactic : Lean.ParserDescr
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso_eq_refl : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {v : Valuation R Γ₀}
  (h : v.IsEquiv v), h.orderMonoidIso = OrderMonoidIso.refl (MonoidWithZeroHom.ofClass v).ValueGroup₀
-- Mathlib.Computability.Partrec
Primrec.to_comp : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ}, Primrec f → Computable f
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPatternCnstr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.ulift_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  (RingHom.ulift.{u₁, u₂, u_1, u_2} f).Flat ↔ f.Flat
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialEvalσ.eq_2 : ∀ (j b : ℕ) (l : List ℕ),
  SimplexCategoryGenRel.simplicialEvalσ (b :: l) j =
    if b < SimplexCategoryGenRel.simplicialEvalσ l j then SimplexCategoryGenRel.simplicialEvalσ l j - 1
    else SimplexCategoryGenRel.simplicialEvalσ l j
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} (pf pf_1 : Q(«$s» = ∅)),
  (Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty pf = Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty pf_1) =
    (pf = pf_1)
-- Mathlib.Tactic.NormNum.Result
/-- Untyped version of `Result.isBool`.  -/
Mathlib.Meta.NormNum.Result'.isBool : Bool → Lean.Expr → Mathlib.Meta.NormNum.Result'
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.mk.injEq : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (toSolution' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  (hab :
    (hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ toSolution' + FermatLastTheoremForThreeGen.Solution'.b✝ toSolution')
  (toSolution'_1 : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  (hab_1 :
    (hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ toSolution'_1 +
        FermatLastTheoremForThreeGen.Solution'.b✝ toSolution'_1),
  ({ toSolution' := toSolution', hab := hab } = { toSolution' := toSolution'_1, hab := hab_1 }) =
    (toSolution' = toSolution'_1)
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_or : ∀ (a b : UInt8), (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRing.default : Lean.Meta.Grind.Arith.CommRing.CommRing
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.tendsto_measure_Ioc_atBot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : Preorder α] [NoMinOrder α] [Filter.atBot.IsCountablyGenerated]
  (μ : MeasureTheory.Measure α) (a : α), Filter.Tendsto (fun x => μ (Set.Ioc x a)) Filter.atBot (nhds (μ (Set.Iic a)))
-- Init.Data.List.Pairwise
List.nodup_iff_count : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α}, l.Nodup ↔ ∀ (a : α), List.count a l ≤ 1
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ediam_preimage_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X]
  (s : Set (Metric.Snowflaking X α hα₀ hα₁)),
  Metric.ediam (⇑Metric.Snowflaking.toSnowflaking ⁻¹' s) = Metric.ediam s ^ α⁻¹
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_hom_left_snd_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) S.hom))
        (CategoryTheory.Limits.pullback.snd S.hom T.hom)) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Eta-expanded form of `Meromorphic.logDeriv_prod_eventuallyEq`

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of `𝕜`, the
logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic
derivatives.
 -/
Meromorphic.logDeriv_fun_prod_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ i ∈ s, Meromorphic (F i)) →
    (∀ i ∈ s, ∀ (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) →
      (logDeriv fun a => ∏ c ∈ s, F c a) =ᶠ[Filter.codiscrete 𝕜] fun a => ∑ c ∈ s, logDeriv (F c) a
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.snd.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCone.snd φ =
    CochainComplex.HomComplex.Cochain.ofHoms (HomologicalComplex.homotopyCofiber.sndX φ)
-- Init.Data.Nat.Lcm
Nat.lcm_lcm_self_right_left : ∀ (m n : ℕ), m.lcm (m.lcm n) = m.lcm n
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.modify.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f : β a → β a) (a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.modify a f (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if h : (a_1 == a) = true then
      have h' := ⋯;
      have b := f (cast ⋯ b);
      Std.DHashMap.Internal.AssocList.cons a b es
    else Std.DHashMap.Internal.AssocList.cons a_1 b (Std.DHashMap.Internal.AssocList.modify a f es)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isBoundary₀_of_mem_coinvariantsKer : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ x ∈ Representation.Coinvariants.ker (Representation.ofDistribMulAction k G A), groupHomology.IsBoundary₀ G x
-- Mathlib.Logic.Equiv.Set
/-- The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `Set S`.  -/
Equiv.Set.powerset : {α : Type u_3} → (S : Set α) → ↑(𝒫 S) ≃ Set ↑S
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ)
  {X Y : (Φ.op.RightResolution X₂)ᵒᵖ} (φ : X ⟶ Y),
  ((CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).map φ).f = φ.unop.f.unop
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eraseLead : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead.support.card = f.support.card - 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.category_comp_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {X Y Z : CategoryTheory.Limits.BinaryBicone P Q} (f : CategoryTheory.Limits.BinaryBiconeMorphism X Y)
  (g : CategoryTheory.Limits.BinaryBiconeMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- Given a π-system, if a sequence of measures converges along all elements of the π-system, then
it also converges along finite unions of elements of the π-system.  -/
IsPiSystem.tendsto_measureReal_biUnion : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Ω] {S : Set (Set Ω)},
  IsPiSystem S →
    ∀ {μ : ι → MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} {l : Filter ι} {t : Finset (Set Ω)},
      (∀ s ∈ t, s ∈ S) →
        (∀ s ∈ S, MeasurableSet s) →
          (∀ s ∈ S, Filter.Tendsto (fun i => (μ i).real s) l (nhds (ν.real s))) →
            autoParam (∀ s ∈ S, ν s ≠ ⊤) IsPiSystem.tendsto_measureReal_biUnion._auto_1 →
              autoParam (∀ s ∈ S, ∀ (i : ι), (μ i) s ≠ ⊤) IsPiSystem.tendsto_measureReal_biUnion._auto_3 →
                Filter.Tendsto (fun i => (μ i).real (⋃ s ∈ t, s)) l (nhds (ν.real (⋃ s ∈ t, s)))
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instIsOrderedAddMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : Preorder β] [IsOrderedAddMonoid β], IsOrderedAddMonoid (α × β)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier : ∀ (X : FinBoolAlg), ↑(CategoryTheory.HasForget₂.forget₂.obj X).toPartOrd = ↑X.toBoolAlg
-- Init.ByCases
/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`.  -/
dite_eq_ite : ∀ {P : Prop} {α : Sort u_1} {a b : α} [inst : Decidable P], (if x : P then a else b) = if P then a else b