mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.Config.mk.sizeOf_spec : ∀ (trace : Bool) (target : Lean.Name) (doc : Option (Lean.TSyntax `Lean.Parser.Command.docComment))
  (allowAutoName : Bool) (reorder? : Option Mathlib.Tactic.Translate.ArgReorder)
  (relevantArg? : Option Mathlib.Tactic.Translate.RelevantArg) (attrs : Array Lean.Syntax) (dontTranslate : List ℕ)
  (ref : Lean.Syntax) (existing self none : Bool) (rename : Lean.NameMap Lean.Name),
  sizeOf
      { trace := trace, target := target, doc := doc, allowAutoName := allowAutoName, reorder? := reorder?,
        relevantArg? := relevantArg?, attrs := attrs, dontTranslate := dontTranslate, ref := ref, existing := existing,
        self := self, none := none, rename := rename } =
    1 + sizeOf trace + sizeOf target + sizeOf doc + sizeOf allowAutoName + sizeOf reorder? + sizeOf relevantArg? +
                  sizeOf attrs +
                sizeOf dontTranslate +
              sizeOf ref +
            sizeOf existing +
          sizeOf self +
        sizeOf none +
      sizeOf rename
-- Mathlib.Computability.TuringMachine.Config
/-- `pred` returns the predecessor of the head of the input:
`pred [] = [0]`, `pred (0 :: v) = [0]`, `pred (n+1 :: v) = [n]`.  -/
Turing.ToPartrec.Code.pred : Turing.ToPartrec.Code
-- Lean.Compiler.IR.Basic
Lean.IR.Decl : Type
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `true` if `x` has been eliminated using an equality constraint.  -/
Lean.Meta.Grind.Arith.Cutsat.eliminated : Int.Internal.Linear.Var → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Data.Set.MulAntidiagonal
Set.antidiagonal.eq_1 : ∀ {α : Type u_1} [inst : Add α] (s t : Set α) (a : α), s.antidiagonal t a = {x | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a}
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupSeminormClass.toSeminormedAddGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddGroup α] [inst_2 : AddGroupSeminormClass F α ℝ]
  (f : F),
  AddGroupSeminormClass.toSeminormedAddGroup f =
    { norm := ⇑f, toAddGroup := inst_1, dist := fun x y => f (-x + y), dist_self := ⋯, dist_comm := ⋯,
      dist_triangle := ⋯, edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.isLeftAdjoint_post : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasPullbacks C] {F : CategoryTheory.Functor C D}
  [F.IsLeftAdjoint], (CategoryTheory.Over.post F).IsLeftAdjoint
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.preservesTerminalIso_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {R S : C}
  (f : R ⟶ S),
  CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (CategoryTheory.Over.pullback f) =
    CategoryTheory.Over.isoMk
      (CategoryTheory.asIso (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id S) f)) ⋯
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.instMonoidWithZeroHomClassReal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], MonoidWithZeroHomClass (NumberField.FinitePlace K) K ℝ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec.injEq : ∀ (h h_1 : Lean.FVarId),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec h = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec h_1) = (h = h_1)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«builder_option(Pattern:=_)» : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Basic
Function.update_comp_equiv : ∀ {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [inst : DecidableEq α'] [inst_1 : DecidableEq α] (f : α → β)
  (g : α' ≃ α) (a : α) (v : β), Function.update f a v ∘ ⇑g = Function.update (f ∘ ⇑g) (g.symm a) v
-- Mathlib.Topology.NhdsWithin
nhdsWithin_eq_map_subtype_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s),
  nhdsWithin a s = Filter.map Subtype.val (nhds ⟨a, h⟩)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {z : ℤ} {a : R},
  ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z
-- Std.Data.ExtHashMap.Basic
/-- The notation `m[a]?` is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
Std.ExtHashMap.get? : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → Option β
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.equivOfEq_apply : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] {S T : IntermediateField F E}
  (h : S = T) (x : ↥S.toSubalgebra), (IntermediateField.equivOfEq h) x = ⟨↑x, ⋯⟩
-- Mathlib.MeasureTheory.Group.Arithmetic
List.aemeasurable_fun_prod : ∀ {M : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : List (α → M)),
  (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable (fun x => (List.map (fun f => f x) l).prod) μ
-- Mathlib.Data.Finset.Dedup
List.mem_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α}, a ∈ l.toFinset ↔ a ∈ l
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
/-- **Integration by parts for Fréchet derivatives**
Version with two scalar functions: `∫ f * g' = - ∫ f' * g` when `f * g'` and `f' * g` and `f * g`
are integrable, where `f'` and `g'` are the derivatives of `f` and `g` in a given direction `v`.  -/
integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {𝕜 : Type u_5}
  [inst_6 : NormedField 𝕜] [inst_7 : NormedAlgebra ℝ 𝕜] {f g : E → 𝕜} {v : E},
  MeasureTheory.Integrable (fun x => (fderiv ℝ f x) v * g x) μ →
    MeasureTheory.Integrable (fun x => f x * (fderiv ℝ g x) v) μ →
      MeasureTheory.Integrable (fun x => f x * g x) μ →
        (∀ x ∈ tsupport g, DifferentiableAt ℝ f x) →
          (∀ x ∈ tsupport f, DifferentiableAt ℝ g x) →
            ∫ (x : E), f x * (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v * g x ∂μ
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.baseChange.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.PreSubmersivePresentation R S ι σ),
  Algebra.PreSubmersivePresentation.baseChange T P =
    { toPresentation := Algebra.Presentation.baseChange T P.toPresentation, map := P.map, map_inj := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.cout : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput old) → self.aig.Ref
-- Init.Data.UInt.Bitwise
UInt32.or_assoc : ∀ (a b c : UInt32), a ||| b ||| c = a ||| (b ||| c)
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.neg_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0), -R.extMk f m hm hf = R.extMk (-f) m hm ⋯
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.ext_iff : ∀ {F : Type u_1} [inst : Field F] {p : Polynomial F} {σ τ : p.Gal}, σ = τ ↔ ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.mul_sSup : ∀ (o : Ordinal.{u_1}) (s : Set Ordinal.{u_1}), o * sSup s = sSup ((fun x => o * x) '' s)
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt8HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`.  -/
CategoryTheory.Functor.splitEpiEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f : X ⟶ Y) → [F.Full] → [F.Faithful] → CategoryTheory.SplitEpi f ≃ CategoryTheory.SplitEpi (F.map f)
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_eq_bot_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} {J : Ideal S},
  I.prod J = ⊥ ↔ I = ⊥ ∧ J = ⊥
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_zero_left : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (y : M), QuadraticMap.polar (⇑Q) 0 y = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t.contains a = (t.getKey? a).isSome
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  k ∈ Std.ExtHashMap.filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') m[k] = true
-- Mathlib.CategoryTheory.Functor.FunctorHom
_private.Mathlib.CategoryTheory.Functor.FunctorHom.0.CategoryTheory.Functor.homObjEquiv.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    (F A : CategoryTheory.Functor C (Type u_2)) →
      (X : C) →
        (motive : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X → Sort u_4) →
          (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X) →
            ((x : F.obj X) → (y : A.obj X) → motive (x, y)) → motive x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx.induct_unfolding : ∀ {α : Type u} {β : α → Type v}
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → (n : ℕ) → n < t.size → α → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
      (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
      (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.lt),
      motive l' ⋯ n ⋯ (l'.keyAtIdx ⋯ n ⋯) →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (l'.keyAtIdx ⋯ n ⋯)) →
    (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
        (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
        (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
        compare n l'.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h k) →
      (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
          (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
          (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.gt),
          motive r' ⋯ (n - l'.size - 1) ⋯ (r'.keyAtIdx ⋯ (n - l'.size - 1) ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (r'.keyAtIdx ⋯ (n - l'.size - 1) ⋯)) →
        ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced) (n : ℕ) (h : n < t.size),
          motive t hl n h (t.keyAtIdx hl n h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a fallback : α} {v : β k},
  (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0.sizeOf_spec : ∀ (a zero : Lean.Expr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 a zero) = 1 + sizeOf a + sizeOf zero
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
_private.Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula.0.termΔ : Lean.ParserDescr
-- Mathlib.NumberTheory.WellApproximable
approxAddOrderOf.eq_1 : ∀ (A : Type u_1) [inst : SeminormedAddGroup A] (n : ℕ) (δ : ℝ),
  approxAddOrderOf A n δ = Metric.thickening δ {y | addOrderOf y = n}
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_zero_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] [inst_1 : Zero α] (i : m),
  Matrix.updateRow 0 i 0 = 0
-- Mathlib.Algebra.Algebra.Operations
/-- Dependent version of `Submodule.pow_induction_on_right`.  -/
Submodule.pow_induction_on_right' : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop},
  (∀ (r : R), C 0 ((algebraMap R A) r) ⋯) →
    (∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) →
      (∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯) →
        ∀ {n : ℕ} {x : A} (hx : x ∈ M ^ n), C n x hx
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.topologicalSpace_eq_of_top : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  RestrictedProduct.topologicalSpace R A ⊤ = TopologicalSpace.induced DFunLike.coe inferInstance
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasStrictDerivAt.exp : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') x
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.isInvariant : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_4} {inst : Group G} {inst_1 : CommSemiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra A B} {inst_4 : MulSemiringAction G B} [self : IsGaloisGroup G A B], Algebra.IsInvariant A B G
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instPartialOrder : {ι : Type u_1} → PartialOrder (AbstractSimplicialComplex ι)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulEquivOfOrderOfEq_symm : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g)
  {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g'),
  (mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg ⋯
-- Mathlib.Algebra.Group.Hom.End
AddMonoid.End.instRing : {M : Type uM} → [inst : AddCommGroup M] → Ring (AddMonoid.End M)
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Algebra.finrank_eq_one_iff_bijective_algebraMap : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [Module.Free F E], Module.finrank F E = 1 ↔ Function.Bijective ⇑(algebraMap F E)
-- Std.Data.ExtDHashMap.Basic
/-- Computes the difference of the given hash maps.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtDHashMap.diff : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → Std.ExtDHashMap α β → Std.ExtDHashMap α β
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.tendstoUniformlyOn_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] {g : β → α} [inst_1 : UniformSpace α] {f : ℕ → β → α},
  HasSumUniformly f g → TendstoUniformly (fun x1 x2 => ∑ i ∈ Finset.range x1, f i x2) g Filter.atTop
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_map : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a},
  (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.map f m)).buckets).Perm
    (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.vanishingIdeal_pointToPoint : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  (V : Set (σ → K)), PrimeSpectrum.vanishingIdeal (MvPolynomial.pointToPoint '' V) = MvPolynomial.vanishingIdeal k V
-- Mathlib.Order.Bounds.Image
StrictMono.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictMono f → (f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s)
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.regular.sizeOf_spec : ∀ (result : Aesop.RuleResult), sizeOf (Aesop.SafeRuleResult.regular result) = 1 + sizeOf result
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom_eq_one_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A]
  [IsDedekindDomain B], I ≠ 0 → ((FractionalIdeal.extendedHom L B) I = 1 ↔ I = 1)
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppFnResolutions.toName.go : List Lean.Syntax → Lean.Name
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_eq_zero : ∀ {a n : ℕ}, n.floorRoot a = 0 ↔ n = 0 ∨ a = 0
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_mulRight₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [MeasurableMul G₀] {g : G₀},
  g ≠ 0 → MeasurableEmbedding fun x => x * g
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.instNormedSpaceSmallComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    (hf : Manifold.IsImmersionAtOfComplement F I J n f x) →
                                                      NormedSpace 𝕜 hf.smallComplement
-- Init.PropLemmas
Bool.ite_then_false : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then false else x) = true ↔ ¬p ∧ x = true
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.const_smul : ∀ {𝕜 : 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}
  {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F],
  Differentiable 𝕜 f → ∀ (c : R), Differentiable 𝕜 (c • f)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A]
  [inst_3 : ∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A]
  [inst_4 : CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A),
  CategoryTheory.IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)
-- Mathlib.CategoryTheory.Comma.Basic
/-- If `F` is an equivalence, then so is `preRight L F R`.  -/
CategoryTheory.Comma.isEquivalence_preRight : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) [F.IsEquivalence], (CategoryTheory.Comma.preRight L F R).IsEquivalence
-- Mathlib.Order.Interval.Finset.Basic
Finset.right_mem_uIcc : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ∈ Finset.uIcc a b
-- Mathlib.GroupTheory.OrderOfElement
multiples_eq_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] [Finite G] (x : G), ↑(AddSubmonoid.multiples x) = ↑(AddSubgroup.zmultiples x)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism C).functor =
    HomotopicalAlgebra.BifibrantObject.ιFibrantObject
-- Mathlib.Data.Nat.Digits.Lemmas
List.fixedLengthDigits_one : ∀ {b : ℕ} (hb : 1 < b), List.fixedLengthDigits hb 1 = Finset.image (fun x => [x]) (Finset.range b)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheafHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (α α_1 : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj),
  α = α_1 → CategoryTheory.Functor.IsCoverDense.sheafHom α = CategoryTheory.Functor.IsCoverDense.sheafHom α_1
-- Init.Data.List.Lemmas
List.eq_or_ne_mem_of_mem : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l → a = b ∨ a ≠ b ∧ a ∈ l
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Extension.H1Cotangent.equivOfFormallySmooth_symm : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (P₁ : Algebra.Extension R A) (P₂ : Algebra.Extension R A) [inst_3 : Algebra.FormallySmooth R P₁.Ring]
  [inst_4 : Algebra.FormallySmooth R P₂.Ring],
  (Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂).symm =
    Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₂ P₁
-- Mathlib.Algebra.GroupWithZero.Indicator
/-- If `f` is everywhere nonzero, then `support (f * g) = support g`.  -/
Function.support_mul_of_ne_zero_left : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {f : ι → M₀},
  (∀ (x : ι), f x ≠ 0) → ∀ (g : ι → M₀), (Function.support fun x => f x * g x) = Function.support g