case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q x

case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ p x
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (x : α), p x) ↔ ∀ (y : β), q y
constructor <;> intro h₂ x
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ p x
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q x

case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ p x
. rw [← f.right_inv x]; apply h.mp; apply h₂
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q (toFun f (invFun f x))
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q x
rw [← f.right_inv x]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ p (invFun f x)
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q (toFun f (invFun f x))
apply h.mp
no goals
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ p (invFun f x)
apply h₂
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ q (↑f x)
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ p x
apply h.mpr
no goals
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ q (↑f x)
apply h₂