[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]
