case mk.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
⊢ ∀ (y : PSet), y ∈ mk β B → Acc (fun x x_1 => x ∈ x_1) y
rintro ⟨γ, C⟩ ⟨b, hc⟩
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
case mk.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
cases' H.exists_right b with a ha
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (Func (mk α A) a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
have H := ha.trans hc.symm
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (A a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (Func (mk α A) a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
rw [mk_func] at H
no goals
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (A a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
exact mem_wf_aux H