mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.AList
Finsupp.toAList_keys_toFinset : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] (f : α →₀ M),
  f.toAList.keys.toFinset = f.support
-- Mathlib.Algebra.WithConv
/-- Lift a linear equivalence between `A` and `B` to `WithConv A` and `WithConv B`.  -/
WithConv.congrLinearEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : AddCommMonoid A] →
        [inst_1 : Semiring R] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoid B] → [inst_4 : Module R B] → (A ≃ₗ[R] B) → WithConv A ≃ₗ[R] WithConv B
-- Mathlib.CategoryTheory.Equivalence
/-- The composition `inverse ⋙ functor` is isomorphic to the identity.  -/
CategoryTheory.Equivalence.counitIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (self : C ≌ D) → self.inverse.comp self.functor ≅ CategoryTheory.Functor.id D
-- Lean.Meta.Tactic.Delta
/-- Delta expand declarations that satisfy `p` at `mvarId` type.
 -/
Lean.MVarId.deltaTarget : Lean.MVarId → (Lean.Name → Bool) → Lean.MetaM Lean.MVarId
-- Aesop.Script.UScriptToSScript
Aesop.Script.isConsecutiveSequence : Array ℕ → Bool
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.isAlgebraic_adjoin : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {S : Set L},
  (∀ x ∈ S, IsIntegral K x) → Algebra.IsAlgebraic K ↥(IntermediateField.adjoin K S)
-- Mathlib.Control.Random
instMonadLiftTRandGTOfMonadLift : {m : Type u_1 → Type u_2} →
  {n : Type u_1 → Type u_3} → {g : Type} → [MonadLift m n] → MonadLiftT (RandGT g m) (RandGT g n)
-- Mathlib.Order.Filter.Finite
Filter.mem_generate_iff : ∀ {α : Type u} {s : Set (Set α)} {U : Set α}, U ∈ Filter.generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_inv`. -/
Antivary.inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {f : ι → α} {g : ι → β},
  Antivary f g → Antivary f⁻¹ g⁻¹
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.neg_add_cancel_right : ∀ {α : Type u} [inst : AddMonoid α] (a : α) (b : AddUnits α), a + ↑(-b) + ↑b = a
-- Lean.Parser.Term
Lean.Parser.Term.byTactic.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_eq_iSup : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore = ⨆ N, ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N
-- Mathlib.Algebra.DirectSum.AddChar
AddChar.directSum_injective : ∀ {ι : Type u_1} {R : Type u_2} {G : ι → Type u_3} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommGroup (G i)]
  [inst_2 : CommMonoid R], Function.Injective AddChar.directSum
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.addDeclWithoutChecking : Lean.Environment → Lean.Declaration → Except Lean.Kernel.Exception Lean.Environment
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.toFun.eq_1 : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g : L ≃+* L),
  modularCyclotomicCharacter.toFun n g = ↑(modularCyclotomicCharacter.aux g n)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instMonadAutoImplicitsTermElabM : Lean.Elab.MonadAutoImplicits Lean.Elab.TermElabM
-- Init.Data.Vector.Basic
Vector.find? : {n : ℕ} → {α : Type} → (α → Bool) → Vector α n → Option α
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.isUniform_one : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [inst_4 : DecidableRel G.Adj],
  P.IsUniform G 1
-- Init.Data.Order.Lemmas
Std.right_le_max : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderSup α] {a b : α},
  b ≤ a ⊔ b
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.natCast_emod : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] (x : ℕ), ↑(x % p) = ↑x
-- Mathlib.GroupTheory.Coset.Basic
/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
of the quotient map `G → G/K`. The classical version is `AddSubgroup.quotientEquivProdOfLE`.  -/
AddSubgroup.quotientEquivProdOfLE' : {α : Type u_1} →
  [inst : AddGroup α] →
    {s t : AddSubgroup α} →
      s ≤ t → (f : α ⧸ t → α) → Function.RightInverse f QuotientAddGroup.mk → α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- **Kummer's Theorem**

The `p`-adic valuation of `n.choose k` is the number of carries when `k` and `n - k` are added
in base `p`. This sum is expressed over the finset `Ico 1 b` where `b` is any bound greater than
`log p n`.  -/
padicValNat_choose : ∀ {p n k b : ℕ} [hp : Fact (Nat.Prime p)],
  k ≤ n → Nat.log p n < b → padicValNat p (n.choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_le_logb : ∀ {b x y : ℝ}, 1 < b → 0 < x → 0 < y → (Real.logb b x ≤ Real.logb b y ↔ x ≤ y)
-- Mathlib.Algebra.Order.Group.Basic
zpow_lt_zpow_left : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α},
  0 < n → a < b → a ^ n < b ^ n
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.majorTypeArgs : Lean.Meta.Cases.Context → Array Lean.Expr
-- Mathlib.CategoryTheory.SingleObj
Units.toAut_hom : ∀ (M : Type u) [inst : Monoid M] (x : Mˣ), ((Units.toAut M) x).hom = (CategoryTheory.SingleObj.toEnd M) ↑x
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_pi : ∀ {ι : Type u_4} [inst : Fintype ι] {X : ι → Type u_5} [inst_1 : (i : ι) → PseudoMetricSpace (X i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (X i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
  [∀ (i : ι), IsUnifLocDoublingMeasure MeasureTheory.volume], IsUnifLocDoublingMeasure MeasureTheory.volume
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.prodEquiv.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (s : Subsemigroup M) (t : Subsemigroup N),
  s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯ }
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddAction.IsMultiplyPretransitive.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α] (n : ℕ),
  AddAction.IsMultiplyPretransitive G α n = AddAction.IsPretransitive G (Fin n ↪ α)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.symm_image_target_eq_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.symm '' e.target = e.source
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isZPowInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat.inj : ∀ {h : Lean.Expr} {x : Int.Internal.Linear.Var} {e' : Int.Internal.Linear.Expr} {h_1 : Lean.Expr}
  {x_1 : Int.Internal.Linear.Var} {e'_1 : Int.Internal.Linear.Expr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat h x e' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat h_1 x_1 e'_1 →
    h = h_1 ∧ x = x_1 ∧ e' = e'_1
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_xor_distrib_right : ∀ {a b c : ℕ}, (a ^^^ b) &&& c = a &&& c ^^^ b &&& c
-- Mathlib.Data.Vector.Snoc
List.Vector.map_snoc : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {x : α} (xs : List.Vector α n) {f : α → β},
  List.Vector.map f (xs.snoc x) = (List.Vector.map f xs).snoc (f x)
-- Lean.Parser.Types
Lean.Parser.instBEqParserCacheKey.beq : Lean.Parser.ParserCacheKey → Lean.Parser.ParserCacheKey → Bool
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.L_diag_ne_zero : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : LinearOrder m] {n : Type u_2} [inst_2 : LinearOrder n] {R : Type u_3}
  [inst_3 : CommRing R] {A : Matrix m n R} (self : Echelon.Decomposition A) (i : m), self.L.diag i ≠ 0
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} {f g : A ⟶ B},
  f = g ↔ f.hom₁ = g.hom₁ ∧ f.hom₂ = g.hom₂ ∧ f.hom₃ = g.hom₃
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- A special case of the **Matrix determinant lemma** for when `A = I`.  -/
Matrix.det_one_add_replicateCol_mul_replicateRow : ∀ {m : Type u_2} {α : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing α] {ι : Type u_5}
  [inst_3 : Unique ι] (u v : m → α), (1 + Matrix.replicateCol ι u * Matrix.replicateRow ι v).det = 1 + v ⬝ᵥ u
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.UniversallyEffectiveEquivalenceRelation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} →
      {p₁ p₂ : R ⟶ A} →
        (toEffectiveEquivalenceRelation : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂) →
          CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f)
              toEffectiveEquivalenceRelation.π →
            CategoryTheory.UniversallyEffectiveEquivalenceRelation p₁ p₂
-- Mathlib.Topology.QuasiSeparated
IsQuasiSeparated.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α),
  IsQuasiSeparated s =
    ∀ (U V : Set α), U ⊆ s → IsOpen U → IsCompact U → V ⊆ s → IsOpen V → IsCompact V → IsCompact (U ∩ V)
-- Mathlib.Algebra.Group.Prod
Prod.commute_iff : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] {x y : M × N},
  Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_center_iff : ∀ {R : Type u_1} [inst : Ring R] {z : R}, z ∈ Subring.center R ↔ ∀ (g : R), g * z = z * g
-- Init.Data.Nat.Lemmas
Nat.min_right_comm : ∀ (a b c : ℕ), min (min a b) c = min (min a c) b
-- Lean.Parser.Basic
Lean.Parser.takeWhile1Fn : (Char → Bool) → String → Lean.Parser.ParserFn
-- Mathlib.Data.Vector.Basic
List.Vector.get_cons_succ : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n) (i : Fin n), (a ::ᵥ v).get i.succ = v.get i
-- Mathlib.GroupTheory.Index
Subgroup.pow_mem_of_relIndex_ne_zero_of_dvd : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H.relIndex K ≠ 0 → ∀ {a : G}, a ∈ K → ∀ {n : ℕ}, (∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n) → a ^ n ∈ H ⊓ K
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The functor `shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w` for a locally `w`-small category `C`
is fully faithful.  -/
CategoryTheory.fullyFaithfulShrinkYoneda : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.shrinkYoneda.{w, v, u}.FullyFaithful
-- Mathlib.Data.NNReal.Defs
NNReal.inv_mk : ∀ {r : ℝ} (hr : 0 ≤ r), (NNReal.mk r hr)⁻¹ = NNReal.mk r⁻¹ ⋯
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The non-unital subring `R` of the ring `R`.  -/
NonUnitalSubring.instTop : {R : Type u} → [inst : NonUnitalNonAssocRing R] → Top (NonUnitalSubring R)
-- Lean.Parser.Term.Doc
Lean.Parser.Term.Doc.RecommendedSpelling.mk : String → String → Option String → Lean.Parser.Term.Doc.RecommendedSpelling
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.getD t.min! fallback = t.min!
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instInhabitedExtTheorem.default : Lean.Meta.Ext.ExtTheorem
-- Mathlib.Topology.Category.Compactum
Compactum.instFunLikeHomA : {X Y : Compactum} → FunLike (X ⟶ Y) X.A Y.A
-- Mathlib.Data.List.Pi
List.Pi.cons_eta : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {i : ι} {l : List ι} (f : (j : ι) → j ∈ i :: l → α j),
  List.Pi.cons i l (List.Pi.head f) (List.Pi.tail f) = f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_ind : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  {motive : Std.DHashMap.Internal.Raw₀ α β → Prop} (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a), motive m → motive (m.insert a b)) →
      motive ↑(m.insertMany l)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.prod_finset_product : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (r : Finset (γ × α)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) → ∀ {f : γ × α → β}, ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_sub_sq_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner ℝ x y + ‖y‖ ^ 2
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.newBasis.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.house.newBasis✝ K = NumberField.house.newBasis✝ K
-- Init.Data.List.Impl
List.findSome?_append : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs ys : List α},
  List.findSome? f (xs ++ ys) = (List.findSome? f xs).or (List.findSome? f ys)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffOn_prod_iff : ∀ {𝕜 : 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'] {F' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {s : Set M} {n : WithTop ℕ∞} (f : M → M' × N'),
  ContMDiffOn I (I'.prod J') n f s ↔ ContMDiffOn I I' n (Prod.fst ∘ f) s ∧ ContMDiffOn I J' n (Prod.snd ∘ f) s
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C}
  (m m' : CategoryTheory.Subobject B), m ⊓ m' = (CategoryTheory.Subobject.inf.obj m).obj m'
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The Mahler measure of a polynomial is bounded above by the sum of the norms of its coefficients.
 -/
Polynomial.mahlerMeasure_le_sum_norm_coeff : ∀ (p : Polynomial ℂ), p.mahlerMeasure ≤ p.sum fun x a => ‖a‖
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.applyOrderedFinpartition_apply : ∀ {𝕜 : 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] {n : ℕ}
  (c : OrderedFinpartition n) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (v : Fin n → E),
  c.applyOrderedFinpartition p v = fun m => (p m) (v ∘ c.emb m)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_7 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (q₁ q₂ : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S (q₁.pred q₂) =
    (Turing.PartrecToTM2.Λ'.Supports S q₁ ∧ Turing.PartrecToTM2.Λ'.Supports S q₂)
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.mul_star_self : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] (x : R), IsSelfAdjoint (x * star x)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.tensorAlgEquiv_root : ∀ {R : Type u_6} {S : Type u_7} {T : Type u_8} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (p : Polynomial S) (q : Polynomial (TensorProduct R T S))
  (h : Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q),
  (AdjoinRoot.tensorAlgEquiv p q h) (1 ⊗ₜ[R] AdjoinRoot.root p) = AdjoinRoot.root q
-- Mathlib.NumberTheory.AbelSummation
integrableOn_mul_sum_Icc : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {a b : ℝ} {m : ℕ},
  0 ≤ a →
    ∀ {g : ℝ → 𝕜},
      MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume →
        MeasureTheory.IntegrableOn (fun t => g t * ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k) (Set.Icc a b) MeasureTheory.volume
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.tmul_sub : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {P : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup P] [inst_3 : Module R M] [inst_4 : Module R P] (m : M) (p₁ p₂ : P),
  m ⊗ₜ[R] (p₁ - p₂) = m ⊗ₜ[R] p₁ - m ⊗ₜ[R] p₂
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instProductivenessRelation : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [inst_2 : Monad m] →
            [Std.Iterators.Productive α₁ m] →
              [Std.Iterators.Productive α₂ m] →
                Std.Iterators.ProductivenessRelation (Std.Iterators.Types.Zip α₁ m α₂ β₂) m
-- Init.Data.Option.Lemmas
Option.right_le_max : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Max α],
  (∀ (x : α), x ≤ x) → (∀ (x y : α), y ≤ x ⊔ y) → ∀ {a b : Option α}, b ≤ a ⊔ b
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.ltb.inductionOn.eq_def : ∀ {motive : String.Legacy.Iterator → String.Legacy.Iterator → Sort u} (it₁ it₂ : String.Legacy.Iterator)
  (ind :
    (s₁ s₂ : String) →
      (i₁ i₂ : String.Pos.Raw) →
        { s := s₂, i := i₂ }.hasNext = true →
          { s := s₁, i := i₁ }.hasNext = true →
            String.Pos.Raw.get s₁ i₁ = String.Pos.Raw.get s₂ i₂ →
              motive { s := s₁, i := i₁ }.next { s := s₂, i := i₂ }.next →
                motive { s := s₁, i := i₁ } { s := s₂, i := i₂ })
  (eq :
    (s₁ s₂ : String) →
      (i₁ i₂ : String.Pos.Raw) →
        { s := s₂, i := i₂ }.hasNext = true →
          { s := s₁, i := i₁ }.hasNext = true →
            ¬String.Pos.Raw.get s₁ i₁ = String.Pos.Raw.get s₂ i₂ → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ })
  (base₁ :
    (s₁ s₂ : String) →
      (i₁ i₂ : String.Pos.Raw) →
        { s := s₂, i := i₂ }.hasNext = true →
          ¬{ s := s₁, i := i₁ }.hasNext = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ })
  (base₂ :
    (s₁ s₂ : String) →
      (i₁ i₂ : String.Pos.Raw) →
        ¬{ s := s₂, i := i₂ }.hasNext = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }),
  String.ltb.inductionOn it₁ it₂ ind eq base₁ base₂ =
    if h₂ : it₂.hasNext = true then
      if h₁ : it₁.hasNext = true then
        if heq : it₁.curr = it₂.curr then
          ind it₁.s it₂.s it₁.i it₂.i h₂ h₁ heq (String.ltb.inductionOn it₁.next it₂.next ind eq base₁ base₂)
        else eq it₁.s it₂.s it₁.i it₂.i h₂ h₁ heq
      else base₁ it₁.s it₂.s it₁.i it₂.i h₂ h₁
    else base₂ it₁.s it₂.s it₁.i it₂.i h₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion X n).left = X
-- Mathlib.CategoryTheory.Center.Linear
/-- The canonical morphism `R →+* CatCenter C` when `C` is an `R`-linear category.  -/
CategoryTheory.Linear.toCatCenter : (R : Type w) →
  [inst : Ring R] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] → [CategoryTheory.Linear R C] → R →+* CategoryTheory.CatCenter C
-- Mathlib.RingTheory.IsGaloisGroup.Defs
/-- If `B/A` is Galois with Galois group `G`, then `A` is isomorphic to the subring of elements of
`B` fixed by `G`.  -/
IsGaloisGroup.ringEquivFixedPoints : (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] →
                [hA : IsGaloisGroup G A B] → [FaithfulSMul A B] → A ≃+* ↥(FixedPoints.subsemiring B G)
-- Mathlib.Data.Part
Part.some_inter_some : ∀ {α : Type u_1} [inst : Inter α] (a b : α), Part.some a ∩ Part.some b = Part.some (a ∩ b)
-- Mathlib.Data.Multiset.Pi
Multiset.mem_pi : ∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a))
  (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialCofibrations_eq_unop : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.trivialCofibrations C = (HomotopicalAlgebra.trivialFibrations Cᵒᵖ).unop
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.symm_map_nhdsWithin_range : ∀ {𝕜 : 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) (x : H),
  Filter.map (↑I.symm) (nhdsWithin (↑I x) (Set.range ↑I)) = nhds x
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.ext_get : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C C' : G.EdgeLabeling K},
  (∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h) → C = C'
-- Mathlib.Algebra.Regular.Basic
/-- Any power of a left-regular element is left-regular.  -/
IsLeftRegular.pow : ∀ {R : Type u_1} [inst : Monoid R] {a : R} (n : ℕ), IsLeftRegular a → IsLeftRegular (a ^ n)
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.prodMk'_flip : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (ν : AbstractMeasure Y R R) [inst_5 : LocallyCompactSpace X] [inst_6 : LocallyCompactSpace Y] (f : C(X × Y, R)),
  ((AbstractMeasure.prodMk' μ) ν) f = ((AbstractMeasure.prodMk ν) μ) (f.comp ContinuousMap.prodSwap)
-- Mathlib.Probability.Independence.Conditional
/-- Two sets of sets `s₁, s₂` are conditionally independent given `m'` with respect to a measure
`μ` if for any sets `t₁ ∈ s₁, t₂ ∈ s₂`, then `μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧`.
See `ProbabilityTheory.condIndepSets_iff`.  -/
ProbabilityTheory.CondIndepSets : {Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      [StandardBorelSpace Ω] →
        m' ≤ mΩ →
          Set (Set Ω) →
            Set (Set Ω) →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndepSets._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  (f : MeasureTheory.SimpleFunc α E) (μ : MeasureTheory.Measure α), MeasureTheory.MemLp (⇑f) 0 μ
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.embed_injective : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i},
  (Pairwise fun x y => ∃ i, f i x ≠ f i y) → Function.Injective (Metric.PiNatEmbed.embed X Y f)