[GOAL]
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
{cases f; cases g; congr
}
[GOAL]
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Sort u
β : Sort v
g : α ↪ β
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝, inj' := inj'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, inj' := inj'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Sort u
β : Sort v
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝¹, inj' := inj'✝¹ }.toFun = { toFun := toFun✝, inj' := inj'✝ }.toFun
⊢ { toFun := toFun✝¹, inj' := inj'✝¹ } = { toFun := toFun✝, inj' := inj'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding e.symm) = Embedding.refl α
[PROOFSTEP]
ext
[GOAL]
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : α
⊢ ↑(Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding e.symm)) x✝ = ↑(Embedding.refl α) x✝
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ Embedding.trans (Equiv.toEmbedding e.symm) (Equiv.toEmbedding e) = Embedding.refl β
[PROOFSTEP]
ext
[GOAL]
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : β
⊢ ↑(Embedding.trans (Equiv.toEmbedding e.symm) (Equiv.toEmbedding e)) x✝ = ↑(Embedding.refl β) x✝
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
⊢ Injective fun a' => if a' = a then b else if ↑f a' = b then ↑f a else ↑f a'
[PROOFSTEP]
intro x y
  (h : ite _ _ _ = ite _ _ _)
    -- TODO: once we have `cc` we can avoid all the manual cases below by doing
        -- split_ifs at h <;> (try subst b) <;> (try simp only [f.injective.eq_iff] at *) <;> cc
[GOAL]
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h : (if x = a then b else if ↑f x = b then ↑f a else ↑f x) = if y = a then b else if ↑f y = b then ↑f a else ↑f y
⊢ x = y
[PROOFSTEP]
split_ifs at h  with h₁ h₂ _ _ h₅ h₆
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : y = a
h : b = b
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : y = a
h : b = b
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : ¬y = a
_ : ↑f y = b
h : b = ↑f a
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : ¬y = a
_ : ↑f y = b
h : b = ↑f a
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : ¬y = a
_ : ¬↑f y = b
h : b = ↑f y
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : ¬y = a
_ : ¬↑f y = b
h : b = ↑f y
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ↑f x = b
h₅ : y = a
h : ↑f a = b
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ↑f x = b
h₅ : y = a
h : ↑f a = b
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ↑f x = b
h₅ : ¬y = a
h₆ : ↑f y = b
h : ↑f a = ↑f a
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ↑f x = b
h₅ : ¬y = a
h₆ : ↑f y = b
h : ↑f a = ↑f a
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ↑f x = b
h₅ : ¬y = a
h₆ : ¬↑f y = b
h : ↑f a = ↑f y
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ↑f x = b
h₅ : ¬y = a
h₆ : ¬↑f y = b
h : ↑f a = ↑f y
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝ : y = a
h : ↑f x = b
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝ : y = a
h : ↑f x = b
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ↑f y = b
h : ↑f x = ↑f a
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ↑f y = b
h : ↑f x = ↑f a
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ¬↑f y = b
h : ↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
try subst b
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ¬↑f y = b
h : ↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : y = a
h : b = b
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : y = a
h : b = b
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : x = a
h₂ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
h : ↑f y = ↑f a
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : x = a
h₂ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
h : ↑f y = ↑f a
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : x = a
h₂ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
_ : ¬↑f y = ↑f y
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : x = a
h₂ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
_ : ¬↑f y = ↑f y
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h : ↑f a = ↑f x
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h : ↑f a = ↑f x
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
h : ↑f a = ↑f a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h₆ : ↑f y = ↑f x
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
h : ↑f a = ↑f a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h₆ : ↑f y = ↑f x
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
h : ↑f a = ↑f y
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h₆ : ¬↑f y = ↑f x
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
h : ↑f a = ↑f y
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h₆ : ¬↑f y = ↑f x
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h✝ : y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
_ : ¬↑f x = ↑f x
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h✝ : y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
_ : ¬↑f x = ↑f x
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h✝ : ¬y = a
h : ↑f x = ↑f a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
_ : ¬↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h✝ : ¬y = a
h : ↑f x = ↑f a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
_ : ¬↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ¬↑f y = b
h : ↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
try simp only [f.injective.eq_iff] at *
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ¬↑f y = b
h : ↑f x = ↑f y
⊢ x = y
[PROOFSTEP]
simp only [f.injective.eq_iff] at *
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : x = a
h₂ : y = a
h : True
⊢ x = y
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : x = a
h₂ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
h : y = a
⊢ x = y
[PROOFSTEP]
rw [h₁, h]
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h : a = x
⊢ x = y
[PROOFSTEP]
rw [h₅, ← h]
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h : True
h₆ : y = x
⊢ x = y
[PROOFSTEP]
exact h₆.symm
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h : a = y
h₆ : ¬y = x
⊢ x = y
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h₅ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f x)
h : a = y
h₆ : ¬y = x
⊢ False
[PROOFSTEP]
exact h₅ h.symm
[GOAL]
case pos
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h✝ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
h : x = a
_ : ¬x = y
⊢ x = y
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
inst✝¹ : (a' : α) → Decidable (a' = a)
x y : α
h₁ : ¬x = a
h✝ : ¬y = a
inst✝ : (a' : α) → Decidable (↑f a' = ↑f y)
h : x = a
_ : ¬x = y
⊢ False
[PROOFSTEP]
exact h₁ h
[GOAL]
case neg
α : Sort ?u.14414
β : Sort ?u.14415
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
x y : α
h₁ : ¬x = a
_ : ¬↑f x = b
h✝¹ : ¬y = a
h✝ : ¬↑f y = b
h : x = y
⊢ x = y
[PROOFSTEP]
exact h
[GOAL]
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (↑f a' = b)
⊢ ↑(setValue f a b) a = b
[PROOFSTEP]
simp [setValue]
[GOAL]
β : Sort u_1
b : β
⊢ Injective fun x => b
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ _
[GOAL]
case unit.unit
β : Sort u_1
b : β
a✝ : (fun x => b) PUnit.unit = (fun x => b) PUnit.unit
⊢ PUnit.unit = PUnit.unit
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
inst✝ : Inhabited γ
e : α ↪ β
f₁ f₂ : α → γ
h : (fun f => extend (↑e) f default) f₁ = (fun f => extend (↑e) f default) f₂
x : α
⊢ f₁ x = f₂ x
[PROOFSTEP]
simpa only [e.injective.extend_apply] using congr_fun h (e x)
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
⊢ (fun f => Embedding.congr h.symm h'.symm f) ((fun f => Embedding.congr h h' f) x) = x
[PROOFSTEP]
ext
[GOAL]
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
x✝ : α
⊢ ↑((fun f => Embedding.congr h.symm h'.symm f) ((fun f => Embedding.congr h h' f) x)) x✝ = ↑x x✝
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
⊢ (fun f => Embedding.congr h h' f) ((fun f => Embedding.congr h.symm h'.symm f) x) = x
[PROOFSTEP]
ext
[GOAL]
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
x✝ : β
⊢ ↑((fun f => Embedding.congr h h' f) ((fun f => Embedding.congr h.symm h'.symm f) x)) x✝ = ↑x x✝
[PROOFSTEP]
simp
[GOAL]
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
⊢ ↑(embeddingCongr ea ec) (Embedding.trans f g) =
    Embedding.trans (↑(embeddingCongr ea eb) f) (↑(embeddingCongr eb ec) g)
[PROOFSTEP]
ext
[GOAL]
case h
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
x✝ : α₂
⊢ ↑(↑(embeddingCongr ea ec) (Embedding.trans f g)) x✝ =
    ↑(Embedding.trans (↑(embeddingCongr ea eb) f) (↑(embeddingCongr eb ec) g)) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective fun x =>
    if h : p ↑x then Sum.inl { val := ↑x, property := h } else Sum.inr { val := ↑x, property := (_ : q ↑x) }
[PROOFSTEP]
intro x y
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
⊢ (fun x => if h : p ↑x then Sum.inl { val := ↑x, property := h } else Sum.inr { val := ↑x, property := (_ : q ↑x) })
        x =
      (fun x =>
          if h : p ↑x then Sum.inl { val := ↑x, property := h } else Sum.inr { val := ↑x, property := (_ : q ↑x) })
        y →
    x = y
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
⊢ ((if h : p ↑x then Sum.inl { val := ↑x, property := h } else Sum.inr { val := ↑x, property := (_ : q ↑x) }) =
      if h : p ↑y then Sum.inl { val := ↑y, property := h } else Sum.inr { val := ↑y, property := (_ : q ↑y) }) →
    x = y
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : p ↑y
⊢ Sum.inl { val := ↑x, property := h✝¹ } = Sum.inl { val := ↑y, property := h✝ } → x = y
[PROOFSTEP]
simp [Subtype.ext_iff]
[GOAL]
case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : ¬p ↑y
⊢ False → x = y
[PROOFSTEP]
simp [Subtype.ext_iff]
[GOAL]
case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : p ↑y
⊢ False → x = y
[PROOFSTEP]
simp [Subtype.ext_iff]
[GOAL]
case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : ¬p ↑y
⊢ Sum.inr { val := ↑x, property := (_ : q ↑x) } = Sum.inr { val := ↑y, property := (_ : q ↑y) } → x = y
[PROOFSTEP]
simp [Subtype.ext_iff]
[GOAL]
α : Type u_1
p q : α → Prop
h : ∀ (x : α), p x → q x
x y : { x // p x }
⊢ (fun x => { val := ↑x, property := (_ : q ↑x) }) x = (fun x => { val := ↑x, property := (_ : q ↑x) }) y → x = y
[PROOFSTEP]
simp [Subtype.ext_iff]


[GOAL]
α : Type u_1
x✝ : Bool × ℕ
b : Bool
n : ℕ
⊢ boddDiv2 (uncurry bit (b, n)) = (b, n)
[PROOFSTEP]
simp only [bodd_bit, div2_bit, uncurry_apply_pair, boddDiv2_eq]
[GOAL]
α : Type u_1
n : ℕ
⊢ uncurry bit (boddDiv2 n) = n
[PROOFSTEP]
simp only [bit_decomp, boddDiv2_eq, uncurry_apply_pair]
[GOAL]
α : Type u_1
⊢ ↑natSumNatEquivNat = Sum.elim bit0 bit1
[PROOFSTEP]
ext (x | x)
[GOAL]
case h.inl
α : Type u_1
x : ℕ
⊢ ↑natSumNatEquivNat (Sum.inl x) = Sum.elim bit0 bit1 (Sum.inl x)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u_1
x : ℕ
⊢ ↑natSumNatEquivNat (Sum.inr x) = Sum.elim bit0 bit1 (Sum.inr x)
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬isSome (↑e (some x)) = true
⊢ isSome (↑e none) = true
[PROOFSTEP]
rw [← Option.ne_none_iff_isSome]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬isSome (↑e (some x)) = true
⊢ ↑e none ≠ none
[PROOFSTEP]
intro hn
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬isSome (↑e (some x)) = true
hn : ↑e none = none
⊢ False
[PROOFSTEP]
rw [Option.not_isSome_iff_eq_none, ← hn] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ↑e (some x) = ↑e none
hn : ↑e none = none
⊢ False
[PROOFSTEP]
exact
  Option.some_ne_none _
    (e.injective h)
      -- Porting note: private
      -- #align equiv.remove_none_aux Equiv.removeNone_aux
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ∃ x', ↑e (some x) = some x'
⊢ some (removeNone_aux e x) = ↑e (some x)
[PROOFSTEP]
simp [removeNone_aux, Option.isSome_iff_exists.mpr h]
  -- Porting note: private
  -- #align equiv.remove_none_aux_some Equiv.removeNone_aux_some
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ some (removeNone_aux e x) = ↑e none
[PROOFSTEP]
simp [removeNone_aux, Option.not_isSome_iff_eq_none.mpr h]
  -- Porting note: private
  -- #align equiv.remove_none_aux_none Equiv.removeNone_aux_none
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
cases h1 : e.symm (some (removeNone_aux e x))
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
cases h2 : e (some x)
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x val✝ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
cases h2 : e (some x)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
rw [removeNone_aux_none _ h1]
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
h2 : ↑e (some x) = none
⊢ ↑e.symm none = some x
[PROOFSTEP]
exact (e.eq_symm_apply.mpr h2).symm
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
rw [removeNone_aux_some _ ⟨_, h2⟩] at h1
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (↑e (some x)) = none
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
simp at h1
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x val✝ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
rw [removeNone_aux_none _ h2] at h1
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x val✝ : α
h1 : ↑e.symm (↑e none) = some val✝
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
simp at h1
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
[PROOFSTEP]
rw [removeNone_aux_some _ ⟨_, h1⟩]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ ↑e.symm (some (removeNone_aux e x)) = some x
[PROOFSTEP]
rw [removeNone_aux_some _ ⟨_, h2⟩]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ ↑e.symm (↑e (some x)) = some x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
h : ↑e.symm none = none
⊢ ↑e none = none
[PROOFSTEP]
simpa using (congr_arg e h).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
h : ↑e none = none
⊢ ↑e.symm none = none
[PROOFSTEP]
simpa using (congr_arg e.symm h).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
cases' h : e (some x) with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
rw [removeNone_none _ h]
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ ↑e none = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
simpa using (congr_arg e.symm h).symm
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
rw [removeNone_some _ ⟨a, h⟩]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
have h1 := congr_arg e.symm h
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : ↑e.symm (↑e (some x)) = ↑e.symm (some a)
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
rw [symm_apply_apply] at h1
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : some x = ↑e.symm (some a)
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
[PROOFSTEP]
simp only [false_iff_iff, apply_eq_iff_eq]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : some x = ↑e.symm (some a)
⊢ ¬↑e.symm none = some x
[PROOFSTEP]
simp [h1, apply_eq_iff_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e✝ : Option α ≃ Option β
e : α ≃ β
x : α
⊢ ↑(optionCongr e) (some x) = some (↑e x)
[PROOFSTEP]
simp [EquivFunctor.map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
a : α
⊢ (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
      ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
    a
[PROOFSTEP]
rw [← some_inj, some_get]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
a : α
⊢ ↑(↑e).symm ↑((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) = some a
[PROOFSTEP]
exact symm_apply_apply (e : Option α ≃ β) a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
b : { y // y ≠ x }
⊢ (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
      ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
    b
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
b : { y // y ≠ x }
⊢ ↑((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
        ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b)) =
    ↑b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : Option α
⊢ (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
    a
[PROOFSTEP]
cases a with
| none => simp
| some a =>
  simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta, symm_apply_apply, dite_eq_ite]
  exact if_neg (e a).property
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : Option α
⊢ (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
    a
[PROOFSTEP]
cases a with
| none => simp
| some a =>
  simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta, symm_apply_apply, dite_eq_ite]
  exact if_neg (e a).property
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
⊢ (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) none) =
    none
[PROOFSTEP]

| none => simp
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
⊢ (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) none) =
    none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) (some a)) =
    some a
[PROOFSTEP]

| some a =>
  simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta, symm_apply_apply, dite_eq_ite]
  exact if_neg (e a).property
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) (some a)) =
    some a
[PROOFSTEP]
simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta, symm_apply_apply, dite_eq_ite]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ (if ↑(↑e a) = x then none else some a) = some a
[PROOFSTEP]
exact if_neg (e a).property
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
⊢ (fun a => casesOn' a x (Subtype.val ∘ ↑e))
      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
    b
[PROOFSTEP]
by_cases h : b = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : b = x
⊢ (fun a => casesOn' a x (Subtype.val ∘ ↑e))
      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
    b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : ¬b = x
⊢ (fun a => casesOn' a x (Subtype.val ∘ ↑e))
      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
    b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
⊢ (fun e =>
        {
          val :=
            { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
              invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
              left_inv :=
                (_ :
                  ∀ (a : Option α),
                    (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                        ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                      a),
              right_inv :=
                (_ :
                  ∀ (b : β),
                    (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                        ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                      b) },
          property :=
            (_ :
              ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                      invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                      left_inv :=
                        (_ :
                          ∀ (a : Option α),
                            (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                              a),
                      right_inv :=
                        (_ :
                          ∀ (b : β),
                            (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                              b) }
                  none =
                ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                      invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                      left_inv :=
                        (_ :
                          ∀ (a : Option α),
                            (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                              a),
                      right_inv :=
                        (_ :
                          ∀ (b : β),
                            (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                              b) }
                  none) })
      ((fun e =>
          { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
            invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
            left_inv :=
              (_ :
                ∀ (a : α),
                  (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                      ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                    a),
            right_inv :=
              (_ :
                ∀ (b : { y // y ≠ x }),
                  (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                      ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                    b) })
        e) =
    e
[PROOFSTEP]
ext a
[GOAL]
case a.H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
a : Option α
⊢ ↑↑((fun e =>
              {
                val :=
                  { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                    invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                    left_inv :=
                      (_ :
                        ∀ (a : Option α),
                          (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                              ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (b : β),
                          (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                              ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                            b) },
                property :=
                  (_ :
                    ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                            invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                            left_inv :=
                              (_ :
                                ∀ (a : Option α),
                                  (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (b : β),
                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        b) =
                                    b) }
                        none =
                      ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                            invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                            left_inv :=
                              (_ :
                                ∀ (a : Option α),
                                  (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (b : β),
                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        b) =
                                    b) }
                        none) })
            ((fun e =>
                { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                  invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                  left_inv :=
                    (_ :
                      ∀ (a : α),
                        (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                            ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                          a),
                  right_inv :=
                    (_ :
                      ∀ (b : { y // y ≠ x }),
                        (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                            ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                          b) })
              e))
      a =
    ↑↑e a
[PROOFSTEP]
cases a
[GOAL]
case a.H.none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
⊢ ↑↑((fun e =>
              {
                val :=
                  { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                    invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                    left_inv :=
                      (_ :
                        ∀ (a : Option α),
                          (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                              ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (b : β),
                          (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                              ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                            b) },
                property :=
                  (_ :
                    ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                            invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                            left_inv :=
                              (_ :
                                ∀ (a : Option α),
                                  (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (b : β),
                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        b) =
                                    b) }
                        none =
                      ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                            invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                            left_inv :=
                              (_ :
                                ∀ (a : Option α),
                                  (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (b : β),
                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        b) =
                                    b) }
                        none) })
            ((fun e =>
                { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                  invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                  left_inv :=
                    (_ :
                      ∀ (a : α),
                        (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                            ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                          a),
                  right_inv :=
                    (_ :
                      ∀ (b : { y // y ≠ x }),
                        (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                            ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                          b) })
              e))
      none =
    ↑↑e none
[PROOFSTEP]
simpa using e.property.symm
[GOAL]
case a.H.some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
val✝ : α
⊢ ↑↑((fun e =>
              {
                val :=
                  { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                    invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                    left_inv :=
                      (_ :
                        ∀ (a : Option α),
                          (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                              ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (b : β),
                          (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                              ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                            b) },
                property :=
                  (_ :
                    ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                            invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                            left_inv :=
                              (_ :
                                ∀ (a : Option α),
                                  (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (b : β),
                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        b) =
                                    b) }
                        none =
                      ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                            invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                            left_inv :=
                              (_ :
                                ∀ (a : Option α),
                                  (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (b : β),
                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                      ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        b) =
                                    b) }
                        none) })
            ((fun e =>
                { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                  invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                  left_inv :=
                    (_ :
                      ∀ (a : α),
                        (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                            ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                          a),
                  right_inv :=
                    (_ :
                      ∀ (b : { y // y ≠ x }),
                        (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                            ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                          b) })
              e))
      (some val✝) =
    ↑↑e (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
⊢ (fun e =>
        { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
          invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
          left_inv :=
            (_ :
              ∀ (a : α),
                (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                    ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                  a),
          right_inv :=
            (_ :
              ∀ (b : { y // y ≠ x }),
                (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                    ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                  b) })
      ((fun e =>
          {
            val :=
              { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                left_inv :=
                  (_ :
                    ∀ (a : Option α),
                      (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                          ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                        a),
                right_inv :=
                  (_ :
                    ∀ (b : β),
                      (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                          ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                        b) },
            property :=
              (_ :
                ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                        invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                        left_inv :=
                          (_ :
                            ∀ (a : Option α),
                              (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                  ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                a),
                        right_inv :=
                          (_ :
                            ∀ (b : β),
                              (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                  ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                    b) =
                                b) }
                    none =
                  ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                        invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                        left_inv :=
                          (_ :
                            ∀ (a : Option α),
                              (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                  ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                a),
                        right_inv :=
                          (_ :
                            ∀ (b : β),
                              (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                  ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                    b) =
                                b) }
                    none) })
        e) =
    e
[PROOFSTEP]
ext a
[GOAL]
case H.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ ↑(↑((fun e =>
              { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                left_inv :=
                  (_ :
                    ∀ (a : α),
                      (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                          ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                        a),
                right_inv :=
                  (_ :
                    ∀ (b : { y // y ≠ x }),
                      (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                          ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                        b) })
            ((fun e =>
                {
                  val :=
                    { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                      invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                      left_inv :=
                        (_ :
                          ∀ (a : Option α),
                            (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                              a),
                      right_inv :=
                        (_ :
                          ∀ (b : β),
                            (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h })) b) =
                              b) },
                  property :=
                    (_ :
                      ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                              invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                              left_inv :=
                                (_ :
                                  ∀ (a : Option α),
                                    (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                      a),
                              right_inv :=
                                (_ :
                                  ∀ (b : β),
                                    (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                        ((fun b =>
                                            if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                          b) =
                                      b) }
                          none =
                        ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                              invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                              left_inv :=
                                (_ :
                                  ∀ (a : Option α),
                                    (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                        ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                      a),
                              right_inv :=
                                (_ :
                                  ∀ (b : β),
                                    (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                        ((fun b =>
                                            if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                          b) =
                                      b) }
                          none) })
              e))
        a) =
    ↑(↑e a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
b : { y // y ≠ x }
⊢ some (↑(↑(optionSubtype x) e).symm b) = ↑(↑e).symm ↑b
[PROOFSTEP]
dsimp only [optionSubtype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // ↑e none = x }
b : { y // y ≠ x }
⊢ some
      (↑(↑{
                  toFun := fun e =>
                    { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                      invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                      left_inv :=
                        (_ :
                          ∀ (a : α),
                            (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                                ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                              a),
                      right_inv :=
                        (_ :
                          ∀ (b : { y // y ≠ x }),
                            (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                                ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true)) b) =
                              b) },
                  invFun := fun e =>
                    {
                      val :=
                        { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                          invFun := fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }),
                          left_inv :=
                            (_ :
                              ∀ (a : Option α),
                                (fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                    ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                  a),
                          right_inv :=
                            (_ :
                              ∀ (b : β),
                                (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                    ((fun b => if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                      b) =
                                  b) },
                      property :=
                        (_ :
                          ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                  invFun := fun b =>
                                    if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                  left_inv :=
                                    (_ :
                                      ∀ (a : Option α),
                                        (fun b =>
                                              if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                            ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                          a),
                                  right_inv :=
                                    (_ :
                                      ∀ (b : β),
                                        (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                            ((fun b =>
                                                if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                              b) =
                                          b) }
                              none =
                            ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                  invFun := fun b =>
                                    if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                  left_inv :=
                                    (_ :
                                      ∀ (a : Option α),
                                        (fun b =>
                                              if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                            ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                          a),
                                  right_inv :=
                                    (_ :
                                      ∀ (b : β),
                                        (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                            ((fun b =>
                                                if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                              b) =
                                          b) }
                              none) },
                  left_inv :=
                    (_ :
                      ∀ (e : { e // ↑e none = x }),
                        (fun e =>
                              {
                                val :=
                                  { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                    invFun := fun b =>
                                      if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                    left_inv :=
                                      (_ :
                                        ∀ (a : Option α),
                                          (fun b =>
                                                if h : b = x then none else some (↑e.symm { val := b, property := h }))
                                              ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                            a),
                                    right_inv :=
                                      (_ :
                                        ∀ (b : β),
                                          (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                              ((fun b =>
                                                  if h : b = x then none
                                                  else some (↑e.symm { val := b, property := h }))
                                                b) =
                                            b) },
                                property :=
                                  (_ :
                                    ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                            invFun := fun b =>
                                              if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                            left_inv :=
                                              (_ :
                                                ∀ (a : Option α),
                                                  (fun b =>
                                                        if h : b = x then none
                                                        else some (↑e.symm { val := b, property := h }))
                                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                                    a),
                                            right_inv :=
                                              (_ :
                                                ∀ (b : β),
                                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                                      ((fun b =>
                                                          if h : b = x then none
                                                          else some (↑e.symm { val := b, property := h }))
                                                        b) =
                                                    b) }
                                        none =
                                      ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                            invFun := fun b =>
                                              if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                            left_inv :=
                                              (_ :
                                                ∀ (a : Option α),
                                                  (fun b =>
                                                        if h : b = x then none
                                                        else some (↑e.symm { val := b, property := h }))
                                                      ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                                    a),
                                            right_inv :=
                                              (_ :
                                                ∀ (b : β),
                                                  (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                                      ((fun b =>
                                                          if h : b = x then none
                                                          else some (↑e.symm { val := b, property := h }))
                                                        b) =
                                                    b) }
                                        none) })
                            ((fun e =>
                                { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                                  invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                                  left_inv :=
                                    (_ :
                                      ∀ (a : α),
                                        (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                                            ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                                          a),
                                  right_inv :=
                                    (_ :
                                      ∀ (b : { y // y ≠ x }),
                                        (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                                            ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                                              b) =
                                          b) })
                              e) =
                          e),
                  right_inv :=
                    (_ :
                      ∀ (e : α ≃ { y // y ≠ x }),
                        (fun e =>
                              { toFun := fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) },
                                invFun := fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true),
                                left_inv :=
                                  (_ :
                                    ∀ (a : α),
                                      (fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                                          ((fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) }) a) =
                                        a),
                                right_inv :=
                                  (_ :
                                    ∀ (b : { y // y ≠ x }),
                                      (fun a => { val := ↑↑e (some a), property := (_ : ↑↑e (some a) ≠ x) })
                                          ((fun b => Option.get (↑(↑e).symm ↑b) (_ : isSome (↑(↑e).symm ↑b) = true))
                                            b) =
                                        b) })
                            ((fun e =>
                                {
                                  val :=
                                    { toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                      invFun := fun b =>
                                        if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                      left_inv :=
                                        (_ :
                                          ∀ (a : Option α),
                                            (fun b =>
                                                  if h : b = x then none
                                                  else some (↑e.symm { val := b, property := h }))
                                                ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                              a),
                                      right_inv :=
                                        (_ :
                                          ∀ (b : β),
                                            (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                                ((fun b =>
                                                    if h : b = x then none
                                                    else some (↑e.symm { val := b, property := h }))
                                                  b) =
                                              b) },
                                  property :=
                                    (_ :
                                      ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                              invFun := fun b =>
                                                if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                              left_inv :=
                                                (_ :
                                                  ∀ (a : Option α),
                                                    (fun b =>
                                                          if h : b = x then none
                                                          else some (↑e.symm { val := b, property := h }))
                                                        ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                                      a),
                                              right_inv :=
                                                (_ :
                                                  ∀ (b : β),
                                                    (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                                        ((fun b =>
                                                            if h : b = x then none
                                                            else some (↑e.symm { val := b, property := h }))
                                                          b) =
                                                      b) }
                                          none =
                                        ↑{ toFun := fun a => casesOn' a x (Subtype.val ∘ ↑e),
                                              invFun := fun b =>
                                                if h : b = x then none else some (↑e.symm { val := b, property := h }),
                                              left_inv :=
                                                (_ :
                                                  ∀ (a : Option α),
                                                    (fun b =>
                                                          if h : b = x then none
                                                          else some (↑e.symm { val := b, property := h }))
                                                        ((fun a => casesOn' a x (Subtype.val ∘ ↑e)) a) =
                                                      a),
                                              right_inv :=
                                                (_ :
                                                  ∀ (b : β),
                                                    (fun a => casesOn' a x (Subtype.val ∘ ↑e))
                                                        ((fun b =>
                                                            if h : b = x then none
                                                            else some (↑e.symm { val := b, property := h }))
                                                          b) =
                                                      b) }
                                          none) })
                              e) =
                          e) }
              e).symm
        b) =
    ↑(↑e).symm ↑b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑(↑(↑(optionSubtype x).symm e)).symm ↑b = some (↑e.symm b)
[PROOFSTEP]
simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk, Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑b = x → False
[PROOFSTEP]
exact fun h => False.elim (b.property h)


[GOAL]
α✝ : Sort u
β✝ : Sort v
f : α✝ ≃ β✝
α : Sort u_1
β : Type u_2
p : β → Prop
e : α ≃ Subtype p
x : β
hs : x ∈ setOf p
⊢ ↑(asEmbedding e) (↑e.symm { val := x, property := hs }) = x
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.1349
β : Type ?u.1350
f : Option α ↪ β
⊢ ∀ (x : Option α),
    ↑((fun f => optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ))
            ((fun f =>
                { fst := Embedding.trans coeWithTop f,
                  snd :=
                    { val := ↑f none, property := (_ : ↑f none ∈ Set.range ↑(Embedding.trans coeWithTop f) → False) } })
              f))
        x =
      ↑f x
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case none
α : Type ?u.1349
β : Type ?u.1350
f : Option α ↪ β
⊢ ↑((fun f => optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ))
          ((fun f =>
              { fst := Embedding.trans coeWithTop f,
                snd :=
                  { val := ↑f none, property := (_ : ↑f none ∈ Set.range ↑(Embedding.trans coeWithTop f) → False) } })
            f))
      none =
    ↑f none
[PROOFSTEP]
simp [Option.coe_def]
[GOAL]
case some
α : Type ?u.1349
β : Type ?u.1350
f : Option α ↪ β
val✝ : α
⊢ ↑((fun f => optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ))
          ((fun f =>
              { fst := Embedding.trans coeWithTop f,
                snd :=
                  { val := ↑f none, property := (_ : ↑f none ∈ Set.range ↑(Embedding.trans coeWithTop f) → False) } })
            f))
      (some val✝) =
    ↑f (some val✝)
[PROOFSTEP]
simp [Option.coe_def]
[GOAL]
case some
α : Type ?u.1349
β : Type ?u.1350
f : Option α ↪ β
val✝ : α
⊢ ↑val✝ = some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.1349
β : Type ?u.1350
x✝ : (f : α ↪ β) × ↑(Set.range ↑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (Set.range ↑f)ᶜ
⊢ (fun f =>
        { fst := Embedding.trans coeWithTop f,
          snd := { val := ↑f none, property := (_ : ↑f none ∈ Set.range ↑(Embedding.trans coeWithTop f) → False) } })
      ((fun f => optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ))
        { fst := f, snd := { val := y, property := hy } }) =
    { fst := f, snd := { val := y, property := hy } }
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type ?u.1349
β : Type ?u.1350
x✝¹ : (f : α ↪ β) × ↑(Set.range ↑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (Set.range ↑f)ᶜ
x✝ : α
⊢ ↑((fun f =>
              { fst := Embedding.trans coeWithTop f,
                snd :=
                  { val := ↑f none, property := (_ : ↑f none ∈ Set.range ↑(Embedding.trans coeWithTop f) → False) } })
            ((fun f => optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ))
              { fst := f, snd := { val := y, property := hy } })).fst
      x✝ =
    ↑{ fst := f, snd := { val := y, property := hy } }.fst x✝
[PROOFSTEP]
simp [Option.coe_def]
[GOAL]
case a
α : Type ?u.1349
β : Type ?u.1350
x✝ : (f : α ↪ β) × ↑(Set.range ↑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (Set.range ↑f)ᶜ
⊢ ↑((fun f =>
            { fst := Embedding.trans coeWithTop f,
              snd :=
                { val := ↑f none, property := (_ : ↑f none ∈ Set.range ↑(Embedding.trans coeWithTop f) → False) } })
          ((fun f => optionElim f.fst ↑f.snd (_ : ↑f.snd ∈ (Set.range ↑f.fst)ᶜ))
            { fst := f, snd := { val := y, property := hy } })).snd =
    ↑{ fst := f, snd := { val := y, property := hy } }.snd
[PROOFSTEP]
simp [Option.coe_def]
[GOAL]
case a.h
α : Type ?u.1349
β : Type ?u.1350
x✝¹ : (f : α ↪ β) × ↑(Set.range ↑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (Set.range ↑f)ᶜ
x✝ : α
⊢ ↑(optionElim f y
          (_ :
            ↑{ fst := f, snd := { val := y, property := hy } }.snd ∈
              (Set.range ↑{ fst := f, snd := { val := y, property := hy } }.fst)ᶜ))
      ↑x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.4882
s t : Set α
h✝ : s ⊆ t
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h :
  (fun x => { val := ↑x, property := (_ : ↑x ∈ t) }) { val := x, property := hx } =
    (fun x => { val := ↑x, property := (_ : ↑x ∈ t) }) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
congr
[GOAL]
case e_val
α : Type ?u.4882
s t : Set α
h✝ : s ⊆ t
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h :
  (fun x => { val := ↑x, property := (_ : ↑x ∈ t) }) { val := x, property := hx } =
    (fun x => { val := ↑x, property := (_ : ↑x ∈ t) }) { val := y, property := hy }
⊢ x = y
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x ∨ q x }
⊢ Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
      (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)))
      (↑(subtypeOrLeftEmbedding p q) x) =
    x
[PROOFSTEP]
by_cases hx : p x
[GOAL]
case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x ∨ q x }
hx : p ↑x
⊢ Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
      (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)))
      (↑(subtypeOrLeftEmbedding p q) x) =
    x
[PROOFSTEP]
rw [subtypeOrLeftEmbedding_apply_left _ hx]
[GOAL]
case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x ∨ q x }
hx : p ↑x
⊢ Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
      (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)))
      (Sum.inl { val := ↑x, property := hx }) =
    x
[PROOFSTEP]
simp [Subtype.ext_iff]
[GOAL]
case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x ∨ q x }
hx : ¬p ↑x
⊢ Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
      (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)))
      (↑(subtypeOrLeftEmbedding p q) x) =
    x
[PROOFSTEP]
rw [subtypeOrLeftEmbedding_apply_right _ hx]
[GOAL]
case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x ∨ q x }
hx : ¬p ↑x
⊢ Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
      (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)))
      (Sum.inr { val := ↑x, property := (_ : q ↑x) }) =
    x
[PROOFSTEP]
simp [Subtype.ext_iff]
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x } ⊕ { x // q x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
        (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x))) x) =
    x
[PROOFSTEP]
cases x with
| inl x =>
  simp only [Sum.elim_inl]
  rw [subtypeOrLeftEmbedding_apply_left]
  · simp
  · simpa using x.prop
| inr x =>
  simp only [Sum.elim_inr]
  rw [subtypeOrLeftEmbedding_apply_right]
  · simp
  · suffices ¬p x by simpa
    intro hp
    simpa using h.le_bot x ⟨hp, x.prop⟩
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x } ⊕ { x // q x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
        (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x))) x) =
    x
[PROOFSTEP]
cases x with
| inl x =>
  simp only [Sum.elim_inl]
  rw [subtypeOrLeftEmbedding_apply_left]
  · simp
  · simpa using x.prop
| inr x =>
  simp only [Sum.elim_inr]
  rw [subtypeOrLeftEmbedding_apply_right]
  · simp
  · suffices ¬p x by simpa
    intro hp
    simpa using h.le_bot x ⟨hp, x.prop⟩
[GOAL]
case inl
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
        (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x))) (Sum.inl x)) =
    Sum.inl x
[PROOFSTEP]

| inl x =>
  simp only [Sum.elim_inl]
  rw [subtypeOrLeftEmbedding_apply_left]
  · simp
  · simpa using x.prop
[GOAL]
case inl
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
        (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x))) (Sum.inl x)) =
    Sum.inl x
[PROOFSTEP]
simp only [Sum.elim_inl]
[GOAL]
case inl
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)) x) =
    Sum.inl x
[PROOFSTEP]
rw [subtypeOrLeftEmbedding_apply_left]
[GOAL]
case inl
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x }
⊢ Sum.inl
      { val := ↑(↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)) x),
        property := ?inl.hx } =
    Sum.inl x
[PROOFSTEP]
simp
[GOAL]
case inl.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x }
⊢ p ↑(↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)) x)
[PROOFSTEP]
simpa using x.prop
[GOAL]
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
        (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x))) (Sum.inr x)) =
    Sum.inr x
[PROOFSTEP]

| inr x =>
  simp only [Sum.elim_inr]
  rw [subtypeOrLeftEmbedding_apply_right]
  · simp
  · suffices ¬p x by simpa
    intro hp
    simpa using h.le_bot x ⟨hp, x.prop⟩
[GOAL]
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (Sum.elim (↑(Subtype.impEmbedding (fun x => p x) (fun x => p x ∨ q x) (_ : ∀ (x : α), p x → p x ∨ q x)))
        (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x))) (Sum.inr x)) =
    Sum.inr x
[PROOFSTEP]
simp only [Sum.elim_inr]
[GOAL]
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ↑(subtypeOrLeftEmbedding p q)
      (↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)) x) =
    Sum.inr x
[PROOFSTEP]
rw [subtypeOrLeftEmbedding_apply_right]
[GOAL]
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ Sum.inr
      { val := ↑(↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)) x),
        property :=
          (_ : q ↑(↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)) x)) } =
    Sum.inr x
[PROOFSTEP]
simp
[GOAL]
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑(↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)) x)
[PROOFSTEP]
suffices ¬p x by simpa
[GOAL]
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
this : ¬p ↑x
⊢ ¬p ↑(↑(Subtype.impEmbedding (fun x => q x) (fun x => p x ∨ q x) (_ : ∀ (x : α), q x → p x ∨ q x)) x)
[PROOFSTEP]
simpa
[GOAL]
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑x
[PROOFSTEP]
intro hp
[GOAL]
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
hp : p ↑x
⊢ False
[PROOFSTEP]
simpa using h.le_bot x ⟨hp, x.prop⟩


[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
simp [h]
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
simp [h]