Theorem: HTPI.exun_elim (HTPILib/HTPIDefs.lean)

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
⊢ b
Tactic:
apply ExistsUnique.elim h2
State after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
⊢ ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
⊢ ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b
Tactic:
intro x h3 h4
State after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ b

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ b
Tactic:
apply h1 x h3
State after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ ∀ (y z : α), p y → p z → y = z

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
⊢ ∀ (y z : α), p y → p z → y = z
Tactic:
intro y z h5 h6
State after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
⊢ y = z

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
⊢ y = z
Tactic:
have h7 := h4 y h5
State after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
⊢ y = z

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
⊢ y = z
Tactic:
have h8 := h4 z h6
State after:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
h8 : z = x
⊢ y = z

State before:
α : Sort u
p : α → Prop
b : Prop
h2 : ∃! x, p x
h1 : ∀ (x : α), p x → (∀ (y z : α), p y → p z → y = z) → b
x : α
h3 : p x
h4 : ∀ (y : α), p y → y = x
y z : α
h5 : p y
h6 : p z
h7 : y = x
h8 : z = x
⊢ y = z
Tactic:
rw [h7,h8]
State after:
no goals