Theorem: WType.SubWType.ext (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 : ℕ
w₁ w₂ : SubWType β s
⊢ ↑w₁ = ↑w₂ → w₁ = w₂
Tactic:
rcases w₁ with ⟨w₁, h₁⟩
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 : ℕ
w₂ : SubWType β s
w₁ : WType β
h₁ : w₁.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑w₂ → ⟨w₁, h₁⟩ = 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 : ℕ
w₂ : SubWType β s
w₁ : WType β
h₁ : w₁.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑w₂ → ⟨w₁, h₁⟩ = w₂
Tactic:
rcases w₂ with ⟨w₂, 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 : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑⟨w₂, h₂⟩ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩

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 : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑⟨w₂, h₂⟩ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
Tactic:
simp
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 : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ w₁ = w₂ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩

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 : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ w₁ = w₂ → ⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
Tactic:
rintro 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 : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ⟨w₁, h₁⟩ = ⟨w₁, h₂⟩

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 : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ⟨w₁, h₁⟩ = ⟨w₁, h₂⟩
Tactic:
apply Subtype.ext (by simp)
State after:
no goals

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 : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ↑⟨w₁, h₁⟩ = ↑⟨w₁, h₂⟩
Tactic:
simp
State after:
no goals