structure Auto.IsomType (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

• f : α → β
• g : β → α
• eq₁ (x : α) : self.g (self.f x) = x
• eq₂ (x : β) : self.f (self.g x) = x

def Auto.IsomType.substForall {α : Sort u_1} {β : Sort u_2} {p : α → Sort u} (I : IsomType α β) (H : (x : α) → p x) (x : β) : p (I.g x)

Equations

• I.substForall H x✝ = H (I.g x✝)

def Auto.IsomType.substForallRev {α : Sort u_1} {β : Sort u_2} {p : α → Sort u} (I : IsomType α β) (H : (x : β) → p (I.g x)) (x : α) : p x

Equations

• I.substForallRev H x = ⋯.mp (H (I.f x))

def Auto.IsomType.eqForall {α : Sort u_1} {β : Sort u_2} {p : α → Prop} (I : IsomType α β) : (∀ (x : α), p x) ↔ ∀ (x : β), p (I.g x)

Equations

• ⋯ = ⋯

def Auto.IsomType.substForall' {β : Sort u_1} {α : Sort u_2} {p : β → Sort u} (I : IsomType α β) (H : (x : β) → p x) (x : α) : p (I.f x)

Equations

• I.substForall' H x✝ = H (I.f x✝)

def Auto.IsomType.substForallRev' {β : Sort u_1} {α : Sort u_2} {p : β → Sort u} (I : IsomType α β) (H : (x : α) → p (I.f x)) (x : β) : p x

Equations

• I.substForallRev' H x = ⋯.mp (H (I.g x))

def Auto.IsomType.eqForall' {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (I : IsomType α β) : (∀ (x : β), p x) ↔ ∀ (x : α), p (I.f x)

Equations

• ⋯ = ⋯

def Auto.IsomType.eqExists {α : Sort u_1} {β : Sort u_2} {p : α → Prop} (I : IsomType α β) : (∃ (x : α), p x) ↔ ∃ (x : β), p (I.g x)

Equations

• ⋯ = ⋯

def Auto.IsomType.eqExists' {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (I : IsomType α β) : (∃ (x : β), p x) ↔ ∃ (x : α), p (I.f x)

Equations

• ⋯ = ⋯

def Auto.Prod.eqForall {α : Type u_1} {β : Type u_2} {p : α × β → Prop} : (∀ (x : α × β), p x) ↔ ∀ (x : α) (y : β), p (x, y)

Equations

• ⋯ = ⋯

def Auto.Prod.eqExist {α : Type u_1} {β : Type u_2} {p : α × β → Prop} : (∃ (x : α × β), p x) ↔ ∃ (x : α), ∃ (y : β), p (x, y)

Equations

• ⋯ = ⋯

def Auto.Prod.eqForall' {α : Type u_1} {β : Type u_2} {p : α × β → Prop} : (∀ (x : α × β), p x) ↔ ∀ (y : β) (x : α), p (x, y)

Equations

• ⋯ = ⋯

def Auto.Prod.eqExist' {α : Type u_1} {β : Type u_2} {p : α × β → Prop} : (∃ (x : α × β), p x) ↔ ∃ (y : β), ∃ (x : α), p (x, y)

Equations

• ⋯ = ⋯

def Auto.PProd.eqForall {α : Sort u_1} {β : Sort u_2} {p : α ×' β → Prop} : (∀ (x : α ×' β), p x) ↔ ∀ (x : α) (y : β), p ⟨x, y⟩

Equations

• ⋯ = ⋯

def Auto.PProd.eqExist {α : Sort u_1} {β : Sort u_2} {p : α ×' β → Prop} : (∃ (x : α ×' β), p x) ↔ ∃ (x : α), ∃ (y : β), p ⟨x, y⟩

Equations

• ⋯ = ⋯

def Auto.PProd.eqForall' {α : Sort u_1} {β : Sort u_2} {p : α ×' β → Prop} : (∀ (x : α ×' β), p x) ↔ ∀ (y : β) (x : α), p ⟨x, y⟩

Equations

• ⋯ = ⋯

def Auto.PProd.eqExist' {α : Sort u_1} {β : Sort u_2} {p : α ×' β → Prop} : (∃ (x : α ×' β), p x) ↔ ∃ (y : β), ∃ (x : α), p ⟨x, y⟩

Equations

• ⋯ = ⋯

def Auto.PUnit.eqForall {p : PUnit → Prop} : (∀ (x : PUnit), p x) ↔ p PUnit.unit

Equations

• ⋯ = ⋯

def Auto.PUnit.eqExist {p : PUnit → Prop} : (∃ (x : PUnit), p x) ↔ p PUnit.unit

Equations

• ⋯ = ⋯