no goals
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
hut : u = True
hvf : v = False
⊢ u ≠ v
simp [hvf, hut, true_ne_false]
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
⊢ ∀ (exU exV : ∃ x, V x), choose exU = choose exV
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
⊢ ∀ (exU : ∃ x, U x) (exV : ∃ x, V x), choose exU = choose exV
rw [hpred]
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
exU✝ exV✝ : ∃ x, V x
⊢ choose exU✝ = choose exV✝
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
⊢ ∀ (exU exV : ∃ x, V x), choose exU = choose exV
intros
no goals
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
exU✝ exV✝ : ∃ x, V x
⊢ choose exU✝ = choose exV✝
rfl