Loogle!

Result

Found 260 declarations mentioning Equiv and Sigma. Of these, only the first 200 are shown.

• Equiv.sigmaEquivProd 📋 Mathlib.Logic.Equiv.Defs
  (α : Type u_1) (β : Type u_2) : (_ : α) × β ≃ α × β
• Equiv.sigmaPLiftEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} (P : α → Prop) : (i : α) × PLift (P i) ≃ Subtype P
• Equiv.psigmaEquivSigma 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_2} (β : α → Type u_1) : (i : α) ×' β i ≃ (i : α) × β i
• Equiv.sigmaULiftPLiftEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} (P : α → Prop) : (i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P
• Equiv.sigmaEquivProdOfEquiv 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} {β₁ : α → Type u_3} (F : (a : α) → β₁ a ≃ β) : Sigma β₁ ≃ α × β
• Equiv.psigmaEquivSigmaPLift 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_2} (β : α → Sort u_1) : (i : α) ×' β i ≃ (i : PLift α) × PLift (β i.down)
• Equiv.sigmaCongrRight 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (a : α) × β₁ a ≃ (a : α) × β₂ a
• Equiv.sigmaCongrLeft 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) : (a : α₁) × β (e a) ≃ (a : α₂) × β a
• Equiv.sigmaCongrRight_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_2} {β : α → Type u_1} : (Equiv.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
• Equiv.sigmaCongrLeft' 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ → Type u_3} (f : α₁ ≃ α₂) : (a : α₁) × β a ≃ (a : α₂) × β (f.symm a)
• Equiv.sigmaCongr 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ ≃ α₂) (F : (a : α₁) → β₁ a ≃ β₂ (f a)) : Sigma β₁ ≃ Sigma β₂
• Equiv.sigmaAssoc 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : α → Type u_2} (γ : (a : α) → β a → Type u_3) : (ab : (a : α) × β a) × γ ab.fst ab.snd ≃ (a : α) × (b : β a) × γ a b
• Equiv.Perm.sigmaCongrRight_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Equiv.Perm (β a)) : Equiv.symm (Equiv.Perm.sigmaCongrRight F) = Equiv.Perm.sigmaCongrRight fun a => Equiv.symm (F a)
• Equiv.sigmaCongrRight_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (Equiv.sigmaCongrRight F).symm = Equiv.sigmaCongrRight fun a => (F a).symm
• Equiv.sigmaEquivProd_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Type u_1) (β : Type u_2) (a : (_ : α) × β) : (Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
• Equiv.sigmaEquivProd_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Type u_1) (β : Type u_2) (a : α × β) : (Equiv.sigmaEquivProd α β).symm a = ⟨a.1, a.2⟩
• Equiv.Perm.sigmaCongrRight_trans 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : α → Type u_2} (F G : (a : α) → Equiv.Perm (β a)) : Equiv.trans (Equiv.Perm.sigmaCongrRight F) (Equiv.Perm.sigmaCongrRight G) = Equiv.Perm.sigmaCongrRight fun a => Equiv.trans (F a) (G a)
• Equiv.psigmaEquivSigma_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_2} (β : α → Type u_1) (a : (i : α) ×' β i) : (Equiv.psigmaEquivSigma β) a = ⟨a.fst, a.snd⟩
• Equiv.sigmaCongrRight_trans 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_4} {β₁ : α → Type u_1} {β₂ : α → Type u_2} {β₃ : α → Type u_3} (F : (a : α) → β₁ a ≃ β₂ a) (G : (a : α) → β₂ a ≃ β₃ a) : (Equiv.sigmaCongrRight F).trans (Equiv.sigmaCongrRight G) = Equiv.sigmaCongrRight fun a => (F a).trans (G a)
• Equiv.psigmaEquivSigma_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_2} (β : α → Type u_1) (a : (i : α) × β i) : (Equiv.psigmaEquivSigma β).symm a = ⟨a.fst, a.snd⟩
• Equiv.psigmaEquivSigmaPLift_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_2} (β : α → Sort u_1) (a : (i : α) ×' β i) : (Equiv.psigmaEquivSigmaPLift β) a = ⟨{ down := a.fst }, { down := a.snd }⟩
• Equiv.psigmaEquivSigmaPLift_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_2} (β : α → Sort u_1) (a : (i : PLift α) × PLift (β i.down)) : (Equiv.psigmaEquivSigmaPLift β).symm a = ⟨a.fst.down, a.snd.down⟩
• Equiv.sigmaCongrRight_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) (a : (a : α) × β₁ a) : (Equiv.sigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩
• Equiv.sigmaCongrLeft_apply 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) (a : (a : α₁) × β (e a)) : e.sigmaCongrLeft a = ⟨e a.fst, a.snd⟩
• Equiv.sigmaPUnit 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) : (_ : α) × PUnit.{u_10 + 1} ≃ α
• Equiv.sigmaUnique 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_10) (β : α → Type u_9) [(a : α) → Unique (β a)] : (a : α) × β a ≃ α
• Equiv.uniqueSigma 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_10} (β : α → Type u_9) [Unique α] : (i : α) × β i ≃ β default
• Equiv.sigmaProdDistrib 📋 Mathlib.Logic.Equiv.Prod
  {ι : Type u_10} (α : ι → Type u_9) (β : Type u_11) : ((i : ι) × α i) × β ≃ (i : ι) × α i × β
• Equiv.subtypeProdEquivSigmaSubtype 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_9} {β : Type u_10} (p : α → β → Prop) : { x // p x.1 x.2 } ≃ (a : α) × { b // p a b }
• Equiv.sigmaPUnit_apply 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) (p : (_ : α) × PUnit.{u_10 + 1}) : (Equiv.sigmaPUnit α) p = p.fst
• Equiv.sigmaPUnit_symm_apply_fst 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) (a : α) : ((Equiv.sigmaPUnit α).symm a).fst = a
• Equiv.sigmaPUnit_symm_apply_snd 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) (a : α) : ((Equiv.sigmaPUnit α).symm a).snd = PUnit.unit
• Equiv.coe_sigmaUnique 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_10} {β : α → Type u_9} [(a : α) → Unique (β a)] : ⇑(Equiv.sigmaUnique α β) = Sigma.fst
• Equiv.sigmaUnique_apply 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_10} {β : α → Type u_9} [(a : α) → Unique (β a)] (x : (a : α) × β a) : (Equiv.sigmaUnique α β) x = x.fst
• Equiv.sigmaCongrRight_sigmaEquivProd 📋 Mathlib.Logic.Equiv.Prod
  {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂) = (Equiv.sigmaEquivProd α₁ β₁).trans (Equiv.prodCongrRight e)
• Equiv.sigmaUnique_symm_apply 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_10} {β : α → Type u_9} [(a : α) → Unique (β a)] (x : α) : (Equiv.sigmaUnique α β).symm x = ⟨x, default⟩
• Equiv.sigmaEquivProd_sigmaCongrRight 📋 Mathlib.Logic.Equiv.Prod
  {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : (Equiv.sigmaEquivProd α₁ β₁).symm.trans (Equiv.sigmaCongrRight e) = (Equiv.prodCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂).symm
• Equiv.uniqueSigma_symm_apply 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_10} {β : α → Type u_9} [Unique α] (y : β default) : (Equiv.uniqueSigma β).symm y = ⟨default, y⟩
• Equiv.uniqueSigma_apply 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_10} {β : α → Type u_9} [Unique α] (x : (a : α) × β a) : (Equiv.uniqueSigma β) x = ⋯ ▸ x.snd
• Equiv.sigmaProdDistrib_apply 📋 Mathlib.Logic.Equiv.Prod
  {ι : Type u_10} (α : ι → Type u_9) (β : Type u_11) (p : ((i : ι) × α i) × β) : (Equiv.sigmaProdDistrib α β) p = ⟨p.1.fst, (p.1.snd, p.2)⟩
• Equiv.sigmaProdDistrib_symm_apply 📋 Mathlib.Logic.Equiv.Prod
  {ι : Type u_10} (α : ι → Type u_9) (β : Type u_11) (p : (i : ι) × α i × β) : (Equiv.sigmaProdDistrib α β).symm p = (⟨p.fst, p.snd.1⟩, p.snd.2)
• Equiv.sigmaEquivOptionOfInhabited 📋 Mathlib.Logic.Equiv.Sum
  (α : Type u) [Inhabited α] [DecidableEq α] : (β : Type u) × (α ≃ Option β)
• Equiv.sumEquivSigmaBool 📋 Mathlib.Logic.Equiv.Sum
  (α β : Type u_9) : α ⊕ β ≃ (b : Bool) × bif b then β else α
• Equiv.sigmaFiberEquiv 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_9} {β : Type u_10} (f : α → β) : (y : β) × { x // f x = y } ≃ α
• Equiv.sigmaSumDistrib 📋 Mathlib.Logic.Equiv.Sum
  {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) : (i : ι) × (α i ⊕ β i) ≃ (i : ι) × α i ⊕ (i : ι) × β i
• Equiv.sumSigmaDistrib 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) : (i : α ⊕ β) × t i ≃ (i : α) × t (Sum.inl i) ⊕ (i : β) × t (Sum.inr i)
• Equiv.sigmaFiberEquiv_symm_apply_fst 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_9} {β : Type u_10} (f : α → β) (x : α) : ((Equiv.sigmaFiberEquiv f).symm x).fst = f x
• Equiv.sigmaFiberEquiv_symm_apply_snd_coe 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_9} {β : Type u_10} (f : α → β) (x : α) : ↑((Equiv.sigmaFiberEquiv f).symm x).snd = x
• Equiv.sigmaFiberEquiv_apply 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_9} {β : Type u_10} (f : α → β) (x : (y : β) × { x // f x = y }) : (Equiv.sigmaFiberEquiv f) x = ↑x.snd
• Equiv.sigmaSumDistrib_apply 📋 Mathlib.Logic.Equiv.Sum
  {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (p : (i : ι) × (α i ⊕ β i)) : (Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd
• Equiv.sigmaSumDistrib_symm_apply 📋 Mathlib.Logic.Equiv.Sum
  {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (a✝ : (i : ι) × α i ⊕ (i : ι) × β i) : (Equiv.sigmaSumDistrib α β).symm a✝ = Sum.elim (Sigma.map id fun x => Sum.inl) (Sigma.map id fun x => Sum.inr) a✝
• Equiv.sumSigmaDistrib_apply 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) (x✝ : (i : α ⊕ β) × t i) : (Equiv.sumSigmaDistrib t) x✝ = match x✝ with | ⟨Sum.inl x, y⟩ => Sum.inl ⟨x, y⟩ | ⟨Sum.inr x, y⟩ => Sum.inr ⟨x, y⟩
• Equiv.sumSigmaDistrib_symm_apply 📋 Mathlib.Logic.Equiv.Sum
  {α : Type u_10} {β : Type u_11} (t : α ⊕ β → Type u_9) (a✝ : (i : α) × t (Sum.inl i) ⊕ (i : β) × t (Sum.inr i)) : (Equiv.sumSigmaDistrib t).symm a✝ = Sum.elim (fun a => ⟨Sum.inl a.fst, a.snd⟩) (fun b => ⟨Sum.inr b.fst, b.snd⟩) a✝
• Equiv.sigmaSubtype 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} (a : α) : { s // s.fst = a } ≃ β a
• Equiv.sigmaOptionEquivOfSome 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} (p : Option α → Type v) (h : ∀ (a : p none), False) : (x : Option α) × p x ≃ (x : α) × p (some x)
• Equiv.sigmaSubtypeEquivOfSubset 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} (p : α → Type v) (q : α → Prop) (h : ∀ (x : α) (a : p x), q x) : (x : Subtype q) × p ↑x ≃ (x : α) × p x
• Equiv.sigmaSubtypeFiberEquiv 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} (f : α → β) (p : β → Prop) (h : ∀ (x : α), p (f x)) : (y : Subtype p) × { x // f x = ↑y } ≃ α
• Equiv.subtypeSigmaEquiv 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} (p : α → Type v) (q : α → Prop) : { y // q y.fst } ≃ (x : Subtype q) × p ↑x
• Equiv.piEquivSubtypeSigma 📋 Mathlib.Logic.Equiv.Basic
  (ι : Type u_10) (π : ι → Type u_9) : ((i : ι) → π i) ≃ { f // ∀ (i : ι), (f i).fst = i }
• Equiv.sigmaAssocProd 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} : (ab : α × β) × γ ab.1 ab.2 ≃ (a : α) × (b : β) × γ a b
• Equiv.piCurry 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) : ((x : (i : α) × β i) → γ x.fst x.snd) ≃ ((a : α) → (b : β a) → γ a b)
• Equiv.sigmaNatSucc 📋 Mathlib.Logic.Equiv.Basic
  (f : ℕ → Type u) : (n : ℕ) × f n ≃ f 0 ⊕ (n : ℕ) × f (n + 1)
• Equiv.sigmaSubtypeFiberEquivSubtype 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} (f : α → β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (f x)) : (y : Subtype q) × { x // f x = ↑y } ≃ Subtype p
• Equiv.sigmaSigmaSubtypeEq 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : α) (b : β) : { s // s.fst = a ∧ s.snd.fst = b } ≃ γ a b
• Equiv.uniqueSigma.eq_1 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_10} (β : α → Type u_9) [Unique α] : Equiv.uniqueSigma β = { toFun := fun p => ⋯ ▸ p.snd, invFun := fun b => ⟨default, b⟩, left_inv := ⋯, right_inv := ⋯ }
• Equiv.sigmaSubtype_symm_apply_coe_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) : (↑((Equiv.sigmaSubtype a).symm b)).fst = a
• Equiv.sigmaSubtype_symm_apply_coe_snd 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) : (↑((Equiv.sigmaSubtype a).symm b)).snd = b
• Equiv.sigmaSigmaSubtype 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop) [uniq : Unique { ab // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩) : { s // p ⟨s.fst, s.snd.fst⟩ } ≃ γ a b
• Equiv.piCurry_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (x : (i : α) × β i) → γ x.fst x.snd) : (Equiv.piCurry γ) f = Sigma.curry f
• Equiv.piCurry_symm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (a : α) → (b : β a) → γ a b) : (Equiv.piCurry γ).symm f = Sigma.uncurry f
• Equiv.sigmaSubtype_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} (a : α) (x✝ : { s // s.fst = a }) : (Equiv.sigmaSubtype a) x✝ = match x✝ with | ⟨⟨fst, b⟩, h⟩ => h ▸ b
• Equiv.ofFiberEquiv_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) (a✝ : α) : (Equiv.ofFiberEquiv e) a✝ = ↑((e (f a✝)) ((Equiv.sigmaFiberEquiv f).symm a✝).snd)
• Equiv.subtypeSigmaEquiv.eq_1 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} (p : α → Type v) (q : α → Prop) : Equiv.subtypeSigmaEquiv p q = { toFun := fun x => ⟨⟨(↑x).fst, ⋯⟩, (↑x).snd⟩, invFun := fun x => ⟨⟨↑x.fst, x.snd⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
• Equiv.sigmaSigmaSubtypeEq.eq_1 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : α) (b : β) : Equiv.sigmaSigmaSubtypeEq a b = Equiv.sigmaSigmaSubtype (fun x => match x with | ⟨a', b'⟩ => a' = a ∧ b' = b) ⋯
• Equiv.sigmaAssocProd_apply_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.1 a.2) : (Equiv.sigmaAssocProd a✝).fst = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.fst
• Equiv.ofFiberEquiv_symm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) (a✝ : β) : (Equiv.ofFiberEquiv e).symm a✝ = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a✝)).snd
• Equiv.sigmaAssoc.eq_1 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_1} {β : α → Type u_2} (γ : (a : α) → β a → Type u_3) : Equiv.sigmaAssoc γ = { toFun := fun x => ⟨x.fst.fst, ⟨x.fst.snd, x.snd⟩⟩, invFun := fun x => ⟨⟨x.fst, x.snd.fst⟩, x.snd.snd⟩, left_inv := ⋯, right_inv := ⋯ }
• Equiv.sigmaAssocProd_symm_apply_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α) × (b : β) × γ a b) : (Equiv.sigmaAssocProd.symm a✝).fst = (((Equiv.sigmaAssoc γ).symm a✝).fst.fst, ((Equiv.sigmaAssoc γ).symm a✝).fst.snd)
• Equiv.sigmaSigmaSubtypeEq_symm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (c : γ a b) : (Equiv.sigmaSigmaSubtypeEq a b).symm c = ⟨⟨a, ⟨b, c⟩⟩, ⋯⟩
• Equiv.sigmaSigmaSubtype_symm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop) [uniq : Unique { ab // p ab }] {a : α} {b : β a} (c : γ a b) (h : p ⟨a, b⟩) : (Equiv.sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩
• Equiv.sigmaSigmaSubtypeEq_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (s : { s // s.fst = a ∧ s.snd.fst = b }) : (Equiv.sigmaSigmaSubtypeEq a b) s = cast ⋯ (↑s).snd.snd
• Equiv.sigmaAssocProd_symm_apply_snd 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α) × (b : β) × γ a b) : (Equiv.sigmaAssocProd.symm a✝).snd = ((Equiv.sigmaAssoc γ).symm a✝).snd
• Equiv.sigmaAssocProd_apply_snd_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.1 a.2) : (Equiv.sigmaAssocProd a✝).snd.fst = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.snd
• Equiv.sigmaAssocProd_apply_snd_snd 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.1 a.2) : (Equiv.sigmaAssocProd a✝).snd.snd = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).snd
• Equiv.sigmaSigmaSubtype_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop) [uniq : Unique { ab // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩) (a✝ : { s // p ⟨s.fst, s.snd.fst⟩ }) : (Equiv.sigmaSigmaSubtype p h) a✝ = cast ⋯ (↑a✝).snd.snd
• Equiv.Perm.sigmaCongrRightHom_apply 📋 Mathlib.Algebra.Group.End
  {α : Type u_6} (β : α → Type u_7) (F : (a : α) → Equiv.Perm (β a)) : (Equiv.Perm.sigmaCongrRightHom β) F = Equiv.Perm.sigmaCongrRight F
• Equiv.sigmaPreimageEquiv 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} (f : α → β) : (b : β) × ↑(f ⁻¹' {b}) ≃ α
• Equiv.setProdEquivSigma 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} (s : Set (α × β)) : ↑s ≃ (x : α) × ↑{y | (x, y) ∈ s}
• Equiv.sigmaPreimageEquiv_symm_apply_fst 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : ((Equiv.sigmaPreimageEquiv f).symm x).fst = f x
• Equiv.sigmaPreimageEquiv_symm_apply_snd_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : ↑((Equiv.sigmaPreimageEquiv f).symm x).snd = x
• Equiv.sigmaPreimageEquiv_apply 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : (y : β) × { x // f x = y }) : (Equiv.sigmaPreimageEquiv f) x = ↑x.snd
• Equiv.ofPreimageEquiv_apply 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) (a✝ : α) : (Equiv.ofPreimageEquiv e) a✝ = ↑((e (f a✝)) ((Equiv.sigmaFiberEquiv f).symm a✝).snd)
• Equiv.ofPreimageEquiv_symm_apply 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) (a✝ : β) : (Equiv.ofPreimageEquiv e).symm a✝ = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a✝)).snd
• Set.sigmaEquiv 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {β : Type u_2} (s : α → Set β) (hs : ∀ (b : β), ∃! i, b ∈ s i) : (i : α) × ↑(s i) ≃ β
• Set.unionEqSigmaOfDisjoint 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {β : Type u_2} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) : ↑(⋃ i, t i) ≃ (i : α) × ↑(t i)
• List.equivSigmaTuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} : List α ≃ (n : ℕ) × (Fin n → α)
• List.equivSigmaTuple_apply_fst 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.equivSigmaTuple l).fst = l.length
• List.equivSigmaTuple_apply_snd 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) (a✝ : Fin l.length) : (List.equivSigmaTuple l).snd a✝ = l.get a✝
• List.equivSigmaTuple_symm_apply 📋 Mathlib.Data.List.OfFn
  {α : Type u} (f : (n : ℕ) × (Fin n → α)) : List.equivSigmaTuple.symm f = List.ofFn f.snd
• Setoid.sigmaQuotientEquivOfLe 📋 Mathlib.Data.Setoid.Basic
  {α : Type u_1} {r s : Setoid α} (hle : r ≤ s) : (q : Quotient s) × Quotient (Setoid.comap Subtype.val r) ≃ Quotient r
• AddAction.selfEquivSigmaOrbits' 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑ω.orbit
• MulAction.selfEquivSigmaOrbits' 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑ω.orbit
• AddAction.selfEquivSigmaOrbits 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑(AddAction.orbit G (Quotient.out ω))
• MulAction.selfEquivSigmaOrbits 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑(MulAction.orbit G (Quotient.out ω))
• AddAction.selfEquivSigmaOrbits.eq_1 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : AddAction.selfEquivSigmaOrbits G α = (AddAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun x => Equiv.setCongr ⋯)
• MulAction.selfEquivSigmaOrbits.eq_1 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : MulAction.selfEquivSigmaOrbits G α = (MulAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun x => Equiv.setCongr ⋯)
• AddAction.selfEquivSigmaOrbits'.eq_1 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : AddAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun x => Equiv.subtypeEquivRight ⋯)
• MulAction.selfEquivSigmaOrbits'.eq_1 📋 Mathlib.GroupTheory.GroupAction.Defs
  (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : MulAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun x => Equiv.subtypeEquivRight ⋯)
• Set.biUnionEqSigmaOfDisjoint 📋 Mathlib.Data.Set.Pairwise.Lattice
  {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) : ↑(⋃ i ∈ s, f i) ≃ (i : ↑s) × ↑(f ↑i)
• Function.Embedding.optionEmbeddingEquiv 📋 Mathlib.Logic.Embedding.Set
  (α : Type u_1) (β : Type u_2) : (Option α ↪ β) ≃ (f : α ↪ β) × ↑(Set.range ⇑f)ᶜ
• Function.Embedding.optionEmbeddingEquiv_apply_fst 📋 Mathlib.Logic.Embedding.Set
  (α : Type u_1) (β : Type u_2) (f : Option α ↪ β) : ((Function.Embedding.optionEmbeddingEquiv α β) f).fst = Function.Embedding.some.trans f
• Function.Embedding.optionEmbeddingEquiv_apply_snd_coe 📋 Mathlib.Logic.Embedding.Set
  (α : Type u_1) (β : Type u_2) (f : Option α ↪ β) : ↑((Function.Embedding.optionEmbeddingEquiv α β) f).snd = f none
• Function.Embedding.optionEmbeddingEquiv_symm_apply 📋 Mathlib.Logic.Embedding.Set
  (α : Type u_1) (β : Type u_2) (f : (f : α ↪ β) × ↑(Set.range ⇑f)ᶜ) : (Function.Embedding.optionEmbeddingEquiv α β).symm f = f.fst.optionElim ↑f.snd ⋯
• Finsupp.sigmaFinsuppEquivPiFinsupp 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {η : Type u_14} [Fintype η] {ιs : η → Type u_15} [Zero α] : ((j : η) × ιs j →₀ α) ≃ ((j : η) → ιs j →₀ α)
• Finsupp.sigmaFinsuppEquivPiFinsupp_apply 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {η : Type u_14} [Fintype η] {ιs : η → Type u_15} [Zero α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) : (Finsupp.sigmaFinsuppEquivPiFinsupp f j) i = f ⟨j, i⟩
• Finset.sigmaAntidiagonalEquivProd 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] : (n : A) × { x // x ∈ Finset.antidiagonal n } ≃ A × A
• Finset.sigmaAntidiagonalEquivProd_symm_apply_fst 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) : (Finset.sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
• Finset.sigmaAntidiagonalEquivProd_symm_apply_snd_coe 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) : ↑(Finset.sigmaAntidiagonalEquivProd.symm x).snd = x
• Finset.sigmaAntidiagonalEquivProd_apply 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : (n : A) × { x // x ∈ Finset.antidiagonal n }) : Finset.sigmaAntidiagonalEquivProd x = ↑x.snd
• Equiv.embeddingFinSucc 📋 Mathlib.Logic.Equiv.Fin.Basic
  (n : ℕ) (ι : Type u_1) : (Fin (n + 1) ↪ ι) ≃ (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }
• Equiv.embeddingFinSucc_fst 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι) : ⇑((Equiv.embeddingFinSucc n ι) e).fst = ⇑e ∘ Fin.succ
• Equiv.coe_embeddingFinSucc_symm 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} {ι : Type u_1} (f : (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }) : ⇑((Equiv.embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst
• Equiv.embeddingFinSucc_snd 📋 Mathlib.Logic.Equiv.Fin.Basic
  {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι) : ↑((Equiv.embeddingFinSucc n ι) e).snd = e 0
• finSigmaFinEquiv 📋 Mathlib.Algebra.BigOperators.Fin
  {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i, n i)
• finSigmaFinEquiv.eq_1 📋 Mathlib.Algebra.BigOperators.Fin
  (n_2 : Fin 0 → ℕ) : finSigmaFinEquiv = Equiv.equivOfIsEmpty ((i : Fin 0) × Fin (n_2 i)) (Fin (∑ i, n_2 i))
• finSigmaFinEquiv_apply 📋 Mathlib.Algebra.BigOperators.Fin
  {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) : ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
• Equiv.sigmaCongrLeft.eq_1 📋 Mathlib.Algebra.BigOperators.Fin
  {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) : e.sigmaCongrLeft = { toFun := fun a => ⟨e a.fst, a.snd⟩, invFun := fun a => ⟨e.symm a.fst, ⋯ ▸ a.snd⟩, left_inv := ⋯, right_inv := ⋯ }
• finSigmaFinEquiv_one 📋 Mathlib.Algebra.BigOperators.Fin
  {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) : ↑(finSigmaFinEquiv ij) = ↑ij.snd
• finSigmaFinEquiv.eq_2 📋 Mathlib.Algebra.BigOperators.Fin
  (m_2 : ℕ) (n_2 : Fin m_2.succ → ℕ) : finSigmaFinEquiv = Trans.trans (Trans.trans (Trans.trans (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm (Equiv.sumSigmaDistrib fun a => Fin (n_2 (finSumFinEquiv a)))) (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n_2 (finSumFinEquiv (Sum.inr i)))))) finSumFinEquiv) (finCongr ⋯)
• DFinsupp.sigmaFinsetFunEquiv 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] : (Π₀ (i : ι), β i) ≃ (s : Finset ι) × ((i : { x // x ∈ s }) → { x // x ≠ 0 })
• DFinsupp.sigmaFinsetFunEquiv_apply_fst 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (a✝ : Π₀ (i : ι), β i) : (DFinsupp.sigmaFinsetFunEquiv a✝).fst = a✝.support
• DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (a✝ : Π₀ (i : ι), β i) (i : { x // x ∈ ((Equiv.sigmaFiberEquiv DFinsupp.support).symm a✝).fst }) : ↑((DFinsupp.sigmaFinsetFunEquiv a✝).snd i) = a✝ ↑i
• DFinsupp.sigmaCurryEquiv 📋 Mathlib.Data.DFinsupp.Sigma
  {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι] : (Π₀ (i : (x : ι) × α x), δ i.fst i.snd) ≃ Π₀ (i : ι) (j : α i), δ i j
• sigmaFinsuppEquivDFinsupp 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [Zero N] : ((i : ι) × η i →₀ N) ≃ Π₀ (i : ι), η i →₀ N
• sigmaFinsuppEquivDFinsupp_apply 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [Zero N] (f : (i : ι) × η i →₀ N) : ⇑(sigmaFinsuppEquivDFinsupp f) = f.split
• sigmaFinsuppEquivDFinsupp_support 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [DecidableEq ι] [Zero N] [(i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)] (f : (i : ι) × η i →₀ N) : (sigmaFinsuppEquivDFinsupp f).support = f.splitSupport
• sigmaFinsuppEquivDFinsupp_single 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [DecidableEq ι] [Zero N] (a : (i : ι) × η i) (n : N) : (sigmaFinsuppEquivDFinsupp fun₀ | a => n) = fun₀ | a.fst => fun₀ | a.snd => n
• sigmaFinsuppEquivDFinsupp_symm_apply 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [Zero N] (f : Π₀ (i : ι), η i →₀ N) (s : (i : ι) × η i) : (sigmaFinsuppEquivDFinsupp.symm f) s = (f s.fst) s.snd
• sigmaFinsuppAddEquivDFinsupp_apply 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : (i : ι) × η i →₀ N) : sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a
• sigmaFinsuppEquivDFinsupp_smul 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} {R : Type u_6} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R) (f : (i : ι) × η i →₀ N) : sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f
• sigmaFinsuppEquivDFinsupp_add 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (f g : (i : ι) × η i →₀ N) : sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
• sigmaFinsuppAddEquivDFinsupp_symm_apply 📋 Mathlib.Data.Finsupp.ToDFinsupp
  {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : Π₀ (i : ι), η i →₀ N) : sigmaFinsuppAddEquivDFinsupp.symm a = sigmaFinsuppEquivDFinsupp.symm a
• equiv_linearIndependent 📋 Mathlib.LinearAlgebra.LinearIndependent.Lemmas
  {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] (n : ℕ) : { s // LinearIndependent K s } ≃ (s : { s // LinearIndependent K s }) × ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ
• Cardinal.mk_sigma_congr 📋 Mathlib.SetTheory.Cardinal.Defs
  {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) : Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)
• Cardinal.mk_sigma_congr' 📋 Mathlib.SetTheory.Cardinal.Defs
  {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) : Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)
• Cardinal.mk_sigma_congr_lift 📋 Mathlib.SetTheory.Cardinal.Defs
  {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.lift.{w', w} (Cardinal.mk (f i)) = Cardinal.lift.{w, w'} (Cardinal.mk (g (e i)))) : Cardinal.lift.{max v' w', max w v} (Cardinal.mk ((i : ι) × f i)) = Cardinal.lift.{max v w, max w' v'} (Cardinal.mk ((i : ι') × g i))
• AddSubgroup.addGroupEquivQuotientProdAddSubgroup.eq_1 📋 Mathlib.GroupTheory.Coset.Basic
  {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : AddSubgroup.addGroupEquivQuotientProdAddSubgroup = Trans.trans (Trans.trans (Trans.trans (Equiv.sigmaFiberEquiv QuotientAddGroup.mk).symm (Equiv.sigmaCongrRight fun L => ⋯.mpr (let_fun this := ⋯.mpr (Equiv.refl { x // Quotient.mk'' x = L }); this))) (Equiv.sigmaCongrRight fun x => AddSubgroup.leftCosetEquivAddSubgroup (Quotient.out x))) (Equiv.sigmaEquivProd (α ⧸ s) ↥s)
• Subgroup.groupEquivQuotientProdSubgroup.eq_1 📋 Mathlib.GroupTheory.Coset.Basic
  {α : Type u_1} [Group α] {s : Subgroup α} : Subgroup.groupEquivQuotientProdSubgroup = Trans.trans (Trans.trans (Trans.trans (Equiv.sigmaFiberEquiv QuotientGroup.mk).symm (Equiv.sigmaCongrRight fun L => ⋯.mpr (let_fun this := ⋯.mpr (Equiv.refl { x // Quotient.mk'' x = L }); this))) (Equiv.sigmaCongrRight fun x => Subgroup.leftCosetEquivSubgroup (Quotient.out x))) (Equiv.sigmaEquivProd (α ⧸ s) ↥s)
• algHomEquivSigma 📋 Mathlib.RingTheory.AlgebraTower
  {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] : (C →ₐ[A] D) ≃ (f : B →ₐ[A] D) × (C →ₐ[B] D)
• AddAction.sigmaFixedByEquivOrbitsProdAddGroup 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] : (a : α) × ↑(AddAction.fixedBy β a) ≃ Quotient (AddAction.orbitRel α β) × α
• MulAction.sigmaFixedByEquivOrbitsProdGroup 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [Group α] [MulAction α β] : (a : α) × ↑(MulAction.fixedBy β a) ≃ Quotient (MulAction.orbitRel α β) × α
• AddAction.selfEquivSigmaOrbitsQuotientStabilizer 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] : β ≃ (ω : Quotient (AddAction.orbitRel α β)) × α ⧸ AddAction.stabilizer α ω.out
• MulAction.selfEquivSigmaOrbitsQuotientStabilizer 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [Group α] [MulAction α β] : β ≃ (ω : Quotient (MulAction.orbitRel α β)) × α ⧸ MulAction.stabilizer α ω.out
• AddAction.selfEquivSigmaOrbitsQuotientStabilizer' 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] {φ : Quotient (AddAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : β ≃ (ω : Quotient (AddAction.orbitRel α β)) × α ⧸ AddAction.stabilizer α (φ ω)
• MulAction.selfEquivSigmaOrbitsQuotientStabilizer' 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [Group α] [MulAction α β] {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : β ≃ (ω : Quotient (MulAction.orbitRel α β)) × α ⧸ MulAction.stabilizer α (φ ω)
• AddAction.selfEquivSigmaOrbitsQuotientStabilizer.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] : AddAction.selfEquivSigmaOrbitsQuotientStabilizer α β = AddAction.selfEquivSigmaOrbitsQuotientStabilizer' α β ⋯
• MulAction.selfEquivSigmaOrbitsQuotientStabilizer.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [Group α] [MulAction α β] : MulAction.selfEquivSigmaOrbitsQuotientStabilizer α β = MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β ⋯
• AddAction.equivAddSubgroupOrbits 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} (β : Type v) [AddGroup α] [AddAction α β] (H : AddSubgroup α) : AddAction.orbitRel.Quotient (↥H) β ≃ (ω : Quotient (AddAction.orbitRel α β)) × AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω)
• MulAction.equivSubgroupOrbits 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} (β : Type v) [Group α] [MulAction α β] (H : Subgroup α) : MulAction.orbitRel.Quotient (↥H) β ≃ (ω : Quotient (MulAction.orbitRel α β)) × MulAction.orbitRel.Quotient ↥H ↑(MulAction.orbitRel.Quotient.orbit ω)
• AddAction.selfEquivSigmaOrbitsQuotientStabilizer'.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] {φ : Quotient (AddAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : AddAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ = Trans.trans (AddAction.selfEquivSigmaOrbits' α β) (Equiv.sigmaCongrRight fun ω => (Equiv.setCongr ⋯).trans (AddAction.orbitEquivQuotientStabilizer α (φ ω)))
• MulAction.selfEquivSigmaOrbitsQuotientStabilizer'.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [Group α] [MulAction α β] {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ = Trans.trans (MulAction.selfEquivSigmaOrbits' α β) (Equiv.sigmaCongrRight fun ω => (Equiv.setCongr ⋯).trans (MulAction.orbitEquivQuotientStabilizer α (φ ω)))
• AddAction.selfEquivOrbitsQuotientProd'.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {φ : Quotient (AddAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : β), AddAction.stabilizer α b = ⊥) : AddAction.selfEquivOrbitsQuotientProd' hφ h = (AddAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ).trans ((Equiv.sigmaCongrRight fun x => (AddSubgroup.quotientEquivOfEq ⋯).trans (QuotientAddGroup.quotientEquivSelf α)).trans (Equiv.sigmaEquivProd (Quotient (AddAction.orbitRel α β)) α))
• MulAction.selfEquivOrbitsQuotientProd'.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} {β : Type v} [Group α] [MulAction α β] {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : β), MulAction.stabilizer α b = ⊥) : MulAction.selfEquivOrbitsQuotientProd' hφ h = (MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ).trans ((Equiv.sigmaCongrRight fun x => (Subgroup.quotientEquivOfEq ⋯).trans (QuotientGroup.quotientEquivSelf α)).trans (Equiv.sigmaEquivProd (Quotient (MulAction.orbitRel α β)) α))
• AddAction.equivAddSubgroupOrbits.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} (β : Type v) [AddGroup α] [AddAction α β] (H : AddSubgroup α) : AddAction.equivAddSubgroupOrbits β H = (Setoid.sigmaQuotientEquivOfLe ⋯).symm.trans (Equiv.sigmaCongrRight fun ω => (AddAction.equivAddSubgroupOrbitsSetoidComap H ω).symm)
• MulAction.equivSubgroupOrbits.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} (β : Type v) [Group α] [MulAction α β] (H : Subgroup α) : MulAction.equivSubgroupOrbits β H = (Setoid.sigmaQuotientEquivOfLe ⋯).symm.trans (Equiv.sigmaCongrRight fun ω => (MulAction.equivSubgroupOrbitsSetoidComap H ω).symm)
• AddAction.sigmaFixedByEquivOrbitsProdAddGroup.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] : AddAction.sigmaFixedByEquivOrbitsProdAddGroup α β = Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Equiv.subtypeProdEquivSigmaSubtype fun a => Membership.mem (AddAction.fixedBy β a)).symm ((Equiv.prodComm α β).subtypeEquiv ⋯)) (Equiv.subtypeProdEquivSigmaSubtype fun b a => a ∈ AddAction.stabilizer α b)) (AddAction.selfEquivSigmaOrbits α β).sigmaCongrLeft') (Equiv.sigmaAssoc fun ω b => ↥(AddAction.stabilizer α ↑b))) (Equiv.sigmaCongrRight fun x => Equiv.sigmaCongrRight fun x_1 => match x_1 with | ⟨val, hb⟩ => (AddAction.stabilizerEquivStabilizerOfOrbitRel hb).toEquiv)) (Equiv.sigmaCongrRight fun x => Equiv.sigmaEquivProd ↑(AddAction.orbit α x.out) ↥(AddAction.stabilizer α x.out))) (Equiv.sigmaCongrRight fun ω => AddAction.orbitProdStabilizerEquivAddGroup α ω.out)) (Equiv.sigmaEquivProd (Quotient (AddAction.orbitRel α β)) α)
• MulAction.sigmaFixedByEquivOrbitsProdGroup.eq_1 📋 Mathlib.GroupTheory.GroupAction.Quotient
  (α : Type u) (β : Type v) [Group α] [MulAction α β] : MulAction.sigmaFixedByEquivOrbitsProdGroup α β = Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans (Equiv.subtypeProdEquivSigmaSubtype fun a => Membership.mem (MulAction.fixedBy β a)).symm ((Equiv.prodComm α β).subtypeEquiv ⋯)) (Equiv.subtypeProdEquivSigmaSubtype fun b a => a ∈ MulAction.stabilizer α b)) (MulAction.selfEquivSigmaOrbits α β).sigmaCongrLeft') (Equiv.sigmaAssoc fun ω b => ↥(MulAction.stabilizer α ↑b))) (Equiv.sigmaCongrRight fun x => Equiv.sigmaCongrRight fun x_1 => match x_1 with | ⟨val, hb⟩ => (MulAction.stabilizerEquivStabilizerOfOrbitRel hb).toEquiv)) (Equiv.sigmaCongrRight fun x => Equiv.sigmaEquivProd ↑(MulAction.orbit α x.out) ↥(MulAction.stabilizer α x.out))) (Equiv.sigmaCongrRight fun ω => MulAction.orbitProdStabilizerEquivGroup α ω.out)) (Equiv.sigmaEquivProd (Quotient (MulAction.orbitRel α β)) α)
• Finset.symInsertEquiv 📋 Mathlib.Data.Finset.Sym
  {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) : { x // x ∈ (insert a s).sym n } ≃ (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }
• Finset.symInsertEquiv_apply_fst 📋 Mathlib.Data.Finset.Sym
  {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) (m : { x // x ∈ (insert a s).sym n }) : ((Finset.symInsertEquiv h) m).fst = (Sym.filterNe a ↑m).fst
• Finset.symInsertEquiv_apply_snd_coe 📋 Mathlib.Data.Finset.Sym
  {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) (m : { x // x ∈ (insert a s).sym n }) : ↑((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a ↑m).snd
• Finset.symInsertEquiv_symm_apply_coe 📋 Mathlib.Data.Finset.Sym
  {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) (m : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }) : ↑((Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst ↑m.snd
• CategoryTheory.Arrow.equivSigma 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] : CategoryTheory.Arrow T ≃ (X : T) × (Y : T) × (X ⟶ Y)
• CategoryTheory.Arrow.equivSigma_apply_fst 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T) : ((CategoryTheory.Arrow.equivSigma T) f).fst = f.left
• CategoryTheory.Arrow.equivSigma_symm_apply_left 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((CategoryTheory.Arrow.equivSigma T).symm x).left = x.fst
• CategoryTheory.Arrow.equivSigma_apply_snd_fst 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T) : ((CategoryTheory.Arrow.equivSigma T) f).snd.fst = f.right
• CategoryTheory.Arrow.equivSigma_symm_apply_right 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((CategoryTheory.Arrow.equivSigma T).symm x).right = x.snd.fst
• CategoryTheory.Arrow.equivSigma_apply_snd_snd 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T) : ((CategoryTheory.Arrow.equivSigma T) f).snd.snd = f.hom
• CategoryTheory.Arrow.equivSigma_symm_apply_hom 📋 Mathlib.CategoryTheory.Comma.Arrow
  (T : Type u) [CategoryTheory.Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)) : ((CategoryTheory.Arrow.equivSigma T).symm x).hom = x.snd.snd
• Composition.blocksFinEquiv 📋 Mathlib.Combinatorics.Enumerative.Composition
  {n : ℕ} (c : Composition n) : (i : Fin c.length) × Fin (c.blocksFun i) ≃ Fin n
• CategoryTheory.Limits.Types.colimitEquivQuot_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] (j : J) (x : F.obj j) : (CategoryTheory.Limits.Types.colimitEquivQuot F) (CategoryTheory.Limits.colimit.ι F j x) = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩
• CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] (j : J) (x : F.obj j) : (CategoryTheory.Limits.Types.colimitEquivQuot F).symm (Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩) = CategoryTheory.Limits.colimit.ι F j x
• CategoryTheory.Limits.Types.colimitCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)] (j : J) (x : F.obj j) : (CategoryTheory.Limits.Types.colimitCocone F).ι.app j x = (equivShrink (CategoryTheory.Limits.Types.Quot F)) (Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩)
• WType.equivSigma 📋 Mathlib.Data.W.Basic
  {α : Type u_1} (β : α → Type u_2) : WType β ≃ (a : α) × (β a → WType β)
• WType.equivSigma_apply 📋 Mathlib.Data.W.Basic
  {α : Type u_1} (β : α → Type u_2) (a✝ : WType β) : (WType.equivSigma β) a✝ = a✝.toSigma
• WType.equivSigma_symm_apply 📋 Mathlib.Data.W.Basic
  {α : Type u_1} (β : α → Type u_2) (a✝ : (a : α) × (β a → WType β)) : (WType.equivSigma β).symm a✝ = WType.ofSigma a✝
• CategoryTheory.OverPresheafAux.unitAuxAuxAux_inv 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) (a✝ : F.obj (Opposite.op X)) : (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).inv a✝ = CategoryTheory.OverPresheafAux.unitBackward η X a✝
• CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf_map 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (p : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X✝)) : (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).map f p = CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f.unop p
• CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁_app 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (x✝ : Cᵒᵖ) (a✝ : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop x✝)) : (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η).app x✝ a✝ = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η a✝
• ContinuousMap.sigmaEquiv 📋 Mathlib.Topology.ContinuousMap.Basic
  {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] : ((i : I) → C(X i, A)) ≃ C((i : I) × X i, A)
• ContinuousMap.sigmaEquiv_apply 📋 Mathlib.Topology.ContinuousMap.Basic
  {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) : (ContinuousMap.sigmaEquiv A X) f = ContinuousMap.sigma f
• ContinuousMap.sigmaEquiv_symm_apply 📋 Mathlib.Topology.ContinuousMap.Basic
  {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : C((i : I) × X i, A)) (i : I) : (ContinuousMap.sigmaEquiv A X).symm f i = f.comp (ContinuousMap.sigmaMk i)
• Homeomorph.sigmaProdDistrib_toEquiv 📋 Mathlib.Topology.Homeomorph.Lemmas
  {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] : Homeomorph.sigmaProdDistrib.toEquiv = Equiv.sigmaProdDistrib X Y
• Subgroup.quotientEquivSigmaZMod 📋 Mathlib.Data.ZMod.QuotientGroup
  {G : Type u_3} [Group G] (H : Subgroup G) (g : G) : G ⧸ H ≃ (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) × ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
• Subgroup.quotientEquivSigmaZMod_symm_apply 📋 Mathlib.Data.ZMod.QuotientGroup
  {G : Type u_3} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))) : (H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out q
• Subgroup.quotientEquivSigmaZMod_apply 📋 Mathlib.Data.ZMod.QuotientGroup
  {G : Type u_3} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ℤ) : (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩
• Matrix.blockDiagonal'.eq_1 📋 Mathlib.LinearAlgebra.Matrix.Trace
  {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) : Matrix.blockDiagonal' M = Matrix.of fun x x_1 => match x with | ⟨k, i⟩ => match x_1 with | ⟨k', j⟩ => if h : k = k' then M k i (cast ⋯ j) else 0
• HomologicalComplex.homotopyCofiber.descEquiv 📋 Mathlib.Algebra.Homology.HomotopyCofiber
  {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (K : HomologicalComplex C c) (hc : ∀ (j : ι), ∃ i, c.Rel i j) : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0 ≃ (HomologicalComplex.homotopyCofiber φ ⟶ K)
• Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted 📋 Mathlib.Logic.Equiv.Embedding
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} : (α ⊕ β ↪ γ) ≃ (f : α ↪ γ) × (β ↪ ↑(Set.range ⇑f)ᶜ)
• Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted 📋 Mathlib.Logic.Equiv.Embedding
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) } ≃ (f : α ↪ γ) × (β ↪ ↑(Set.range ⇑f)ᶜ)
• LinearIsometryEquiv.piLpCurry_apply 📋 Mathlib.Analysis.Normed.Lp.PiLp
  {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7) [(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [(i : ι) → (k : κ i) → Module 𝕜 (α i k)] (f : PiLp p fun i => α i.fst i.snd) : (LinearIsometryEquiv.piLpCurry 𝕜 p α) f = (WithLp.equiv p ((i : ι) → WithLp p ((y : κ i) → α i y))).symm fun i => (WithLp.equiv p ((y : κ i) → α i y)).symm (Sigma.curry ((WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)) f) i)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision f167e8d