[GOAL]
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ { val := b, property := hb } = default
[PROOFSTEP]
congr
[GOAL]
case e_val
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ b = a
[PROOFSTEP]
exact he b hb
[GOAL]
n : ℕ
⊢ 0 < 1 + n
[PROOFSTEP]
rw [Nat.add_comm]
[GOAL]
n : ℕ
⊢ 0 < n + 1
[PROOFSTEP]
exact Nat.zero_lt_succ _
[GOAL]
α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p x
[PROOFSTEP]
rwa [Unique.eq_default x]
[GOAL]
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ { toInhabited := { default := x }, uniq := h } = { toInhabited := { default := y }, uniq := uniq✝ }
[PROOFSTEP]
congr
[GOAL]
case e_toInhabited.e_default
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
[PROOFSTEP]
rw [h x, h y]
[GOAL]
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α
[PROOFSTEP]
constructor
[GOAL]
case left
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α
[PROOFSTEP]
exact inferInstance
[GOAL]
case right
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Nonempty α
[PROOFSTEP]
exact inferInstance
[GOAL]
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
⊢ Unique α
[PROOFSTEP]
inhabit α
[GOAL]
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
inhabited_h : Inhabited α
⊢ Unique α
[PROOFSTEP]
exact Unique.mk' α
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
⊢ f = Function.const α (f default)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f x = Function.const α (f default) x
[PROOFSTEP]
rw [Subsingleton.elim x default]
[GOAL]
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f default = Function.const α (f default) default
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f i) (Function.const α (f default) x✝¹)
[PROOFSTEP]
rw [Subsingleton.elim i default]
[GOAL]
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f default) (Function.const α (f default) x✝¹)
[PROOFSTEP]
rfl
[GOAL]
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f
[PROOFSTEP]
rw [Function.bijective_iff_has_inverse]
[GOAL]
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
[PROOFSTEP]
refine' ⟨default, _, _⟩
[GOAL]
case refine'_1
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.LeftInverse default f
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.RightInverse default f
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : A
⊢ default (f x) = x
[PROOFSTEP]
simp
[GOAL]
case refine'_2
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : B
⊢ f (default x) = x
[PROOFSTEP]
simp
[GOAL]
α : Sort u
y : α
x✝ : { x // x = y }
x : α
hx : x = y
⊢ { val := x, property := hx } = default
[PROOFSTEP]
congr
[GOAL]
α : Sort u
y : α
x✝ : { x // y = x }
x : α
hx : y = x
⊢ { val := x, property := hx } = default
[PROOFSTEP]
subst hx
[GOAL]
α : Sort u
y : α
x✝ : { x // y = x }
⊢ { val := y, property := (_ : y = y) } = default
[PROOFSTEP]
congr
