ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ P x
ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
⊢ P x
let Q : s → Prop := fun y => P y
ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ Q { val := x, property := hx }
ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ P x
change Q ⟨x, hx⟩
ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ ∀ (x : ↑s), (∀ (y : ↑s), r ↑y ↑x → Q y) → Q x
ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ Q { val := x, property := hx }
refine' WellFounded.induction hs ⟨x, hx⟩ _
no goals
ι : Type ?u.4297
α : Type u_1
β : Type ?u.4303
r r' : α → α → Prop
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ ∀ (x : ↑s), (∀ (y : ↑s), r ↑y ↑x → Q y) → Q x
simpa only [Subtype.forall]