Theorem: WType.SubWType.elim_const (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₁ : SubWType β s₁
w₂ : SubWType β s₂
h : ↑w₁ = ↑w₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
⊢ elim' γ fγ s₁ w₁ = elim' γ fγ s₂ w₂
Tactic:
rcases w₁ with ⟨w, hw₁⟩
State after:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₂ : SubWType β s₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
h : ↑⟨w, hw₁⟩ = ↑w₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ w₂

State before:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₂ : SubWType β s₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
h : ↑⟨w, hw₁⟩ = ↑w₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ w₂
Tactic:
rcases w₂ with ⟨w, hw₂⟩
State after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : ↑⟨w✝, hw₁⟩ = ↑⟨w, hw₂⟩
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩

State before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : ↑⟨w✝, hw₁⟩ = ↑⟨w, hw₂⟩
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Tactic:
simp at h
State after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : w✝ = w
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩

State before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : w✝ = w
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Tactic:
rcases h with rfl
State after:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
hw₂ : w.depth ≤ s₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩

State before:
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
hw₂ : w.depth ≤ s₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
Tactic:
simp[elim']
State after:
no goals