case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₂ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ of p✝ → of p✝ = d₂
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂
induction d₁ using ManyOneDegree.ind_on
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₂ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ of p✝ → of p✝ = d₂
induction d₂ using ManyOneDegree.ind_on
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝¹ p✝ : Set ℕ
hp : of p✝¹ ≤ of p✝
hq : of p✝ ≤ of p✝¹
⊢ of p✝¹ = of p✝
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝
intro hp hq
no goals
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝¹ p✝ : Set ℕ
hp : of p✝¹ ≤ of p✝
hq : of p✝ ≤ of p✝¹
⊢ of p✝¹ = of p✝
simp_all only [ManyOneEquiv, of_le_of, of_eq_of, true_and_iff]