Loogle!

Result

Found 240 declarations mentioning ExistsUnique. Of these, only the first 200 are shown.

• ExistsUnique 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} (p : α → Prop) : Prop
• existsUnique_false 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} : ¬∃! x, False
• existsUnique_eq 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {a' : α} : ∃! a, a = a'
• existsUnique_eq' 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {a' : α} : ∃! a, a' = a
• existsUnique_prop 📋 Mathlib.Basic.ExistsUnique
  {p q : Prop} : (∃! x, q) ↔ p ∧ q
• existsUnique_const 📋 Mathlib.Basic.ExistsUnique
  {b : Prop} (α : Sort u_2) [i : Nonempty α] [Subsingleton α] : (∃! x, b) ↔ b
• existsUnique_prop_of_true 📋 Mathlib.Basic.ExistsUnique
  {p : Prop} {q : p → Prop} (h : p) : (∃! h', q h') ↔ q h
• ExistsUnique.exists 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Prop} : (∃! x, p x) → ∃ x, p x
• existsUnique_iff_exists 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} [Subsingleton α] {p : α → Prop} : (∃! x, p x) ↔ ∃ x, p x
• ExistsUnique.intro 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p y → y = w) : ∃! x, p x
• ExistsUnique.unique 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂
• ExistsUnique.elim 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Prop} {b : Prop} (h₂ : ∃! x, p x) (h₁ : ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b) : b
• existsUnique_congr 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) : (∃! a, p a) ↔ ∃! a, q a
• existsUnique_of_exists_of_unique 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x) (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x
• List.decidableBExistsUnique 📋 Mathlib.Basic.ExistsUnique
  {α : Type u_2} [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) : Decidable (∃! x, x ∈ l ∧ p x)
• ExistsUnique.exists₂ 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Sort u_2} {q : (x : α) → p x → Prop} (h : ∃! x, ∃! hx, q x hx) : ∃ x hx, q x hx
• ExistsUnique.choose_eq_iff 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Prop} {a : α} (h : ∃! x, p x) : Exists.choose h = a ↔ p a
• ExistsUnique.intro₂ 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (w : α) (hp : p w) (hq : q w hp) (H : ∀ (y : α) (hy : p y), q y hy → y = w) : ∃! x, ∃! hx, q x hx
• ExistsUnique.unique₂ 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (h : ∃! x, ∃! hx, q x hx) {y₁ y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) : y₁ = y₂
• ExistsUnique.elim₂ 📋 Mathlib.Basic.ExistsUnique
  {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} {b : Prop} (h₂ : ∃! x, ∃! h, q x h) (h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) : b
• Function.Bijective.existsUnique 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) (b : β) : ∃! a, f a = b
• Function.bijective_iff_existsUnique 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} (f : α → β) : Function.Bijective f ↔ ∀ (b : β), ∃! a, f a = b
• Function.Bijective.existsUnique_iff 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) {p : β → Prop} : (∃! y, p y) ↔ ∃! x, p (f x)
• forall_existsUnique_iff 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop} : (∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b
• forall_existsUnique_iff' 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop} : (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x1 x2 => f x1 = x2
• Symmetric.forall_existsUnique_iff 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b
• Std.Symm.forall_existsUnique_iff 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b
• Symmetric.forall_existsUnique_iff' 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ r = fun x1 x2 => f x1 = x2
• Std.Symm.forall_existsUnique_iff' 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ r = fun x1 x2 => f x1 = x2
• unique_iff_existsUnique 📋 Mathlib.Basic.Unique
  (α : Sort u) : Nonempty (Unique α) ↔ ∃! x, True
• unique_subtype_iff_existsUnique 📋 Mathlib.Basic.Unique
  {α : Sort u_1} (p : α → Prop) : Nonempty (Unique (Subtype p)) ↔ ∃! a, p a
• Equiv.existsUnique_subtype_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : { a // p a } ≃ { b // q b }) : (∃! a, p a) ↔ ∃! b, q b
• Equiv.existsUnique_congr_right 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∃! a, q (e a)) ↔ ∃! b, q b
• Equiv.existsUnique_congr_left 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∃! a, p a) ↔ ∃! b, p (e.symm b)
• Equiv.existsUnique_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∃! a, p a) ↔ ∃! b, q b
• Equiv.existsUnique_congr' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∃! a, p a) ↔ ∃! b, q b
• Set.singleton_iff_unique_mem 📋 Mathlib.Data.Set.Insert
  {α : Type u_1} {s : Set α} : (∃ a, s = {a}) ↔ ∃! a, a ∈ s
• ExistsUnique.setSubsingleton 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u_1} {p : α → Prop} (h : ExistsUnique p) : {x | p x}.Subsingleton
• Function.Injective.existsUnique_of_mem_range 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) {b : β} : b ∈ Set.range f → ∃! a, f a = b
• Function.Injective.mem_range_iff_existsUnique 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) {b : β} : b ∈ Set.range f ↔ ∃! a, f a = b
• existsUnique_div_zpow_mem_Ico 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) : ∃! m, b / a ^ m ∈ Set.Ico c (c * a)
• existsUnique_sub_zpow_mem_Ioc 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) : ∃! m, b / a ^ m ∈ Set.Ioc c (c * a)
• existsUnique_sub_zsmul_mem_Ico 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b - m • a ∈ Set.Ico c (c + a)
• existsUnique_sub_zsmul_mem_Ioc 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b - m • a ∈ Set.Ioc c (c + a)
• existsUnique_add_zpow_mem_Ioc 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) : ∃! m, b * a ^ m ∈ Set.Ioc c (c * a)
• existsUnique_add_zsmul_mem_Ico 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b + m • a ∈ Set.Ico c (c + a)
• existsUnique_add_zsmul_mem_Ioc 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b + m • a ∈ Set.Ioc c (c + a)
• existsUnique_mul_zpow_mem_Ico 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) : ∃! m, b * a ^ m ∈ Set.Ico c (c * a)
• existsUnique_zpow_near_of_one_lt 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (g : G) : ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
• existsUnique_zsmul_near_of_pos 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (g : G) : ∃! k, k • a ≤ g ∧ g < (k + 1) • a
• existsUnique_zpow_near_of_one_lt' 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (g : G) : ∃! k, 1 ≤ g / a ^ k ∧ g / a ^ k < a
• existsUnique_zsmul_near_of_pos' 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (g : G) : ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
• Multiset.choose 📋 Mathlib.Data.Multiset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a) : α
• Multiset.choose_property 📋 Mathlib.Data.Multiset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a) : p (Multiset.choose p l hp)
• Multiset.choose_mem 📋 Mathlib.Data.Multiset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a) : Multiset.choose p l hp ∈ l
• Multiset.chooseX 📋 Mathlib.Data.Multiset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (_hp : ∃! a, a ∈ l ∧ p a) : { a // a ∈ l ∧ p a }
• Multiset.choose_spec 📋 Mathlib.Data.Multiset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a) : Multiset.choose p l hp ∈ l ∧ p (Multiset.choose p l hp)
• Multiset.choose_eq_iff 📋 Mathlib.Data.Multiset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a, a ∈ l ∧ p a) {a : α} : Multiset.choose p l hp = a ↔ a ∈ l ∧ p a
• Finset.singleton_iff_unique_mem 📋 Mathlib.Data.Finset.Insert
  {α : Type u_1} (s : Finset α) : (∃ a, s = {a}) ↔ ∃! a, a ∈ s
• Finset.choose 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) : α
• Finset.choose_property 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) : p (Finset.choose p l hp)
• Finset.choose_mem 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) : Finset.choose p l hp ∈ l
• Finset.chooseX 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) : { a // a ∈ l ∧ p a }
• Finset.choose_spec 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) : Finset.choose p l hp ∈ l ∧ p (Finset.choose p l hp)
• Finset.choose_eq_iff 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a) {a : α} : Finset.choose p l hp = a ↔ a ∈ l ∧ p a
• Finset.card_eq_one_iff_existsUnique 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {s : Finset α} : s.card = 1 ↔ ∃! a, a ∈ s
• Finset.existsUnique_notMem_image_of_injOn_of_card_eq_add_one 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {t : Finset β} [DecidableEq β] (hf : Set.InjOn f ↑s) (hf' : Set.MapsTo f ↑s ↑t) (h : t.card = s.card + 1) : ∃! x, x ∈ t ∧ x ∉ Finset.image f s
• Fintype.existsUnique_iff_card_one 📋 Mathlib.Data.Fintype.Card
  {α : Type u_3} [Fintype α] (p : α → Prop) [DecidablePred p] : (∃! a, p a) ↔ {x | p x}.card = 1
• Fintype.existsUnique_notMem_image_of_injective_of_card_eq_add_one 📋 Mathlib.Data.Fintype.Card
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (h : Fintype.card β = Fintype.card α + 1) : ∃! x, x ∉ Finset.image f Finset.univ
• Set.sigmaEquiv 📋 Mathlib.Data.Set.Lattice.Disjoint
  {α : Type u_1} {β : Type u_2} (s : α → Set β) (hs : ∀ (b : β), ∃! i, b ∈ s i) : (i : α) × ↑(s i) ≃ β
• pairwiseDisjoint_unique 📋 Mathlib.Data.Set.Pairwise.Lattice
  {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s : Set ι} {y : α} (h_disjoint : s.PairwiseDisjoint f) (hy : y ∈ ⋃ i ∈ s, f i) : ∃! i, i ∈ s ∧ y ∈ f i
• Cardinal.mk_eq_two_iff' 📋 Mathlib.SetTheory.Cardinal.Basic
  {α : Type u} (x : α) : Cardinal.mk α = 2 ↔ ∃! y, y ≠ x
• Multiset.find?_eq_choose 📋 Mathlib.Data.Multiset.Find
  {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Multiset α} (hp : ∃! x, x ∈ s ∧ p x) : Multiset.find? p s ⋯ = some (Multiset.choose p s hp)
• Nat.card_eq_two_iff' 📋 Mathlib.SetTheory.Cardinal.Finite
  {α : Type u_1} (x : α) : Nat.card α = 2 ↔ ∃! y, y ≠ x
• uniq_inv_of_isField 📋 Mathlib.Algebra.Field.IsField
  (R : Type u) [Ring R] (hf : IsField R) (x : R) : x ≠ 0 → ∃! y, x * y = 1
• UniqueAdd.iff_existsUnique 📋 Mathlib.Algebra.Group.UniqueProds.Basic
  {G : Type u_1} [Add G] {A B : Finset G} {a0 b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) : UniqueAdd A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 + ab.2 = a0 + b0
• UniqueMul.iff_existsUnique 📋 Mathlib.Algebra.Group.UniqueProds.Basic
  {G : Type u_1} [Mul G] {A B : Finset G} {a0 b0 : G} (aA : a0 ∈ A) (bB : b0 ∈ B) : UniqueMul A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
• UniqueAdd.exists_iff_exists_existsUnique 📋 Mathlib.Algebra.Group.UniqueProds.Basic
  {G : Type u_1} [Add G] {A B : Finset G} : (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueAdd A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 + ab.2 = g
• UniqueMul.exists_iff_exists_existsUnique 📋 Mathlib.Algebra.Group.UniqueProds.Basic
  {G : Type u_1} [Mul G] {A B : Finset G} : (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
• Submodule.existsUnique_add_of_isCompl_prod 📋 Mathlib.LinearAlgebra.Projection
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {p q : Submodule R E} (hc : IsCompl p q) (x : E) : ∃! u, ↑u.1 + ↑u.2 = x
• SetRel.exists_graph_eq_iff 📋 Mathlib.Basic.Rel
  {α : Type u_1} {β : Type u_2} (R : SetRel α β) : (∃! f, Function.graph f = R) ↔ ∀ (a : α), ∃! b, (a, b) ∈ R
• LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one 📋 Mathlib.LinearAlgebra.Dimension.Free
  {R : Type u_2} [CommSemiring R] [StrongRankCondition R] {M : Type u_3} [AddCommMonoid M] [Module R M] [Module.Free R M] (d1 : Module.finrank R M = 1) (u : M →ₗ[R] M) : ∃! c, u = c • LinearMap.id
• Submodule.existsUnique_from_graph 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_4} [AddCommGroup E] [Module R E] {F : Type u_5} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0) {a : E} (ha : a ∈ Submodule.map (LinearMap.fst R E F) g) : ∃! b, (a, b) ∈ g
• CharP.existsUnique 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [NonAssocSemiring R] : ∃! p, CharP R p
• ExpChar.exists_unique 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [Ring R] [IsDomain R] : ∃! q, ExpChar R q
• existsUnique_eq_principal_sup_free 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} (f : Filter α) : ∃! p, p.2 ≤ Filter.cofinite ∧ Disjoint (Filter.principal p.1) p.2 ∧ f = Filter.principal p.1 ⊔ p.2
• IsBaseChange.of_lift_unique 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) (h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g) : IsBaseChange S f
• IsBaseChange.iff_lift_unique 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} : IsBaseChange S f ↔ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
• CategoryTheory.Limits.IsColimit.existsUnique 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone F) : ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) l = s.ι.app j
• CategoryTheory.Limits.IsColimit.ofExistsUnique 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (ht : ∀ (s : CategoryTheory.Limits.Cocone F), ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) l = s.ι.app j) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.IsLimit.existsUnique 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) : ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.π.app j) = s.π.app j
• CategoryTheory.Limits.IsLimit.ofExistsUnique 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (ht : ∀ (s : CategoryTheory.Limits.Cone F), ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.π.app j) = s.π.app j) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.colimit.existsUnique 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) : ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) l = t.ι.app j
• CategoryTheory.Limits.limit.existsUnique 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.Cone F) : ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.limit.π F j) = t.π.app j
• CategoryTheory.CostructuredArrow.IsUniversal.existsUnique 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.CostructuredArrow S T) : ∃! η, CategoryTheory.CategoryStruct.comp (S.map η) f.hom = g.hom
• CategoryTheory.StructuredArrow.IsUniversal.existsUnique 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.StructuredArrow S T) : ∃! η, CategoryTheory.CategoryStruct.comp f.hom (T.map η) = g.hom
• CategoryTheory.Limits.coequalizer.existsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasCoequalizer f g] {W : C} (k : Y ⟶ W) (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k) : ∃! d, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) d = k
• CategoryTheory.Limits.equalizer.existsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : ∃! l, CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k
• CategoryTheory.Limits.Cofork.IsColimit.existsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k) : ∃! d, CategoryTheory.CategoryStruct.comp s.π d = k
• CategoryTheory.Limits.Fork.IsLimit.existsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : ∃! l, CategoryTheory.CategoryStruct.comp l s.ι = k
• CategoryTheory.Limits.Cofork.IsColimit.ofExistsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {t : CategoryTheory.Limits.Cofork f g} (hs : ∀ (s : CategoryTheory.Limits.Cofork f g), ∃! d, CategoryTheory.CategoryStruct.comp t.π d = s.π) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g} (hs : ∀ (s : CategoryTheory.Limits.Fork f g), ∃! l, CategoryTheory.CategoryStruct.comp l t.ι = s.ι) : CategoryTheory.Limits.IsLimit t
• IsAddCyclic.unique_zsmul_zmod 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
  {α : Type u_1} {a : α} [AddGroup α] [Fintype α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) (x : α) : ∃! n, x = n.val • a
• IsCyclic.unique_zpow_zmod 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
  {α : Type u_1} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) (x : α) : ∃! n, x = a ^ n.val
• Fintype.choose 📋 Mathlib.Data.Fintype.Inv
  {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a, p a) : α
• Fintype.chooseX 📋 Mathlib.Data.Fintype.Inv
  {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a, p a) : { a // p a }
• Fintype.choose_spec 📋 Mathlib.Data.Fintype.Inv
  {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a, p a) : p (Fintype.choose p hp)
• Fintype.choose_subtype_eq 📋 Mathlib.Data.Fintype.Inv
  {α : Type u_3} (p : α → Prop) [Fintype { a // p a }] [DecidableEq α] (x : { a // p a }) (h : ∃! a, ↑a = ↑x := ⋯) : Fintype.choose (fun y => ↑y = ↑x) h = x
• CategoryTheory.Limits.Types.isLimit_iff 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x = s j
• Localization.existsUnique_algebraMap_eq_of_span_eq_top 📋 Mathlib.RingTheory.Localization.Away.Basic
  {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Ideal.span s = ⊤) (f : (a : ↑s) → Localization.Away ↑a) (h : ∀ (a b : ↑s), (IsLocalization.Away.awayToAwayRight ↑a ↑b) (f a) = (IsLocalization.Away.awayToAwayLeft ↑b ↑a) (f b)) : ∃! r, ∀ (a : ↑s), (algebraMap R (Localization.Away ↑a)) r = f a
• IsLocalRing.of_unique_max_ideal 📋 Mathlib.RingTheory.LocalRing.Basic
  {R : Type u_1} [CommSemiring R] (h : ∃! I, I.IsMaximal) : IsLocalRing R
• IsLocalRing.of_unique_nonzero_prime 📋 Mathlib.RingTheory.LocalRing.Basic
  {R : Type u_1} [CommSemiring R] (h : ∃! P, P ≠ ⊥ ∧ P.IsPrime) : IsLocalRing R
• IsLocalRing.maximal_ideal_unique 📋 Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  (R : Type u_1) [CommSemiring R] [IsLocalRing R] : ∃! I, I.IsMaximal
• IsLocalizedModule.is_universal 📋 Mathlib.Algebra.Module.LocalizedModule.Basic
  {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') : (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → ∃! l, l ∘ₗ f = g
• CategoryTheory.IsCodetector.def 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : C} : CategoryTheory.IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h', CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f
• CategoryTheory.IsDetector.def 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : C} : CategoryTheory.IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f
• CategoryTheory.isCodetector_def 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : C) : CategoryTheory.IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h', CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f
• CategoryTheory.isDetector_def 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : C) : CategoryTheory.IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f
• PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : IsClopen s) : ∃! e, IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
• CategoryTheory.Presieve.isSheafFor_arrows_iff 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.Compatible P π x → ∃! t, ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x i
• CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.PullbackCompatible P π x → ∃! t, ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x i
• CategoryTheory.Presieve.isSheafFor_singleton 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {f : X ⟶ Y} : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton f) ↔ ∀ (x : P.obj (Opposite.op X)), (∀ {Z : C} (p₁ p₂ : Z ⟶ X), CategoryTheory.CategoryStruct.comp p₁ f = CategoryTheory.CategoryStruct.comp p₂ f → (CategoryTheory.ConcreteCategory.hom (P.map p₁.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map p₂.op)) x) → ∃! y, (CategoryTheory.ConcreteCategory.hom (P.map f.op)) y = x
• CategoryTheory.Limits.Types.typeEqualizerOfUnique 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
  {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : ∀ (y : Y), (CategoryTheory.ConcreteCategory.hom g) y = (CategoryTheory.ConcreteCategory.hom h) y → ∃! x, (CategoryTheory.ConcreteCategory.hom f) x = y) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)
• CategoryTheory.Limits.Types.unique_of_type_equalizer 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
  {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) (y : Y) (hy : (CategoryTheory.ConcreteCategory.hom g) y = (CategoryTheory.ConcreteCategory.hom h) y) : ∃! x, (CategoryTheory.ConcreteCategory.hom f) x = y
• CategoryTheory.Limits.Types.type_equalizer_iff_unique 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
  {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) ↔ ∀ (y : Y), (CategoryTheory.ConcreteCategory.hom g) y = (CategoryTheory.ConcreteCategory.hom h) y → ∃! x, (CategoryTheory.ConcreteCategory.hom f) x = y
• CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : I → C} (f : (i : I) → X i ⟶ S) (hf : CategoryTheory.Sieve.ofArrows X f ∈ J S) {E : A} (x : (i : I) → E ⟶ P.obj (Opposite.op (X i))) (hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) → CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) : ∃! g, ∀ (i : I), CategoryTheory.CategoryStruct.comp g (P.map (f i).op) = x i
• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.existsUnique_section 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i
• TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types 📋 Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
  {X : TopCat} {F : TopCat.Presheaf (Type u_4) X} {ι : Type u_5} {U : ι → TopologicalSpace.Opens ↑X} (h : F.IsSheaf) (sf : (i : ι) → F.obj (Opposite.op (U i))) (cpt : F.IsCompatible U sf) : ∃! s, F.IsGluing U sf s
• TopCat.Presheaf.IsSheaf.isSheafUniqueGluing 📋 Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat} {F : TopCat.Presheaf C X} (h : F.IsSheaf) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X) (sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))) (cpt : F.IsCompatible U sf) : ∃! s, F.IsGluing U sf s
• TopCat.Sheaf.existsUnique_gluing 📋 Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat} (F : TopCat.Sheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X) (sf : (i : ι) → CategoryTheory.ToType (F.obj.obj (Opposite.op (U i)))) (h : TopCat.Presheaf.IsCompatible F.obj U sf) : ∃! s, TopCat.Presheaf.IsGluing F.obj U sf s
• TopCat.Sheaf.existsUnique_gluing' 📋 Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat} (F : TopCat.Sheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X) (iUV : (i : ι) → U i ⟶ V) (hcover : V ≤ iSup U) (sf : (i : ι) → CategoryTheory.ToType (F.obj.obj (Opposite.op (U i)))) (h : TopCat.Presheaf.IsCompatible F.obj U sf) : ∃! s, ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i
• existsUnique_isIdempotentElem_eq_of_ker_isNilpotent 📋 Mathlib.RingTheory.Idempotents
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] (f : R →+* S) (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) : ∃! e', IsIdempotentElem e' ∧ f e' = e
• SSet.S.existsUnique_n 📋 Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
  {X : SSet} (x : X.S) : ∃! y, y.subcomplex = x.subcomplex
• SSet.S.existsUnique_toNπ 📋 Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
  {X : SSet} {x : X.S} {y : X.N} (hy : x.toN = y) : ∃! f, CategoryTheory.Epi f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
• Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsNilpotent ((Polynomial.aeval x) P)) (h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : ∃! r, IsNilpotent (x - r) ∧ (Polynomial.aeval r) P = 0
• IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime 📋 Mathlib.RingTheory.DiscreteValuationRing.Basic
  (R : Type u) [CommRing R] [IsDomain R] : IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
• Ring.KrullDimLE.existsUnique_isPrime 📋 Mathlib.RingTheory.KrullDimension.Zero
  (R : Type u_1) [CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R] : ∃! I, I.IsPrime
• Ring.krullDimLE_zero_and_isLocalRing_tfae 📋 Mathlib.RingTheory.KrullDimension.Zero
  (R : Type u_1) [CommSemiring R] : [Ring.KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE
• IsDiscreteValuationRing.TFAE 📋 Mathlib.RingTheory.DiscreteValuationRing.TFAE
  (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] (h : ¬IsField R) : [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (IsLocalRing.maximalIdeal R), Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n].TFAE
• Equiv.Perm.IsCycle.existsUnique_cycle 📋 Mathlib.GroupTheory.Perm.Cycle.Concrete
  {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) : ∃! s, ∃ (h : s.Nodup), s.formPerm h = f
• Equiv.Perm.IsCycle.existsUnique_cycle_subtype 📋 Mathlib.GroupTheory.Perm.Cycle.Concrete
  {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) : ∃! s, (↑s).formPerm ⋯ = f
• Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype 📋 Mathlib.GroupTheory.Perm.Cycle.Concrete
  {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : f.IsCycle) : ∃! s, (↑s).formPerm ⋯ = f
• summable_partition 📋 Mathlib.Topology.Algebra.InfiniteSum.Real
  {α : Type u_3} {β : Type u_4} {f : β → ℝ} (hf : 0 ≤ f) {s : α → Set β} (hs : ∀ (i : β), ∃! j, i ∈ s j) : Summable f ↔ (∀ (j : α), Summable fun i => f ↑i) ∧ Summable fun j => ∑' (i : ↑(s j)), f ↑i
• AddSubgroup.isComplement_addSubgroup_left_iff_existsUnique_quotientMk'' 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} : AddSubgroup.IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientAddGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q
• Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'' 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} : Subgroup.IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q
• AddSubgroup.isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : AddSubgroup.IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q
• Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : Subgroup.IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q
• AddSubgroup.isComplement_iff_existsUnique_add_neg_mem 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [AddGroup G] {S T : Set G} : AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! t, g + -↑t ∈ S
• AddSubgroup.isComplement_iff_existsUnique_neg_add_mem 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [AddGroup G] {S T : Set G} : AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! s, -↑s + g ∈ T
• Subgroup.isComplement_iff_existsUnique_inv_mul_mem 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {S T : Set G} : Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
• Subgroup.isComplement_iff_existsUnique_mul_inv_mem 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {S T : Set G} : Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! t, g * (↑t)⁻¹ ∈ S
• AddSubgroup.IsComplement.existsUnique 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [AddGroup G] {S T : Set G} (h : AddSubgroup.IsComplement S T) (g : G) : ∃! x, ↑x.1 + ↑x.2 = g
• Subgroup.IsComplement.existsUnique 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {S T : Set G} (h : Subgroup.IsComplement S T) (g : G) : ∃! x, ↑x.1 * ↑x.2 = g
• AddSubgroup.isComplement_iff_existsUnique 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [AddGroup G] {S T : Set G} : AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 + ↑x.2 = g
• Subgroup.isComplement_iff_existsUnique 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {S T : Set G} : Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
• discrim_eq_zero_of_existsUnique 📋 Mathlib.Algebra.QuadraticDiscriminant
  {K : Type u_1} [Field K] [NeZero 2] {a b c : K} (ha : a ≠ 0) (h : ∃! x, a * (x * x) + b * x + c = 0) : discrim a b c = 0
• discrim_eq_zero_iff 📋 Mathlib.Algebra.QuadraticDiscriminant
  {K : Type u_1} [Field K] [NeZero 2] {a b c : K} (ha : a ≠ 0) : discrim a b c = 0 ↔ ∃! x, a * (x * x) + b * x + c = 0
• MeasureTheory.IsAddFundamentalDomain.mk' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
  {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h_meas : MeasureTheory.NullMeasurableSet s μ) (h_exists : ∀ (x : α), ∃! g, g +ᵥ x ∈ s) : MeasureTheory.IsAddFundamentalDomain G s μ
• MeasureTheory.IsFundamentalDomain.mk' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
  {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h_meas : MeasureTheory.NullMeasurableSet s μ) (h_exists : ∀ (x : α), ∃! g, g • x ∈ s) : MeasureTheory.IsFundamentalDomain G s μ
• ZSpan.exist_unique_vadd_mem_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
  {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Module.Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Finite ι] (x : E) : ∃! v, v +ᵥ x ∈ ZSpan.fundamentalDomain b
• BoxIntegral.Prepartition.IsPartition.existsUnique 📋 Mathlib.Analysis.BoxIntegral.Partition.Basic
  {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {x : ι → ℝ} (h : π.IsPartition) (hx : x ∈ I) : ∃! J, J ∈ π ∧ x ∈ J
• isPrimePow_iff_unique_prime_dvd 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} : IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
• Nat.finMulAntidiag_existsUnique_prime_dvd 📋 Mathlib.Algebra.Order.Antidiag.Nat
  {d n p : ℕ} (hn : Squarefree n) (hp : p ∈ n.primeFactorsList) (f : Fin d → ℕ) (hf : f ∈ d.finMulAntidiag n) : ∃! i, p ∣ f i
• AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul 📋 Mathlib.GroupTheory.ArchimedeanDensely
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (ha : a ≠ 0) : b ∈ AddSubgroup.closure {a} ↔ ∃! k, k • a = b
• Subgroup.mem_closure_singleton_iff_existsUnique_zpow 📋 Mathlib.GroupTheory.ArchimedeanDensely
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (ha : a ≠ 1) : b ∈ Subgroup.closure {a} ↔ ∃! k, a ^ k = b
• StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot 📋 Mathlib.RingTheory.Etale.StandardEtale
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (I : Ideal S) (hI : I ^ 2 = ⊥) (x : S) (hx : P.HasMap ((Ideal.Quotient.mk I) x)) : ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
• SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex 📋 Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
  {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) : ∃! i, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) (y.cast ⋯).simplex = (x.cast hd).simplex
• SSet.S.IsUniquelyCodimOneFace.iff 📋 Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
  {X : SSet} {d : ℕ} (x : X.obj (Opposite.op { len := d })) (y : X.obj (Opposite.op { len := d + 1 })) : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } ↔ ∃! i, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) y = x
• SSet.N.existsUnique_of_le 📋 Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
  {X : SSet} [X.Nonsingular] {x y : X.N} (h : x ≤ y) : ∃! f, CategoryTheory.Mono f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
• IsCoveringMap.existsUnique_continuousMap_lifts 📋 Mathlib.Topology.Homotopy.Lifting
  {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E) (he : p e₀ = f a₀) : ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
• IsCoveringMapOn.existsUnique_continuousMap_lifts 📋 Mathlib.Topology.Homotopy.Lifting
  {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] {s : Set X} (cov : IsCoveringMapOn p s) (f : C(A, X)) {a₀ : A} {e₀ : E} (he : p e₀ = f a₀) (hs : ∀ (a : A), f a ∈ s) : ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
• IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le 📋 Mathlib.Topology.Homotopy.Lifting
  {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) [PathConnectedSpace A] [LocallyPathConnectedSpace A] {f : C(A, X)} {a₀ : A} {e₀ : E} (he : p e₀ = f a₀) (le : (FundamentalGroup.map f a₀).range ≤ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range) : ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
• IsLocalHomeomorph.existsUnique_continuousMap_lifts 📋 Mathlib.Topology.Homotopy.Lifting
  {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (homeo : IsLocalHomeomorph p) [PathConnectedSpace A] [LocallyPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E) (he : p e₀ = f a₀) (ex : ∀ (γ : C(↑unitInterval, A)), γ 0 = a₀ → ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)) (uniq : ∀ (γ γ' : C(↑unitInterval, A)) (Γ Γ' : C(↑unitInterval, E)), γ 0 = a₀ → γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → p ∘ ⇑Γ = ⇑(f.comp γ) → p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1) : ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
• IsPrimitiveRoot.existsUnique 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {M : Type u_1} [CommMonoid M] {ζ : M} : ∃! k, IsPrimitiveRoot ζ k
• Polynomial.unique_int_coeff_of_cycl 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
  {K : Type u_2} [CommRing K] [IsDomain K] [CharZero K] {ζ : K} {n : ℕ+} (h : IsPrimitiveRoot ζ ↑n) : ∃! P, Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' (↑n) K
• DirichletCharacter.FactorsThrough.existsUnique 📋 Mathlib.NumberTheory.DirichletCharacter.Basic
  {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} [NeZero n] (h : χ.FactorsThrough d) : ∃! χ', χ = (DirichletCharacter.changeLevel ⋯) χ'
• LinearPMap.IsClosable.existsUnique 📋 Mathlib.Topology.Algebra.Module.LinearPMap
  {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup E] [AddCommGroup F] [Module R E] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousAdd E] [ContinuousAdd F] [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F] {f : E →ₗ.[R] F} (hf : f.IsClosable) : ∃! f', f.graph.topologicalClosure = f'.graph
• Int.existsUnique_mem_box 📋 Mathlib.Order.Interval.Finset.Box
  (x : ℤ × ℤ) : ∃! n, x ∈ Finset.box n
• CategoryTheory.Bicategory.Lan.existsUnique 📋 Mathlib.CategoryTheory.Bicategory.Kan.HasKan
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} [CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g) : ∃! τ, CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g) (CategoryTheory.Bicategory.whiskerLeft f τ) = s.unit
• CategoryTheory.Bicategory.LanLift.existsUnique 📋 Mathlib.CategoryTheory.Bicategory.Kan.HasKan
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} [CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) : ∃! τ, CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g) (CategoryTheory.Bicategory.whiskerRight τ f) = s.unit
• CategoryTheory.Functor.IsCartesian.universal_property 📋 Mathlib.CategoryTheory.FiberedCategory.Cartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} 𝒳} {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] : ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
• CategoryTheory.Functor.IsCartesian.mk 📋 Mathlib.CategoryTheory.FiberedCategory.Cartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ] (universal_property : ∀ {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'], ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ') : p.IsCartesian f φ
• CategoryTheory.Functor.IsStronglyCartesian.universal_property 📋 Mathlib.CategoryTheory.FiberedCategory.Cartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R) (f' : R' ⟶ S) (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] : ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
• CategoryTheory.Functor.IsStronglyCartesian.universal_property' 📋 Mathlib.CategoryTheory.FiberedCategory.Cartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} 𝒳} {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsStronglyCartesian f φ] {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'] : ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
• CategoryTheory.Functor.IsStronglyCartesian.mk 📋 Mathlib.CategoryTheory.FiberedCategory.Cartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ] (universal_property' : ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'], ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ') : p.IsStronglyCartesian f φ
• CategoryTheory.Functor.IsCocartesian.universal_property 📋 Mathlib.CategoryTheory.FiberedCategory.Cocartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} 𝒳} {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] : ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id S) χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'
• CategoryTheory.Functor.IsCocartesian.mk 📋 Mathlib.CategoryTheory.FiberedCategory.Cocartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ] (universal_property : ∀ {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'], ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id S) χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ') : p.IsCocartesian f φ
• CategoryTheory.Functor.IsStronglyCocartesian.universal_property 📋 Mathlib.CategoryTheory.FiberedCategory.Cocartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') (f' : R ⟶ S') (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] : ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'
• CategoryTheory.Functor.IsStronglyCocartesian.universal_property' 📋 Mathlib.CategoryTheory.FiberedCategory.Cocartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} 𝒳} {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsStronglyCocartesian f φ] {b' : 𝒳} (g : S ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) φ'] : ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'
• CategoryTheory.Functor.IsStronglyCocartesian.mk 📋 Mathlib.CategoryTheory.FiberedCategory.Cocartesian
  {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ] (universal_property' : ∀ {b' : 𝒳} (g : S ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) φ'], ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ') : p.IsStronglyCocartesian f φ
• CategoryTheory.PreGaloisCategory.exists_autMap 📋 Mathlib.CategoryTheory.Galois.GaloisObjects
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] {A B : C} (f : A ⟶ B) [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B] (σ : CategoryTheory.Aut A) : ∃! τ, CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f
• CategoryTheory.ModObj.isIso_leftSMul_iff 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {X : C} [CategoryTheory.ModObj M X] : CategoryTheory.IsIso (CategoryTheory.ModObj.leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m, m • x = y
• SimpleGraph.degree_eq_one_iff_existsUnique_adj 📋 Mathlib.Combinatorics.SimpleGraph.Finite
  {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ↑(G.neighborSet v)] : G.degree v = 1 ↔ ∃! w, G.Adj v w
• Finpartition.existsUnique_mem 📋 Mathlib.Order.Partition.Finpartition
  {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : ∃! t, t ∈ P.parts ∧ a ∈ t
• Finpartition.ofExistsUnique 📋 Mathlib.Order.Partition.Finpartition
  {α : Type u_1} [DecidableEq α] {s : Finset α} (parts : Finset (Finset α)) (h : ∀ p ∈ parts, p ⊆ s) (h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t) (h'' : ∅ ∉ parts) : Finpartition s
• Finpartition.ofExistsUnique_parts 📋 Mathlib.Order.Partition.Finpartition
  {α : Type u_1} [DecidableEq α] {s : Finset α} (parts : Finset (Finset α)) (h : ∀ p ∈ parts, p ⊆ s) (h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t) (h'' : ∅ ∉ parts) : (Finpartition.ofExistsUnique parts h h' h'').parts = parts
• SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adj 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [Fintype ↑(G'.neighborSet v)] : G'.degree v = 1 ↔ ∃! w, G'.Adj v w
• Configuration.HasLines.existsUnique_line 📋 Mathlib.Combinatorics.Configuration
  (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.HasLines P L] (p₁ p₂ : P) (hp : p₁ ≠ p₂) : ∃! l, p₁ ∈ l ∧ p₂ ∈ l
• Configuration.HasPoints.existsUnique_point 📋 Mathlib.Combinatorics.Configuration
  (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.HasPoints P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) : ∃! p, p ∈ l₁ ∧ p ∈ l₂
• Setoid.classes_eqv_classes 📋 Mathlib.Data.Setoid.Partition
  {α : Type u_1} {r : Setoid α} (a : α) : ∃! b, b ∈ r.classes ∧ a ∈ b

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c